SchrodingerConsequences.lean

1 import PaperXI.SchrodingerUniversal
2 import PaperXI.HeisenbergSelector
3 
4 /-! Character support and actual isotropic selectors in every irreducible
5 representation with the prescribed nontrivial central character. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.SchrodingerConsequences
9 open scoped Classical
10 open PaperXI.Heisenberg PaperXI.HeisenbergForm PaperXI.HeisenbergGeometry
11 variable {K X W : Type*} [Field K] [AddCommGroup X] [Module K X]
12 variable [AddCommGroup W] [Module ℂ W]
13 
14 /-- Restriction of the arbitrary representation to the actual zero-central lift. -/
15 def restriction (σ : Representation ℂ (Element K X) W)
16     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) :
17     Representation ℂ (Multiplicative L) W :=
18   σ.comp (HeisenbergProjector.liftHom L hL)
19 
20 /-- The literal isotropic averaging operator in the arbitrary target. -/
21 def projector (σ : Representation ℂ (Element K X) W)
22     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) [Fintype L] :
23     Module.End ℂ W := FiniteAverage.average (G := Multiplicative L) (restriction σ L hL)
24 
25 /-- These actual target averages are idempotent without any irreducibility assumption. -/
26 theorem projector_idempotent (σ : Representation ℂ (Element K X) W)
27     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) [Fintype L] :
28     (projector σ L hL).comp (projector σ L hL) = projector σ L hL := by
29   simpa only [projector] using
30     FiniteAverage.idempotent (G := Multiplicative L) (restriction σ L hL)
31 
32 /-- The range is the target's actual common fixed subspace. -/
33 theorem range_eq_invariants (σ : Representation ℂ (Element K X) W)
34     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) [Fintype L] :
35     LinearMap.range (projector σ L hL) =
36       Representation.invariants (G := Multiplicative L) (restriction σ L hL) := by
37   simpa only [projector] using
38     FiniteAverage.range_eq (G := Multiplicative L) (restriction σ L hL)
39 
40 /-- The same target average indexed by the actual embedded subgroup. -/
41 def subgroupProjector (σ : Representation ℂ (Element K X) W)
42     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) [Fintype L] :
43     Module.End ℂ W :=
44   FiniteAverage.average (σ.comp (HeisenbergProjector.liftedSubgroup L hL).subtype)
45 
46 /-- The additive-coordinate and actual-subgroup averages agree. -/
47 theorem projector_eq_subgroupProjector (σ : Representation ℂ (Element K X) W)
48     (L : Submodule K (X × Module.Dual K X)) (hL : IsIsotropic form L) [Fintype L] :
49     projector σ L hL = subgroupProjector σ L hL := by
50   ext w
51   simp only [projector, subgroupProjector, FiniteAverage.average_apply]
52   change (Fintype.card (Multiplicative L) : ℂ)⁻¹ •
53       ∑ a : Multiplicative L, σ (HeisenbergProjector.liftHom L hL a) w =
54     (Fintype.card (HeisenbergProjector.liftedSubgroup L hL) : ℂ)⁻¹ •
55       ∑ a : HeisenbergProjector.liftedSubgroup L hL, σ a.val w
56   rw [← Fintype.card_congr (HeisenbergProjector.liftEquiv L hL).toEquiv]
57   congr 1
58   exact Function.Bijective.sum_comp (HeisenbergProjector.liftEquiv L hL).bijective
59     (fun a : HeisenbergProjector.liftedSubgroup L hL => σ a.val w)
60 
61 variable [Fintype X] [Fintype (Module.Dual K X)] [FiniteDimensional K X]
62 variable (ψ : AddChar K ℂ) (hψ : ψ ≠ 1) (h2 : (2 : K) ≠ 0)
63 variable (σ : Representation ℂ (Element K X) W) [Representation.IsIrreducible σ]
64 variable (hcentral : ∀ z, σ (centralElement z) = ψ z • LinearMap.id)
65 include hψ h2 hcentral
66 
67 /-- The constructed equivalence conjugates each actual model operator to the target. -/
68 theorem conjugates (g : Element K X) :
69     (SchrodingerUniversal.equiv ψ hψ h2 σ hcentral).toLinearEquiv.conj
70       (representation ψ h2 g) = σ g := by
71   ext w
72   rw [LinearEquiv.conj_apply_apply]
73   let U := (SchrodingerUniversal.equiv ψ hψ h2 σ hcentral).toLinearEquiv
74   have h : U ((representation ψ h2 g) (U.symm w)) = σ g (U (U.symm w)) :=
75     SchrodingerUniversal.equiv_intertwines ψ hψ h2 σ hcentral g (U.symm w)
76   simpa only [LinearEquiv.apply_symm_apply] using h
77 
78 /-- Trace is preserved under the constructed equivalence, not postulated. -/
79 theorem trace_eq_model (g : Element K X) :
80     LinearMap.trace ℂ W (σ g) =
81       LinearMap.trace ℂ (X → ℂ) (representation ψ h2 g) := by
82   rw [← conjugates ψ hψ h2 σ hcentral g, LinearMap.trace_conj']
83 
84 /-- The irreducible target character is supported exactly on the center. -/
85 theorem character_support (g : Element K X) :
86     LinearMap.trace ℂ W (σ g) =
87       if g.position = 0 ∧ g.frequency = 0 then
88         (Fintype.card X : ℂ) * ψ g.central else 0 := by
89   rw [trace_eq_model ψ hψ h2 σ hcentral]
90   exact SchrodingerTrace.character_support hψ g.position g.frequency g.central
91 
92 /-- The equivalence transports the actual finite averaging operator. -/
93 theorem conjugates_projector (L : Submodule K (X × Module.Dual K X))
94     (hL : IsIsotropic form L) [Fintype L] :
95     (SchrodingerUniversal.equiv ψ hψ h2 σ hcentral).toLinearEquiv.conj
96       (HeisenbergProjector.projector ψ h2 L hL) = projector σ L hL := by
97   change (SchrodingerUniversal.equiv ψ hψ h2 σ hcentral).toLinearEquiv.conj
98       ((Fintype.card (Multiplicative L) : ℂ)⁻¹ •
99         ∑ a : Multiplicative L, representation ψ h2 (HeisenbergProjector.liftHom L hL a)) =
100     (Fintype.card (Multiplicative L) : ℂ)⁻¹ •
101       ∑ a : Multiplicative L, σ (HeisenbergProjector.liftHom L hL a)
102   rw [map_smul, map_sum]
103   simp_rw [conjugates ψ hψ h2 σ hcentral]
104 
105 /-- The target isotropic projector has the same exact cardinality-ratio trace. -/
106 theorem trace_projector (L : Submodule K (X × Module.Dual K X))
107     (hL : IsIsotropic form L) [Fintype L] :
108     LinearMap.trace ℂ W (projector σ L hL) =
109       (Fintype.card L : ℂ)⁻¹ * Fintype.card X := by
110   rw [← conjugates_projector ψ hψ h2 σ hcentral L hL, LinearMap.trace_conj']
111   exact HeisenbergSelector.trace_projector hψ h2 L hL
112 
113 /-- The dimension of every isotropic selector range is the cardinality ratio. -/
114 theorem rank_projector (L : Submodule K (X × Module.Dual K X))
115     (hL : IsIsotropic form L) [Fintype L] :
116     (Module.finrank ℂ (LinearMap.range (projector σ L hL)) : ℂ) =
117       (Fintype.card L : ℂ)⁻¹ * Fintype.card X := by
118   let : FiniteDimensional ℂ W := SchrodingerUniversal.finiteDimensional ψ hψ h2 σ hcentral
119   have h := HeisenbergSelector.rank_average (G := Multiplicative L) (V := W)
120     (restriction σ L hL)
121   exact h.trans (trace_projector ψ hψ h2 σ hcentral L hL)
122 
123 /-- Every maximal isotropic selector has trace one in the arbitrary target. -/
124 theorem maximal_trace_one (L : Submodule K (X × Module.Dual K X))
125     (hL : IsMaximalIsotropic form L) [Fintype L] :
126     LinearMap.trace ℂ W (projector σ L hL.1) = 1 := by
127   rw [← conjugates_projector ψ hψ h2 σ hcentral L hL.1, LinearMap.trace_conj']
128   exact HeisenbergSelector.maximal_trace_one hψ h2 L hL
129 
130 /-- A maximal isotropic average has a one-dimensional range in the target.
131 Target finite dimensionality is derived from Stone–von Neumann inside the proof. -/
132 theorem maximal_rank_one (L : Submodule K (X × Module.Dual K X))
133     (hL : IsMaximalIsotropic form L) [Fintype L] :
134     Module.finrank ℂ (LinearMap.range (projector σ L hL.1)) = 1 := by
135   let : FiniteDimensional ℂ W := SchrodingerUniversal.finiteDimensional ψ hψ h2 σ hcentral
136   have h := HeisenbergSelector.rank_average (G := Multiplicative L) (V := W)
137     (restriction σ L hL.1)
138   change (Module.finrank ℂ (LinearMap.range (projector σ L hL.1)) : ℂ) =
139     LinearMap.trace ℂ W (projector σ L hL.1) at h
140   rw [maximal_trace_one ψ hψ h2 σ hcentral L hL] at h
141   exact_mod_cast h
142 
143 /-- Every maximal isotropic zero-central lift fixes exactly a line in the target. -/
144 theorem maximal_fixed_line (L : Submodule K (X × Module.Dual K X))
145     (hL : IsMaximalIsotropic form L) [Fintype L] :
146     Module.finrank ℂ
147       (Representation.invariants (G := Multiplicative L) (restriction σ L hL.1)) = 1 := by
148   rw [← range_eq_invariants]
149   exact maximal_rank_one ψ hψ h2 σ hcentral L hL
150 
151 end PaperXI.SchrodingerConsequences

Back to source controls