FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/InClass/Augmentation.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.StageCoeffMap
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/InClass/Augmentation.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed coefficient algebras
14Coefficient algebras, residue stages, and completed group-algebra maps are kept as the scalar layer for completed Fox calculus.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups.InverseSystems
21open ProCGroups.ProC
23universe u
25variable (n : ℕ) [Fact (0 < n)]
26variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28/-- The augmentation on one class-restricted residue-coefficient finite stage. -/
30 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
31 ModNCompletedGroupAlgebraStageInClass n G C U →+* ModNCompletedCoeff n :=
32 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)
33 (CompletedGroupAlgebraQuotientInClass G C U)
34 (1 : CompletedGroupAlgebraQuotientInClass G C U →* ModNCompletedCoeff n)
36omit [Fact (0 < n)] in
37/-- Evaluation formula for modNCompletedGroupAlgebraStageAugmentationInClass_of. -/
38@[simp]
40 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
41 (q : CompletedGroupAlgebraQuotientInClass G C U) :
43 (MonoidAlgebra.of (ModNCompletedCoeff n) _ q) = 1 := by
44 classical
45 simp only [modNCompletedGroupAlgebraStageAugmentationInClass, MonoidAlgebra.of, MonoidAlgebra.single,
46 MonoidHom.coe_mk, OneHom.coe_mk, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul,
47 mul_one]
49omit [Fact (0 < n)] in
50/-- 法 n 係数で定めた 有限群クラスを固定した augmentation または augmentation ideal への標準写像が群環の単項基底元を有限商段階の対応する単項基底元へ送ることを述べる。 -/
51@[simp]
53 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
54 (q : CompletedGroupAlgebraQuotientInClass G C U) (a : ModNCompletedCoeff n) :
56 (MonoidAlgebra.single q a) = a := by
57 classical
58 simp only [modNCompletedGroupAlgebraStageAugmentationInClass, MonoidAlgebra.single, RingHom.coe_coe,
59 MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one]
61omit [Fact (0 < n)] in
62/-- Compatibility lemma modNCompletedGroupAlgebraStageAugmentationInClass_compatible. -/
63@[simp 900]
65 (C : ProCGroups.FiniteGroupClass.{u})
66 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
67 (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
68 (modNCompletedGroupAlgebraTransitionInClass n G C hUV) =
69 modNCompletedGroupAlgebraStageAugmentationInClass n G C V := by
70 apply RingHom.ext
71 intro x
72 refine MonoidAlgebra.induction_on
73 (p := fun x =>
74 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
75 (modNCompletedGroupAlgebraTransitionInClass n G C hUV)) x =
77 x ?_ ?_ ?_
78 · intro q
79 rw [RingHom.comp_apply, modNCompletedGroupAlgebraTransitionInClass_of]
80 simp only [modNCompletedGroupAlgebraStageAugmentationInClass, MonoidAlgebra.single, RingHom.coe_coe,
81 MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one, MonoidAlgebra.of, MonoidHom.coe_mk,
82 OneHom.coe_mk]
83 · intro x y hx hy
84 simp only [RingHom.map_add, hx, hy]
85 · intro a x hx
86 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
87 have hcoeff :
88 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
89 (modNCompletedGroupAlgebraTransitionInClass n G C hUV))
90 (algebraMap (ModNCompletedCoeff n)
91 (ModNCompletedGroupAlgebraStageInClass n G C V) a) =
93 (algebraMap (ModNCompletedCoeff n)
94 (ModNCompletedGroupAlgebraStageInClass n G C V) a) := by
95 simp only [modNCompletedGroupAlgebraStageAugmentationInClass, modNCompletedGroupAlgebraTransitionInClass,
96 MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
97 RingHom.comp_apply, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one, RingHom.coe_coe,
98 MonoidAlgebra.lift_single, smul_eq_mul, mul_one]
99 rw [hcoeff]
101omit [Fact (0 < n)] in
102/-- Composition lemma modNCompletedGroupAlgebraStageAugmentationInClass_comp_stageMap. -/
103@[simp 900]
105 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
106 (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
107 (modNCompletedGroupAlgebraStageMapInClass n G C U) =
108 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
109 (1 : G →* ModNCompletedCoeff n) := by
110 apply RingHom.ext
111 intro x
112 refine MonoidAlgebra.induction_on
113 (p := fun x =>
114 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
115 (modNCompletedGroupAlgebraStageMapInClass n G C U)) x =
116 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
117 (1 : G →* ModNCompletedCoeff n)) x)
118 x ?_ ?_ ?_
119 · intro g
120 rw [RingHom.comp_apply, modNCompletedGroupAlgebraStageMapInClass_of]
121 simp only [modNCompletedGroupAlgebraStageAugmentationInClass, MonoidAlgebra.single, RingHom.coe_coe,
122 MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one, MonoidAlgebra.of, MonoidHom.coe_mk,
123 OneHom.coe_mk]
124 · intro x y hx hy
126 · intro a x hx
127 have hcoeff :
128 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
129 (modNCompletedGroupAlgebraStageMapInClass n G C U))
130 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) = a := by
131 simp only [modNCompletedGroupAlgebraStageAugmentationInClass, modNCompletedGroupAlgebraStageMapInClass,
132 MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
133 RingHom.comp_apply, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one, RingHom.coe_coe,
134 MonoidAlgebra.lift_single, smul_eq_mul, mul_one]
135 have hcoeff' :
136 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
137 (modNCompletedGroupAlgebraStageMapInClass n G C U))
138 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) =
139 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
140 (1 : G →* ModNCompletedCoeff n))
141 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) := by
142 rw [hcoeff]
143 simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,
144 MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one]
145 rw [Algebra.smul_def]
146 calc
147 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
148 (modNCompletedGroupAlgebraStageMapInClass n G C U))
149 ((algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) * x)
150 =
151 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
152 (modNCompletedGroupAlgebraStageMapInClass n G C U))
153 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) *
154 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
155 (modNCompletedGroupAlgebraStageMapInClass n G C U)) x := by
156 rw [RingHom.map_mul]
157 _ =
158 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
159 (modNCompletedGroupAlgebraStageMapInClass n G C U))
160 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) *
161 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
162 (1 : G →* ModNCompletedCoeff n)) x := by
163 rw [hx]
164 _ =
165 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
166 (1 : G →* ModNCompletedCoeff n))
167 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) *
168 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
169 (1 : G →* ModNCompletedCoeff n)) x := by
170 rw [hcoeff']
171 _ =
172 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
173 (1 : G →* ModNCompletedCoeff n))
174 ((algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) * x) := by
175 exact
177 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G
178 (1 : G →* ModNCompletedCoeff n))
179 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) x).symm
181omit [Fact (0 < n)] in
182/-- Stage augmentations commute with coefficient reduction on class-restricted finite quotient
183stages. -/
184@[simp 900]
186 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
187 {m : ℕ} [Fact (0 < m)] (hnm : n ∣ m) :
188 (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
190 (n := n) (m := m) (G := G) C U hnm) =
191 (modNCompletedCoeffMap (n := n) (m := m) hnm).comp
192 (modNCompletedGroupAlgebraStageAugmentationInClass m G C U) := by
193 apply RingHom.ext
194 intro x
195 refine MonoidAlgebra.induction_on
196 (p := fun x =>
197 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
199 (n := n) (m := m) (G := G) C U hnm)) x =
200 ((modNCompletedCoeffMap (n := n) (m := m) hnm).comp
201 (modNCompletedGroupAlgebraStageAugmentationInClass m G C U)) x)
202 x ?_ ?_ ?_
203 · intro q
204 rw [RingHom.comp_apply, RingHom.comp_apply,
208 exact (map_one (modNCompletedCoeffMap (n := n) (m := m) hnm)).symm
209 · intro x y hx hy
210 simp only [RingHom.map_add, hx, RingHom.coe_comp, Function.comp_apply, hy]
211 · intro a x hx
212 letI : Algebra (ModNCompletedCoeff m) (ModNCompletedCoeff n) :=
213 ZMod.algebra' (R := ModNCompletedCoeff n) (m := n) (n := m) hnm
214 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
215 have hcoeff :
216 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
218 (n := n) (m := m) (G := G) C U hnm))
219 (algebraMap (ModNCompletedCoeff m)
220 (ModNCompletedGroupAlgebraStageInClass m G C U) a) =
221 ((modNCompletedCoeffMap (n := n) (m := m) hnm).comp
223 (algebraMap (ModNCompletedCoeff m)
224 (ModNCompletedGroupAlgebraStageInClass m G C U) a) := by
225 have hleft :
226 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
228 (n := n) (m := m) (G := G) C U hnm))
229 (algebraMap (ModNCompletedCoeff m)
230 (ModNCompletedGroupAlgebraStageInClass m G C U) a) =
231 algebraMap (ModNCompletedCoeff m) (ModNCompletedCoeff n) a := by
232 simp only [modNCompletedGroupAlgebraStageAugmentationInClass, modNCompletedGroupAlgebraStageCoeffMapInClass,
233 modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,
234 RingHom.coe_id, Function.comp_apply, id_eq, RingHom.comp_apply, RingHom.coe_coe, MonoidAlgebra.lift_single,
235 MonoidAlgebra.of_apply, Algebra.smul_def, MonoidAlgebra.single_mul_single, mul_one,
236 MonoidHom.one_apply]
237 have hright :
238 ((modNCompletedCoeffMap (n := n) (m := m) hnm).comp
240 (algebraMap (ModNCompletedCoeff m)
241 (ModNCompletedGroupAlgebraStageInClass m G C U) a) =
242 algebraMap (ModNCompletedCoeff m) (ModNCompletedCoeff n) a := by
243 simp only [modNCompletedGroupAlgebraStageAugmentationInClass, MonoidAlgebra.coe_algebraMap,
244 Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq, RingHom.comp_apply, RingHom.coe_coe,
245 MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one]
246 rfl
247 exact hleft.trans hright.symm
248 rw [hcoeff]
250end
252end FoxDifferential