HeisenbergSelector.lean

1 import PaperXI.FiniteAverage
2 import PaperXI.SchrodingerTrace
3 import PaperXI.HeisenbergCardinality
4 import PaperXI.HeisenbergProjector
5 
6 /-! Trace and rank of the literal maximal isotropic averaging projector. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.HeisenbergSelector
10 open scoped Classical
11 
12 variable {G V : Type*} [Group G] [Fintype G]
13   [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
14 
15 omit [FiniteDimensional ℂ V] in
16 /-- The trace of a finite group average is the average of the traces. -/
17 theorem trace_average (ρ : Representation ℂ G V) :
18     LinearMap.trace ℂ V (FiniteAverage.average ρ) =
19       (Fintype.card G : ℂ)⁻¹ * ∑ g : G, LinearMap.trace ℂ V (ρ g) := by
20   simp [FiniteAverage.average]
21 
22 /-- The rank equals the trace because the actual average is an idempotent. -/
23 theorem rank_average (ρ : Representation ℂ G V) :
24     (Module.finrank ℂ (LinearMap.range (FiniteAverage.average ρ)) : ℂ) =
25       LinearMap.trace ℂ V (FiniteAverage.average ρ) := by
26   have hid : IsIdempotentElem (FiniteAverage.average ρ) := FiniteAverage.idempotent ρ
27   exact (LinearMap.IsIdempotentElem.isProj_range _ hid).trace.symm
28 
29 /-- Trace one gives a genuine one-dimensional invariant subspace. -/
30 theorem invariants_rank_one_of_trace_one (ρ : Representation ℂ G V)
31     (htrace : LinearMap.trace ℂ V (FiniteAverage.average ρ) = 1) :
32     Module.finrank ℂ ρ.invariants = 1 := by
33   have h := rank_average ρ
34   rw [FiniteAverage.range_eq, htrace] at h
35   exact_mod_cast h
36 
37 section Isotropic
38 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]
39 open HeisenbergProjector HeisenbergGeometry HeisenbergForm
40 
41 /-- A zero vector in a subspace is exactly the identity after multiplicative tagging. -/
42 theorem coordinates_zero_iff (L : Submodule K (X × Module.Dual K X))
43     (a : Multiplicative L) :
44     ((a.toAdd : X × Module.Dual K X).1 = 0 ∧
45       (a.toAdd : X × Module.Dual K X).2 = 0) ↔ a = 1 := by
46   constructor
47   · intro h
48     have ha : a.toAdd = 0 := Subtype.ext (Prod.ext h.1 h.2)
49     exact congrArg Multiplicative.ofAdd ha
50   · intro h
51     subst a
52     simp
53 
54 variable [Fintype X]
55 
56 /-- A zero-central lift has nonzero trace only at its identity. -/
57 theorem trace_restriction {ψ : AddChar K ℂ} (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
58     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L)
59     (a : Multiplicative L) :
60     LinearMap.trace ℂ (X → ℂ) (restriction ψ h2 L hL a) =
61       if a = 1 then (Fintype.card X : ℂ) else 0 := by
62   rw [restriction_apply, SchrodingerTrace.character_support hψ]
63   simp only [coordinates_zero_iff, AddChar.map_zero_eq_one, mul_one]
64 
65 /-- The actual isotropic projector has trace equal to the cardinality ratio. -/
66 theorem trace_projector {ψ : AddChar K ℂ} (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
67     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) [Fintype L] :
68     LinearMap.trace ℂ (X → ℂ) (projector ψ h2 L hL) =
69       (Fintype.card L : ℂ)⁻¹ * Fintype.card X := by
70   rw [projector, trace_average (G := Multiplicative L) (V := X → ℂ)]
71   simp only [trace_restriction hψ, Fintype.card_multiplicative]
72   simp
73 
74 variable [FiniteDimensional K X]
75 
76 /-- Maximality supplies the denominator, so the actual projector has trace one. -/
77 theorem maximal_trace_one {ψ : AddChar K ℂ} (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
78     (L : Submodule K (X × Module.Dual K X)) (hL : IsMaximalIsotropic form L)
79     [Fintype L] : LinearMap.trace ℂ (X → ℂ) (projector ψ h2 L hL.1) = 1 := by
80   rw [trace_projector hψ]
81   have hcard : Fintype.card L = Fintype.card X := by
82     simpa only [Nat.card_eq_fintype_card] using HeisenbergCardinality.natCard_eq L hL
83   rw [hcard]
84   exact inv_mul_cancel₀ (by exact_mod_cast Fintype.card_ne_zero (α := X))
85 
86 /-- Every maximal isotropic subgroup selects an actual one-dimensional range
87 in the Schrödinger model. -/
88 theorem maximal_rank_one {ψ : AddChar K ℂ} (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
89     (L : Submodule K (X × Module.Dual K X)) (hL : IsMaximalIsotropic form L)
90     [Fintype L] :
91     Module.finrank ℂ (LinearMap.range (projector ψ h2 L hL.1)) = 1 := by
92   have h := rank_average (G := Multiplicative L) (V := X → ℂ) (restriction ψ h2 L hL.1)
93   change (Module.finrank ℂ (LinearMap.range (projector ψ h2 L hL.1)) : ℂ) = _ at h
94   rw [show FiniteAverage.average (G := Multiplicative L) (V := X → ℂ)
95       (restriction ψ h2 L hL.1) =
96     projector ψ h2 L hL.1 from rfl, maximal_trace_one hψ h2 L hL] at h
97   exact_mod_cast h
98 
99 /-- The common fixed subspace of any maximal isotropic zero-central lift is a line. -/
100 theorem maximal_fixed_line {ψ : AddChar K ℂ} (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
101     (L : Submodule K (X × Module.Dual K X)) (hL : IsMaximalIsotropic form L)
102     [Fintype L] : Module.finrank ℂ
103       (Representation.invariants (G := Multiplicative L) (restriction ψ h2 L hL.1)) = 1 := by
104   rw [← range_eq_invariants]
105   exact maximal_rank_one hψ h2 L hL
106 
107 end Isotropic
108 
109 end PaperXI.HeisenbergSelector

Back to source controls