Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Map
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Projection
3/-!
4# Fox differential: coefficient rings — prime-power completed group algebra — in class — map
6The principal declarations in this module are:
8- `primePowerCompletedGroupAlgebraMapStageInClass`
9 The finite-stage component of a class-restricted prime-power completed group-algebra map.
10- `primePowerCompletedGroupAlgebraMapInClass`
11 The class-restricted prime-power completed group-algebra map induced by a continuous homomorphism,
12 as an additive map on the inverse-limit subtype.
13- `primePowerCompletedGroupAlgebraMapStageInClass_of`
14 The class-indexed prime-power stage map sends a group-like basis element to the basis element
15 supported at its quotient image.
16- `primePowerCompletedGroupAlgebraMapStageInClass_single`
17 The class-indexed prime-power stage map transports a singleton coefficient to the singleton at its
18 quotient image.
19-/
21namespace FoxDifferential
23noncomputable section
25open ProCGroups.InverseSystems
26open ProCGroups.ProC
28universe u
30variable (ℓ : ℕ)
31variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
33section MapStageInClass
35variable {G0 H0 : Type u}
36variable [Group G0] [TopologicalSpace G0] [IsTopologicalGroup G0]
37variable [Group H0] [TopologicalSpace H0] [IsTopologicalGroup H0]
39/-- The finite-stage component of a class-restricted prime-power completed group-algebra map. -/
40def primePowerCompletedGroupAlgebraMapStageInClass
41 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
42 (ψ : ContinuousMonoidHom G0 H0) (i : PrimePowerCompletedGroupAlgebraIndexInClass H0 C) :
43 PrimePowerCompletedGroupAlgebraStageInClass ℓ G0 C
44 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2) →+*
45 PrimePowerCompletedGroupAlgebraStageInClass ℓ H0 C i :=
46 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff (ℓ ^ i.1))
47 (completedGroupAlgebraComapQuotientMapInClass (G := G0) (H := H0) C hC ψ i.2)
49/--
50The class-indexed prime-power stage map sends a group-like basis element to the basis element
51supported at its quotient image.
52-/
53@[simp]
54theorem primePowerCompletedGroupAlgebraMapStageInClass_of
55 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
56 (ψ : ContinuousMonoidHom G0 H0) (i : PrimePowerCompletedGroupAlgebraIndexInClass H0 C)
57 (q : CompletedGroupAlgebraQuotientInClass G0 C
58 (completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2)) :
59 primePowerCompletedGroupAlgebraMapStageInClass (ℓ := ℓ) C hC ψ i
60 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _ q) =
61 MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _
62 (completedGroupAlgebraComapQuotientMapInClass (G := G0) (H := H0) C hC ψ i.2 q) := by
63 simp only [primePowerCompletedGroupAlgebraMapStageInClass, MonoidAlgebra.of_apply,
64 MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_single]
66/--
67The class-indexed prime-power stage map transports a singleton coefficient to the singleton at its
68quotient image.
69-/
70theorem primePowerCompletedGroupAlgebraMapStageInClass_single
71 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
72 (ψ : ContinuousMonoidHom G0 H0) (i : PrimePowerCompletedGroupAlgebraIndexInClass H0 C)
73 (q : CompletedGroupAlgebraQuotientInClass G0 C
74 (completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2))
75 (a : ModNCompletedCoeff (ℓ ^ i.1)) :
76 primePowerCompletedGroupAlgebraMapStageInClass (ℓ := ℓ) C hC ψ i
77 (MonoidAlgebra.single q a) =
78 MonoidAlgebra.single
79 (completedGroupAlgebraComapQuotientMapInClass (G := G0) (H := H0) C hC ψ i.2 q) a := by
80 simp only [primePowerCompletedGroupAlgebraMapStageInClass,
81 MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_single]
83/--
84Surjectivity of the underlying continuous homomorphism implies surjectivity of the finite-stage
85class-restricted completed maps.
86-/
87theorem primePowerCompletedGroupAlgebraMapStageInClass_surjective_of_surjective
88 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
89 (ψ : ContinuousMonoidHom G0 H0) (hψ : Function.Surjective ψ)
90 (i : PrimePowerCompletedGroupAlgebraIndexInClass H0 C) :
91 Function.Surjective
92 (primePowerCompletedGroupAlgebraMapStageInClass (ℓ := ℓ) C hC ψ i) := by
93 intro x
94 obtain ⟨y, hy⟩ :=
95 Finsupp.mapDomain_surjective (M := ModNCompletedCoeff (ℓ ^ i.1))
96 (completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
97 (G := G0) (H := H0) C hC ψ hψ i.2) x.coeff
98 refine ⟨MonoidAlgebra.ofCoeff y, ?_⟩
99 apply MonoidAlgebra.coeff_injective
100 exact hy
102/-- Class-restricted finite-stage maps commute with the prime-power transition maps. -/
103theorem primePowerCompletedGroupAlgebraMapStageInClass_compatible
104 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
105 (ψ : ContinuousMonoidHom G0 H0)
106 {i j : PrimePowerCompletedGroupAlgebraIndexInClass H0 C} (hij : i ≤ j) :
107 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := H0) C hij).comp
108 (primePowerCompletedGroupAlgebraMapStageInClass (ℓ := ℓ) C hC ψ j) =
109 (primePowerCompletedGroupAlgebraMapStageInClass (ℓ := ℓ) C hC ψ i).comp
110 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G0) C
111 (show
112 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2) ≤
113 (j.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ j.2) from
114 ⟨hij.1,
115 completedGroupAlgebraComapIndexInClass_mono
116 (G := G0) (H := H0) C hC ψ hij.2⟩)) := by
117 apply RingHom.ext
118 intro x
119 refine MonoidAlgebra.induction_on
120 (p := fun x =>
121 ((primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := H0) C hij).comp
122 (primePowerCompletedGroupAlgebraMapStageInClass (ℓ := ℓ) C hC ψ j)) x =
123 ((primePowerCompletedGroupAlgebraMapStageInClass (ℓ := ℓ) C hC ψ i).comp
124 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G0) C
125 (show
126 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2) ≤
127 (j.1,
128 completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ j.2) from
129 ⟨hij.1,
130 completedGroupAlgebraComapIndexInClass_mono
131 (G := G0) (H := H0) C hC ψ hij.2⟩))) x)
132 x ?_ ?_ ?_
133 · intro q
134 rw [RingHom.comp_apply, RingHom.comp_apply,
135 primePowerCompletedGroupAlgebraMapStageInClass_of,
136 primePowerCompletedGroupAlgebraTransitionInClass_of,
137 primePowerCompletedGroupAlgebraTransitionInClass_of]
138 change
139 MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1))
140 (CompletedGroupAlgebraQuotientInClass H0 C i.2)
141 ((OpenNormalSubgroupInClass.map
142 (C := C) (G := H0)
143 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2)
144 (completedGroupAlgebraComapQuotientMapInClass
145 (G := G0) (H := H0) C hC ψ j.2 q)) =
146 primePowerCompletedGroupAlgebraMapStageInClass (ℓ := ℓ) C hC ψ i
147 (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1))
148 (CompletedGroupAlgebraQuotientInClass G0 C
149 (completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2))
150 ((OpenNormalSubgroupInClass.map
151 (C := C) (G := G0)
152 (U := OrderDual.ofDual
153 (completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2))
154 (V := OrderDual.ofDual
155 (completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ j.2))
156 (completedGroupAlgebraComapIndexInClass_mono
157 (G := G0) (H := H0) C hC ψ hij.2)) q))
158 rw [primePowerCompletedGroupAlgebraMapStageInClass_of]
159 exact congrArg (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1))
160 (CompletedGroupAlgebraQuotientInClass H0 C i.2))
161 (congrFun
162 (congrArg DFunLike.coe
163 (completedGroupAlgebraComapQuotientMapInClass_compatible
164 (G := G0) (H := H0) C hC ψ hij.2)) q)
165 · intro x y hx hy
166 rw [map_add, map_add, hx, hy]
167 · intro a x hx
168 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
169 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
170 simp only [primePowerCompletedGroupAlgebraTransitionInClass,
171 modNCompletedGroupAlgebraStageCoeffMapInClass,
172 modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe,
173 primePowerCompletedGroupAlgebraMapStageInClass,
174 map_intCast, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
175 MonoidAlgebra.mapDomainRingHom_apply]
177/--
178The class-restricted prime-power completed group-algebra map induced by a continuous
179homomorphism, as an additive map on the inverse-limit subtype.
180-/
181def primePowerCompletedGroupAlgebraMapInClass
182 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
183 (ψ : ContinuousMonoidHom G0 H0) :
184 PrimePowerCompletedGroupAlgebraInClass ℓ G0 C →+
185 PrimePowerCompletedGroupAlgebraInClass ℓ H0 C where
186 toFun x := ⟨fun i =>
187 primePowerCompletedGroupAlgebraMapStageInClass (ℓ := ℓ) C hC ψ i
188 (primePowerCompletedGroupAlgebraProjectionInClass
189 (ℓ := ℓ) (G := G0) C
190 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2) x), by
191 intro i j hij
192 let hsource :
193 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2) ≤
194 (j.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ j.2) :=
195 ⟨hij.1,
196 completedGroupAlgebraComapIndexInClass_mono (G := G0) (H := H0) C hC ψ hij.2⟩
197 have hx := x.2
198 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2)
199 (j.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ j.2)
200 hsource
201 change
202 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G0) C hsource
203 (primePowerCompletedGroupAlgebraProjectionInClass
204 (ℓ := ℓ) (G := G0) C
205 (j.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ j.2) x) =
206 primePowerCompletedGroupAlgebraProjectionInClass
207 (ℓ := ℓ) (G := G0) C
208 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2) x at hx
209 have hcompat := congrFun
210 (congrArg DFunLike.coe
211 (primePowerCompletedGroupAlgebraMapStageInClass_compatible
212 (ℓ := ℓ) C hC ψ hij))
213 (primePowerCompletedGroupAlgebraProjectionInClass
214 (ℓ := ℓ) (G := G0) C
215 (j.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ j.2) x)
216 rw [RingHom.comp_apply, RingHom.comp_apply] at hcompat
217 rw [hx] at hcompat
218 change
219 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := H0) C hij
220 ((primePowerCompletedGroupAlgebraMapStageInClass (ℓ := ℓ) C hC ψ j)
221 (primePowerCompletedGroupAlgebraProjectionInClass
222 (ℓ := ℓ) (G := G0) C
223 (j.1, completedGroupAlgebraComapIndexInClass
224 (G := G0) (H := H0) C hC ψ j.2) x)) =
225 (primePowerCompletedGroupAlgebraMapStageInClass (ℓ := ℓ) C hC ψ i)
226 (primePowerCompletedGroupAlgebraProjectionInClass
227 (ℓ := ℓ) (G := G0) C
228 (i.1, completedGroupAlgebraComapIndexInClass
229 (G := G0) (H := H0) C hC ψ i.2) x)
230 simpa using hcompat⟩
231 map_zero' := by
232 apply Subtype.ext
233 funext i
234 simp only [primePowerCompletedGroupAlgebraMapStageInClass,
235 primePowerCompletedGroupAlgebraProjectionInClass_zero,
236 MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_zero,
237 coe_zero_primePowerCompletedGroupAlgebraInClass, Pi.zero_apply]
238 map_add' := by
239 intro x y
240 apply Subtype.ext
241 funext i
242 simp only [primePowerCompletedGroupAlgebraProjectionInClass_add, map_add,
243 coe_add_primePowerCompletedGroupAlgebraInClass, Pi.add_apply]
245/--
246The class-indexed prime-power completed group-algebra projection is computed by the
247corresponding finite-stage map.
248-/
249@[simp]
250theorem primePowerCompletedGroupAlgebraProjectionInClass_map
251 (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
252 (ψ : ContinuousMonoidHom G0 H0) (i : PrimePowerCompletedGroupAlgebraIndexInClass H0 C)
253 (x : PrimePowerCompletedGroupAlgebraInClass ℓ G0 C) :
254 primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := H0) C i
255 (primePowerCompletedGroupAlgebraMapInClass (ℓ := ℓ) C hC ψ x) =
256 primePowerCompletedGroupAlgebraMapStageInClass (ℓ := ℓ) C hC ψ i
257 (primePowerCompletedGroupAlgebraProjectionInClass
258 (ℓ := ℓ) (G := G0) C
259 (i.1, completedGroupAlgebraComapIndexInClass (G := G0) (H := H0) C hC ψ i.2) x) := rfl
261end MapStageInClass
262end
264end FoxDifferential