FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/System/Basic.lean
1import CompletedGroupAlgebra.Basic.AllFinite.Index
2import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmentation
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/System/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
31abbrev ModNCompletedGroupAlgebraStage (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) : Type _ :=
32 ModNCompletedGroupRing n (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)
34instance instFiniteModNCompletedGroupAlgebraStage (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
35 Finite (ModNCompletedGroupAlgebraStage n G U) := by
36 classical
37 letI : Finite (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) := (OrderDual.ofDual U).2
38 letI : Fintype (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) := Fintype.ofFinite _
39 letI : DecidableEq (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) := Classical.decEq _
40 letI : NeZero n := ⟨Nat.ne_of_gt (show 0 < n from Fact.out)⟩
41 letI : Fintype (ModNCompletedCoeff n) := Fintype.ofEquiv (Fin n) (ZMod.finEquiv n)
42 letI : Finite (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U → ModNCompletedCoeff n) := by
43 letI : Fintype (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U → ModNCompletedCoeff n) := inferInstance
44 exact Finite.of_fintype _
45 let f :
46 ModNCompletedGroupAlgebraStage n G U →
47 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U → ModNCompletedCoeff n := fun x q => x q
48 refine Finite.of_injective f ?_
49 intro x y hxy
50 ext q
51 exact congrFun hxy q
53omit [Fact (0 < n)] in
54/-- The transition map between residue-coefficient stages. -/
56 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
57 ModNCompletedGroupAlgebraStage n G V →+* ModNCompletedGroupAlgebraStage n G U :=
58 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
59 (OpenNormalSubgroupInClass.map
60 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
61 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
63omit [Fact (0 < n)] in
64/-- Evaluation formula for modNCompletedGroupAlgebraTransition_of. -/
65@[simp]
67 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
68 (g : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V) :
69 modNCompletedGroupAlgebraTransition n G hUV (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
70 MonoidAlgebra.single ((OpenNormalSubgroupInClass.map
71 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
72 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1 := by
73 classical
74 simp only [modNCompletedGroupAlgebraTransition, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,
75 OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
76 rfl
78omit [Fact (0 < n)] in
79/-- Identity case for modNCompletedGroupAlgebraTransition_id. -/
80@[simp]
81theorem modNCompletedGroupAlgebraTransition_id (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
82 modNCompletedGroupAlgebraTransition n G (le_rfl : U ≤ U) = RingHom.id _ := by
83 rw [modNCompletedGroupAlgebraTransition, OpenNormalSubgroupInClass.map_id]
84 exact MonoidAlgebra.mapDomainRingHom_id
85 (R := ModNCompletedCoeff n) (M := _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)
87omit [Fact (0 < n)] in
88/-- Composition lemma modNCompletedGroupAlgebraTransition_comp. -/
89@[simp]
91 {U V W : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (hVW : V ≤ W) :
92 (modNCompletedGroupAlgebraTransition n G hUV).comp
93 (modNCompletedGroupAlgebraTransition n G hVW) =
94 modNCompletedGroupAlgebraTransition n G (hUV.trans hVW) := by
96 modNCompletedGroupAlgebraTransition, ← MonoidAlgebra.mapDomainRingHom_comp]
97 congr 1
98 exact OpenNormalSubgroupInClass.map_comp
99 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
100 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) (W := OrderDual.ofDual W)
101 hUV hVW
103omit [Fact (0 < n)] in
104/-- Evaluation formula for modNCompletedGroupAlgebraTransition_single_apply. -/
106 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
107 (q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V)
108 (a : ModNCompletedCoeff n) :
109 modNCompletedGroupAlgebraTransition n G hUV (MonoidAlgebra.single q a) =
110 MonoidAlgebra.single
111 ((OpenNormalSubgroupInClass.map
112 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
113 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) a := by
114 simp only [modNCompletedGroupAlgebraTransition, MonoidAlgebra.single, MonoidAlgebra.mapDomainRingHom_apply,
115 Finsupp.mapDomain_single]
116 rfl
118omit [Fact (0 < n)] in
119/-- Surjectivity lemma modNCompletedGroupAlgebraTransition_surjective. -/
121 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
122 Function.Surjective (modNCompletedGroupAlgebraTransition n G hUV) := by
123 intro x
124 induction x using Finsupp.induction with
127 | single_add q a x _ _ ih =>
128 rcases OpenNormalSubgroupInClass.map_surjective
129 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
130 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV q with
131 ⟨q', hq'⟩
132 rcases ih with ⟨y, hy⟩
133 refine ⟨(MonoidAlgebra.single q' a : ModNCompletedGroupAlgebraStage n G V) + y, ?_⟩
134 rw [map_add, modNCompletedGroupAlgebraTransition_single_apply, hy, hq']
136omit [Fact (0 < n)] in
137/-- The quotient map `(ZMod n)[G] → (ZMod n)[G/U]`. -/
138def modNCompletedGroupAlgebraStageMap (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
139 ModNCompletedGroupRing n G →+* ModNCompletedGroupAlgebraStage n G U :=
140 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
142 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U)
144omit [Fact (0 < n)] in
145/-- Evaluation formula for modNCompletedGroupAlgebraStageMap_of. -/
146@[simp]
148 (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (g : G) :
149 modNCompletedGroupAlgebraStageMap n G U (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
150 MonoidAlgebra.single (openNormalSubgroupInClassProj
151 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1 := by
152 classical
153 simp only [modNCompletedGroupAlgebraStageMap, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,
154 OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
155 rfl
157omit [Fact (0 < n)] in
158/-- Compatibility lemma modNCompletedGroupAlgebraStageMap_compatible. -/
159@[simp]
161 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
162 (modNCompletedGroupAlgebraTransition n G hUV).comp
163 (modNCompletedGroupAlgebraStageMap n G V) =
164 modNCompletedGroupAlgebraStageMap n G U := by
166 modNCompletedGroupAlgebraStageMap, ← MonoidAlgebra.mapDomainRingHom_comp]
167 congr 1
169omit [Fact (0 < n)] in
170/-- The inverse system `U ↦ (ZMod n)[G/U]`. -/
172 InverseSystem (I := _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) where
173 X := ModNCompletedGroupAlgebraStage n G
174 topologicalSpace := fun _ => ⊥
175 map := fun {U V} hUV => modNCompletedGroupAlgebraTransition n G hUV
176 continuous_map := by
177 intro U V hUV
178 letI : TopologicalSpace (ModNCompletedGroupAlgebraStage n G U) := ⊥
179 letI : TopologicalSpace (ModNCompletedGroupAlgebraStage n G V) := ⊥
180 letI : DiscreteTopology (ModNCompletedGroupAlgebraStage n G V) := ⟨rfl⟩
181 exact continuous_of_discreteTopology
182 map_id := by
183 intro U
184 funext x
185 exact congrFun
186 (congrArg DFunLike.coe (modNCompletedGroupAlgebraTransition_id (n := n) (G := G) U)) x
187 map_comp := by
188 intro U V W hUV hVW
189 funext x
190 exact congrFun
191 (congrArg DFunLike.coe
192 (modNCompletedGroupAlgebraTransition_comp (n := n) (G := G) hUV hVW)) x
194omit [Fact (0 < n)] in
195/-- The inverse-limit object of the residue-coefficient stage tower. -/
196abbrev ModNCompletedGroupAlgebra :=
197 (modNCompletedGroupAlgebraSystem n G).inverseLimit
199omit [Fact (0 < n)] in
200/-- The projection from the residue-coefficient inverse limit to one finite stage. -/
201abbrev modNCompletedGroupAlgebraProjection (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
202 ModNCompletedGroupAlgebra n G → ModNCompletedGroupAlgebraStage n G U :=
203 (modNCompletedGroupAlgebraSystem n G).projection U
206end
208end FoxDifferential