ResidualAugmentation.lean

1 import PaperXII.AuxiliaryGroupAlgebra
2 import PaperXII.LocalIdempotents
3 import Mathlib.Algebra.CharP.Lemmas
4 import Mathlib.Algebra.CharP.Algebra
5 import Mathlib.GroupTheory.PGroup
6 import Mathlib.RingTheory.Nilpotent.Basic
7 
8 set_option autoImplicit false
9 
10 /-! Paper XII, the locality conclusion of 5.2 and Corollary 5.3 in the
11 finite abelian p-group context of Section 5. The argument only needs an
12 abelian p-group; finiteness is unnecessary. Augmentation is the actual
13 group-algebra homomorphism, not an abstract residue map. -/
14 namespace PaperXII.ResidualAugmentation
15 
16 open scoped MonoidAlgebra
17 open PaperXII.AuxiliaryGroupAlgebra
18 
19 variable {k G : Type*} [Field k] [CommGroup G]
20 variable {p : ℕ} [Fact p.Prime] [CharP k p]
21 
22 /-- Every group-basis difference is nilpotent in residue characteristic p. -/
23 theorem generator_nilpotent (hG : IsPGroup p G) (g : G) :
24     IsNilpotent (MonoidAlgebra.single g (1 : k) - 1) := by
25   let : CharP k[G] p := charP_of_injective_algebraMap (algebraMap k k[G]).injective p
26   obtain ⟨n, hn⟩ := hG g
27   refine ⟨p ^ n, ?_⟩
28   rw [sub_pow_char_pow, MonoidAlgebra.single_pow, hn, one_pow, one_pow]
29   simp [MonoidAlgebra.one_def]
30 
31 /-- Subtracting the scalar augmentation leaves a nilpotent element. -/
32 theorem augmentation_difference_nilpotent (hG : IsPGroup p G) (x : k[G]) :
33     IsNilpotent (x - algebraMap k k[G] (augmentation x)) := by
34   induction x using MonoidAlgebra.induction_on with
35   | of g =>
36       simpa [augmentation_single, MonoidAlgebra.one_def] using
37         generator_nilpotent (k := k) hG g
38   | add x y hx hy =>
39       simpa only [map_add, add_sub_add_comm] using
40         (Commute.all _ _).isNilpotent_add hx hy
41   | smul r x hx =>
42       simpa only [map_smul, Algebra.algebraMap_eq_smul_one, smul_sub,
43         smul_smul, smul_eq_mul] using hx.smul r
44 
45 /-- The actual augmentation ideal consists of nilpotents. -/
46 theorem augmentation_kernel_nilpotent (hG : IsPGroup p G) (x : k[G])
47     (hx : augmentation x = 0) : IsNilpotent x := by
48   simpa [hx] using augmentation_difference_nilpotent hG x
49 
50 /-- A group-algebra element is invertible exactly when its augmentation is nonzero. -/
51 theorem isUnit_iff_augmentation_ne_zero (hG : IsPGroup p G) (x : k[G]) :
52     IsUnit x ↔ augmentation x ≠ 0 := by
53   constructor
54   · intro hx
55     exact (hx.map augmentation.toMonoidHom).ne_zero
56   · intro hx
57     have hu : IsUnit (algebraMap k k[G] (augmentation x)) :=
58       (isUnit_iff_ne_zero.mpr hx).map (algebraMap k k[G])
59     simpa using (augmentation_difference_nilpotent hG x).isUnit_add_left_of_commute
60       hu (Commute.all _ _)
61 
62 /-- The residual group algebra is local. -/
63 theorem isLocalRing (hG : IsPGroup p G) : IsLocalRing k[G] := by
64   apply IsLocalRing.of_isUnit_or_isUnit_one_sub_self
65   intro x
66   by_cases hx : augmentation x = 0
67   · right
68     apply (isUnit_iff_augmentation_ne_zero hG _).mpr
69     simp [hx]
70   · exact Or.inl ((isUnit_iff_augmentation_ne_zero hG x).mpr hx)
71 
72 /-- Corollary 5.3: there are no nontrivial residual character projectors. -/
73 theorem idempotent_eq_zero_or_one (hG : IsPGroup p G) (e : k[G])
74     (he : e * e = e) : e = 0 ∨ e = 1 := by
75   let := isLocalRing (k := k) hG
76   exact PaperXII.LocalIdempotents.eq_zero_or_one e he
77 
78 end PaperXII.ResidualAugmentation

Back to source controls