CuspidalAnnihilation.lean

1 import PaperXI.PrimitiveCharacterBlock
2 import PaperXI.FiniteAverage
3 
4 /-! Subgroup averages and annihilation of an actual central character block.
5 The cuspidal input is the vanishing of genuine restricted invariants. -/
6 set_option autoImplicit false
7 noncomputable section
8 open scoped MonoidAlgebra BigOperators Classical
9 namespace PaperXI.CuspidalAnnihilation
10 open PaperXI.CharacterProjector PaperXI.PrimitiveCharacterBlock
11 universe u v
12 variable {G : Type u} [Group G] [Fintype G]
13 variable {V : Type v} [AddCommGroup V] [Module ℂ V]
14 
15 /-- The normalized subgroup sum, viewed in the ambient group algebra. -/
16 def subgroupAverage (U : Subgroup G) : MonoidAlgebra ℂ G :=
17   (Fintype.card U : ℂ)⁻¹ • ∑ g : U, MonoidAlgebra.single (g : G) 1
18 
19 /-- The actual group-algebra action is the Reynolds average of the restricted action. -/
20 theorem average_action (ρ : Representation ℂ G V) (U : Subgroup G) :
21     ρ.asAlgebraHom (subgroupAverage U) = PaperXI.FiniteAverage.average (ρ.comp U.subtype) := by
22   simp [subgroupAverage, PaperXI.FiniteAverage.average]
23 
24 /-- The average has precisely the genuine U-fixed vectors as its range. -/
25 theorem average_range (ρ : Representation ℂ G V) (U : Subgroup G) :
26     LinearMap.range (ρ.asAlgebraHom (subgroupAverage U)) = Representation.invariants (ρ.comp U.subtype) := by
27   rw [average_action]
28   exact PaperXI.FiniteAverage.range_eq _
29 
30 /-- No invariant-vector assumption is needed to prove idempotence of the average. -/
31 theorem average_idempotent (U : Subgroup G) :
32     subgroupAverage U * subgroupAverage U = subgroupAverage U := by
33   apply PaperXI.SemisimpleDetection.eq_of_irreducible_actions
34   intro W _ _ _ σ _
35   rw [map_mul, average_action]
36   exact PaperXI.FiniteAverage.idempotent _
37 
38 theorem average_zero_iff (ρ : Representation ℂ G V) (U : Subgroup G) :
39     ρ.asAlgebraHom (subgroupAverage U) = 0 ↔ Representation.invariants (ρ.comp U.subtype) = ⊥ := by
40   rw [← average_range, LinearMap.range_eq_bot]
41 
42 variable [FiniteDimensional ℂ V]
43 
44 /-- A central character projector acts as the identity on its designated irreducible. -/
45 theorem own_block_action (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ] :
46     ρ.asAlgebraHom (element ρ) = 1 := by
47   have he : Nonempty (Representation.Equiv ρ ρ) := ⟨Representation.Equiv.refl ρ⟩
48   simp [irreducible_action ρ ρ, he]
49 
50 /-- A sharp criterion in the group algebra: annihilation is equivalent to no U-fixed vectors. -/
51 theorem left_annihilation_iff (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
52     (U : Subgroup G) :
53     subgroupAverage U * element ρ = 0 ↔ Representation.invariants (ρ.comp U.subtype) = ⊥ := by
54   constructor
55   · intro h
56     apply (average_zero_iff ρ U).mp
57     have hm := congrArg ρ.asAlgebraHom h
58     simpa [own_block_action ρ] using hm
59   · intro h
60     have hz := (average_zero_iff ρ U).mpr h
61     apply supported_eq_zero ρ
62     · rw [mul_assoc, idempotent ρ]
63     · simp [hz]
64 
65 /-- The opposite multiplication order has the same exact criterion. -/
66 theorem right_annihilation_iff (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
67     (U : Subgroup G) :
68     element ρ * subgroupAverage U = 0 ↔ Representation.invariants (ρ.comp U.subtype) = ⊥ := by
69   rw [← Submonoid.mem_center_iff.mp (central ρ) (subgroupAverage U)]
70   exact left_annihilation_iff ρ U
71 
72 /-- Proposition 4.3, specialized to any supplied unipotent radical whose invariants vanish. -/
73 theorem parabolic_annihilation (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
74     (U : Subgroup G) (hcuspidal : Representation.invariants (ρ.comp U.subtype) = ⊥) :
75     subgroupAverage U * element ρ = 0 ∧ element ρ * subgroupAverage U = 0 :=
76   ⟨(left_annihilation_iff ρ U).mpr hcuspidal, (right_annihilation_iff ρ U).mpr hcuspidal⟩
77 
78 /-- A nonzero fixed vector rules out annihilation; irreducibility alone is not cuspidality. -/
79 theorem nonzero_of_fixed_vector (ρ : Representation ℂ G V) [Representation.IsIrreducible ρ]
80     (U : Subgroup G) (v : V) (hv : v ≠ 0) (hfixed : v ∈ Representation.invariants (ρ.comp U.subtype)) :
81     subgroupAverage U * element ρ ≠ 0 := by
82   intro hz
83   have hbot := (left_annihilation_iff ρ U).mp hz
84   rw [hbot] at hfixed
85   exact hv hfixed
86 
87 end PaperXI.CuspidalAnnihilation

Back to source controls