FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/InClass/Basic.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebra
2import Mathlib.Data.ZMod.Basic
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/InClass/Basic.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Completed coefficient algebras
15Coefficient algebras, residue stages, and completed group-algebra maps are kept as the scalar layer for completed Fox calculus.
16-/
17namespace FoxDifferential
19noncomputable section
21open ProCGroups.InverseSystems
22open ProCGroups.ProC
24universe u
27variable (n : ℕ) [Fact (0 < n)]
28variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
30omit [Fact (0 < n)] in
31/-- The coefficient ring `Z/nZ` used in one residue-coefficient stage. -/
32abbrev ModNCompletedCoeff : Type := ZMod n
34omit [Fact (0 < n)] in
35/-- The group ring `(ZMod n)[H]` used in the residue-coefficient tower. -/
36abbrev ModNCompletedGroupRing (H : Type*) : Type _ :=
37 MonoidAlgebra (ModNCompletedCoeff n) H
39omit [Fact (0 < n)] in
40/-- The residue-coefficient stage over a class-restricted finite quotient `G/U`. -/
42 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) : Type _ :=
43 ModNCompletedGroupRing n (CompletedGroupAlgebraQuotientInClass G C U)
45/-- 法 n 係数で定めた 有限群クラスを固定した 標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
47 (C : ProCGroups.FiniteGroupClass.{u})
48 (hFinite : ∀ {Q : Type u} [Group Q], C Q → Finite Q)
49 (U : CompletedGroupAlgebraIndexInClass G C) :
50 Finite (ModNCompletedGroupAlgebraStageInClass n G C U) := by
51 classical
52 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
53 hFinite (OrderDual.ofDual U).2
54 letI : Fintype (CompletedGroupAlgebraQuotientInClass G C U) := Fintype.ofFinite _
55 letI : DecidableEq (CompletedGroupAlgebraQuotientInClass G C U) := Classical.decEq _
56 letI : NeZero n := ⟨Nat.ne_of_gt (show 0 < n from Fact.out)⟩
57 letI : Fintype (ModNCompletedCoeff n) := Fintype.ofEquiv (Fin n) (ZMod.finEquiv n)
58 letI :
59 Finite (CompletedGroupAlgebraQuotientInClass G C U → ModNCompletedCoeff n) := by
60 letI :
61 Fintype (CompletedGroupAlgebraQuotientInClass G C U → ModNCompletedCoeff n) :=
62 inferInstance
63 exact Finite.of_fintype _
64 let f :
65 ModNCompletedGroupAlgebraStageInClass n G C U →
66 CompletedGroupAlgebraQuotientInClass G C U → ModNCompletedCoeff n := fun x q => x q
67 refine Finite.of_injective f ?_
68 intro x y hxy
69 ext q
70 exact congrFun hxy q
72omit [Fact (0 < n)] in
73/-- The transition map between class-restricted residue-coefficient stages. -/
75 (C : ProCGroups.FiniteGroupClass.{u})
76 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
77 ModNCompletedGroupAlgebraStageInClass n G C V →+*
78 ModNCompletedGroupAlgebraStageInClass n G C U :=
79 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
80 (OpenNormalSubgroupInClass.map
81 (C := C) (G := G)
82 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
84omit [Fact (0 < n)] in
85/-- Evaluation formula for modNCompletedGroupAlgebraTransitionInClass_of. -/
86@[simp]
88 (C : ProCGroups.FiniteGroupClass.{u})
89 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
90 (g : CompletedGroupAlgebraQuotientInClass G C V) :
91 modNCompletedGroupAlgebraTransitionInClass n G C hUV
92 (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
93 MonoidAlgebra.single
94 ((OpenNormalSubgroupInClass.map
95 (C := C) (G := G)
96 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1 := by
97 classical
98 simp only [modNCompletedGroupAlgebraTransitionInClass, MonoidAlgebra.of, MonoidAlgebra.single,
99 MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
100 rfl
102omit [Fact (0 < n)] in
103/-- 法 n 係数で定めた 有限群クラスを固定した 遷移写像が群環の単項基底元を有限商段階の対応する単項基底元へ送ることを述べる。 -/
104@[simp]
106 (C : ProCGroups.FiniteGroupClass.{u})
107 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
108 (q : CompletedGroupAlgebraQuotientInClass G C V)
109 (a : ModNCompletedCoeff n) :
111 (MonoidAlgebra.single q a) =
112 MonoidAlgebra.single
113 ((OpenNormalSubgroupInClass.map
114 (C := C) (G := G)
115 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) a := by
116 classical
117 simp only [modNCompletedGroupAlgebraTransitionInClass, MonoidAlgebra.mapDomainRingHom_apply,
118 Finsupp.mapDomain_single]
119 rfl
121omit [Fact (0 < n)] in
122/-- Identity case for modNCompletedGroupAlgebraTransitionInClass_id. -/
123@[simp]
125 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
126 modNCompletedGroupAlgebraTransitionInClass n G C (le_rfl : U ≤ U) = RingHom.id _ := by
127 rw [modNCompletedGroupAlgebraTransitionInClass, OpenNormalSubgroupInClass.map_id]
128 exact MonoidAlgebra.mapDomainRingHom_id
129 (R := ModNCompletedCoeff n) (M := CompletedGroupAlgebraQuotientInClass G C U)
131omit [Fact (0 < n)] in
132/-- Composition lemma modNCompletedGroupAlgebraTransitionInClass_comp. -/
133@[simp]
135 (C : ProCGroups.FiniteGroupClass.{u})
136 {U V W : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hVW : V ≤ W) :
137 (modNCompletedGroupAlgebraTransitionInClass n G C hUV).comp
138 (modNCompletedGroupAlgebraTransitionInClass n G C hVW) =
139 modNCompletedGroupAlgebraTransitionInClass n G C (hUV.trans hVW) := by
141 modNCompletedGroupAlgebraTransitionInClass, ← MonoidAlgebra.mapDomainRingHom_comp]
142 congr 1
143 exact OpenNormalSubgroupInClass.map_comp
144 (C := C) (G := G)
145 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) (W := OrderDual.ofDual W)
146 hUV hVW
148omit [Fact (0 < n)] in
149/-- The class-restricted inverse system `U ↦ (ZMod n)[G/U]`. -/
151 (C : ProCGroups.FiniteGroupClass.{u}) :
152 InverseSystem (I := CompletedGroupAlgebraIndexInClass G C) where
153 X := ModNCompletedGroupAlgebraStageInClass n G C
154 topologicalSpace := fun _ => ⊥
155 map := fun {U V} hUV => modNCompletedGroupAlgebraTransitionInClass n G C hUV
156 continuous_map := by
157 intro U V hUV
158 letI : TopologicalSpace (ModNCompletedGroupAlgebraStageInClass n G C U) := ⊥
159 letI : TopologicalSpace (ModNCompletedGroupAlgebraStageInClass n G C V) := ⊥
160 letI : DiscreteTopology (ModNCompletedGroupAlgebraStageInClass n G C V) := ⟨rfl⟩
161 exact continuous_of_discreteTopology
162 map_id := by
163 intro U
164 funext x
165 exact congrFun
166 (congrArg DFunLike.coe
167 (modNCompletedGroupAlgebraTransitionInClass_id n G C U)) x
168 map_comp := by
169 intro U V W hUV hVW
170 funext x
171 exact congrFun
172 (congrArg DFunLike.coe
173 (modNCompletedGroupAlgebraTransitionInClass_comp n G C hUV hVW)) x
175omit [Fact (0 < n)] in
176/-- Surjectivity lemma modNCompletedGroupAlgebraTransitionInClass_surjective. -/
178 (C : ProCGroups.FiniteGroupClass.{u})
179 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
180 Function.Surjective (modNCompletedGroupAlgebraTransitionInClass n G C hUV) := by
181 intro x
182 induction x using Finsupp.induction with
185 | single_add q a x _ _ ih =>
186 rcases OpenNormalSubgroupInClass.map_surjective
187 (C := C) (G := G)
188 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV q with
189 ⟨q', hq'⟩
190 rcases ih with ⟨y, hy⟩
191 refine
192 ⟨(MonoidAlgebra.single q' a : ModNCompletedGroupAlgebraStageInClass n G C V) + y,
193 ?_⟩
194 rw [map_add, modNCompletedGroupAlgebraTransitionInClass_single, hy, hq']
196omit [Fact (0 < n)] in
197/-- The quotient map `(ZMod n)[G] -> (ZMod n)[G/U]` for a class-restricted stage. -/
199 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
200 ModNCompletedGroupRing n G →+* ModNCompletedGroupAlgebraStageInClass n G C U :=
201 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
202 (openNormalSubgroupInClassProj (C := C) (G := G) U)
204omit [Fact (0 < n)] in
205/-- Evaluation formula for modNCompletedGroupAlgebraStageMapInClass_of. -/
206@[simp]
208 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (g : G) :
210 (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
211 MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1 := by
212 classical
213 simp only [modNCompletedGroupAlgebraStageMapInClass, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,
214 OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
215 rfl
217omit [Fact (0 < n)] in
218/-- Compatibility lemma modNCompletedGroupAlgebraStageMapInClass_compatible. -/
219@[simp]
221 (C : ProCGroups.FiniteGroupClass.{u})
222 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
223 (modNCompletedGroupAlgebraTransitionInClass n G C hUV).comp
224 (modNCompletedGroupAlgebraStageMapInClass n G C V) =
225 modNCompletedGroupAlgebraStageMapInClass n G C U := by
227 modNCompletedGroupAlgebraStageMapInClass, ← MonoidAlgebra.mapDomainRingHom_comp]
228 congr 1
230omit [Fact (0 < n)] in
231/-- Compatibility for a class-restricted residue-coefficient completed group algebra family. -/
233 (C : ProCGroups.FiniteGroupClass.{u})
234 (x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
235 ModNCompletedGroupAlgebraStageInClass n G C U) : Prop :=
238omit [Fact (0 < n)] in
239/-- The class-restricted residue-coefficient completed group algebra as an inverse-limit subtype. -/
240abbrev ModNCompletedGroupAlgebraInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
241 {x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
242 ModNCompletedGroupAlgebraStageInClass n G C U //
245omit [Fact (0 < n)] in
246/-- Projection from the class-restricted residue-coefficient completed group algebra to a stage. -/
248 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
249 ModNCompletedGroupAlgebraInClass n G C →
250 ModNCompletedGroupAlgebraStageInClass n G C U :=
251 (modNCompletedGroupAlgebraSystemInClass n G C).projection U
252end
254end FoxDifferential