PrimitiveCharacterBlock.lean

1 import PaperXI.SemisimpleDetection
2 
3 /-! Primitive central character blocks in the literal finite group algebra.
4 Primitivity means absence of nontrivial central sub-idempotents, not rank one. -/
5 set_option autoImplicit false
6 noncomputable section
7 open scoped MonoidAlgebra BigOperators Classical
8 namespace PaperXI.PrimitiveCharacterBlock
9 open PaperXI.CharacterProjector PaperXI.SemisimpleDetection
10 universe u v w
11 variable {G : Type u} [Group G] [Fintype G]
12 variable {V : Type v} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
13 variable {W : Type w} [AddCommGroup W] [Module ℂ W]
14 
15 omit [Fintype G] [FiniteDimensional ℂ V] in
16 /-- Representation equivalences intertwine the full group-algebra action. -/
17 theorem equiv_algebra_action (ρ : Representation ℂ G V) (σ : Representation ℂ G W)
18     (e : Representation.Equiv ρ σ) (a : MonoidAlgebra ℂ G) (x : V) :
19     e (ρ.asAlgebraHom a x) = σ.asAlgebraHom a (e x) := by
20   induction a using MonoidAlgebra.induction_on with
21   | of g => simpa using Representation.IntertwiningMap.isIntertwining ρ σ e.toIntertwiningMap g x
22   | add a b ha hb => simp [ha, hb]
23   | smul c a ha => simp [ha]
24 
25 /-- The character element is nonzero. -/
26 theorem nonzero (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ] :
27     element ρ ≠ 0 := by
28   have := nontrivial_space ρ
29   intro h
30   have he : Nonempty (Representation.Equiv ρ ρ) := ⟨Representation.Equiv.refl ρ⟩
31   have hi := irreducible_action ρ ρ
32   simp [h, he] at hi
33 
34 /-- Idempotence is an equality in C[G], detected through all simple modules. -/
35 theorem idempotent (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ] :
36     element ρ * element ρ = element ρ := by
37   apply eq_of_irreducible_actions
38   intro W _ _ _ σ _
39   rw [map_mul, irreducible_action ρ σ]
40   split_ifs <;> simp
41 
42 /-- The target irreducible detects every element supported on its central block. -/
43 theorem supported_eq_zero (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
44     (a : MonoidAlgebra ℂ G) (hs : a * element ρ = a)
45     (ha : ρ.asAlgebraHom a = 0) : a = 0 := by
46   apply eq_zero_of_irreducible_actions
47   intro W _ _ _ σ _
48   by_cases he : Nonempty (Representation.Equiv ρ σ)
49   · let e := Classical.choice he
50     ext y
51     obtain ⟨x, rfl⟩ := e.toLinearEquiv.surjective y
52     change σ.asAlgebraHom a (e x) = 0
53     rw [← equiv_algebra_action ρ σ e a x, ha]
54     simp
55   · calc
56       σ.asAlgebraHom a = σ.asAlgebraHom (a * element ρ) := congrArg σ.asAlgebraHom hs.symm
57       _ = 0 := by simp [irreducible_action ρ σ, he]
58 
59 /-- Faithfulness on the designated block, not on the whole group algebra. -/
60 theorem block_action_injective (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
61     (a b : MonoidAlgebra ℂ G) (ha : a * element ρ = a) (hb : b * element ρ = b)
62     (hab : ρ.asAlgebraHom a = ρ.asAlgebraHom b) : a = b := by
63   apply sub_eq_zero.mp
64   apply supported_eq_zero ρ (a - b)
65   · simp [sub_mul, ha, hb]
66   · simp [hab]
67 
68 /-- The standard central-primitive condition, stated directly. -/
69 def IsPrimitiveCentral {A : Type*} [Ring A] (e : A) : Prop :=
70   e ≠ 0 ∧ e * e = e ∧ e ∈ Submonoid.center A ∧
71     ∀ p : A, p ∈ Submonoid.center A → p * p = p → p * e = p → p = 0 ∨ p = e
72 
73 /-- Proposition 4.2 for every finite group and irreducible complex representation. -/
74 theorem primitive_central (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ] :
75     IsPrimitiveCentral (element ρ) := by
76   refine ⟨nonzero ρ, idempotent ρ, central ρ, ?_⟩
77   intro p hp hpp hpe
78   have := nontrivial_space ρ
79   obtain ⟨c, hc⟩ := central_scalar ρ hp
80   have hmul := congrArg ρ.asAlgebraHom hpp
81   rw [map_mul, hc] at hmul
82   have hcc : c * c = c := by
83     apply smul_left_injective ℂ (one_ne_zero : (1 : Module.End ℂ V) ≠ 0)
84     simpa only [smul_mul_assoc, mul_smul_comm, one_mul, smul_smul] using hmul
85   have hz : c * (c - 1) = 0 := by
86     calc
87       c * (c - 1) = c * c - c := by ring
88       _ = 0 := by rw [hcc, sub_self]
89   rcases mul_eq_zero.mp hz with hc0 | hc1
90   · left
91     exact supported_eq_zero ρ p hpe (by simp [hc, hc0])
92   · right
93     have hc1' : c = 1 := sub_eq_zero.mp hc1
94     apply block_action_injective ρ p (element ρ) hpe (idempotent ρ)
95     have he : Nonempty (Representation.Equiv ρ ρ) := ⟨Representation.Equiv.refl ρ⟩
96     simp [hc, hc1', irreducible_action ρ ρ, he]
97 
98 /-- A decomposition into orthogonal central sub-idempotents has a zero summand. -/
99 theorem no_nontrivial_central_split (ρ : Representation ℂ G V)
100     [Representation.IsIrreducible ρ] (p q : MonoidAlgebra ℂ G)
101     (hp : p ∈ Submonoid.center (MonoidAlgebra ℂ G))
102     (hpp : p * p = p) (hpq : p * q = 0) (hs : p + q = element ρ) :
103     p = 0 ∨ q = 0 := by
104   have hpe : p * element ρ = p := by rw [← hs, mul_add, hpp, hpq, add_zero]
105   rcases (primitive_central ρ).2.2.2 p hp hpp hpe with hz | he
106   · exact Or.inl hz
107   · right
108     have hq : element ρ + q = element ρ + 0 := by simpa [he] using hs
109     exact add_left_cancel hq
110 
111 /-- Nonisomorphic irreducible characters give orthogonal central idempotents. -/
112 theorem orthogonal [FiniteDimensional ℂ W]
113     (ρ : Representation ℂ G V) (σ : Representation ℂ G W)
114     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ]
115     (h : ¬Nonempty (Representation.Equiv ρ σ)) :
116     element ρ * element σ = 0 := by
117   apply supported_eq_zero σ
118   · rw [mul_assoc, idempotent σ]
119   · simp [irreducible_action ρ σ, h]
120 
121 omit [FiniteDimensional ℂ V] in
122 /-- An isomorphic presentation does not change the literal character element. -/
123 theorem presentation_invariant
124     (ρ : Representation ℂ G V) (σ : Representation ℂ G W)
125     (e : Representation.Equiv ρ σ) : element ρ = element σ := by
126   simp only [element, e.toLinearEquiv.finrank_eq, Representation.char_iso e]
127 
128 end PaperXI.PrimitiveCharacterBlock

Back to source controls