Skip to content

Commit a12a22f

Browse files
BryceT233pre-commit-ci-lite[bot]
BryceT233
and
pre-commit-ci-lite[bot]
committed
feat(RingTheory/AdicCompletion): completeness of AdicCompletion (leanprover-community#35670)
This is the last PR split from leanprover-community#34936, which follows [[Stacks 05GG](https://stacks.math.columbia.edu/tag/05GG)] and formalizes the result that `AdicCompletion I M` is `I`-adically complete when the ideal `I` is finitely generated. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
1 parent 70599e7 commit a12a22f

4 files changed

Lines changed: 230 additions & 7 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6142,6 +6142,7 @@ public import Mathlib.RepresentationTheory.Tannaka
61426142
public import Mathlib.RingTheory.AdicCompletion.Algebra
61436143
public import Mathlib.RingTheory.AdicCompletion.AsTensorProduct
61446144
public import Mathlib.RingTheory.AdicCompletion.Basic
6145+
public import Mathlib.RingTheory.AdicCompletion.Completeness
61456146
public import Mathlib.RingTheory.AdicCompletion.Exactness
61466147
public import Mathlib.RingTheory.AdicCompletion.Functoriality
61476148
public import Mathlib.RingTheory.AdicCompletion.LocalRing

‎Mathlib/LinearAlgebra/SModEq/Basic.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ module
88
public import Mathlib.Algebra.Module.Submodule.Map
99
public import Mathlib.Algebra.Polynomial.Eval.Defs
1010
public import Mathlib.RingTheory.Ideal.Quotient.Defs
11+
public import Mathlib.Algebra.Module.Submodule.RestrictScalars
1112

1213
/-!
1314
# modular equivalence for submodule
@@ -162,6 +163,10 @@ theorem eval {R : Type*} [CommRing R] {I : Ideal R} {x y : R} (h : x ≡ y [SMOD
162163
simp_rw [Polynomial.eval_eq_sum, Polynomial.sum]
163164
gcongr
164165

166+
variable (S) in
167+
theorem restrictScalars [SMul S R] [IsScalarTower S R M] : x ≡ y [SMOD U.restrictScalars S] ↔
168+
x ≡ y [SMOD U] := by simp [SModEq.sub_mem]
169+
165170
theorem idealQuotientMk {R : Type*} [CommRing R] {I : Ideal R} {x y : R} :
166171
x ≡ y [SMOD I] ↔ Ideal.Quotient.mk I x = Ideal.Quotient.mk I y := Iff.rfl
167172

‎Mathlib/RingTheory/AdicCompletion/Basic.lean‎

Lines changed: 30 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -72,12 +72,10 @@ theorem IsHausdorff.eq_iff_smodEq [IsHausdorff I M] {x y : M} :
7272
apply IsHausdorff.haus' (I := I) (x - y)
7373
simpa [SModEq.sub_mem] using h
7474

75-
theorem IsHausdorff.map_algebraMap_iff [CommRing S] [Algebra R S] :
76-
IsHausdorff (I.map (algebraMap R S)) S ↔ IsHausdorff I S := by
77-
simp only [isHausdorff_iff, smul_eq_mul, Ideal.mul_top, Ideal.smul_top_eq_map]
78-
congr!
79-
simp only [← Ideal.map_pow]
80-
rfl
75+
theorem IsHausdorff.map_algebraMap_iff [CommRing S] [Module S M] [Algebra R S]
76+
[IsScalarTower R S M] : IsHausdorff (I.map (algebraMap R S)) M ↔ IsHausdorff I M := by
77+
simp [isHausdorff_iff, ← Ideal.map_pow, ← SModEq.restrictScalars R,
78+
restrictScalars_map_smul_eq]
8179

8280
theorem IsHausdorff.of_map [CommRing S] [Module S M] {J : Ideal S} [Algebra R S]
8381
[IsScalarTower R S M] (hIJ : I.map (algebraMap R S) ≤ J) [IsHausdorff J M] :
@@ -151,6 +149,11 @@ theorem isPrecomplete_iff :
151149
∃ L : M, ∀ n, f n ≡ L [SMOD (I ^ n • ⊤ : Submodule R M)] :=
152150
⟨fun h => h.1, fun h => ⟨h⟩⟩
153151

152+
theorem IsPrecomplete.map_algebraMap_iff [CommRing S] [Module S M] [Algebra R S]
153+
[IsScalarTower R S M] : IsPrecomplete (I.map (algebraMap R S)) M ↔ IsPrecomplete I M := by
154+
simp [isPrecomplete_iff, ← Ideal.map_pow, ← SModEq.restrictScalars R,
155+
restrictScalars_map_smul_eq]
156+
154157
variable (I M)
155158

156159
/-- The Hausdorffification of a module with respect to an ideal. -/
@@ -164,7 +167,7 @@ abbrev AdicCompletion.transitionMap {m n : ℕ} (hmn : m ≤ n) := factorPow I M
164167
/-- The completion of a module with respect to an ideal.
165168
166169
This is Hausdorff but not necessarily complete: a classical sufficient condition for
167-
completeness is that `M` be finitely generated [Stacks, 0G1Q]. -/
170+
completeness is that `I` be finitely generated [Stacks, 05GG]. -/
168171
def AdicCompletion : Type _ :=
169172
{ f : ∀ n : ℕ, M ⧸ (I ^ n • ⊤ : Submodule R M) //
170173
∀ {m n} (hmn : m ≤ n), AdicCompletion.transitionMap I M hmn (f n) = f m }
@@ -675,12 +678,32 @@ theorem of_ofLinearEquiv_symm (x : AdicCompletion I M) :
675678

676679
end Bijective
677680

681+
set_option backward.isDefEq.respectTransparency false in
682+
theorem pow_smul_top_le_ker_eval (n : ℕ) : I ^ n • ⊤ ≤ (eval I M n).ker := by
683+
simp only [smul_le, mem_top, LinearMap.mem_ker, map_smul, coe_eval, forall_const]
684+
intro r r_in x
685+
rw [← Submodule.Quotient.mk_out (x.val n), ← Quotient.mk_smul, Quotient.mk_eq_zero]
686+
exact smul_mem_smul r_in mem_top
687+
688+
set_option backward.isDefEq.respectTransparency false in
689+
lemma val_apply_mem_smul_top_iff {m n : ℕ} {x : AdicCompletion I M}
690+
(m_ge : n ≤ m) : x.val m ∈ I ^ n • (⊤ : Submodule R (M ⧸ I ^ m • ⊤)) ↔ x.val n = 0 := by
691+
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
692+
· rw [← x.prop m_ge, transitionMap, Submodule.factorPow, Submodule.factor, mapQ,
693+
← LinearMap.mem_ker]
694+
simpa [ker_liftQ]
695+
simpa [mapQ, h, ← LinearMap.mem_ker, ker_liftQ] using x.prop m_ge
696+
678697
end AdicCompletion
679698

680699
namespace IsAdicComplete
681700

682701
open AdicCompletion
683702

703+
theorem map_algebraMap_iff [CommRing S] [Module S M] [Algebra R S]
704+
[IsScalarTower R S M] : IsAdicComplete (I.map (algebraMap R S)) M ↔ IsAdicComplete I M := by
705+
simp [isAdicComplete_iff, IsPrecomplete.map_algebraMap_iff, IsHausdorff.map_algebraMap_iff]
706+
684707
section lift
685708

686709
variable [IsAdicComplete I N]

‎Mathlib/RingTheory/AdicCompletion/Completeness.lean‎

Lines changed: 194 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,194 @@
1+
/-
2+
Copyright (c) 2026 Bingyu Xia. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Bingyu Xia
5+
-/
6+
module
7+
8+
public import Mathlib.Algebra.Lie.OfAssociative
9+
public import Mathlib.RingTheory.AdicCompletion.Exactness
10+
public import Mathlib.RingTheory.Finiteness.Ideal
11+
12+
/-!
13+
# Completeness of the Adic Completion for Finitely Generated Ideals
14+
15+
This file establishes that `AdicCompletion I M` is itself `I`-adically complete
16+
when the ideal `I` is finitely generated.
17+
18+
## Main definitions
19+
20+
* `AdicCompletion.ofPowSMul`: The canonical inclusion between adic completions
21+
induced by the inclusion from `I ^ n • M` to `M`.
22+
23+
* `AdicCompletion.ofValEqZero`: Given `x` in `AdicCompletion I M` projecting to zero
24+
in `M / I ^ n • M`, `ofValEqZero` constructs the corresponding element in
25+
the adic completion of `I ^ n • M`.
26+
27+
## Main results
28+
29+
* `AdicCompletion.pow_smul_top_eq_ker_eval`: `I ^ n • AdicCompletion I M` is exactly the kernel
30+
of the evaluation map `eval I M n` when `I` is finitely generated.
31+
32+
* `AdicCompletion.isAdicComplete`: `AdicCompletion I M` is `I`-adically complete if `I` is
33+
finitely generated.
34+
35+
-/
36+
37+
public section
38+
39+
noncomputable section
40+
41+
open Submodule Finsupp
42+
43+
variable {R : Type*} [CommRing R] (I : Ideal R)
44+
variable {M : Type*} [AddCommGroup M] [Module R M]
45+
variable {a b c : ℕ}
46+
47+
namespace AdicCompletion
48+
49+
variable (M) in
50+
/-- The canonical inclusion from the adic completion of `I ^ n • M` to
51+
the adic completion of `M`. -/
52+
abbrev ofPowSMul (n : ℕ) : AdicCompletion I ↥(I ^ n • ⊤ : Submodule R M)
53+
→ₗ[AdicCompletion I R] AdicCompletion I M := map I (I ^ n • ⊤ : Submodule R M).subtype
54+
55+
theorem ofPowSMul_val_apply (h : c = b + a) {x : AdicCompletion I ↥(I ^ a • ⊤ : Submodule R M)} :
56+
(ofPowSMul I M a x).val c = powSMulQuotInclusion I M h ⊤ (x.val b) := by
57+
rw [← x.prop (show b ≤ c by lia), map_val_apply]
58+
refine Quotient.induction_on _ (x.val c) fun z ↦ ?_
59+
simp [powSMulQuotInclusion]
60+
61+
theorem ofPowSMul_val_apply_eq_zero (h : a ≤ b)
62+
{x : AdicCompletion I ↥(I ^ b • ⊤ : Submodule R M)} : (ofPowSMul I M b x).val a = 0 := by
63+
rw [map_val_apply]
64+
refine Quotient.induction_on _ (x.val a) fun z ↦ ?_
65+
simpa using pow_smul_top_le _ _ h z.prop
66+
67+
set_option backward.isDefEq.respectTransparency false in
68+
theorem ofPowSMul_injective (n : ℕ) : Function.Injective (ofPowSMul I M n) := by
69+
rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
70+
intro x hx; ext i
71+
simp only [AdicCompletion.ext_iff, val_zero, Pi.zero_apply] at hx
72+
specialize hx (i + n)
73+
rw [ofPowSMul_val_apply I (by rw [add_comm]),
74+
LinearMap.map_eq_zero_iff _ (powSMulQuotInclusion_injective ..)] at hx
75+
simp [hx]
76+
77+
private lemma ofValEqZeroAux_exists {x : AdicCompletion I M} (h : c = b + a)
78+
(ha : x.val a = 0) : ∃ t, powSMulQuotInclusion I M h ⊤ t = x.val c := by
79+
simpa [← LinearMap.mem_range, range_powSMulQuotInclusion] using
80+
(val_apply_mem_smul_top_iff I (show a ≤ c by lia)).mpr ha
81+
82+
/-- An auxillary lift function used in the definition of `ofValEqZero`.
83+
Use `ofValEqZero` instead. -/
84+
def ofValEqZeroAux {x : AdicCompletion I M} (h : c = b + a) (ha : x.val a = 0) :
85+
↥(I ^ a • ⊤ : Submodule R M) ⧸ I ^ b • (⊤ : Submodule R ↥(I ^ a • ⊤ : Submodule R M)) :=
86+
Exists.choose (ofValEqZeroAux_exists I h ha)
87+
88+
private lemma ofValEqZeroAux_prop {x : AdicCompletion I M} (h : c = b + a)
89+
(ha : x.val a = 0) : (powSMulQuotInclusion I M h ⊤) (ofValEqZeroAux I h ha) = x.val c :=
90+
Exists.choose_spec (ofValEqZeroAux_exists I h ha)
91+
92+
/-- Given an element `x` in the adic completion of `M` whose projection to `M / I ^ n • M` is zero,
93+
`ofValEqZero` constructs the corresponding element in the adic completion of `I ^ n • M`. -/
94+
@[no_expose]
95+
def ofValEqZero {n : ℕ} {x : AdicCompletion I M} (hxn : x.val n = 0) :
96+
AdicCompletion I ↥(I ^ n • (⊤ : Submodule R M)) where
97+
val i := ofValEqZeroAux I (Eq.refl (i + n)) hxn
98+
property {i j} h := by
99+
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
100+
rw [← (powSMulQuotInclusion_injective I (by rfl) ⊤).eq_iff, ofValEqZeroAux_prop,
101+
← LinearMap.comp_apply, ← factorPow_comp_powSMulQuotInclusion I (by rfl)
102+
(show i + k + n = k + (i + n) by ring), LinearMap.comp_apply, ofValEqZeroAux_prop]
103+
exact x.prop (by lia)
104+
105+
@[simp]
106+
theorem ofPowSMul_ofValEqZero {n : ℕ} {x : AdicCompletion I M} (hxn : x.val n = 0) :
107+
ofPowSMul I M n (ofValEqZero I hxn) = x := by
108+
ext i; by_cases! h : n ≤ i
109+
· obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' h
110+
rw [ofPowSMul_val_apply _ (by rfl), ofValEqZero, ofValEqZeroAux_prop]
111+
rw [ofPowSMul_val_apply_eq_zero _ h.le, ← x.prop h.le, hxn, _root_.map_zero]
112+
113+
set_option backward.isDefEq.respectTransparency false in
114+
theorem restrictScalars_range_ofPowSMul_eq_ker_eval {n : ℕ} :
115+
(ofPowSMul I M n).range.restrictScalars R = (eval I M n).ker := by
116+
refine le_antisymm (fun x hx ↦ ?_) (fun x hx ↦ ?_)
117+
· rcases hx with ⟨y, rfl⟩
118+
rw [LinearMap.mem_ker, eval_apply, ofPowSMul_val_apply_eq_zero _ (by rfl)]
119+
simp only [LinearMap.mem_ker, coe_eval] at hx
120+
use ofValEqZero I hx; simp
121+
122+
set_option backward.isDefEq.respectTransparency false in
123+
/- An intermediate helper lemma for the theorem below to avoid introducing
124+
`AdicCompletion.finsuppSum` (the `Finsupp` version of `AdicCompletion.sum`).
125+
It proves the equality of two linear maps:
126+
127+
The LHS evaluates a linear combination with coefficients `f i` on
128+
the direct sum of the completed modules `AdicCompletion I M`.
129+
130+
The RHS first commutes the direct sum and the completion via `sumEquivOfFintype`,
131+
and then applies the completion of the standard linear combination operator on `M`. -/
132+
private lemma lsum_smul_comp_finsuppLEquivDirectSum_symm {ι : Type*} [DecidableEq ι] [Fintype ι]
133+
(f : ι → R) : ((lsum (AdicCompletion I R))
134+
fun i ↦ ((algebraMap R (AdicCompletion I R)) (f i) • .id :
135+
AdicCompletion I M →ₗ[AdicCompletion I R] AdicCompletion I M)) ∘ₗ
136+
(finsuppLEquivDirectSum (AdicCompletion I R) (AdicCompletion I M) ι).symm.toLinearMap =
137+
(map I (lsum R fun i ↦ f i • .id) ∘ₗ map I (finsuppLEquivDirectSum R M ι).symm.toLinearMap) ∘ₗ
138+
(sumEquivOfFintype I (fun _ : ι ↦ M)) := by
139+
ext
140+
-- simp [-algebraMap_smul, algebraMap_apply, -smul_eq_mul]
141+
simp only [algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply, LinearMap.coe_comp,
142+
coe_lsum, LinearMap.coe_smul, LinearMap.id_coe, LinearEquiv.coe_coe, Function.comp_apply,
143+
finsuppLEquivDirectSum_symm_lof, Pi.smul_apply, id_eq, smul_zero, sum_single_index, smul_eval,
144+
mapQ_eq_factor, factor_eq_factor, of_apply, mkQ_apply, Ideal.Quotient.mk_eq_mk, mk_apply_coe,
145+
sumEquivOfFintype_apply, sum_lof, map_mk, AdicCauchySequence.map_apply_coe, map_smul]
146+
rw [← Ideal.Quotient.algebraMap_eq, algebraMap_smul]
147+
148+
set_option backward.isDefEq.respectTransparency false in
149+
variable {I} in
150+
@[stacks 05GG "(2)"]
151+
theorem pow_smul_top_eq_ker_eval {n : ℕ} (h : I.FG) : I ^ n • ⊤ = (eval I M n).ker := by
152+
classical
153+
refine le_antisymm (pow_smul_top_le_ker_eval ..) ?_
154+
replace h := Ideal.FG.pow (n := n) h
155+
rcases h with ⟨s, hs⟩
156+
simp only [← hs, span_smul_eq]
157+
rw [← restrictScalars_top R (AdicCompletion I R) (AdicCompletion I M),
158+
← restrictScalars_image_smul_eq (R := AdicCompletion I R),
159+
← restrictScalars_range_ofPowSMul_eq_ker_eval, restrictScalars_le,
160+
image_smul_top_eq_range_lsum]
161+
simp only [SetLike.coe_sort_coe]
162+
rw [← LinearMap.range_comp_of_range_eq_top (f := (finsuppLEquivDirectSum ..).symm.toLinearMap)
163+
_ (by simp), lsum_smul_comp_finsuppLEquivDirectSum_symm,
164+
LinearMap.range_comp_of_range_eq_top _ (LinearEquiv.range _),
165+
LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_eq_top_of_surjective _ <|
166+
Function.RightInverse.surjective (g := map I (finsuppLEquivDirectSum R M s)) (fun _ ↦ by
167+
simp [← LinearMap.comp_apply, map_comp]))]
168+
rintro _ ⟨x, rfl⟩
169+
have : Function.Surjective ((lsum R fun i : s ↦ i.val • (LinearMap.id : M →ₗ[R] M)).codRestrict
170+
(I ^ n • ⊤) (fun _ ↦ by simp [← hs, span_smul_eq, smul_top_eq_range_lsum])) := by
171+
rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict, ← hs, span_smul_eq,
172+
smul_top_eq_range_lsum]
173+
simp
174+
rcases map_surjective I this x with ⟨x, rfl⟩
175+
exact ⟨x, by rw [← LinearMap.comp_apply, map_comp, LinearMap.subtype_comp_codRestrict]⟩
176+
177+
variable {I} in
178+
/-- `AdicCompletion I M` is adic complete when `I` is finitely generated. -/
179+
@[stacks 05GG "(1)"]
180+
theorem isAdicComplete (h : I.FG) : IsAdicComplete I (AdicCompletion I M) where
181+
prec' x hx := by
182+
let L : AdicCompletion I M := {
183+
val i := (x i).val i
184+
property {m n} h' := by
185+
simp only [transitionMap_comp_eval_apply]
186+
specialize hx h'
187+
rwa [SModEq.sub_mem, pow_smul_top_eq_ker_eval h, LinearMap.mem_ker, _root_.map_sub,
188+
sub_eq_zero, eval_apply, eval_apply, eq_comm] at hx
189+
}
190+
use L; intro i
191+
rw [SModEq.sub_mem, pow_smul_top_eq_ker_eval h]
192+
simp [L]
193+
194+
end AdicCompletion

0 commit comments

Comments
 (0)