Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Basic
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebra
2import Mathlib.Data.ZMod.Basic
4/-!
5# Fox differential: coefficient rings — mod-\(n\) completed group algebra — in class — basic
7The principal declarations in this module are:
9- `ModNCompletedCoeff`
10 The coefficient ring \(\mathbb{Z}/n\mathbb{Z}\) used in one residue-coefficient stage.
11- `ModNCompletedGroupRing`
12 The group ring \((\mathbb{Z}/n\mathbb{Z})[H]\) used in the residue-coefficient tower.
13- `finite_modNCompletedGroupAlgebraStageInClass`
14 Each \(C\)-indexed finite stage of the mod-\(n\) completed group algebra is finite.
15- `modNCompletedGroupAlgebraTransitionInClass_of`
16 The transition map sends a group-like basis element to the basis element supported at its image in
17 the coarser quotient in the Fox differential construction.
18-/
20namespace FoxDifferential
22noncomputable section
24open ProCGroups.InverseSystems
25open ProCGroups.ProC
27universe u
30variable (n : ℕ) [Fact (0 < n)]
31variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
33omit [Fact (0 < n)] in
34/-- The coefficient ring \(\mathbb{Z}/n\mathbb{Z}\) used in one residue-coefficient stage. -/
35abbrev ModNCompletedCoeff : Type := ZMod n
37omit [Fact (0 < n)] in
38/-- The group ring \((\mathbb{Z}/n\mathbb{Z})[H]\) used in the residue-coefficient tower. -/
39abbrev ModNCompletedGroupRing (H : Type*) : Type _ :=
40 MonoidAlgebra (ModNCompletedCoeff n) H
42omit [Fact (0 < n)] in
43/-- The residue-coefficient stage over a class-restricted finite quotient \(G/U\). -/
44abbrev ModNCompletedGroupAlgebraStageInClass
45 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) : Type _ :=
46 ModNCompletedGroupRing n (CompletedGroupAlgebraQuotientInClass G C U)
48/-- Each \(C\)-indexed finite stage of the mod-\(n\) completed group algebra is finite. -/
49theorem finite_modNCompletedGroupAlgebraStageInClass
50 (C : ProCGroups.FiniteGroupClass.{u})
51 (U : CompletedGroupAlgebraIndexInClass G C) :
52 Finite (ModNCompletedGroupAlgebraStageInClass n G C U) := by
53 classical
54 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
55 C.finite (OrderDual.ofDual U).2
56 letI : Fintype (CompletedGroupAlgebraQuotientInClass G C U) := Fintype.ofFinite _
57 letI : DecidableEq (CompletedGroupAlgebraQuotientInClass G C U) := Classical.decEq _
58 letI : NeZero n := ⟨Nat.ne_of_gt (show 0 < n from Fact.out)⟩
59 letI : Fintype (ModNCompletedCoeff n) := Fintype.ofEquiv (Fin n) (ZMod.finEquiv n)
60 letI :
61 Finite (CompletedGroupAlgebraQuotientInClass G C U → ModNCompletedCoeff n) := by
62 letI :
63 Fintype (CompletedGroupAlgebraQuotientInClass G C U → ModNCompletedCoeff n) :=
64 inferInstance
65 exact Finite.of_fintype _
66 let f :
67 ModNCompletedGroupAlgebraStageInClass n G C U →
68 CompletedGroupAlgebraQuotientInClass G C U → ModNCompletedCoeff n :=
69 fun x q => x.coeff q
70 refine Finite.of_injective f ?_
71 intro x y hxy
72 ext q
73 exact congrFun hxy q
75omit [Fact (0 < n)] in
76/-- The transition map between class-restricted residue-coefficient stages. -/
77def modNCompletedGroupAlgebraTransitionInClass
78 (C : ProCGroups.FiniteGroupClass.{u})
79 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
80 ModNCompletedGroupAlgebraStageInClass n G C V →+*
81 ModNCompletedGroupAlgebraStageInClass n G C U :=
82 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
83 (OpenNormalSubgroupInClass.map
84 (C := C) (G := G)
85 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
87omit [Fact (0 < n)] in
88/--
89The transition map sends a group-like basis element to the basis element supported at its image
90in the coarser quotient in the Fox differential construction.
91-/
92@[simp]
93theorem modNCompletedGroupAlgebraTransitionInClass_of
94 (C : ProCGroups.FiniteGroupClass.{u})
95 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
96 (g : CompletedGroupAlgebraQuotientInClass G C V) :
97 modNCompletedGroupAlgebraTransitionInClass n G C hUV
98 (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
99 MonoidAlgebra.single
100 ((OpenNormalSubgroupInClass.map
101 (C := C) (G := G)
102 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1 := by
103 classical
104 change
105 MonoidAlgebra.mapDomain
106 (OpenNormalSubgroupInClass.map
107 (C := C) (G := G)
108 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
109 (MonoidAlgebra.single g 1) =
110 MonoidAlgebra.single
111 ((OpenNormalSubgroupInClass.map
112 (C := C) (G := G)
113 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1
114 exact MonoidAlgebra.mapDomain_single
116omit [Fact (0 < n)] in
117/--
118The \(C\)-indexed transition map between finite stages sends a singleton supported at a class of
119the finer quotient to the singleton supported at its image in the coarser quotient, preserving
120the coefficient.
121-/
122@[simp]
123theorem modNCompletedGroupAlgebraTransitionInClass_single
124 (C : ProCGroups.FiniteGroupClass.{u})
125 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
126 (q : CompletedGroupAlgebraQuotientInClass G C V)
127 (a : ModNCompletedCoeff n) :
128 modNCompletedGroupAlgebraTransitionInClass n G C hUV
129 (MonoidAlgebra.single q a) =
130 MonoidAlgebra.single
131 ((OpenNormalSubgroupInClass.map
132 (C := C) (G := G)
133 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) a := by
134 classical
135 change
136 MonoidAlgebra.mapDomain
137 (OpenNormalSubgroupInClass.map
138 (C := C) (G := G)
139 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
140 (MonoidAlgebra.single q a) =
141 MonoidAlgebra.single
142 ((OpenNormalSubgroupInClass.map
143 (C := C) (G := G)
144 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) a
145 exact MonoidAlgebra.mapDomain_single
147omit [Fact (0 < n)] in
148/--
149The transition map attached to the identity refinement is the identity homomorphism in the Fox
150differential construction.
151-/
152@[simp]
153theorem modNCompletedGroupAlgebraTransitionInClass_id
154 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
155 modNCompletedGroupAlgebraTransitionInClass n G C (le_rfl : U ≤ U) = RingHom.id _ := by
156 rw [modNCompletedGroupAlgebraTransitionInClass, OpenNormalSubgroupInClass.map_id]
157 exact MonoidAlgebra.mapDomainRingHom_id
158 (R := ModNCompletedCoeff n) (M := CompletedGroupAlgebraQuotientInClass G C U)
160omit [Fact (0 < n)] in
161/--
162Class-indexed mod-\(n\) completed group-algebra transitions compose along quotient refinements.
163-/
164@[simp]
165theorem modNCompletedGroupAlgebraTransitionInClass_comp
166 (C : ProCGroups.FiniteGroupClass.{u})
167 {U V W : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hVW : V ≤ W) :
168 (modNCompletedGroupAlgebraTransitionInClass n G C hUV).comp
169 (modNCompletedGroupAlgebraTransitionInClass n G C hVW) =
170 modNCompletedGroupAlgebraTransitionInClass n G C (hUV.trans hVW) := by
171 rw [modNCompletedGroupAlgebraTransitionInClass, modNCompletedGroupAlgebraTransitionInClass,
172 modNCompletedGroupAlgebraTransitionInClass, ← MonoidAlgebra.mapDomainRingHom_comp]
173 congr 1
174 exact OpenNormalSubgroupInClass.map_comp
175 (C := C) (G := G)
176 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) (W := OrderDual.ofDual W)
177 hUV hVW
179omit [Fact (0 < n)] in
180/-- The class-restricted inverse system \(U \mapsto (\mathbb{Z}/n\mathbb{Z})[G/U]\). -/
181def modNCompletedGroupAlgebraSystemInClass
182 (C : ProCGroups.FiniteGroupClass.{u}) :
183 InverseSystem (I := CompletedGroupAlgebraIndexInClass G C) where
184 X := ModNCompletedGroupAlgebraStageInClass n G C
185 topologicalSpace := fun _ => ⊥
186 map := fun {U V} hUV => modNCompletedGroupAlgebraTransitionInClass n G C hUV
187 continuous_map := by
188 intro U V hUV
189 letI : TopologicalSpace (ModNCompletedGroupAlgebraStageInClass n G C U) := ⊥
190 letI : TopologicalSpace (ModNCompletedGroupAlgebraStageInClass n G C V) := ⊥
191 letI : DiscreteTopology (ModNCompletedGroupAlgebraStageInClass n G C V) := ⟨rfl⟩
192 exact continuous_of_discreteTopology
193 map_id := by
194 intro U
195 funext x
196 exact congrFun
197 (congrArg DFunLike.coe
198 (modNCompletedGroupAlgebraTransitionInClass_id n G C U)) x
199 map_comp := by
200 intro U V W hUV hVW
201 funext x
202 exact congrFun
203 (congrArg DFunLike.coe
204 (modNCompletedGroupAlgebraTransitionInClass_comp n G C hUV hVW)) x
206omit [Fact (0 < n)] in
207/--
208The finite-stage transition map is surjective, with preimages obtained by lifting quotient
209representatives.
210-/
211theorem modNCompletedGroupAlgebraTransitionInClass_surjective
212 (C : ProCGroups.FiniteGroupClass.{u})
213 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
214 Function.Surjective (modNCompletedGroupAlgebraTransitionInClass n G C hUV) := by
215 intro x
216 induction x using MonoidAlgebra.induction with
217 | zero =>
218 exact ⟨0, map_zero _⟩
219 | single_add q a x _ _ ih =>
220 rcases OpenNormalSubgroupInClass.map_surjective
221 (C := C) (G := G)
222 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV q with
223 ⟨q', hq'⟩
224 rcases ih with ⟨y, hy⟩
225 refine
226 ⟨(MonoidAlgebra.single q' a : ModNCompletedGroupAlgebraStageInClass n G C V) + y,
227 ?_⟩
228 rw [map_add, modNCompletedGroupAlgebraTransitionInClass_single, hy, hq']
229 rfl
231omit [Fact (0 < n)] in
232/--
233The quotient map \((\mathbb{Z}/n\mathbb{Z})[G] \to (\mathbb{Z}/n\mathbb{Z})[G/U]\) for a
234class-restricted stage.
235-/
236def modNCompletedGroupAlgebraStageMapInClass
237 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
238 ModNCompletedGroupRing n G →+* ModNCompletedGroupAlgebraStageInClass n G C U :=
239 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
240 (openNormalSubgroupInClassProj (C := C) (G := G) U)
242omit [Fact (0 < n)] in
243/--
244The finite-stage group-like map sends a group element to the corresponding singleton basis
245element in the quotient group algebra in the Fox differential construction.
246-/
247@[simp]
248theorem modNCompletedGroupAlgebraStageMapInClass_of
249 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (g : G) :
250 modNCompletedGroupAlgebraStageMapInClass n G C U
251 (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
252 MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1 := by
253 classical
254 change
255 MonoidAlgebra.mapDomain
256 (openNormalSubgroupInClassProj (C := C) (G := G) U)
257 (MonoidAlgebra.single g 1) =
258 MonoidAlgebra.single
259 (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1
260 exact MonoidAlgebra.mapDomain_single
262omit [Fact (0 < n)] in
263/--
264The class-restricted mod-\(n\) completed group-algebra stage maps are compatible with quotient
265refinement.
266-/
267@[simp]
268theorem modNCompletedGroupAlgebraStageMapInClass_compatible
269 (C : ProCGroups.FiniteGroupClass.{u})
270 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
271 (modNCompletedGroupAlgebraTransitionInClass n G C hUV).comp
272 (modNCompletedGroupAlgebraStageMapInClass n G C V) =
273 modNCompletedGroupAlgebraStageMapInClass n G C U := by
274 rw [modNCompletedGroupAlgebraTransitionInClass, modNCompletedGroupAlgebraStageMapInClass,
275 modNCompletedGroupAlgebraStageMapInClass, ← MonoidAlgebra.mapDomainRingHom_comp]
276 congr 1
278omit [Fact (0 < n)] in
279/-- Compatibility for a class-restricted residue-coefficient completed group algebra family. -/
280def ModNCompletedGroupAlgebraCompatibleInClass
281 (C : ProCGroups.FiniteGroupClass.{u})
282 (x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
283 ModNCompletedGroupAlgebraStageInClass n G C U) : Prop :=
284 (modNCompletedGroupAlgebraSystemInClass n G C).Compatible x
286omit [Fact (0 < n)] in
287/-- The class-restricted residue-coefficient completed group algebra as an inverse-limit subtype. -/
288abbrev ModNCompletedGroupAlgebraInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
289 {x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
290 ModNCompletedGroupAlgebraStageInClass n G C U //
291 ModNCompletedGroupAlgebraCompatibleInClass n G C x}
293omit [Fact (0 < n)] in
294/--
295The projection from the class-restricted residue-coefficient completed group algebra to a stage.
296-/
297def modNCompletedGroupAlgebraProjectionInClass
298 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
299 ModNCompletedGroupAlgebraInClass n G C →
300 ModNCompletedGroupAlgebraStageInClass n G C U :=
301 (modNCompletedGroupAlgebraSystemInClass n G C).projection U
302end
304end FoxDifferential