FoxDifferential/Completed/ProCIntegerCoefficients/Augmentation.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmentation
2import FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Basic
3import Mathlib.Algebra.Exact
4import Mathlib.RingTheory.Ideal.Maps
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/FoxDifferential/Completed/ProCIntegerCoefficients/Augmentation.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Completed group algebra coefficients
17This module defines and analyzes the pro-\(C\) integer completed augmentation map and its compatibility with coefficient projections.
18-/
19namespace FoxDifferential
21noncomputable section
23open ProCGroups.Completion
24open ProCGroups.ProC
26universe u
28section Augmentation
30variable (C : ProCGroups.FiniteGroupClass.{u})
32variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
34/-- The canonical trivial group quotient used to read the completed augmentation. -/
35abbrev zcCompletedGroupAlgebraTopIndex : CompletedGroupAlgebraIndexInClass H C :=
36 OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := H))
38omit [IsTopologicalGroup H] in
39/-- The canonical trivial quotient is below every finite quotient index. -/
41 (U : CompletedGroupAlgebraIndexInClass H C) :
42 zcCompletedGroupAlgebraTopIndex C H ≤ U := by
43 change ((OrderDual.ofDual U).1 : Subgroup H) ≤ (⊤ : Subgroup H)
44 exact le_top
46/-- The finite coefficient coordinate of the completed augmentation
47`Z_C[[H]] -> Z_C`. -/
49 (x : ZCCompletedGroupAlgebra C H) (i : ProCIntegerIndex C) :
50 ProCIntegerStage C i := by
51 letI : Fact (0 < i.modulus) := ⟨i.positive⟩
52 exact
53 modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C
56 (i, zcCompletedGroupAlgebraTopIndex C H) x)
58/-- The finite coefficient coordinates of the completed augmentation are compatible. -/
60 (x : ZCCompletedGroupAlgebra C H) {i j : ProCIntegerIndex C} (hij : i ≤ j) :
61 proCIntegerTransition (C := C) hij
62 (zcCompletedGroupAlgebraAugmentationFamily C H x j) =
63 zcCompletedGroupAlgebraAugmentationFamily C H x i := by
64 letI : Fact (0 < i.modulus) := ⟨i.positive⟩
65 letI : Fact (0 < j.modulus) := ⟨j.positive⟩
66 let U := zcCompletedGroupAlgebraTopIndex C H
67 have hx := x.2 (i, U) (j, U) ⟨hij, le_rfl⟩
69 change
70 modNCompletedCoeffMap (n := i.modulus) (m := j.modulus) hij
71 ((modNCompletedGroupAlgebraStageAugmentationInClass j.modulus H C U)
72 (x.1 (j, U))) =
73 (modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C U)
74 (x.1 (i, U))
75 rw [← hx]
76 simp only [zcCompletedGroupAlgebraTransition, RingHom.comp_apply,
77 modNCompletedGroupAlgebraTransitionInClass_id, RingHom.id_apply]
78 change
79 modNCompletedCoeffMap (n := i.modulus) (m := j.modulus) hij
80 ((modNCompletedGroupAlgebraStageAugmentationInClass j.modulus H C U)
81 (x.1 (j, U))) =
82 (modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C U)
84 (n := i.modulus) (m := j.modulus) (G := H) C U hij)
85 (x.1 (j, U)))
86 exact
87 (congrFun
88 (congrArg DFunLike.coe
90 (n := i.modulus) (G := H) C U (m := j.modulus) hij))
91 (x.1 (j, U))).symm
93/-- The completed augmentation `Z_C[[H]] -> Z_C`, obtained by augmenting every finite
94`(Z/nZ)[H/U]` stage at the canonical trivial quotient of `H`. -/
96 ZCCompletedGroupAlgebra C H →+* ZCCoeff C where
97 toFun x :=
98 Subtype.mk
100 (by
101 intro i j hij
102 exact zcCompletedGroupAlgebraAugmentationFamily_compatible C H x hij)
103 map_zero' := by
104 ext i
105 change zcCompletedGroupAlgebraAugmentationFamily C H
106 (0 : ZCCompletedGroupAlgebra C H) i = 0
107 simp only [zcCompletedGroupAlgebraAugmentationFamily, zcCompletedGroupAlgebraProjection_zero, map_zero]
108 map_one' := by
109 ext i
110 change zcCompletedGroupAlgebraAugmentationFamily C H
111 (1 : ZCCompletedGroupAlgebra C H) i = 1
112 simp only [zcCompletedGroupAlgebraAugmentationFamily, zcCompletedGroupAlgebraProjection_one, map_one]
113 map_add' x y := by
114 ext i
115 change zcCompletedGroupAlgebraAugmentationFamily C H (x + y) i =
116 zcCompletedGroupAlgebraAugmentationFamily C H x i +
118 simp only [zcCompletedGroupAlgebraAugmentationFamily, zcCompletedGroupAlgebraProjection_add, map_add]
119 map_mul' x y := by
120 ext i
121 change zcCompletedGroupAlgebraAugmentationFamily C H (x * y) i =
122 zcCompletedGroupAlgebraAugmentationFamily C H x i *
124 simp only [zcCompletedGroupAlgebraAugmentationFamily, zcCompletedGroupAlgebraProjection_mul, map_mul]
126/-- Projection formula for the completed augmentation. -/
127@[simp]
129 (i : ProCIntegerIndex C) (x : ZCCompletedGroupAlgebra C H) :
130 proCIntegerProj (C := C) i (zcCompletedGroupAlgebraAugmentation C H x) =
131 zcCompletedGroupAlgebraAugmentationFamily C H x i :=
132 rfl
134/-- The completed augmentation can be read after projecting to any finite group quotient stage,
135not only the canonical trivial quotient used in its definition. -/
137 (i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
138 proCIntegerProj (C := C) i.1 (zcCompletedGroupAlgebraAugmentation C H x) =
139 modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C i.2
140 (zcCompletedGroupAlgebraProjection C H i x) := by
141 let T := zcCompletedGroupAlgebraTopIndex C H
142 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
143 have hT : T ≤ i.2 := zcCompletedGroupAlgebraTopIndex_le C H i.2
144 have hx := x.2 (i.1, T) i ⟨le_rfl, hT⟩
146 change
147 (modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C T) (x.1 (i.1, T)) =
148 (modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C i.2) (x.1 i)
149 rw [← hx]
150 simp only [zcCompletedGroupAlgebraTransition, RingHom.comp_apply,
151 modNCompletedGroupAlgebraStageCoeffMapInClass_rfl, RingHom.id_apply]
152 exact congrFun
153 (congrArg DFunLike.coe
155 (n := i.1.modulus) (G := H) C hT)) (x.1 i)
157/-- The completed augmentation sends every group-like element to `1`. -/
158@[simp]
159theorem zcCompletedGroupAlgebraAugmentation_groupLike (h : H) :
160 zcCompletedGroupAlgebraAugmentation C H (zcGroupLike C H h) = 1 := by
161 ext i
162 simp only [proCIntegerProj_zcCompletedGroupAlgebraAugmentation, zcCompletedGroupAlgebraAugmentationFamily,
163 zcCompletedGroupAlgebraProjection_groupLike, OrderDual.ofDual_toDual, MonoidAlgebra.of_apply,
166/-- The completed Fox boundary has augmentation zero. -/
167@[simp]
169 {G : Type u} [Group G] (ψ : G →* H) (g : G) :
171 (zcCompletedGroupAlgebraBoundary C ψ g) = 0 := by
172 simp only [zcCompletedGroupAlgebraBoundary, map_sub, zcCompletedGroupAlgebraAugmentation_groupLike, map_one,
173 sub_self]
175/-- The completed augmentation ideal, defined as the kernel of `Z_C[[H]] -> Z_C`. -/
177 Ideal (ZCCompletedGroupAlgebra C H) :=
178 RingHom.ker (zcCompletedGroupAlgebraAugmentation C H)
180/-- The completed augmentation ideal as a subtype. -/
181abbrev ZCCompletedGroupAlgebraAugmentationIdeal : Type u :=
184@[simp]
186 {x : ZCCompletedGroupAlgebra C H} :
187 x ∈ zcCompletedGroupAlgebraAugmentationIdeal C H ↔
188 zcCompletedGroupAlgebraAugmentation C H x = 0 := by
189 rw [zcCompletedGroupAlgebraAugmentationIdeal, RingHom.mem_ker]
191/-- The algebraic standard-generator ideal is contained in the completed augmentation ideal. -/
194 zcCompletedGroupAlgebraAugmentationIdeal C H := by
196 refine Ideal.span_le.2 ?_
197 rintro x ⟨h, rfl⟩
198 change zcGroupLike C H h - 1 ∈ zcCompletedGroupAlgebraAugmentationIdeal C H
200 simp only [map_sub, zcCompletedGroupAlgebraAugmentation_groupLike, map_one, sub_self]
202/-- The completed Fox boundary lands in the completed augmentation ideal. -/
204 {G : Type u} [Group G] (ψ : G →* H) (g : G) :
205 zcCompletedGroupAlgebraBoundary C ψ g ∈
206 zcCompletedGroupAlgebraAugmentationIdeal C H := by
208 simp only [zcCompletedGroupAlgebraAugmentation_boundary]
210/-- If the completed augmentation kernel is the algebraic standard-generator ideal, then a
211surjective completed Fox boundary gives exactness at `Z_C[[H]]`. -/
213 {G : Type u} [Group G] (ψ : G →* H) (hψ : Function.Surjective ψ)
214 (hstandard :
217 Function.Exact
218 (zcToCompletedGroupAlgebra C ψ :
221 ZCCompletedGroupAlgebra C H → ZCCoeff C) := by
222 intro z
223 constructor
224 · intro hz
225 have hzmem :
226 z ∈ zcCompletedGroupAlgebraStandardAugmentationIdeal C H := by
227 rw [hstandard]
229 (C := C) (H := H) (x := z)).2 hz
230 have hzrange :
231 z ∈ LinearMap.range (zcToCompletedGroupAlgebra C ψ) := by
233 C H ψ hψ]
234 exact hzmem
235 exact hzrange
236 · rintro ⟨m, rfl⟩
237 have hmem :
238 zcToCompletedGroupAlgebra C ψ m ∈
243 (C := C) (H := H) (x := zcToCompletedGroupAlgebra C ψ m)).1 hmem
245/-- For a surjective coefficient group map, exactness of the algebraic completed Fox tail is
246equivalent to the algebraic standard-generator ideal already being the completed augmentation
247ideal. This isolates the closed-range obstruction for infinite completed group algebras. -/
249 {G : Type u} [Group G] (ψ : G →* H) (hψ : Function.Surjective ψ) :
250 Function.Exact
251 (zcToCompletedGroupAlgebra C ψ :
254 ZCCompletedGroupAlgebra C H → ZCCoeff C) ↔
256 zcCompletedGroupAlgebraAugmentationIdeal C H := by
257 constructor
258 · intro hexact
259 apply le_antisymm
261 · intro z hz
262 have hz0 :
263 zcCompletedGroupAlgebraAugmentation C H z = 0 :=
265 (C := C) (H := H) (x := z)).1 hz
266 rcases (hexact z).1 hz0 with ⟨m, hm⟩
267 have hzrange :
268 z ∈ LinearMap.range (zcToCompletedGroupAlgebra C ψ) := ⟨m, hm⟩
270 C H ψ hψ] at hzrange
271 · intro hstandard
272 exact
274 C H ψ hψ hstandard
276/-- The completed augmentation is surjective. -/
278 Function.Surjective (zcCompletedGroupAlgebraAugmentation C H) := by
279 intro a
280 refine ⟨⟨fun i => ?_, ?_⟩, ?_⟩
281 · letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
282 exact MonoidAlgebra.single
283 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
284 (proCIntegerProj (C := C) i.1 a)
285 · intro i j hij
286 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
287 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
288 change zcCompletedGroupAlgebraTransition C H hij
289 (MonoidAlgebra.single
290 (1 : CompletedGroupAlgebraQuotientInClass H C j.2)
291 (proCIntegerProj (C := C) j.1 a)) =
292 MonoidAlgebra.single
293 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
294 (proCIntegerProj (C := C) i.1 a)
296 have ha :
297 modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1
298 (proCIntegerProj (C := C) j.1 a) =
299 proCIntegerProj (C := C) i.1 a :=
300 proCIntegerProj_transition (C := C) hij.1 a
301 simpa using congrArg
302 (fun b : ProCIntegerStage C i.1 =>
303 MonoidAlgebra.single
304 (1 : CompletedGroupAlgebraQuotientInClass H C i.2) b)
305 ha
306 · ext i
307 let T := zcCompletedGroupAlgebraTopIndex C H
308 letI : Fact (0 < i.modulus) := ⟨i.positive⟩
309 change
310 (modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C T)
311 (MonoidAlgebra.single
312 (1 : CompletedGroupAlgebraQuotientInClass H C T)
313 (proCIntegerProj (C := C) i a)) =
314 proCIntegerProj (C := C) i a
317end Augmentation
319end
321end FoxDifferential