CharacterProjector.lean

1 import Mathlib.RepresentationTheory.Character
2 import Mathlib.Analysis.Complex.Polynomial.Basic
3 
4 /-! The literal character element of a finite complex group algebra.
5 Centrality and scalar action are proved from character orthogonality. -/
6 set_option autoImplicit false
7 noncomputable section
8 open scoped BigOperators MonoidAlgebra Classical
9 namespace PaperXI.CharacterProjector
10 variable {G V W : Type*} [Group G] [Fintype G]
11 variable [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
12 variable [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
13 
14 /-- The character sum, with the actual inverse and degree normalization. -/
15 def element (ρ : Representation ℂ G V) : MonoidAlgebra ℂ G :=
16   ((Module.finrank ℂ V : ℂ) / Fintype.card G) •
17     ∑ g : G, MonoidAlgebra.single g (ρ.character g⁻¹)
18 
19 omit [FiniteDimensional ℂ V] in
20 @[simp] theorem coeff_element (ρ : Representation ℂ G V) (g : G) :
21     (element ρ).coeff g =
22       ((Module.finrank ℂ V : ℂ) / Fintype.card G) * ρ.character g⁻¹ := by
23   simp [element, MonoidAlgebra.coeff_sum, Finsupp.single_apply]
24 
25 omit [FiniteDimensional ℂ V] in
26 theorem central (ρ : Representation ℂ G V) :
27     element ρ ∈ Submonoid.center (MonoidAlgebra ℂ G) := by
28   rw [Submonoid.mem_center_iff]
29   intro a
30   induction a using MonoidAlgebra.induction_on with
31   | of h =>
32     ext g
33     simp only [MonoidAlgebra.of_apply, MonoidAlgebra.coeff_single_mul_apply,
34       MonoidAlgebra.coeff_mul_single_apply, one_mul, mul_one, coeff_element, mul_inv_rev,
35       inv_inv]
36     rw [ρ.char_mul_comm]
37   | add a b ha hb => simp only [add_mul, mul_add, ha, hb]
38   | smul c a ha => simp only [smul_mul_assoc, mul_smul_comm, ha]
39 
40 omit [FiniteDimensional ℂ V] [FiniteDimensional ℂ W] in
41 /-- Expanded action of the literal group-algebra element. -/
42 theorem action (ρ : Representation ℂ G V) (σ : Representation ℂ G W) :
43     σ.asAlgebraHom (element ρ) =
44       ((Module.finrank ℂ V : ℂ) / Fintype.card G) •
45         ∑ g : G, ρ.character g⁻¹ • σ g := by
46   simp [element]
47 
48 omit [Fintype G] in
49 /-- Every central element acts scalarly on an irreducible complex representation. -/
50 theorem central_scalar (σ : Representation ℂ G W) [Representation.IsIrreducible σ]
51     {a : MonoidAlgebra ℂ G} (ha : a ∈ Submonoid.center (MonoidAlgebra ℂ G)) :
52     ∃ c : ℂ, σ.asAlgebraHom a = c • (1 : Module.End ℂ W) := by
53   obtain ⟨c, hc⟩ := (Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed
54     (ρ := σ)).surjective (Representation.IntertwiningMap.centralAlgebraMul σ ha)
55   exact ⟨c, (congrArg Representation.IntertwiningMap.toLinearMap hc).symm⟩
56 
57 omit [Fintype G] [FiniteDimensional ℂ V] in
58 theorem nontrivial_space (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ] :
59     Nontrivial V := by
60   by_contra h
61   have : Subsingleton V := not_nontrivial_iff_subsingleton.mp h
62   exact bot_ne_top (Subrepresentation.toSubmodule_injective
63     (Subsingleton.elim (⊥ : Subrepresentation ρ).toSubmodule ⊤))
64 
65 omit [Fintype G] in
66 theorem degree_ne_zero (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ] :
67     (Module.finrank ℂ V : ℂ) ≠ 0 := by
68   have := nontrivial_space ρ
69   exact_mod_cast (Module.finrank_pos (R := ℂ) (M := V)).ne'
70 
71 /-- Selection of the designated irreducible isomorphism class. -/
72 theorem irreducible_action (ρ : Representation ℂ G V) (σ : Representation ℂ G W)
73     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ] :
74     σ.asAlgebraHom (element ρ) =
75       if Nonempty (Representation.Equiv ρ σ) then 1 else 0 := by
76   have hcard : (Nat.card G : ℂ) ≠ 0 := by exact_mod_cast (Nat.card_pos (α := G)).ne'
77   let : Invertible (Nat.card G : ℂ) := invertibleOfNonzero hcard
78   obtain ⟨c, hc⟩ := central_scalar σ (central ρ)
79   have ht := congrArg (LinearMap.trace ℂ W) hc
80   rw [action ρ σ] at ht
81   simp only [map_smul, map_sum, smul_eq_mul, LinearMap.trace_one] at ht
82   change (Module.finrank ℂ V : ℂ) / Fintype.card G *
83     (∑ g : G, ρ.character g⁻¹ * σ.character g) = c * Module.finrank ℂ W at ht
84   have ho := Representation.char_orthonormal σ ρ
85   rw [Fintype.card_eq_nat_card, div_eq_mul_inv, mul_assoc] at ht
86   simp_rw [mul_comm (ρ.character _)] at ht
87   rw [ho] at ht
88   by_cases he : Nonempty (Representation.Equiv ρ σ)
89   · let e := Classical.choice he
90     have hd := e.toLinearEquiv.finrank_eq
91     have hc1 : c = 1 := by
92       simp only [ite_eq_left he, mul_one] at ht
93       rw [hd] at ht
94       exact (mul_right_cancel₀ (degree_ne_zero σ)) (by simpa using ht.symm)
95     simp [he, hc, hc1]
96   · have hc0 : c = 0 := by
97       simpa [he, degree_ne_zero σ] using ht.symm
98     simp [he, hc, hc0]
99 
100 end PaperXI.CharacterProjector

Back to source controls