Yamaguchi Lean 4 Library
Source: ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Functoriality
ProCGroups/CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra/Functoriality/Source

Source: ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Functoriality

1import Mathlib.Data.ZMod.Basic
2import ProCGroups.CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Topology
4/-!
5# Functoriality of finite group algebras
7This file studies group-algebra maps induced by homomorphisms of finite groups, including
8composition, basis formulas, continuity, and surjectivity. It also develops coefficient
9calculations for cyclic reductions used in later kernel arguments.
10-/
12open scoped Topology
13open ProCGroups
15namespace CompletedGroupAlgebra
17universe u v
19/-- Finite-stage group algebras are functorial by continuous ring homomorphisms. -/
20theorem finiteGroupAlgebra_mapDomainRingHom_continuous
21 (R : Type u) (G H : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
22 [Group G] [Group H] [Finite G] [Finite H] (φ : G →* H) :
23 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
24 letI : TopologicalSpace (MonoidAlgebra R H) := finiteGroupAlgebraTopology R H
25 Continuous (MonoidAlgebra.mapDomainRingHom R φ : MonoidAlgebra R G → MonoidAlgebra R H) := by
26 classical
27 letI : Fintype G := Fintype.ofFinite G
28 letI : Fintype H := Fintype.ofFinite H
29 letI : TopologicalSpace (MonoidAlgebra R G) := finiteGroupAlgebraTopology R G
30 letI : TopologicalSpace (MonoidAlgebra R H) := finiteGroupAlgebraTopology R H
31 let e : MonoidAlgebra R H ≃ (H → R) :=
32 (MonoidAlgebra.coeffEquiv (R := R) (M := H)).trans Finsupp.equivFunOnFinite
33 have he : Topology.IsInducing (e : MonoidAlgebra R H → H → R) :=
34 Topology.IsInducing.induced e
35 have hcoord : ∀ g : G, Continuous fun x : MonoidAlgebra R G => x.coeff g :=
36 finiteGroupAlgebra_coordinate_continuous R G
37 rw [he.continuous_iff]
38 apply continuous_pi
39 intro h
40 change Continuous fun x : MonoidAlgebra R G =>
41 (MonoidAlgebra.mapDomainRingHom R φ x : MonoidAlgebra R H).coeff h
42 rw [show (fun x : MonoidAlgebra R G =>
43 (MonoidAlgebra.mapDomainRingHom R φ x : MonoidAlgebra R H).coeff h) =
44 (fun x : MonoidAlgebra R G =>
45 ∑ g ∈ Finset.univ.filter (fun g : G => φ g = h), x.coeff g) from ?_]
46 · apply continuous_finsetSum
47 intro g _hg
48 exact hcoord g
49 · funext x
50 change (Finsupp.mapDomain φ x.coeff) h =
51 ∑ g ∈ Finset.univ.filter (fun g : G => φ g = h), x.coeff g
52 rw [Finsupp.mapDomain, Finsupp.sum]
53 rw [Finsupp.finsetSum_apply]
54 simp only [Finsupp.single_apply]
55 change (∑ g ∈ x.coeff.support, if φ g = h then x.coeff g else 0) =
56 ∑ g ∈ Finset.univ.filter (fun g : G => φ g = h), x.coeff g
57 rw [Finset.sum_filter]
58 exact Finset.sum_subset (by intro g _hg; simp only [Finset.mem_univ]) (by
59 intro g _hguniv hgnot
60 by_cases hφ : φ g = h
61 · simp only [hφ, ↓reduceIte, Finsupp.notMem_support_iff.mp hgnot]
62 · simp only [hφ, ↓reduceIte])
64/-- The finite-stage group algebra functor sends the identity homomorphism to the identity. -/
65theorem finiteGroupAlgebra_mapDomainRingHom_id
66 (R : Type u) (G : Type v) [CommRing R] [Group G] :
67 MonoidAlgebra.mapDomainRingHom R (MonoidHom.id G) = RingHom.id (MonoidAlgebra R G) := by
68 exact MonoidAlgebra.mapDomainRingHom_id
70/-- The finite-stage group algebra functor respects composition. -/
71theorem finiteGroupAlgebra_mapDomainRingHom_comp
72 (R : Type u) (G H K : Type v) [CommRing R] [Group G] [Group H] [Group K]
73 (φ : G →* H) (ψ : H →* K) :
74 (MonoidAlgebra.mapDomainRingHom R ψ).comp (MonoidAlgebra.mapDomainRingHom R φ) =
75 MonoidAlgebra.mapDomainRingHom R (ψ.comp φ) := by
76 exact (MonoidAlgebra.mapDomainRingHom_comp (R := R) ψ φ).symm
78/-- Functoriality on the canonical group-like basis elements of a finite-stage group algebra. -/
79theorem finiteGroupAlgebra_mapDomainRingHom_of
80 (R : Type u) (G H : Type v) [CommRing R] [Group G] [Group H]
81 (φ : G →* H) (g : G) :
82 MonoidAlgebra.mapDomainRingHom R φ (MonoidAlgebra.of R G g) =
83 MonoidAlgebra.of R H (φ g) := by
84 change MonoidAlgebra.mapDomain φ (MonoidAlgebra.single g 1) =
85 MonoidAlgebra.single (φ g) 1
86 exact MonoidAlgebra.mapDomain_single
88/--
89A finite group-algebra relation is preserved by pushing the group variable along a homomorphism.
90-/
91theorem finiteGroupAlgebra_mapDomain_sub_one_mul_eq_zero
92 {R G H : Type*} [Ring R] [Group G] [Group H]
93 (f : G →* H) (g : G) (y : MonoidAlgebra R G)
94 (hrel : (MonoidAlgebra.of R G g - 1) * y = 0) :
95 (MonoidAlgebra.of R H (f g) - 1) *
96 MonoidAlgebra.mapDomainRingHom R f y = 0 := by
97 have hmap := congrArg (MonoidAlgebra.mapDomainRingHom R f) hrel
98 calc
99 (MonoidAlgebra.of R H (f g) - 1) *
100 MonoidAlgebra.mapDomainRingHom R f y
101 = MonoidAlgebra.mapDomainRingHom R f
102 ((MonoidAlgebra.of R G g - 1) * y) := by
103 rw [map_mul, map_sub, map_one]
104 rw [show MonoidAlgebra.mapDomainRingHom R f (MonoidAlgebra.of R G g) =
105 MonoidAlgebra.of R H (f g) by
106 change MonoidAlgebra.mapDomain f (MonoidAlgebra.single g 1) =
107 MonoidAlgebra.single (f g) 1
108 exact MonoidAlgebra.mapDomain_single]
109 _ = 0 := by simpa only [map_zero] using hmap
111/-- Integer-power version of finite group-algebra relation functoriality. -/
112theorem finiteGroupAlgebra_mapDomain_zpow_sub_one_mul_eq_zero
113 {R G H : Type*} [Ring R] [Group G] [Group H]
114 (f : G →* H) (g : G) (n : ℤ) (y : MonoidAlgebra R G)
115 (hrel : (MonoidAlgebra.of R G (g ^ n) - 1) * y = 0) :
116 (MonoidAlgebra.of R H ((f g) ^ n) - 1) *
117 MonoidAlgebra.mapDomainRingHom R f y = 0 := by
118 simpa only [map_zpow] using
119 finiteGroupAlgebra_mapDomain_sub_one_mul_eq_zero f (g ^ n) y hrel
121/--
122A finite group-algebra relation \((a - 1)y = 0\) makes coefficients constant along the left
123\(a\)-orbits.
124-/
125theorem finiteGroupAlgebra_coeff_eq_zpow_mul_of_sub_one_mul_eq_zero
126 {R G : Type*} [Ring R] [Group G] (a : G) (y : MonoidAlgebra R G)
127 (hrel : (MonoidAlgebra.of R G a - 1) * y = 0) :
128 ∀ k : ℤ, ∀ t : G, y.coeff (a ^ k * t) = y.coeff t := by
129 have hmul : MonoidAlgebra.of R G a * y = y := by
130 have h : MonoidAlgebra.of R G a * y - y = 0 := by
131 simpa [sub_mul] using hrel
132 exact sub_eq_zero.mp h
133 have hpowmul : ∀ m : ℕ, MonoidAlgebra.of R G (a ^ m) * y = y := by
134 intro m
135 induction m with
136 | zero =>
137 rw [pow_zero]
138 change MonoidAlgebra.single (1 : G) (1 : R) * y = y
139 rw [← MonoidAlgebra.one_def]
140 simp only [one_mul]
141 | succ m ih =>
142 calc
143 MonoidAlgebra.of R G (a ^ (m + 1)) * y
144 = MonoidAlgebra.of R G (a ^ m) * (MonoidAlgebra.of R G a * y) := by
145 rw [← mul_assoc, ← map_mul]
146 simp only [pow_succ, MonoidAlgebra.of_apply]
147 _ = MonoidAlgebra.of R G (a ^ m) * y := by rw [hmul]
148 _ = y := ih
149 have hneg : ∀ m : ℕ, ∀ t : G, y.coeff ((a ^ m)⁻¹ * t) = y.coeff t := by
150 intro m t
151 have hcoeff :=
152 congrArg (fun z : MonoidAlgebra R G => z.coeff t) (hpowmul m)
153 have hleft :
154 (MonoidAlgebra.of R G (a ^ m) * y).coeff t =
155 y.coeff ((a ^ m)⁻¹ * t) := by
156 change (MonoidAlgebra.single (a ^ m) (1 : R) * y).coeff t =
157 y.coeff ((a ^ m)⁻¹ * t)
158 rw [MonoidAlgebra.coeff_single_mul_apply]
159 simp only [one_mul]
160 simpa [hleft] using hcoeff
161 have hpos : ∀ m : ℕ, ∀ t : G, y.coeff (a ^ m * t) = y.coeff t := by
162 intro m t
163 have h := hneg m (a ^ m * t)
164 have hsimp : (a ^ m)⁻¹ * (a ^ m * t) = t := by simp only [inv_mul_cancel_left]
165 exact (by simpa [hsimp] using h.symm)
166 intro k
167 cases k with
168 | ofNat m =>
169 intro t
170 simpa using hpos m t
171 | negSucc m =>
172 intro t
173 simpa [zpow_negSucc] using hneg (m + 1) t
175/--
176A finite group-algebra relation \((a - 1)y = 0\) also gives \((a^k - 1)y = 0\) for every integer
177power \(k\).
178-/
179theorem finiteGroupAlgebra_zpow_sub_one_mul_eq_zero_of_sub_one_mul_eq_zero
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 :=
185 finiteGroupAlgebra_coeff_eq_zpow_mul_of_sub_one_mul_eq_zero
186 (R := R) (G := G) a y hrel (-k) t
187 have hleft :
188 (MonoidAlgebra.of R G (a ^ k) * y).coeff t =
189 y.coeff ((a ^ k)⁻¹ * t) := by
190 change (MonoidAlgebra.single (a ^ k) (1 : R) * y).coeff t =
191 y.coeff ((a ^ k)⁻¹ * t)
192 rw [MonoidAlgebra.coeff_single_mul_apply]
193 simp only [one_mul]
194 have harg : a ^ (-k) * t = (a ^ k)⁻¹ * t := by simp only [zpow_neg]
195 rw [sub_mul, one_mul]
196 change (MonoidAlgebra.of R G (a ^ k) * y).coeff t - y.coeff t = 0
197 rw [hleft]
198 simpa [harg] using sub_eq_zero.mpr horbit
200/--
201The standard finite cyclic reduction from \(\mathbb{Z}/(K M)\mathbb{Z}\) to
202\(\mathbb{Z}/M\mathbb{Z}\).
203-/
204def finiteCyclicReduction (M K : ℕ) :
205 Multiplicative (ZMod (K * M)) →* Multiplicative (ZMod M) :=
206 (ZMod.castHom (Nat.dvd_mul_left M K) (ZMod M)).toAddMonoidHom.toMultiplicative
208/--
209The finite product cyclic reduction keeps an auxiliary finite quotient coordinate while reducing
210only the cyclic coordinate.
211-/
212def finiteProductCyclicReduction (Q : Type*) [Group Q] (M K : ℕ) :
213 Q × Multiplicative (ZMod (K * M)) →*
214 Q × Multiplicative (ZMod M) where
215 toFun x := (x.1, finiteCyclicReduction M K x.2)
216 map_one' := by
217 ext <;> simp [finiteCyclicReduction]
218 map_mul' x y := by
219 ext <;> simp [finiteCyclicReduction]
221/--
222An integer cast to \(\mathbb{Z}/n\mathbb{Z}\) is represented by either its absolute value or the
223negative of its absolute value, depending on its sign.
224-/
225theorem int_cast_eq_natAbs_or_neg_natAbs_zmod_of_modulus (L : ℕ) (n : ℤ) :
226 (n : ZMod L) = (n.natAbs : ZMod L) ∨
227 (n : ZMod L) = -(n.natAbs : ZMod L) := by
228 rcases Int.natAbs_eq n with hn | hn
229 · left
230 rw [hn]
231 norm_num
232 · right
233 rw [hn]
234 norm_num
236/--
237A natural number cast into \(\mathbb{Z}/n\mathbb{Z}\) lies in the subgroup generated by an
238integer cast whenever the required gcd divisibility condition holds.
239-/
240theorem zmod_natCast_mem_zmultiples_intCast_of_gcd_dvd
241 {L M : ℕ} (n : ℤ) (hdiv : Nat.gcd n.natAbs L ∣ M) :
242 ∃ q : ℤ, (M : ZMod L) = q • (n : ZMod L) := by
243 rcases hdiv with ⟨c, hc⟩
244 let d : ℕ := Nat.gcd n.natAbs L
245 have hbez :
246 ((d : ℤ) : ZMod L) =
247 ((n.natAbs : ℤ) * (Nat.gcdA n.natAbs L : ℤ) +
248 (L : ℤ) * (Nat.gcdB n.natAbs L : ℤ) : ℤ) := by
249 exact congrArg (fun z : ℤ => (z : ZMod L)) (Nat.gcd_eq_gcd_ab n.natAbs L)
250 have hd_natAbs :
251 (d : ZMod L) =
252 (Nat.gcdA n.natAbs L : ℤ) • (n.natAbs : ZMod L) := by
253 calc
254 (d : ZMod L)
255 = ((d : ℤ) : ZMod L) := by norm_num
256 _ = ((n.natAbs : ℤ) * (Nat.gcdA n.natAbs L : ℤ) +
257 (L : ℤ) * (Nat.gcdB n.natAbs L : ℤ) : ℤ) := hbez
258 _ = (Nat.gcdA n.natAbs L : ℤ) • (n.natAbs : ZMod L) := by
259 simp only [Nat.cast_natAbs, Int.cast_abs, Int.cast_eq, mul_comm, Int.cast_add,
260 Int.cast_mul, Int.cast_natCast, CharP.cast_eq_zero, mul_zero, add_zero,
261 zsmul_eq_mul]
262 rcases int_cast_eq_natAbs_or_neg_natAbs_zmod_of_modulus L n with hn | hn
263 · refine ⟨(c : ℤ) * Nat.gcdA n.natAbs L, ?_⟩
264 rw [hc]
265 calc
266 ((d * c : ℕ) : ZMod L)
267 = (c : ℕ) • (d : ZMod L) := by
268 rw [nsmul_eq_mul]
269 norm_num [mul_comm]
270 _ = (c : ℕ) • ((Nat.gcdA n.natAbs L : ℤ) • (n.natAbs : ZMod L)) := by
271 rw [hd_natAbs]
272 _ = ((c : ℤ) * Nat.gcdA n.natAbs L) • (n.natAbs : ZMod L) := by
273 simp only [Nat.cast_natAbs, zsmul_eq_mul, nsmul_eq_mul, Int.cast_mul,
274 Int.cast_natCast, mul_assoc]
275 _ = ((c : ℤ) * Nat.gcdA n.natAbs L) • (n : ZMod L) := by
276 rw [hn]
277 · refine ⟨-((c : ℤ) * Nat.gcdA n.natAbs L), ?_⟩
278 rw [hc]
279 calc
280 ((d * c : ℕ) : ZMod L)
281 = (c : ℕ) • (d : ZMod L) := by
282 rw [nsmul_eq_mul]
283 norm_num [mul_comm]
284 _ = (c : ℕ) • ((Nat.gcdA n.natAbs L : ℤ) • (n.natAbs : ZMod L)) := by
285 rw [hd_natAbs]
286 _ = ((c : ℤ) * Nat.gcdA n.natAbs L) • (n.natAbs : ZMod L) := by
287 simp only [Nat.cast_natAbs, zsmul_eq_mul, nsmul_eq_mul, Int.cast_mul,
288 Int.cast_natCast, mul_assoc]
289 _ = -(((c : ℤ) * Nat.gcdA n.natAbs L) • (n : ZMod L)) := by
290 rw [hn]
291 simp only [Nat.cast_natAbs, zsmul_eq_mul, Int.cast_mul, Int.cast_natCast, smul_neg,
292 neg_neg]
293 _ = (-((c : ℤ) * Nat.gcdA n.natAbs L)) • (n : ZMod L) := by
294 rw [neg_zsmul]
296/--
297The kernel direction of the map from \(\mathbb{Z}/(K M)\mathbb{Z}\) to
298\(\mathbb{Z}/M\mathbb{Z}\) is described by integer multiples of \(M\).
299-/
300theorem exists_zsmul_natCast_of_zmod_castHom_eq
301 {M K : ℕ} [NeZero (K * M)] {a b : ZMod (K * M)}
302 (h :
303 (ZMod.castHom (Nat.dvd_mul_left M K) (ZMod M)) a =
304 (ZMod.castHom (Nat.dvd_mul_left M K) (ZMod M)) b) :
305 ∃ q : ℤ, a = b + q • (M : ZMod (K * M)) := by
306 have hval : (a.val : ZMod M) = (b.val : ZMod M) := by
307 rw [ZMod.castHom_apply, ZMod.castHom_apply] at h
308 rw [ZMod.cast_eq_val, ZMod.cast_eq_val] at h
309 exact h
310 have hmodNat : a.val ≡ b.val [MOD M] :=
311 (ZMod.natCast_eq_natCast_iff a.val b.val M).mp hval
312 rcases (Nat.modEq_iff_dvd.mp hmodNat) with ⟨q, hq⟩
313 use -q
314 rw [← ZMod.natCast_zmod_val a, ← ZMod.natCast_zmod_val b]
315 have hcast :
316 (((b.val : ℤ) - (a.val : ℤ) : ℤ) : ZMod (K * M)) =
317 (((M : ℤ) * q : ℤ) : ZMod (K * M)) :=
318 congrArg (fun z : ℤ => (z : ZMod (K * M))) hq
319 have hdiff :
320 (b.val : ZMod (K * M)) - (a.val : ZMod (K * M)) =
321 (M : ZMod (K * M)) * (q : ZMod (K * M)) := by
322 simpa [Int.cast_sub, Int.cast_natCast, Int.cast_mul] using hcast
323 calc
324 (a.val : ZMod (K * M))
325 = (b.val : ZMod (K * M)) -
326 (M : ZMod (K * M)) * (q : ZMod (K * M)) := by
327 rw [← hdiff]
328 abel
329 _ = (b.val : ZMod (K * M)) + (-q : ℤ) • (M : ZMod (K * M)) := by
330 rw [zsmul_eq_mul]
331 norm_num
332 ring
334/-- Every fiber of \(\mathbb{Z}/(K M)\mathbb{Z} \to \mathbb{Z}/M\mathbb{Z}\) has \(K\) elements. -/
335theorem finiteCyclicReduction_fiber_card
336 {M K : ℕ} [NeZero (K * M)] (i : Multiplicative (ZMod M)) :
337 Fintype.card {t : Multiplicative (ZMod (K * M)) //
338 finiteCyclicReduction M K t = i} = K := by
339 classical
340 have hMne : M ≠ 0 := by
341 intro hM
342 exact NeZero.ne (K * M) (by simp only [hM, mul_zero])
343 letI : NeZero M := ⟨hMne⟩
344 let f : Multiplicative (ZMod (K * M)) →* Multiplicative (ZMod M) :=
345 finiteCyclicReduction M K
346 have hsurj : Function.Surjective f := by
347 intro y
348 cases y with
349 | ofAdd y =>
350 rcases ZMod.castHom_surjective (Nat.dvd_mul_left M K) y with ⟨x, hx⟩
351 exact
352 ⟨Multiplicative.ofAdd x,
353 by simpa [f, finiteCyclicReduction] using congrArg Multiplicative.ofAdd hx⟩
354 have hcardFiberKer :
355 Fintype.card {t : Multiplicative (ZMod (K * M)) // f t = i} =
356 Fintype.card {t : Multiplicative (ZMod (K * M)) // f t = 1} := by
357 rw [Fintype.card_subtype, Fintype.card_subtype]
358 exact MonoidHom.card_fiber_eq_of_mem_range f (hsurj i) (hsurj 1)
359 have hkerSubtype :
360 Fintype.card {t : Multiplicative (ZMod (K * M)) // f t = 1} =
361 Nat.card f.ker := by
362 rw [Nat.card_eq_fintype_card]
363 exact Fintype.card_congr
364 { toFun := fun t => ⟨t.1, MonoidHom.mem_ker.mpr t.2⟩
365 invFun := fun t => ⟨t.1, MonoidHom.mem_ker.mp t.2⟩
366 left_inv := by intro t; rfl
367 right_inv := by intro t; rfl }
368 have hdomain : Nat.card (Multiplicative (ZMod (K * M))) = K * M := by
369 rw [Nat.card_eq_fintype_card]
370 exact (Fintype.card_congr Multiplicative.toAdd).trans (ZMod.card (K * M))
371 have hrange : Nat.card f.range = M := by
372 have htop : f.range = ⊤ := MonoidHom.range_eq_top.mpr hsurj
373 rw [htop]
374 have htopcard :
375 Nat.card (↥(⊤ : Subgroup (Multiplicative (ZMod M)))) =
376 Nat.card (Multiplicative (ZMod M)) :=
377 Nat.card_congr Subgroup.topEquiv.toEquiv
378 rw [htopcard]
379 rw [Nat.card_eq_fintype_card]
380 exact (Fintype.card_congr Multiplicative.toAdd).trans (ZMod.card M)
381 have hkerMul : Nat.card f.ker * M = K * M := by
382 have h := Subgroup.card_mul_index f.ker
383 rw [Subgroup.index_ker, hdomain, hrange] at h
384 exact h
385 have hker : Nat.card f.ker = K :=
386 Nat.mul_right_cancel (Nat.pos_of_ne_zero hMne) hkerMul
387 rw [hcardFiberKer, hkerSubtype, hker]
389/--
390The product-with-other-coordinates fiber over \((q,i)\) has the same size as the cyclic fiber,
391namely \(K\).
392-/
393theorem finiteProductCyclicReduction_fiber_card
394 {Q : Type*} [Group Q] [Fintype Q] [DecidableEq Q]
395 {M K : ℕ} [NeZero (K * M)] (i : Q × Multiplicative (ZMod M)) :
396 Fintype.card {t : Q × Multiplicative (ZMod (K * M)) //
397 finiteProductCyclicReduction Q M K t = i} = K := by
398 classical
399 let e :
400 {t : Q × Multiplicative (ZMod (K * M)) //
401 finiteProductCyclicReduction Q M K t = i} ≃
402 {z : Multiplicative (ZMod (K * M)) //
403 finiteCyclicReduction M K z = i.2} :=
404 {
405 toFun t := ⟨t.1.2, by
406 simpa [finiteProductCyclicReduction] using congrArg Prod.snd t.2⟩
407 invFun z := ⟨(i.1, z.1), by
408 ext <;> first | rfl | assumption | exact finiteProductCyclicReduction |
409 exact finiteProductCyclicReduction.symm |
410 simp only [finiteProductCyclicReduction, MonoidHom.coe_mk, OneHom.coe_mk, z.2,
411 Prod.mk.eta]⟩
412 left_inv t := by
413 apply Subtype.ext
414 have hfst := congrArg Prod.fst t.2
415 ext <;> first | rfl | assumption | exact finiteProductCyclicReduction |
416 exact finiteProductCyclicReduction.symm |
417 simp only [finiteProductCyclicReduction, MonoidHom.coe_mk, OneHom.coe_mk] at hfst ⊢
418 exact hfst.symm
419 right_inv z := by
420 apply Subtype.ext
421 rfl }
422 calc
423 Fintype.card {t : Q × Multiplicative (ZMod (K * M)) //
424 finiteProductCyclicReduction Q M K t = i}
425 = Fintype.card {z : Multiplicative (ZMod (K * M)) //
426 finiteCyclicReduction M K z = i.2} := Fintype.card_congr e
427 _ = K := finiteCyclicReduction_fiber_card (M := M) (K := K) (i := i.2)
429/-- Product-coordinate version of the GCD-conditioned fiber constancy. -/
430theorem finiteProductCyclicGroupAlgebra_coeff_eq_of_same_reduction_of_int_sub_one_mul_eq_zero
431 {R Q : Type*} [Ring R] [Group Q] {M K : ℕ} [NeZero (K * M)] (n : ℤ)
432 (hgcd : Nat.gcd n.natAbs (K * M) ∣ M)
433 (y : MonoidAlgebra R (Q × Multiplicative (ZMod (K * M))))
434 (hrel :
435 (MonoidAlgebra.of R (Q × Multiplicative (ZMod (K * M)))
436 (1, Multiplicative.ofAdd (n : ZMod (K * M))) - 1) * y = 0)
437 {s t : Q × Multiplicative (ZMod (K * M))}
438 (hst : finiteProductCyclicReduction Q M K s = finiteProductCyclicReduction Q M K t) :
439 y.coeff s = y.coeff t := by
440 rcases s with ⟨qs, s⟩
441 rcases t with ⟨qt, t⟩
442 cases s with
443 | ofAdd a =>
444 cases t with
445 | ofAdd b =>
446 have hq : qs = qt := by
447 simpa [finiteProductCyclicReduction] using congrArg Prod.fst hst
448 subst qs
449 have hcyc :
450 finiteCyclicReduction M K (Multiplicative.ofAdd a) =
451 finiteCyclicReduction M K (Multiplicative.ofAdd b) := by
452 simpa [finiteProductCyclicReduction] using congrArg Prod.snd hst
453 rcases
454 exists_zsmul_natCast_of_zmod_castHom_eq
455 (M := M) (K := K) (a := a) (b := b)
456 (Multiplicative.ofAdd.injective hcyc) with
457 ⟨q, hqM0⟩
458 rcases
459 zmod_natCast_mem_zmultiples_intCast_of_gcd_dvd
460 (L := K * M) (M := M) n hgcd with
461 ⟨c, hc⟩
462 have hqM :
463 q • (M : ZMod (K * M)) =
464 (q * c) • (n : ZMod (K * M)) := by
465 rw [hc, smul_smul]
466 have harg : a = b + (q * c) • (n : ZMod (K * M)) := by
467 rw [← hqM]
468 exact hqM0
469 let g : Q × Multiplicative (ZMod (K * M)) :=
470 (1, Multiplicative.ofAdd (n : ZMod (K * M)))
471 let t0 : Q × Multiplicative (ZMod (K * M)) :=
472 (qt, Multiplicative.ofAdd b)
473 have horbit :=
474 finiteGroupAlgebra_coeff_eq_zpow_mul_of_sub_one_mul_eq_zero
475 (R := R) (G := Q × Multiplicative (ZMod (K * M))) g y hrel
476 (q * c) t0
477 have hgt : g ^ (q * c) * t0 = (qt, Multiplicative.ofAdd a) := by
478 ext
479 · simp only [Prod.pow_mk, one_zpow, Prod.mk_mul_mk, one_mul, g, t0]
480 · change
481 Multiplicative.ofAdd
482 ((q * c) • (n : ZMod (K * M)) + b) =
483 Multiplicative.ofAdd a
484 rw [harg]
485 abel_nf
486 simpa [t0] using hgt ▸ horbit
488/--
489In a finite-stage group algebra projection, coefficients that are constant on a fiber aggregate
490to the fiber cardinality times the common coefficient.
491-/
492theorem mapDomain_coeff_eq_nsmul_of_fiber_const
493 {R G H : Type*} [Semiring R] [Monoid G] [Monoid H] [Fintype G] [DecidableEq H]
494 (f : G →* H) (y : MonoidAlgebra R G) (h : H) (c : R)
495 (hconst : ∀ g : G, f g = h → y.coeff g = c) :
496 (MonoidAlgebra.mapDomainRingHom R f y).coeff h =
497 Fintype.card {g : G // f g = h} • c := by
498 classical
499 have hy : y = ∑ g : G, MonoidAlgebra.single g (y.coeff g) := by
500 have hsum : y.coeff.sum MonoidAlgebra.single = y :=
501 MonoidAlgebra.sum_coeff_single y
502 have hfin :
503 y.coeff.sum MonoidAlgebra.single =
504 ∑ g : G, MonoidAlgebra.single g (y.coeff g) :=
505 Finsupp.sum_fintype y.coeff (fun g r => MonoidAlgebra.single g r)
506 (by intro g; simp only [MonoidAlgebra.single_zero])
507 exact hsum.symm.trans hfin
508 rw [hy, map_sum]
509 simp only [MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_single]
510 rw [show (∑ g : G, MonoidAlgebra.single (f g) (y.coeff g)).coeff h =
511 ∑ g : G, (MonoidAlgebra.single (f g) (y.coeff g) :
512 MonoidAlgebra R H).coeff h by
513 simpa only [Finsupp.finsetSum_apply] using
514 congrArg (fun z : H →₀ R => z h)
515 (MonoidAlgebra.coeff_sum (R := R) (M := H) Finset.univ
516 (fun g : G => MonoidAlgebra.single (f g) (y.coeff g)))]
517 simp only [MonoidAlgebra.coeff_single, Finsupp.single_apply]
518 let s : Finset G := Finset.univ.filter fun x : G => f x = h
519 calc
520 (∑ x : G, if f x = h then y.coeff x else 0)
521 = ∑ x ∈ s, y.coeff x := by
522 simp only [Finset.sum_filter, s]
523 _ = ∑ x ∈ s, c := by
524 apply Finset.sum_congr rfl
525 intro x hx
526 exact hconst x (by simpa [s] using (Finset.mem_filter.mp hx).2)
527 _ = ∑ x : {g : G // f g = h}, c := by
528 rw [← Finset.sum_subtype
529 (s := s)
530 (h := by intro x; simp only [Finset.mem_filter, Finset.mem_univ, true_and, s])
531 (f := fun _ => c)]
532 _ = Fintype.card {g : G // f g = h} • c := by
533 simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
535/-- Product-coordinate coefficient aggregation with the GCD-conditioned cyclic depth. -/
536theorem
537 finiteProductCyclicGroupAlgebra_projection_coeff_eq_K_nsmul_of_int_sub_one_mul_eq_zero_of_gcd
538 {R Q : Type*} [Ring R] [Group Q] [Finite Q]
539 {M K : ℕ} [NeZero (K * M)] (n : ℤ)
540 (hgcd : Nat.gcd n.natAbs (K * M) ∣ M)
541 (y : MonoidAlgebra R (Q × Multiplicative (ZMod (K * M))))
542 (i : Q × Multiplicative (ZMod M)) (t0 : Q × Multiplicative (ZMod (K * M)))
543 (ht0 : finiteProductCyclicReduction Q M K t0 = i)
544 (hrel :
545 (MonoidAlgebra.of R (Q × Multiplicative (ZMod (K * M)))
546 (1, Multiplicative.ofAdd (n : ZMod (K * M))) - 1) * y = 0) :
547 (MonoidAlgebra.mapDomainRingHom R
548 (finiteProductCyclicReduction Q M K) y).coeff i =
549 K • y.coeff t0 := by
550 classical
551 letI : Fintype Q := Fintype.ofFinite Q
552 rw [mapDomain_coeff_eq_nsmul_of_fiber_const
553 (finiteProductCyclicReduction Q M K) y i (y.coeff t0)]
554 · rw [finiteProductCyclicReduction_fiber_card (Q := Q) (M := M) (K := K) (i := i)]
555 · intro t ht
556 exact
557 finiteProductCyclicGroupAlgebra_coeff_eq_of_same_reduction_of_int_sub_one_mul_eq_zero
558 (R := R) (Q := Q) (M := M) (K := K) n hgcd y hrel (by rw [ht, ht0])
560/--
561With \(\mathbb{Z}/K\mathbb{Z}\) coefficients, the product-coordinate projection vanishes under
562the stated gcd-conditioned multiple of \(g-1\).
563-/
564theorem finiteProductCyclicGroupAlgebra_projection_eq_zero_of_int_sub_one_mul_eq_zero_of_gcd
565 {Q : Type*} [Group Q] [Finite Q]
566 {M K : ℕ} [NeZero (K * M)] (n : ℤ)
567 (hgcd : Nat.gcd n.natAbs (K * M) ∣ M)
568 (y : MonoidAlgebra (ZMod K) (Q × Multiplicative (ZMod (K * M))))
569 (hrel :
570 (MonoidAlgebra.of (ZMod K) (Q × Multiplicative (ZMod (K * M)))
571 (1, Multiplicative.ofAdd (n : ZMod (K * M))) - 1) * y = 0) :
572 MonoidAlgebra.mapDomainRingHom (ZMod K) (finiteProductCyclicReduction Q M K) y = 0 := by
573 classical
574 letI : Fintype Q := Fintype.ofFinite Q
575 have hMne : M ≠ 0 := by
576 intro hM
577 exact NeZero.ne (K * M) (by simp only [hM, mul_zero])
578 letI : NeZero M := ⟨hMne⟩
579 let projectionCoeff :=
580 finiteProductCyclicGroupAlgebra_projection_coeff_eq_K_nsmul_of_int_sub_one_mul_eq_zero_of_gcd
581 (R := ZMod K) (Q := Q) (M := M) (K := K)
582 ext x
583 rcases x with ⟨q, i⟩
584 cases i with
585 | ofAdd i =>
586 rcases ZMod.castHom_surjective (Nat.dvd_mul_left M K) i with ⟨t0, ht0⟩
587 have ht0' :
588 finiteProductCyclicReduction Q M K (q, Multiplicative.ofAdd t0) =
589 (q, Multiplicative.ofAdd i) := by
590 ext
591 · simp only [finiteProductCyclicReduction, MonoidHom.coe_mk, OneHom.coe_mk]
592 · change Multiplicative.ofAdd
593 ((ZMod.castHom (Nat.dvd_mul_left M K) (ZMod M)) t0) =
594 Multiplicative.ofAdd i
595 exact congrArg Multiplicative.ofAdd ht0
596 have hcoeff :=
597 projectionCoeff n hgcd y
598 (q, Multiplicative.ofAdd i) (q, Multiplicative.ofAdd t0) ht0' hrel
599 rw [hcoeff]
600 rw [nsmul_eq_mul]
601 simp only [CharP.cast_eq_zero, zero_mul, MonoidAlgebra.coeff_zero,
602 Finsupp.zero_apply]
604/--
605Product-coordinate vanishing when the first coordinate is killed by taking a finite integer
606power of the relation element.
607-/
608theorem finiteProductCyclicGroupAlgebra_projection_eq_zero_of_pair_relation_of_order
609 {Q : Type*} [Group Q] [Finite Q]
610 {M K : ℕ} [NeZero (K * M)] (a : Q) (n : ℤ) (d : ℕ)
611 (had : a ^ d = 1)
612 (hgcd : Nat.gcd (((d : ℤ) * n).natAbs) (K * M) ∣ M)
613 (y : MonoidAlgebra (ZMod K) (Q × Multiplicative (ZMod (K * M))))
614 (hrel :
615 (MonoidAlgebra.of (ZMod K) (Q × Multiplicative (ZMod (K * M)))
616 (a, Multiplicative.ofAdd (n : ZMod (K * M))) - 1) * y = 0) :
617 MonoidAlgebra.mapDomainRingHom (ZMod K) (finiteProductCyclicReduction Q M K) y = 0 := by
618 classical
619 letI : Fintype Q := Fintype.ofFinite Q
620 let g : Q × Multiplicative (ZMod (K * M)) :=
621 (a, Multiplicative.ofAdd (n : ZMod (K * M)))
622 have hpowrel :
623 (MonoidAlgebra.of (ZMod K) (Q × Multiplicative (ZMod (K * M)))
624 (g ^ (d : ℤ)) - 1) * y = 0 :=
625 finiteGroupAlgebra_zpow_sub_one_mul_eq_zero_of_sub_one_mul_eq_zero
626 (R := ZMod K) (G := Q × Multiplicative (ZMod (K * M))) g (d : ℤ) y hrel
627 have hgpow :
628 g ^ (d : ℤ) =
629 (1, Multiplicative.ofAdd (((d : ℤ) * n : ℤ) : ZMod (K * M))) := by
630 ext
631 · change a ^ (d : ℤ) = 1
632 simpa [zpow_natCast] using had
633 · change (Multiplicative.ofAdd (n : ZMod (K * M))) ^ (d : ℤ) =
634 Multiplicative.ofAdd (((d : ℤ) * n : ℤ) : ZMod (K * M))
635 change Multiplicative.ofAdd ((d : ℤ) • (n : ZMod (K * M))) =
636 Multiplicative.ofAdd (((d : ℤ) * n : ℤ) : ZMod (K * M))
637 simp only [zsmul_eq_mul, Int.cast_natCast, mul_comm, Int.cast_mul]
638 have hrel' :
639 (MonoidAlgebra.of (ZMod K) (Q × Multiplicative (ZMod (K * M)))
640 (1, Multiplicative.ofAdd (((d : ℤ) * n : ℤ) : ZMod (K * M))) - 1) * y = 0 := by
641 rw [hgpow] at hpowrel
642 exact hpowrel
643 exact
644 finiteProductCyclicGroupAlgebra_projection_eq_zero_of_int_sub_one_mul_eq_zero_of_gcd
645 (Q := Q) (M := M) (K := K) ((d : ℤ) * n) hgcd y hrel'
647/--
648A surjective group homomorphism lets each group-like basis element be lifted through the induced
649group-algebra map.
650-/
651theorem finiteGroupAlgebra_mapDomainRingHom_of_preimage
652 (R : Type u) (G H : Type v) [CommRing R] [Group G] [Group H]
653 (φ : MonoidHom G H) (hφ : Function.Surjective φ) (h : H) :
654 ∃ g : G, φ g = h ∧
655 MonoidAlgebra.mapDomainRingHom R φ (MonoidAlgebra.of R G g) =
656 MonoidAlgebra.of R H h := by
657 rcases hφ h with ⟨g, hg⟩
658 refine ⟨g, hg, ?_⟩
659 rw [← hg]
660 exact finiteGroupAlgebra_mapDomainRingHom_of R G H φ g
662/--
663A coefficient supported at a target group element has a coefficient-supported lift along a
664surjective group homomorphism.
665-/
666theorem finiteGroupAlgebra_mapDomainRingHom_single_preimage
667 (R : Type u) (G H : Type v) [CommRing R] [Group G] [Group H]
668 (φ : MonoidHom G H) (hφ : Function.Surjective φ) (h : H) (r : R) :
669 ∃ g : G, φ g = h ∧
670 MonoidAlgebra.mapDomainRingHom R φ (MonoidAlgebra.single g r) =
671 MonoidAlgebra.single h r := by
672 rcases hφ h with ⟨g, hg⟩
673 refine ⟨g, hg, ?_⟩
674 rw [MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_single, hg]
676/-- A surjective group homomorphism induces a surjective map on group algebras. -/
677theorem finiteGroupAlgebra_mapDomainRingHom_surjective
678 (R : Type u) (G H : Type v) [CommRing R] [Group G] [Group H]
679 (φ : MonoidHom G H) (hφ : Function.Surjective φ) :
680 Function.Surjective (MonoidAlgebra.mapDomainRingHom R φ) := by
681 classical
682 intro x
683 induction x using MonoidAlgebra.induction with
684 | zero =>
685 exact ⟨0, map_zero _⟩
686 | single_add h r x _ _ ih =>
687 rcases hφ h with ⟨g, hg⟩
688 rcases ih with ⟨y, hy⟩
689 refine ⟨MonoidAlgebra.single g r + y, ?_⟩
690 rw [map_add, hy]
691 rw [MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_single, hg]
693end CompletedGroupAlgebra