feat(RingTheory/AdicCompletion): completeness of adic completion

[BryceT233]

Following [Stacks 05GG], this PR formalizes the result that AdicCompletion I M is I-adically complete when the ideal I is finitely generated.

Key contributions:

1. Generalized Finsupp.pointwiseModule to support a pointwise module structure Module (ι → R) (ι →₀ M) where R is a semiring and M is an R-module (Note: This generalization is an independent API improvement identified during development and is not required for the main proof.)

2. Constructed AdicCompletion.finsupp_sum, the canonical map from the finitely supported functions of adic completions to the adic completion of finitely supported functions, and established its inverse map when the index type is finite

3. Provided auxiliary lemmas regarding the canonical inclusion from I ^ a • N ⧸ I ^ b • (I ^ a • N) to M ⧸ I ^ c • N where c = b + a

4. Formalized helper lemmas concerning the canonical inclusion from the adic completion of I ^ n • M into the adic completion of M

5. Main Result: Formalized part (2) of [Stacks 05GG], from which the completeness of AdicCompletion I M follows

---

[github-actions]

PR summary fc502c3375

Import changes exceeding 2%

%	File
+12.21%	Mathlib.LinearAlgebra.Finsupp.Span

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.Finsupp.Span	811	910	+99 (+12.21%)
Mathlib.Data.Finsupp.Pointwise	513	521	+8 (+1.56%)

Import changes for all files

Files	Import difference
3 files Mathlib.Algebra.Category.ModuleCat.Ext.HasExt Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.RingTheory.AdicCompletion.Functoriality	1
7 files Mathlib.Algebra.Category.ContinuousCohomology.Basic Mathlib.Algebra.Category.ModuleCat.Topology.Basic Mathlib.Algebra.Category.ModuleCat.Topology.Homology Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Algebra.Module.ModuleTopology Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Topology.Algebra.SeparationQuotient.Section	4
16 files Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Algebra.Category.ModuleCat.Ulift Mathlib.Algebra.Module.Presentation.Free Mathlib.Algebra.Module.Projective Mathlib.LinearAlgebra.DirectSum.Basis Mathlib.LinearAlgebra.Finsupp.VectorSpace Mathlib.LinearAlgebra.FreeModule.Finite.Basic Mathlib.LinearAlgebra.Matrix.StdBasis Mathlib.LinearAlgebra.PiTensorProduct.Basis Mathlib.LinearAlgebra.PiTensorProduct.Dual Mathlib.LinearAlgebra.StdBasis Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.LinearAlgebra.TensorProduct.Free Mathlib.RingTheory.Finiteness.Cardinality Mathlib.RingTheory.Finiteness.Projective Mathlib.RingTheory.OrzechProperty	6
Mathlib.Data.Finsupp.Pointwise	8
Mathlib.LinearAlgebra.Finsupp.Span	99
Mathlib.RingTheory.AdicCompletion.Completeness (new file)	1559

---

Declarations diff

+ Submodule.image_smul_top_eq_range_lsum
+ Submodule.range_lsum_smul
+ Submodule.smul_top_eq_range_lsum
+ coordinateProj
+ factorPow_powSmulQuotInclusion_comm
+ finsupp_sum
+ finsupp_sumInv
+ finsupp_sumInv_comp_sum
+ finsupp_sumInv_single_of
+ finsupp_sum_comp_sumInv
+ finsupp_sum_single_of
+ instance {ι R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] :
+ isAdicComplete
+ liftOfValZero
+ liftOfValZeroAux
+ liftOfValZeroAux_exists
+ liftOfValZeroAux_prop
+ lmap
+ lmap_apply
+ lsingle_comp_lapply_same
+ map_finsuppLEquivDirectSum_comp_finsupp_sum
+ map_lsum_smul_comp_finsuppSum
+ ofPowSmul
+ ofPowSmul_injective
+ ofPowSmul_liftOfValZero
+ ofPowSmul_val_apply
+ ofPowSmul_val_apply_eq_zero
+ pointwiseScalarModule
+ pointwise_smul_support_finite
+ powSmulQuotInclusion
+ powSmulQuotInclusion_injective
+ powSmulQuotInclusion_range
+ pow_smul_top_eq_eval_ker
+ pow_smul_top_le_eval_ker
+ restrictScalars_image_smul_eq_smul_restrictScalars
+ restrictScalars_ofPowSmul_range_eq_eval_ker
+ span_single_eq_top
+ sum_coordinateProj
+ val_apply_mem_smul_top_iff
- pointwiseScalarSemiring

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[erdOne]

