NonabelianResidual.lean

1 import PaperXII.AuxiliaryGroupAlgebra
2 import Mathlib.Algebra.Algebra.ZMod
3 import Mathlib.Algebra.CharP.Algebra
4 import Mathlib.GroupTheory.PGroup
5 import Mathlib.FieldTheory.Finiteness
6 import Mathlib.Algebra.Field.ZMod
7 import Mathlib.RingTheory.Idempotents
8 
9 set_option autoImplicit false
10 
11 /-! The residual group algebra of a finite p-group has no nontrivial
12 idempotents, without an abelian hypothesis. The finite prime-field span of
13 an orbit supplies the fixed vector by p-group fixed-point counting. -/
14 namespace PaperXII.NonabelianResidual
15 
16 open scoped MonoidAlgebra
17 open PaperXII.AuxiliaryGroupAlgebra
18 
19 variable {k G : Type*} [Field k] [Group G]
20 variable {p : ℕ}
21 
22 section PrimeFieldSpan
23 variable [Algebra (ZMod p) k[G]]
24 
25 /-- The prime-field span of the left translates of an element. -/
26 noncomputable def orbitSpan (e : k[G]) : Submodule (ZMod p) k[G] :=
27   Submodule.span (ZMod p) (Set.range fun g : G => MonoidAlgebra.single g 1 * e)
28 
29 theorem self_mem_orbitSpan (e : k[G]) : e ∈ orbitSpan (p := p) e := by
30   exact Submodule.subset_span ⟨1, by
31     change MonoidAlgebra.single (1 : G) (1 : k) * e = e
32     rw [← MonoidAlgebra.one_def, one_mul]⟩
33 
34 theorem translate_mem_orbitSpan (e : k[G]) (g : G) {v : k[G]}
35     (hv : v ∈ orbitSpan (p := p) e) :
36     MonoidAlgebra.single g 1 * v ∈ orbitSpan (p := p) e := by
37   induction hv using Submodule.span_induction with
38   | mem v hv =>
39       obtain ⟨h, rfl⟩ := hv
40       exact Submodule.subset_span ⟨g * h, by simp [← mul_assoc, MonoidAlgebra.single_mul_single]⟩
41   | zero => simp
42   | add x y hx hy ihx ihy => simpa [mul_add] using (orbitSpan e).add_mem ihx ihy
43   | smul r x hx ih => simpa [mul_smul_comm] using (orbitSpan e).smul_mem r ih
44 
45 /-- Left multiplication by group elements on the finite orbit span. -/
46 @[instance_reducible]
47 noncomputable def orbitAction (e : k[G]) : MulAction G (orbitSpan (p := p) e) where
48   smul g v := ⟨MonoidAlgebra.single g 1 * v.1, translate_mem_orbitSpan e g v.2⟩
49   one_smul v := by
50     apply Subtype.ext
51     change MonoidAlgebra.single 1 1 * v.1 = v.1
52     rw [← MonoidAlgebra.one_def, one_mul]
53   mul_smul g h v := by
54     apply Subtype.ext
55     change MonoidAlgebra.single (g * h) 1 * v.1 =
56       MonoidAlgebra.single g 1 * (MonoidAlgebra.single h 1 * v.1)
57     simp [← mul_assoc, MonoidAlgebra.single_mul_single]
58 
59 theorem orbitSpan_mul_idempotent (e : k[G]) (he : e * e = e)
60     {v : k[G]} (hv : v ∈ orbitSpan (p := p) e) : v * e = v := by
61   induction hv using Submodule.span_induction with
62   | mem v hv => obtain ⟨g, rfl⟩ := hv; simp [mul_assoc, he]
63   | zero => simp
64   | add x y hx hy ihx ihy => simp [add_mul, ihx, ihy]
65   | smul r x hx ih => simp [ih]
66 
67 /-- Every nonzero orbit span contains a nonzero regular invariant vector. -/
68 theorem exists_nonzero_invariant [Fact p.Prime] [Finite G] (hG : IsPGroup p G) (e : k[G]) (he : e ≠ 0) :
69     ∃ v : k[G], v ∈ orbitSpan (p := p) e ∧ v ≠ 0 ∧
70       ∀ g : G, MonoidAlgebra.single g 1 * v = v := by
71   classical
72   let V := orbitSpan (p := p) e
73   let : Module.Finite (ZMod p) V :=
74     Module.Finite.span_of_finite (ZMod p) (Set.finite_range _)
75   let : Finite V := Module.finite_of_finite (ZMod p)
76   let : Fintype V := Fintype.ofFinite V
77   let : Nontrivial V := ⟨⟨⟨e, self_mem_orbitSpan e⟩, 0, by
78     intro h
79     exact he (congrArg Subtype.val h)⟩⟩
80   let : MulAction G V := orbitAction e
81   have hd : p ∣ Nat.card V := by
82     rw [Nat.card_eq_fintype_card, Module.card_eq_pow_finrank (K := ZMod p), ZMod.card]
83     exact dvd_pow_self _ (ne_of_gt (Module.finrank_pos (R := ZMod p) (M := V)))
84   obtain ⟨v, hv, h0v⟩ := hG.exists_fixed_point_of_prime_dvd_card_of_fixed_point V hd
85     (a := 0) (by intro g; apply Subtype.ext; exact mul_zero _)
86   refine ⟨v.1, v.2, ?_, ?_⟩
87   · intro hv0
88     exact h0v (Subtype.ext hv0.symm)
89   · intro g
90     exact congrArg Subtype.val (hv g)
91 
92 end PrimeFieldSpan
93 
94 /-- A vector fixed by every left translation has constant coefficients. -/
95 theorem invariant_coeff (v : k[G])
96     (hv : ∀ g : G, MonoidAlgebra.single g 1 * v = v) (g : G) :
97     v.coeff g = v.coeff 1 := by
98   have h := congrArg (fun w : k[G] => w.coeff g) (hv g)
99   simpa using h.symm
100 
101 /-- On a regular invariant vector, right multiplication is scalar augmentation. -/
102 theorem invariant_mul (v e : k[G])
103     (hv : ∀ g : G, MonoidAlgebra.single g 1 * v = v) :
104     v * e = augmentation e • v := by
105   induction e using MonoidAlgebra.induction_on with
106   | of g =>
107       ext h
108       simp [augmentation_single, invariant_coeff v hv]
109   | add x y hx hy => simp [mul_add, hx, hy, add_smul]
110   | smul r x hx => simp [hx, smul_smul]
111 
112 /-- An idempotent with zero augmentation is zero, for any finite p-group. -/
113 theorem idempotent_augmentation_zero [Fact p.Prime] [Finite G] [CharP k p]
114     (hG : IsPGroup p G) (e : k[G]) (he : e * e = e) (ha : augmentation e = 0) :
115     e = 0 := by
116   let : CharP k[G] p := charP_of_injective_algebraMap (algebraMap k k[G]).injective p
117   let : Algebra (ZMod p) k[G] := ZMod.algebra k[G] p
118   by_contra hne
119   obtain ⟨v, hv, hv0, hfixed⟩ := exists_nonzero_invariant hG e hne
120   exact hv0 (by
121     calc v = v * e := (orbitSpan_mul_idempotent e he hv).symm
122          _ = augmentation e • v := invariant_mul v e hfixed
123          _ = 0 := by simp [ha])
124 
125 /-- Corollary 5.3 in full: no nontrivial residual idempotent survives even
126 for a noncommutative finite p-group. -/
127 theorem idempotent_eq_zero_or_one [Fact p.Prime] [Finite G] [CharP k p]
128     (hG : IsPGroup p G) (e : k[G]) (he : e * e = e) : e = 0 ∨ e = 1 := by
129   have ha : augmentation e * augmentation e = augmentation e := by
130     simpa only [← map_mul] using congrArg augmentation he
131   have hcases : augmentation e = 0 ∨ augmentation e = 1 := by
132     by_cases h : augmentation e = 0
133     · exact Or.inl h
134     · exact Or.inr (mul_left_cancel₀ h (ha.trans (mul_one _).symm))
135   rcases hcases with hzero | hone
136   · exact Or.inl (idempotent_augmentation_zero hG e he hzero)
137   · right
138     have h : 1 - e = 0 := idempotent_augmentation_zero hG (1 - e)
139       (show IsIdempotentElem (1 - e) from (show IsIdempotentElem e from he).one_sub) (by simp [hone])
140     exact (sub_eq_zero.mp h).symm
141 
142 end PaperXII.NonabelianResidual

Back to source controls