Yamaguchi Lean 4 Library
CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/Functoriality.lean
CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/Functoriality/Source

CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/Functoriality.lean

1import Mathlib.Data.ZMod.Basic
2import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Topology
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/Functoriality.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Finite group algebra functoriality in the group variable
15This module records functoriality of finite group algebras in the finite group variable and the compatibility of the induced maps with module structures.
16-/
18open scoped Topology
19open ProCGroups
23universe u v w z
25/-- Finite-stage group algebras are functorial by continuous ring homomorphisms. -/
27 (R : Type u) (G H : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
28 [Group G] [Group H] [Finite G] [Finite H] (φ : G →* H) :
29 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
30 letI : TopologicalSpace (MonoidAlgebra R H) := finiteGroupAlgebraTopology R H
31 Continuous (MonoidAlgebra.mapDomainRingHom R φ : MonoidAlgebra R G → MonoidAlgebra R H) := by
32 classical
33 letI : Fintype G := Fintype.ofFinite G
34 letI : Fintype H := Fintype.ofFinite H
35 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
36 letI : TopologicalSpace (MonoidAlgebra R H) := finiteGroupAlgebraTopology R H
37 let e : MonoidAlgebra R H ≃ (H → R) := Finsupp.equivFunOnFinite
38 have he : Topology.IsInducing (e : MonoidAlgebra R H → H → R) :=
39 Topology.IsInducing.induced e
40 have hcoord : ∀ g : G, Continuous fun x : MonoidAlgebra R G => x g :=
42 rw [he.continuous_iff]
43 apply continuous_pi
44 intro h
45 change Continuous fun x : MonoidAlgebra R G =>
46 (MonoidAlgebra.mapDomainRingHom R φ x : MonoidAlgebra R H) h
47 rw [show (fun x : MonoidAlgebra R G =>
48 (MonoidAlgebra.mapDomainRingHom R φ x : MonoidAlgebra R H) h) =
49 (fun x : MonoidAlgebra R G =>
50 ∑ g ∈ Finset.univ.filter (fun g : G => φ g = h), x g) from ?_]
51 · apply continuous_finset_sum
52 intro g _hg
53 exact hcoord g
54 · funext x
55 change (Finsupp.mapDomain φ x) h =
56 ∑ g ∈ Finset.univ.filter (fun g : G => φ g = h), x g
57 rw [Finsupp.mapDomain, Finsupp.sum]
58 rw [Finsupp.finset_sum_apply]
59 simp only [Finsupp.single_apply]
60 change (∑ g ∈ x.support, if φ g = h then x g else 0) =
61 ∑ g ∈ Finset.univ.filter (fun g : G => φ g = h), x g
62 rw [Finset.sum_filter]
63 exact Finset.sum_subset (by intro g _hg; simp only [Finset.mem_univ]) (by
64 intro g _hguniv hgnot
65 by_cases hφ : φ g = h
66 · simp only [hφ, ↓reduceIte, Finsupp.notMem_support_iff.mp hgnot]
67 · simp only [hφ, ↓reduceIte])
69/-- The finite-stage group algebra functor sends the identity homomorphism to the identity. -/
71 (R : Type u) (G : Type v) [CommRing R] [Group G] :
72 MonoidAlgebra.mapDomainRingHom R (MonoidHom.id G) = RingHom.id (MonoidAlgebra R G) := by
73 apply RingHom.ext
74 intro x
75 rw [MonoidAlgebra.mapDomainRingHom_apply]
76 exact Finsupp.mapDomain_id
78/-- The finite-stage group algebra functor respects composition. -/
80 (R : Type u) (G H K : Type v) [CommRing R] [Group G] [Group H] [Group K]
81 (φ : G →* H) (ψ : H →* K) :
82 (MonoidAlgebra.mapDomainRingHom R ψ).comp (MonoidAlgebra.mapDomainRingHom R φ) =
83 MonoidAlgebra.mapDomainRingHom R (ψ.comp φ) := by
84 apply RingHom.ext
85 intro x
86 rw [RingHom.comp_apply, MonoidAlgebra.mapDomainRingHom_apply,
87 MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomainRingHom_apply]
88 exact (Finsupp.mapDomain_comp (v := x) (f := φ) (g := ψ)).symm
90/-- Functoriality on the canonical group-like basis elements of a finite-stage group algebra. -/
92 (R : Type u) (G H : Type v) [CommRing R] [Group G] [Group H]
93 (φ : G →* H) (g : G) :
94 MonoidAlgebra.mapDomainRingHom R φ (MonoidAlgebra.of R G g) =
95 MonoidAlgebra.of R H (φ g) := by
96 simp only [MonoidAlgebra.of_apply, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
98/-- A finite group-algebra relation is preserved by pushing the group variable along a homomorphism. -/
100 {R G H : Type*} [Ring R] [Group G] [Group H]
101 (f : G →* H) (g : G) (y : MonoidAlgebra R G)
102 (hrel : (MonoidAlgebra.of R G g - 1) * y = 0) :
103 (MonoidAlgebra.of R H (f g) - 1) *
104 MonoidAlgebra.mapDomainRingHom R f y = 0 := by
105 have hmap := congrArg (MonoidAlgebra.mapDomainRingHom R f) hrel
106 calc
107 (MonoidAlgebra.of R H (f g) - 1) *
108 MonoidAlgebra.mapDomainRingHom R f y
109 = MonoidAlgebra.mapDomainRingHom R f
110 ((MonoidAlgebra.of R G g - 1) * y) := by
111 rw [map_mul, map_sub, map_one]
112 simp only [MonoidAlgebra.of_apply, MonoidAlgebra.mapDomainRingHom_apply,
113 Finsupp.mapDomain_single]
114 _ = 0 := by simpa only [map_zero] using hmap
116/-- Integer-power version of finite group-algebra relation functoriality. -/
118 {R G H : Type*} [Ring R] [Group G] [Group H]
119 (f : G →* H) (g : G) (n : ℤ) (y : MonoidAlgebra R G)
120 (hrel : (MonoidAlgebra.of R G (g ^ n) - 1) * y = 0) :
121 (MonoidAlgebra.of R H ((f g) ^ n) - 1) *
122 MonoidAlgebra.mapDomainRingHom R f y = 0 := by
123 simpa only [map_zpow] using
126/-- A finite group-algebra relation `(a - 1)y = 0` makes coefficients constant along the
127left `a`-orbits. -/
129 {R G : Type*} [Ring R] [Group G] (a : G) (y : MonoidAlgebra R G)
130 (hrel : (MonoidAlgebra.of R G a - 1) * y = 0) :
131 ∀ k : ℤ, ∀ t : G, y (a ^ k * t) = y t := by
132 have hmul : MonoidAlgebra.of R G a * y = y := by
133 have h : MonoidAlgebra.of R G a * y - y = 0 := by
134 simpa [sub_mul] using hrel
135 exact sub_eq_zero.mp h
136 have hpowmul : ∀ m : ℕ, MonoidAlgebra.of R G (a ^ m) * y = y := by
137 intro m
138 induction m with
139 | zero =>
140 rw [pow_zero]
141 change MonoidAlgebra.single (1 : G) (1 : R) * y = y
142 rw [← MonoidAlgebra.one_def]
143 simp only [one_mul]
144 | succ m ih =>
145 calc
146 MonoidAlgebra.of R G (a ^ (m + 1)) * y
147 = MonoidAlgebra.of R G (a ^ m) * (MonoidAlgebra.of R G a * y) := by
148 rw [← mul_assoc, ← map_mul]
149 simp only [pow_succ, MonoidAlgebra.of_apply]
150 _ = MonoidAlgebra.of R G (a ^ m) * y := by rw [hmul]
151 _ = y := ih
152 have hneg : ∀ m : ℕ, ∀ t : G, y ((a ^ m)⁻¹ * t) = y t := by
153 intro m t
154 have hcoeff :=
155 congrArg (fun z : MonoidAlgebra R G => z t) (hpowmul m)
156 have hleft :
157 (MonoidAlgebra.of R G (a ^ m) * y) t = y ((a ^ m)⁻¹ * t) := by
158 change (MonoidAlgebra.single (a ^ m) (1 : R) * y) t =
159 y ((a ^ m)⁻¹ * t)
160 rw [MonoidAlgebra.single_mul_apply]
161 simp only [one_mul]
162 simpa [hleft] using hcoeff
163 have hpos : ∀ m : ℕ, ∀ t : G, y (a ^ m * t) = y t := by
164 intro m t
165 have h := hneg m (a ^ m * t)
166 have hsimp : (a ^ m)⁻¹ * (a ^ m * t) = t := by simp only [inv_mul_cancel_left]
167 exact (by simpa [hsimp] using h.symm)
168 intro k
169 cases k with
170 | ofNat m =>
171 intro t
172 simpa using hpos m t
173 | negSucc m =>
174 intro t
175 simpa [zpow_negSucc] using hneg (m + 1) t
177/-- A finite group-algebra relation `(a - 1)y = 0` also gives `(a^k - 1)y = 0` for every
178integer power `k`. -/
180 {R G : Type*} [Ring R] [Group G] (a : G) (k : ℤ) (y : MonoidAlgebra R G)
181 (hrel : (MonoidAlgebra.of R G a - 1) * y = 0) :
182 (MonoidAlgebra.of R G (a ^ k) - 1) * y = 0 := by
183 ext t
184 have horbit :=
186 (R := R) (G := G) a y hrel (-k) t
187 have hleft :
188 (MonoidAlgebra.of R G (a ^ k) * y) t = y ((a ^ k)⁻¹ * t) := by
189 change (MonoidAlgebra.single (a ^ k) (1 : R) * y) t =
190 y ((a ^ k)⁻¹ * t)
191 rw [MonoidAlgebra.single_mul_apply]
192 simp only [one_mul]
193 have harg : a ^ (-k) * t = (a ^ k)⁻¹ * t := by simp only [zpow_neg]
194 rw [sub_mul, Finsupp.sub_apply, hleft]
195 simpa [harg] using sub_eq_zero.mpr horbit
197/-- The standard finite cyclic reduction from `ZMod (K * M)` to `ZMod M`. -/
198def finiteCyclicReduction (M K : ℕ) :
199 Multiplicative (ZMod (K * M)) →* Multiplicative (ZMod M) :=
200 (ZMod.castHom (Nat.dvd_mul_left M K) (ZMod M)).toAddMonoidHom.toMultiplicative
202/-- Keep an auxiliary finite quotient coordinate while reducing only the cyclic coordinate. -/
203def finiteProductCyclicReduction (Q : Type*) [Group Q] (M K : ℕ) :
204 Q × Multiplicative (ZMod (K * M)) →*
205 Q × Multiplicative (ZMod M) where
206 toFun x := (x.1, finiteCyclicReduction M K x.2)
207 map_one' := by
208 ext <;> simp [finiteCyclicReduction]
209 map_mul' x y := by
210 ext <;> simp [finiteCyclicReduction]
213 (n : ZMod L) = (n.natAbs : ZMod L) ∨
214 (n : ZMod L) = -(n.natAbs : ZMod L) := by
215 rcases Int.natAbs_eq n with hn | hn
216 · left
217 rw [hn]
218 norm_num
219 · right
220 rw [hn]
221 norm_num
224 {L M : ℕ} (n : ℤ) (hdiv : Nat.gcd n.natAbs L ∣ M) :
225 ∃ q : ℤ, (M : ZMod L) = q • (n : ZMod L) := by
226 rcases hdiv with ⟨c, hc⟩
227 let d : ℕ := Nat.gcd n.natAbs L
228 have hbez :
229 ((d : ℤ) : ZMod L) =
230 ((n.natAbs : ℤ) * (Nat.gcdA n.natAbs L : ℤ) +
231 (L : ℤ) * (Nat.gcdB n.natAbs L : ℤ) : ℤ) := by
232 exact congrArg (fun z : ℤ => (z : ZMod L)) (Nat.gcd_eq_gcd_ab n.natAbs L)
233 have hd_natAbs :
234 (d : ZMod L) =
235 (Nat.gcdA n.natAbs L : ℤ) • (n.natAbs : ZMod L) := by
236 calc
237 (d : ZMod L)
238 = ((d : ℤ) : ZMod L) := by norm_num
239 _ = ((n.natAbs : ℤ) * (Nat.gcdA n.natAbs L : ℤ) +
240 (L : ℤ) * (Nat.gcdB n.natAbs L : ℤ) : ℤ) := hbez
241 _ = (Nat.gcdA n.natAbs L : ℤ) • (n.natAbs : ZMod L) := by
242 simp only [Nat.cast_natAbs, Int.cast_abs, Int.cast_eq, mul_comm, Int.cast_add,
243 Int.cast_mul, Int.cast_natCast, CharP.cast_eq_zero, mul_zero, add_zero,
244 zsmul_eq_mul]
246 · refine ⟨(c : ℤ) * Nat.gcdA n.natAbs L, ?_⟩
247 rw [hc]
248 calc
249 ((d * c : ℕ) : ZMod L)
250 = (c : ℕ) • (d : ZMod L) := by
251 rw [nsmul_eq_mul]
252 norm_num [mul_comm]
253 _ = (c : ℕ) • ((Nat.gcdA n.natAbs L : ℤ) • (n.natAbs : ZMod L)) := by
254 rw [hd_natAbs]
255 _ = ((c : ℤ) * Nat.gcdA n.natAbs L) • (n.natAbs : ZMod L) := by
256 simp only [Nat.cast_natAbs, zsmul_eq_mul, nsmul_eq_mul, Int.cast_mul,
257 Int.cast_natCast, mul_assoc]
258 _ = ((c : ℤ) * Nat.gcdA n.natAbs L) • (n : ZMod L) := by
259 rw [hn]
260 · refine ⟨-((c : ℤ) * Nat.gcdA n.natAbs L), ?_⟩
261 rw [hc]
262 calc
263 ((d * c : ℕ) : ZMod L)
264 = (c : ℕ) • (d : ZMod L) := by
265 rw [nsmul_eq_mul]
266 norm_num [mul_comm]
267 _ = (c : ℕ) • ((Nat.gcdA n.natAbs L : ℤ) • (n.natAbs : ZMod L)) := by
268 rw [hd_natAbs]
269 _ = ((c : ℤ) * Nat.gcdA n.natAbs L) • (n.natAbs : ZMod L) := by
270 simp only [Nat.cast_natAbs, zsmul_eq_mul, nsmul_eq_mul, Int.cast_mul,
271 Int.cast_natCast, mul_assoc]
272 _ = -(((c : ℤ) * Nat.gcdA n.natAbs L) • (n : ZMod L)) := by
273 rw [hn]
274 simp only [Nat.cast_natAbs, zsmul_eq_mul, Int.cast_mul, Int.cast_natCast, smul_neg,
275 neg_neg]
276 _ = (-((c : ℤ) * Nat.gcdA n.natAbs L)) • (n : ZMod L) := by
277 rw [neg_zsmul]
279/-- The kernel direction of `ZMod (K * M) → ZMod M` is described by integer multiples of `M`. -/
281 {M K : ℕ} [NeZero (K * M)] {a b : ZMod (K * M)}
282 (h :
283 (ZMod.castHom (Nat.dvd_mul_left M K) (ZMod M)) a =
284 (ZMod.castHom (Nat.dvd_mul_left M K) (ZMod M)) b) :
285 ∃ q : ℤ, a = b + q • (M : ZMod (K * M)) := by
286 have hval : (a.val : ZMod M) = (b.val : ZMod M) := by
287 rw [ZMod.castHom_apply, ZMod.castHom_apply] at h
288 rw [ZMod.cast_eq_val, ZMod.cast_eq_val] at h
289 exact h
290 have hmodNat : a.val ≡ b.val [MOD M] :=
291 (ZMod.natCast_eq_natCast_iff a.val b.val M).mp hval
292 rcases (Nat.modEq_iff_dvd.mp hmodNat) with ⟨q, hq⟩
293 use -q
294 rw [← ZMod.natCast_zmod_val a, ← ZMod.natCast_zmod_val b]
295 have hcast :
296 (((b.val : ℤ) - (a.val : ℤ) : ℤ) : ZMod (K * M)) =
297 (((M : ℤ) * q : ℤ) : ZMod (K * M)) :=
298 congrArg (fun z : ℤ => (z : ZMod (K * M))) hq
299 have hdiff :
300 (b.val : ZMod (K * M)) - (a.val : ZMod (K * M)) =
301 (M : ZMod (K * M)) * (q : ZMod (K * M)) := by
302 simpa [Int.cast_sub, Int.cast_natCast, Int.cast_mul] using hcast
303 calc
304 (a.val : ZMod (K * M))
305 = (b.val : ZMod (K * M)) -
306 (M : ZMod (K * M)) * (q : ZMod (K * M)) := by
307 rw [← hdiff]
308 abel
309 _ = (b.val : ZMod (K * M)) + (-q : ℤ) • (M : ZMod (K * M)) := by
310 rw [zsmul_eq_mul]
311 norm_num
312 ring
314/-- Every fiber of `ZMod (K * M) → ZMod M` has `K` elements. -/
316 {M K : ℕ} [NeZero (K * M)] (i : Multiplicative (ZMod M)) :
317 Fintype.card {t : Multiplicative (ZMod (K * M)) //
318 finiteCyclicReduction M K t = i} = K := by
319 classical
320 have hMne : M ≠ 0 := by
321 intro hM
322 exact NeZero.ne (K * M) (by simp only [hM, mul_zero])
323 letI : NeZero M := ⟨hMne⟩
324 let f : Multiplicative (ZMod (K * M)) →* Multiplicative (ZMod M) :=
326 have hsurj : Function.Surjective f := by
327 intro y
328 cases y with
329 | ofAdd y =>
330 rcases ZMod.castHom_surjective (Nat.dvd_mul_left M K) y with ⟨x, hx⟩
331 exact
332 ⟨Multiplicative.ofAdd x,
333 by simpa [f, finiteCyclicReduction] using congrArg Multiplicative.ofAdd hx⟩
334 have hcardFiberKer :
335 Fintype.card {t : Multiplicative (ZMod (K * M)) // f t = i} =
336 Fintype.card {t : Multiplicative (ZMod (K * M)) // f t = 1} := by
337 rw [Fintype.card_subtype, Fintype.card_subtype]
338 exact MonoidHom.card_fiber_eq_of_mem_range f (hsurj i) (hsurj 1)
339 have hkerSubtype :
340 Fintype.card {t : Multiplicative (ZMod (K * M)) // f t = 1} =
341 Nat.card f.ker := by
342 rw [Nat.card_eq_fintype_card]
343 exact Fintype.card_congr
344 { toFun := fun t => ⟨t.1, MonoidHom.mem_ker.mpr t.2⟩
345 invFun := fun t => ⟨t.1, MonoidHom.mem_ker.mp t.2⟩
346 left_inv := by intro t; rfl
347 right_inv := by intro t; rfl }
348 have hdomain : Nat.card (Multiplicative (ZMod (K * M))) = K * M := by
349 rw [Nat.card_eq_fintype_card]
350 exact (Fintype.card_congr Multiplicative.toAdd).trans (ZMod.card (K * M))
351 have hrange : Nat.card f.range = M := by
352 have htop : f.range = ⊤ := MonoidHom.range_eq_top.mpr hsurj
353 rw [htop]
354 have htopcard :
355 Nat.card (↥(⊤ : Subgroup (Multiplicative (ZMod M)))) =
356 Nat.card (Multiplicative (ZMod M)) :=
357 Nat.card_congr Subgroup.topEquiv.toEquiv
358 rw [htopcard]
359 rw [Nat.card_eq_fintype_card]
360 exact (Fintype.card_congr Multiplicative.toAdd).trans (ZMod.card M)
361 have hkerMul : Nat.card f.ker * M = K * M := by
362 have h := Subgroup.card_mul_index f.ker
363 rw [Subgroup.index_ker, hdomain, hrange] at h
364 exact h
365 have hker : Nat.card f.ker = K :=
366 Nat.mul_right_cancel (Nat.pos_of_ne_zero hMne) hkerMul
367 rw [hcardFiberKer, hkerSubtype, hker]
369/-- The product-with-other-coordinates fiber over `(q, i)` has the same size as the cyclic
370fiber, namely `K`. -/
372 {Q : Type*} [Group Q] [Fintype Q] [DecidableEq Q]
373 {M K : ℕ} [NeZero (K * M)] (i : Q × Multiplicative (ZMod M)) :
374 Fintype.card {t : Q × Multiplicative (ZMod (K * M)) //
375 finiteProductCyclicReduction Q M K t = i} = K := by
376 classical
377 let e :
378 {t : Q × Multiplicative (ZMod (K * M)) //
380 {z : Multiplicative (ZMod (K * M)) //
381 finiteCyclicReduction M K z = i.2} :=
382 {
383 toFun t := ⟨t.1.2, by
384 have h := congrArg Prod.snd t.2
386 invFun z := ⟨(i.1, z.1), by
387 ext <;> first | rfl | assumption | exact finiteProductCyclicReduction |
388 exact finiteProductCyclicReduction.symm |
389 simp only [finiteProductCyclicReduction, MonoidHom.coe_mk, OneHom.coe_mk, z.2,
390 Prod.mk.eta]⟩
391 left_inv t := by
392 apply Subtype.ext
393 have hfst := congrArg Prod.fst t.2
394 ext <;> first | rfl | assumption | exact finiteProductCyclicReduction |
395 exact finiteProductCyclicReduction.symm |
396 simp only [finiteProductCyclicReduction, MonoidHom.coe_mk, OneHom.coe_mk] at hfst ⊢
397 exact hfst.symm
398 right_inv z := by
399 apply Subtype.ext
400 rfl }
401 calc
402 Fintype.card {t : Q × Multiplicative (ZMod (K * M)) //
404 = Fintype.card {z : Multiplicative (ZMod (K * M)) //
405 finiteCyclicReduction M K z = i.2} := Fintype.card_congr e
406 _ = K := finiteCyclicReduction_fiber_card (M := M) (K := K) (i := i.2)
408/-- Product-coordinate version of the GCD-conditioned fiber constancy. -/
410 {R Q : Type*} [Ring R] [Group Q] {M K : ℕ} [NeZero (K * M)] (n : ℤ)
411 (hgcd : Nat.gcd n.natAbs (K * M) ∣ M)
412 (y : MonoidAlgebra R (Q × Multiplicative (ZMod (K * M))))
413 (hrel :
414 (MonoidAlgebra.of R (Q × Multiplicative (ZMod (K * M)))
415 (1, Multiplicative.ofAdd (n : ZMod (K * M))) - 1) * y = 0)
416 {s t : Q × Multiplicative (ZMod (K * M))}
418 y s = y t := by
419 rcases s with ⟨qs, s⟩
420 rcases t with ⟨qt, t⟩
421 cases s with
422 | ofAdd a =>
423 cases t with
424 | ofAdd b =>
425 have hq : qs = qt := by
426 have h := congrArg Prod.fst hst
428 subst qs
429 have hcyc :
430 finiteCyclicReduction M K (Multiplicative.ofAdd a) =
431 finiteCyclicReduction M K (Multiplicative.ofAdd b) := by
432 have h := congrArg Prod.snd hst
434 rcases
436 (M := M) (K := K) (a := a) (b := b)
437 (Multiplicative.ofAdd.injective hcyc) with
438 ⟨q, hqM0⟩
439 rcases
441 (L := K * M) (M := M) n hgcd with
442 ⟨c, hc⟩
443 have hqM :
444 q • (M : ZMod (K * M)) =
445 (q * c) • (n : ZMod (K * M)) := by
446 rw [hc, smul_smul]
447 have harg : a = b + (q * c) • (n : ZMod (K * M)) := by
448 rw [← hqM]
449 exact hqM0
450 let g : Q × Multiplicative (ZMod (K * M)) :=
451 (1, Multiplicative.ofAdd (n : ZMod (K * M)))
452 let t0 : Q × Multiplicative (ZMod (K * M)) :=
453 (qt, Multiplicative.ofAdd b)
454 have horbit :=
456 (R := R) (G := Q × Multiplicative (ZMod (K * M))) g y hrel
457 (q * c) t0
458 have hgt : g ^ (q * c) * t0 = (qt, Multiplicative.ofAdd a) := by
459 ext
460 · simp only [Prod.pow_mk, one_zpow, Prod.mk_mul_mk, one_mul, g, t0]
461 · change
462 Multiplicative.ofAdd
463 ((q * c) • (n : ZMod (K * M)) + b) =
464 Multiplicative.ofAdd a
465 rw [harg]
466 abel_nf
467 simpa [t0] using hgt ▸ horbit
469/-- In a finite-stage group algebra projection, coefficients that are constant on a fiber
470aggregate to the fiber cardinality times the common coefficient. -/
472 {R G H : Type*} [Semiring R] [Monoid G] [Monoid H] [Fintype G] [DecidableEq H]
473 (f : G →* H) (y : MonoidAlgebra R G) (h : H) (c : R)
474 (hconst : ∀ g : G, f g = h → y g = c) :
475 (MonoidAlgebra.mapDomainRingHom R f y) h =
476 Fintype.card {g : G // f g = h} • c := by
477 classical
478 have hy : y = ∑ g : G, MonoidAlgebra.single g (y g) := by
479 have hsum : y.sum MonoidAlgebra.single = y := MonoidAlgebra.sum_single y
480 have hfin :
481 y.sum MonoidAlgebra.single = ∑ g : G, MonoidAlgebra.single g (y g) :=
482 Finsupp.sum_fintype y (fun g r => MonoidAlgebra.single g r)
483 (by intro g; simp only [Finsupp.single_zero])
484 exact hsum.symm.trans hfin
485 rw [hy, map_sum]
486 simp only [MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_single]
487 rw [show (∑ g : G, MonoidAlgebra.single (f g) (y g)) h =
488 ∑ g : G, (MonoidAlgebra.single (f g) (y g) : MonoidAlgebra R H) h by
489 exact (map_sum (Finsupp.applyAddHom h)
490 (fun g : G => (MonoidAlgebra.single (f g) (y g) : MonoidAlgebra R H)) Finset.univ)]
491 simp only [Finsupp.single_apply]
492 let s : Finset G := Finset.univ.filter fun x : G => f x = h
493 calc
494 (∑ x : G, if f x = h then y x else 0)
495 = ∑ x ∈ s, y x := by
496 simp only [Finset.sum_filter, s]
497 _ = ∑ x ∈ s, c := by
498 apply Finset.sum_congr rfl
499 intro x hx
500 exact hconst x (by simpa [s] using (Finset.mem_filter.mp hx).2)
501 _ = ∑ x : {g : G // f g = h}, c := by
502 rw [← Finset.sum_subtype
503 (s := s)
504 (h := by intro x; simp only [Finset.mem_filter, Finset.mem_univ, true_and, s])
505 (f := fun _ => c)]
506 _ = Fintype.card {g : G // f g = h} • c := by
507 simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
509/-- Product-coordinate coefficient aggregation with the GCD-conditioned cyclic depth. -/
511 {R Q : Type*} [Ring R] [Group Q] [Finite Q]
512 {M K : ℕ} [NeZero (K * M)] (n : ℤ)
513 (hgcd : Nat.gcd n.natAbs (K * M) ∣ M)
514 (y : MonoidAlgebra R (Q × Multiplicative (ZMod (K * M))))
515 (i : Q × Multiplicative (ZMod M)) (t0 : Q × Multiplicative (ZMod (K * M)))
516 (ht0 : finiteProductCyclicReduction Q M K t0 = i)
517 (hrel :
518 (MonoidAlgebra.of R (Q × Multiplicative (ZMod (K * M)))
519 (1, Multiplicative.ofAdd (n : ZMod (K * M))) - 1) * y = 0) :
520 (MonoidAlgebra.mapDomainRingHom R (finiteProductCyclicReduction Q M K) y) i =
521 K • y t0 := by
522 classical
523 letI : Fintype Q := Fintype.ofFinite Q
525 (finiteProductCyclicReduction Q M K) y i (y t0)]
526 · rw [finiteProductCyclicReduction_fiber_card (Q := Q) (M := M) (K := K) (i := i)]
527 · intro t ht
528 exact
530 (R := R) (Q := Q) (M := M) (K := K) n hgcd y hrel (by rw [ht, ht0])
532/-- With `ZMod K` coefficients, the product-coordinate GCD-conditioned projection vanishes. -/
534 {Q : Type*} [Group Q] [Finite Q]
535 {M K : ℕ} [NeZero (K * M)] (n : ℤ)
536 (hgcd : Nat.gcd n.natAbs (K * M) ∣ M)
537 (y : MonoidAlgebra (ZMod K) (Q × Multiplicative (ZMod (K * M))))
538 (hrel :
539 (MonoidAlgebra.of (ZMod K) (Q × Multiplicative (ZMod (K * M)))
540 (1, Multiplicative.ofAdd (n : ZMod (K * M))) - 1) * y = 0) :
541 MonoidAlgebra.mapDomainRingHom (ZMod K) (finiteProductCyclicReduction Q M K) y = 0 := by
542 classical
543 letI : Fintype Q := Fintype.ofFinite Q
544 have hMne : M ≠ 0 := by
545 intro hM
546 exact NeZero.ne (K * M) (by simp only [hM, mul_zero])
547 letI : NeZero M := ⟨hMne⟩
548 ext x
549 rcases x with ⟨q, i⟩
550 cases i with
551 | ofAdd i =>
552 rcases ZMod.castHom_surjective (Nat.dvd_mul_left M K) i with ⟨t0, ht0⟩
553 have ht0' :
554 finiteProductCyclicReduction Q M K (q, Multiplicative.ofAdd t0) =
555 (q, Multiplicative.ofAdd i) := by
556 ext
557 · simp only [finiteProductCyclicReduction, MonoidHom.coe_mk, OneHom.coe_mk]
558 · simpa [finiteProductCyclicReduction] using congrArg Multiplicative.ofAdd ht0
559 have hcoeff :=
561 (Q := Q) (M := M) (K := K) n hgcd y
562 (q, Multiplicative.ofAdd i) (q, Multiplicative.ofAdd t0) ht0' hrel
563 rw [hcoeff]
564 rw [nsmul_eq_mul]
565 simp only [CharP.cast_eq_zero, zero_mul, Finsupp.coe_zero, Pi.zero_apply]
567/-- Product-coordinate vanishing when the first coordinate is killed by taking a finite
568integer power of the relation element. -/
570 {Q : Type*} [Group Q] [Finite Q]
571 {M K : ℕ} [NeZero (K * M)] (a : Q) (n : ℤ) (d : ℕ)
572 (had : a ^ d = 1)
573 (hgcd : Nat.gcd (((d : ℤ) * n).natAbs) (K * M) ∣ M)
574 (y : MonoidAlgebra (ZMod K) (Q × Multiplicative (ZMod (K * M))))
575 (hrel :
576 (MonoidAlgebra.of (ZMod K) (Q × Multiplicative (ZMod (K * M)))
577 (a, Multiplicative.ofAdd (n : ZMod (K * M))) - 1) * y = 0) :
578 MonoidAlgebra.mapDomainRingHom (ZMod K) (finiteProductCyclicReduction Q M K) y = 0 := by
579 classical
580 letI : Fintype Q := Fintype.ofFinite Q
581 let g : Q × Multiplicative (ZMod (K * M)) :=
582 (a, Multiplicative.ofAdd (n : ZMod (K * M)))
583 have hpowrel :
584 (MonoidAlgebra.of (ZMod K) (Q × Multiplicative (ZMod (K * M)))
585 (g ^ (d : ℤ)) - 1) * y = 0 :=
587 (R := ZMod K) (G := Q × Multiplicative (ZMod (K * M))) g (d : ℤ) y hrel
588 have hgpow :
589 g ^ (d : ℤ) =
590 (1, Multiplicative.ofAdd (((d : ℤ) * n : ℤ) : ZMod (K * M))) := by
591 ext
592 · change a ^ (d : ℤ) = 1
593 simpa [zpow_natCast] using had
594 · change (Multiplicative.ofAdd (n : ZMod (K * M))) ^ (d : ℤ) =
595 Multiplicative.ofAdd (((d : ℤ) * n : ℤ) : ZMod (K * M))
596 change Multiplicative.ofAdd ((d : ℤ) • (n : ZMod (K * M))) =
597 Multiplicative.ofAdd (((d : ℤ) * n : ℤ) : ZMod (K * M))
598 simp only [zsmul_eq_mul, Int.cast_natCast, mul_comm, Int.cast_mul]
599 have hrel' :
600 (MonoidAlgebra.of (ZMod K) (Q × Multiplicative (ZMod (K * M)))
601 (1, Multiplicative.ofAdd (((d : ℤ) * n : ℤ) : ZMod (K * M))) - 1) * y = 0 := by
602 rw [hgpow] at hpowrel
603 exact hpowrel
604 exact
606 (Q := Q) (M := M) (K := K) ((d : ℤ) * n) hgcd y hrel'
608/-- A surjective group homomorphism lets each group-like basis element be lifted through the
609induced group-algebra map. -/
611 (R : Type u) (G H : Type v) [CommRing R] [Group G] [Group H]
612 (φ : MonoidHom G H) (hφ : Function.Surjective φ) (h : H) :
613 ∃ g : G, φ g = h ∧
614 MonoidAlgebra.mapDomainRingHom R φ (MonoidAlgebra.of R G g) =
615 MonoidAlgebra.of R H h := by
616 rcases hφ h with ⟨g, hg⟩
617 refine ⟨g, hg, ?_⟩
618 rw [← hg]
621/-- A coefficient supported at a target group element has a coefficient-supported lift along a
622surjective group homomorphism. -/
624 (R : Type u) (G H : Type v) [CommRing R] [Group G] [Group H]
625 (φ : MonoidHom G H) (hφ : Function.Surjective φ) (h : H) (r : R) :
626 ∃ g : G, φ g = h ∧
627 MonoidAlgebra.mapDomainRingHom R φ (MonoidAlgebra.single g r) =
628 MonoidAlgebra.single h r := by
629 rcases hφ h with ⟨g, hg⟩
630 refine ⟨g, hg, ?_⟩
631 rw [MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_single, hg]
633/-- A surjective group homomorphism induces a surjective map on group algebras. -/
635 (R : Type u) (G H : Type v) [CommRing R] [Group G] [Group H]
636 (φ : MonoidHom G H) (hφ : Function.Surjective φ) :
637 Function.Surjective (MonoidAlgebra.mapDomainRingHom R φ) := by
638 classical
639 intro x
640 induction x using Finsupp.induction with
641 | zero =>
642 exact ⟨0, by simp only [MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_zero]⟩
643 | single_add h r x _ _ ih =>
644 rcases hφ h with ⟨g, hg⟩
645 rcases ih with ⟨y, hy⟩
646 refine ⟨MonoidAlgebra.single g r + y, ?_⟩
647 rw [map_add, hy]
648 rw [MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_single, hg]
650/-- For a finite discrete group, the finite group algebra itself is a completed group algebra
651model. -/
653 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
654 [TopologicalSpace G] [Finite G] [DiscreteTopology G] (hR : IsProfiniteRing R) :
655 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
656 IsCompletedGroupAlgebraModel R G (MonoidAlgebra R G) := by
657 classical
658 letI : Fintype G := Fintype.ofFinite G
659 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
660 have hG : IsProfiniteGroup G :=
661 ProCGroups.IsProfiniteGroup.of_finite_discrete (G := G)
662 have hRG : IsProfiniteRing (MonoidAlgebra R G) :=
664 refine ⟨hR, hG, hRG, ?_⟩
665 refine ⟨finiteGroupAlgebraTopology R G, ?_⟩
666 exact ⟨RingHom.id (MonoidAlgebra R G), denseRange_id, continuous_id⟩