PacketTrace.lean

1 import Mathlib.LinearAlgebra.Trace
2 import Mathlib.LinearAlgebra.Dimension.LinearMap
3 
4 set_option autoImplicit false
5 
6 /-! Paper XII, Corollary 8.4. The projector is the actual action of a supplied
7 idempotent of the Hecke algebra, and the packet is its actual image submodule.
8 This block does not construct the canonical Artin idempotents (Fact 8.1), nor
9 prove the localization/direct-sum comparisons in Theorem 8.2. Its conclusions
10 apply to every supplied idempotent, in particular to those canonical inputs.
11 No semisimplicity or faithful action is assumed. -/
12 namespace PaperXII.PacketTrace
13 
14 variable {E T V : Type*} [Field E] [CommRing T] [Algebra E T]
15     [AddCommGroup V] [Module E V] [Module T V] [IsScalarTower E T V]
16 
17 /-- The actual E-linear action of the Hecke element. -/
18 def projector (e : T) : V →ₗ[E] V := Algebra.lsmul E E V e
19 
20 /-- The packet eV, as a submodule of the original representation space. -/
21 def packet (e : T) : Submodule E V := LinearMap.range (projector (V := V) e)
22 
23 theorem projector_apply (e : T) (v : V) : projector (E := E) e v = e • v := rfl
24 
25 theorem projector_idempotent {e : T} (he : IsIdempotentElem e) :
26     IsIdempotentElem (projector (E := E) (V := V) e) := by
27   change projector e * projector e = projector e
28   ext v
29   change e • (e • v) = e • v
30   rw [← mul_smul, he]
31 
32 theorem mem_packet_iff (e : T) (v : V) :
33     v ∈ packet (E := E) e ↔ ∃ w : V, e • w = v := Iff.rfl
34 
35 /-- An element lies in eV exactly when e fixes it. -/
36 theorem mem_packet_iff_fixed {e : T} (he : IsIdempotentElem e) (v : V) :
37     v ∈ packet (E := E) e ↔ e • v = v := by
38   rw [mem_packet_iff]
39   constructor
40   · rintro ⟨w, rfl⟩
41     rw [← mul_smul, he]
42   · intro hv
43     exact ⟨v, hv⟩
44 
45 variable [FiniteDimensional E V]
46 
47 /-- Operator rank is the natural image dimension, with its cardinal cast. -/
48 theorem rank_eq_dimension (e : T) :
49     LinearMap.rank (projector (E := E) (V := V) e) =
50       (Module.finrank E (packet (E := E) (V := V) e) : Cardinal) := by
51   exact (Module.finrank_eq_rank (R := E) (M := packet (E := E) (V := V) e)).symm
52 
53 /-- The trace formula includes the necessary cast from natural dimension to E.
54 The equality itself holds in every characteristic. -/
55 theorem trace_eq_cast_finrank {e : T} (he : IsIdempotentElem e) :
56     LinearMap.trace E V (projector e) =
57       (Module.finrank E (packet (E := E) (V := V) e) : E) := by
58   exact ((LinearMap.isProj_range_iff_isIdempotentElem _).mpr
59     (projector_idempotent (E := E) (V := V) he)).trace
60 
61 /-- Occupancy means a nonzero image, and rank positivity is a statement in N. -/
62 theorem occupied_iff_positive_rank (e : T) :
63     packet (E := E) (V := V) e ≠ ⊥ ↔
64       0 < Module.finrank E (packet (E := E) (V := V) e) := by
65   rw [Module.finrank_pos_iff, Submodule.nontrivial_iff_ne_bot]
66 
67 /-- Characteristic zero is needed only for nonzero scalar trace detection. -/
68 theorem occupied_iff_trace_ne_zero [CharZero E] {e : T} (he : IsIdempotentElem e) :
69     packet (E := E) (V := V) e ≠ ⊥ ↔
70       LinearMap.trace E V (projector e) ≠ 0 := by
71   rw [trace_eq_cast_finrank he, Nat.cast_ne_zero, occupied_iff_positive_rank,
72     Nat.pos_iff_ne_zero]
73 
74 end PaperXII.PacketTrace

Back to source controls