Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.Basic
ProCGroups/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/System/Basic/Source

Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.Basic

1import ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Index
2import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmentation
4/-!
5# Fox differential: coefficient rings — mod-\(n\) completed group algebra — system — basic
7The principal declarations in this module are:
9- `ModNCompletedGroupAlgebraStage`
10 The mod-\(N\) completed group-algebra stage combines the finite group quotient with the
11 coefficient quotient modulo \(N\).
12- `modNCompletedGroupAlgebraTransition`
13 The mod-\(n\) group-algebra transition from a finer finite quotient stage to a coarser stage.
14- `modNCompletedGroupAlgebraTransition_of`
15 The transition map sends a group-like basis element to the basis element supported at its image in
16 the coarser quotient in the Fox differential construction.
17- `modNCompletedGroupAlgebraTransition_id`
18 The transition map attached to the identity refinement is the identity homomorphism in the Fox
19 differential construction.
20-/
22namespace FoxDifferential
24noncomputable section
26open ProCGroups.InverseSystems
27open ProCGroups.ProC
29universe u
32variable (n : ℕ) [Fact (0 < n)]
33variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
35omit [Fact (0 < n)] in
36/--
37The mod-\(N\) completed group-algebra stage combines the finite group quotient with the
38coefficient quotient modulo \(N\).
39-/
40abbrev ModNCompletedGroupAlgebraStage (U :
41 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) : Type _ :=
42 ModNCompletedGroupRing n (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)
44/-- Each mod-\(n\) completed group-algebra stage is finite. -/
45instance instFiniteModNCompletedGroupAlgebraStage (U :
46 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
47 Finite (ModNCompletedGroupAlgebraStage n G U) := by
48 classical
49 letI : Finite (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) :=
50 (OrderDual.ofDual U).2
51 letI : Fintype (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) :=
52 Fintype.ofFinite _
53 letI : DecidableEq (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) :=
54 Classical.decEq _
55 letI : NeZero n := ⟨Nat.ne_of_gt (show 0 < n from Fact.out)⟩
56 letI : Fintype (ModNCompletedCoeff n) := Fintype.ofEquiv (Fin n) (ZMod.finEquiv n)
57 letI : Finite (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →
58 ModNCompletedCoeff n) := by
59 letI : Fintype (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →
60 ModNCompletedCoeff n) := inferInstance
61 exact Finite.of_fintype _
62 let f :
63 ModNCompletedGroupAlgebraStage n G U →
64 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →
65 ModNCompletedCoeff n := fun x q => x.coeff q
66 refine Finite.of_injective f ?_
67 intro x y hxy
68 ext q
69 exact congrFun hxy q
71omit [Fact (0 < n)] in
72/-- The mod-\(n\) group-algebra transition from a finer finite quotient stage to a coarser stage. -/
73def modNCompletedGroupAlgebraTransition
74 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
75 ModNCompletedGroupAlgebraStage n G V →+* ModNCompletedGroupAlgebraStage n G U :=
76 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
77 (OpenNormalSubgroupInClass.map
79 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
81omit [Fact (0 < n)] in
82/--
83The transition map sends a group-like basis element to the basis element supported at its image
84in the coarser quotient in the Fox differential construction.
85-/
86@[simp]
87theorem modNCompletedGroupAlgebraTransition_of
88 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
89 (g : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V) :
90 modNCompletedGroupAlgebraTransition n G hUV (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
91 MonoidAlgebra.single ((OpenNormalSubgroupInClass.map
93 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1 := by
94 classical
95 change
96 MonoidAlgebra.mapDomain
97 (OpenNormalSubgroupInClass.map
99 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
100 (MonoidAlgebra.single g 1) =
101 MonoidAlgebra.single
102 ((OpenNormalSubgroupInClass.map
104 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1
105 exact MonoidAlgebra.mapDomain_single
107omit [Fact (0 < n)] in
108/--
109The transition map attached to the identity refinement is the identity homomorphism in the Fox
110differential construction.
111-/
112@[simp]
113theorem modNCompletedGroupAlgebraTransition_id (U :
114 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
115 modNCompletedGroupAlgebraTransition n G (le_rfl : U ≤ U) = RingHom.id _ := by
116 rw [modNCompletedGroupAlgebraTransition, OpenNormalSubgroupInClass.map_id]
117 exact MonoidAlgebra.mapDomainRingHom_id
118 (R := ModNCompletedCoeff n) (M := _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient
119 G U)
121omit [Fact (0 < n)] in
122/-- Mod-\(n\) completed group-algebra transitions compose along quotient refinements. -/
123@[simp]
124theorem modNCompletedGroupAlgebraTransition_comp
125 {U V W : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (hVW : V ≤
126 W) :
127 (modNCompletedGroupAlgebraTransition n G hUV).comp
128 (modNCompletedGroupAlgebraTransition n G hVW) =
129 modNCompletedGroupAlgebraTransition n G (hUV.trans hVW) := by
130 rw [modNCompletedGroupAlgebraTransition, modNCompletedGroupAlgebraTransition,
131 modNCompletedGroupAlgebraTransition, ← MonoidAlgebra.mapDomainRingHom_comp]
132 congr 1
133 exact OpenNormalSubgroupInClass.map_comp
135 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) (W := OrderDual.ofDual W)
136 hUV hVW
138omit [Fact (0 < n)] in
139/--
140The \(n\)-modular completed group-algebra transition sends a singleton to the singleton
141supported at the induced quotient class with the same coefficient.
142-/
143theorem modNCompletedGroupAlgebraTransition_single_apply
144 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
145 (q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V)
146 (a : ModNCompletedCoeff n) :
147 modNCompletedGroupAlgebraTransition n G hUV (MonoidAlgebra.single q a) =
148 MonoidAlgebra.single
149 ((OpenNormalSubgroupInClass.map
151 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) a := by
152 change
153 MonoidAlgebra.mapDomain
154 (OpenNormalSubgroupInClass.map
156 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
157 (MonoidAlgebra.single q a) =
158 MonoidAlgebra.single
159 ((OpenNormalSubgroupInClass.map
161 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) a
162 exact MonoidAlgebra.mapDomain_single
164omit [Fact (0 < n)] in
165/--
166The finite-stage transition map is surjective, with preimages obtained by lifting quotient
167representatives.
168-/
169theorem modNCompletedGroupAlgebraTransition_surjective
170 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
171 Function.Surjective (modNCompletedGroupAlgebraTransition n G hUV) := by
172 intro x
173 induction x using MonoidAlgebra.induction with
174 | zero =>
175 exact ⟨0, map_zero _⟩
176 | single_add q a x _ _ ih =>
177 rcases OpenNormalSubgroupInClass.map_surjective
179 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV q with
180 ⟨q', hq'⟩
181 rcases ih with ⟨y, hy⟩
182 refine ⟨(MonoidAlgebra.single q' a : ModNCompletedGroupAlgebraStage n G V) + y, ?_⟩
183 rw [map_add, modNCompletedGroupAlgebraTransition_single_apply, hy, hq']
184 rfl
186omit [Fact (0 < n)] in
187/-- The quotient map \((\mathbb{Z}/n\mathbb{Z})[G] \to (\mathbb{Z}/n\mathbb{Z})[G/U]\). -/
188def modNCompletedGroupAlgebraStageMap (U :
189 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
190 ModNCompletedGroupRing n G →+* ModNCompletedGroupAlgebraStage n G U :=
191 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
192 (openNormalSubgroupInClassProj
195omit [Fact (0 < n)] in
196/--
197The finite-stage group-like map sends a group element to the corresponding singleton basis
198element in the quotient group algebra in the Fox differential construction.
199-/
200@[simp]
201theorem modNCompletedGroupAlgebraStageMap_of
202 (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (g : G) :
203 modNCompletedGroupAlgebraStageMap n G U (MonoidAlgebra.of (ModNCompletedCoeff n) _ g) =
204 MonoidAlgebra.single (openNormalSubgroupInClassProj
205 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1 := by
206 classical
207 change
208 MonoidAlgebra.mapDomain
209 (openNormalSubgroupInClassProj
211 (MonoidAlgebra.single g 1) =
212 MonoidAlgebra.single
213 (openNormalSubgroupInClassProj
215 exact MonoidAlgebra.mapDomain_single
217omit [Fact (0 < n)] in
218/-- The mod-\(n\) completed group-algebra stage maps are compatible with quotient refinement. -/
219@[simp]
220theorem modNCompletedGroupAlgebraStageMap_compatible
221 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
222 (modNCompletedGroupAlgebraTransition n G hUV).comp
223 (modNCompletedGroupAlgebraStageMap n G V) =
224 modNCompletedGroupAlgebraStageMap n G U := by
225 rw [modNCompletedGroupAlgebraTransition, modNCompletedGroupAlgebraStageMap,
226 modNCompletedGroupAlgebraStageMap, ← MonoidAlgebra.mapDomainRingHom_comp]
227 congr 1
229omit [Fact (0 < n)] in
230/-- The inverse system \(U \mapsto (\mathbb{Z}/n\mathbb{Z})[G/U]\). -/
231def modNCompletedGroupAlgebraSystem :
232 InverseSystem (I := _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) where
233 X := ModNCompletedGroupAlgebraStage n G
234 topologicalSpace := fun _ => ⊥
235 map := fun {U V} hUV => modNCompletedGroupAlgebraTransition n G hUV
236 continuous_map := by
237 intro U V hUV
238 letI : TopologicalSpace (ModNCompletedGroupAlgebraStage n G U) := ⊥
239 letI : TopologicalSpace (ModNCompletedGroupAlgebraStage n G V) := ⊥
240 letI : DiscreteTopology (ModNCompletedGroupAlgebraStage n G V) := ⟨rfl⟩
241 exact continuous_of_discreteTopology
242 map_id := by
243 intro U
244 funext x
245 exact congrFun
246 (congrArg DFunLike.coe (modNCompletedGroupAlgebraTransition_id (n := n) (G := G) U)) x
247 map_comp := by
248 intro U V W hUV hVW
249 funext x
250 exact congrFun
251 (congrArg DFunLike.coe
252 (modNCompletedGroupAlgebraTransition_comp (n := n) (G := G) hUV hVW)) x
254omit [Fact (0 < n)] in
255/-- The inverse-limit object of the residue-coefficient stage tower. -/
256abbrev ModNCompletedGroupAlgebra :=
257 (modNCompletedGroupAlgebraSystem n G).inverseLimit
259omit [Fact (0 < n)] in
260/-- The projection from the residue-coefficient inverse limit to one finite stage. -/
261abbrev modNCompletedGroupAlgebraProjection (U :
262 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
263 ModNCompletedGroupAlgebra n G → ModNCompletedGroupAlgebraStage n G U :=
264 (modNCompletedGroupAlgebraSystem n G).projection U
267end
269end FoxDifferential