Please give definitions proper signatures.

[erdOne]

Same here.

[erdOne]

And for this I think this is easier to work with

def powSmulQuotInclusion {a b c : ℕ} (h : c = b + a) (N : Submodule R M) : 
    ↑(I ^ a • N) ⧸ (I ^ b • ⊤ : Submodule R ↑(I ^ a • N)) →ₗ[R] M ⧸ (I ^ c • N) :=
  mapQ _ _ (I ^ a • N).subtype <| by simp [← map_le_iff_le_comap, h, pow_add, mul_smul]

[erdOne]

For example, under the new definition, this is just

theorem powSmulQuotInclusion_injective {a b c : ℕ} (h : c = b + a) (N : Submodule R M) : 
    Function.Injective (powSmulQuotInclusion I M h N) := by
  rw [← LinearMap.ker_eq_bot]
  simp [powSmulQuotInclusion, mapQ, ← le_bot_iff, ker_liftQ, LinearMap.ker_comp, pow_add, mul_smul,
    map_le_iff_le_comap, ← Submodule.map_le_map_iff_of_injective (I ^ a • N).subtype_injective, h]

[BryceT233]

Thanks for the suggustions! Indeed, the new definition simplified the arguments a lot

[erdOne]

And there is Submodule.subtype that you can use instead.

[erdOne]

This section shouldn't be here.

[erdOne]

open Classical is usually really bad.

[erdOne]

DirectSum is usually for dependent products. Here it might be better to use Finsupp instead, e.g. something like

lemma Finsupp.span_single_eq_top {R M σ : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] :
    Submodule.span R {Finsupp.single i x | (i : σ) (x : M)} = ⊤ := by
  sorry

open Pointwise in
lemma Finsupp.range_lsum_smul
    {R M N σ : Type*} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M]
    [Module R N] (φ : M →ₗ[R] N) (f : σ → R) :
    (Finsupp.lsum (S := R) (f · • φ)).range = Set.range f • φ.range := by
  simp_rw [LinearMap.range_eq_map,  ← Finsupp.span_single_eq_top,
    ← span_univ, map_span, set_smul_span]
  congr 1
  aesop (add simp Set.mem_smul)

open Pointwise in
theorem image_smul_top_eq_range_directSum {σ : Type*} (s : Set σ) (f : σ → R) :
    (f '' s • ⊤ : Submodule R M) = (Finsupp.lsum (S := R) fun i : s ↦ f i • .id).range := by
  simpa [Set.range_comp] using
    (Finsupp.range_lsum_smul (.id (R := R) (M := M)) (f ∘ (↑) : s → R)).symm

[BryceT233]

I am trying this approach and it might become another PR if I keep doing it. Basically, I think I need to copy the APIs for AdicCompletion.sum and AdicCompletion.sumInv to support the following two definitions:

def finsupp_sum : (σ →₀ (AdicCompletion I M)) →ₗ[AdicCompletion I R] AdicCompletion I (σ →₀ M) :=
  lsum (AdicCompletion I R) (fun i ↦ map I (lsingle i))

variable [Fintype σ]

def finsupp_sumInv : AdicCompletion I (σ →₀ M) →ₗ[AdicCompletion I R] (σ →₀ (AdicCompletion I M)) :=
  (linearEquivFunOnFinite (AdicCompletion I R) (AdicCompletion I M) σ).symm ∘ₗ
    LinearMap.pi (fun i ↦ map I (lapply i))

[erdOne]

Here the equality should be swapped, since we prefer putting the more complex side on the left.
And ⊤ should be generalized to arbitrary N : Submodule R M, saying
((algebraMap S R) '' s • N).restrictScalars S = s • N.restrictScalars S

[BryceT233]

I have updated the necessary APIs to support the finsupp_sum approach. The proof no longer relies on directSum

-awaiting-author