BilinearHeisenberg.lean

1 import PaperXI.SymplecticHeisenbergUniqueness
2 import Mathlib.Tactic.Ring
3 
4 /-! Actual finite central extensions from bilinear factor sets.  The extension,
5 commutator, central character and Stone--von Neumann endpoint are distinct data.
6 No multiplication law, irrep, dimension or initial intertwiner is assumed. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.BilinearHeisenberg
10 
11 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
12 
13 @[ext] structure Element (c : LinearMap.BilinForm K V) where
14   vector : V
15   central : K
16 
17 variable (c : LinearMap.BilinForm K V)
18 
19 instance instMul : Mul (Element c) :=
20   ⟨fun h k => ⟨h.vector + k.vector, h.central + k.central + c h.vector k.vector⟩⟩
21 instance instOne : One (Element c) := ⟨⟨0, 0⟩⟩
22 instance instInv : Inv (Element c) :=
23   ⟨fun h => ⟨-h.vector, -h.central + c h.vector h.vector⟩⟩
24 
25 @[simp] theorem mul_vector (h k : Element c) :
26     (h * k).vector = h.vector + k.vector := rfl
27 @[simp] theorem mul_central (h k : Element c) :
28     (h * k).central = h.central + k.central + c h.vector k.vector := rfl
29 @[simp] theorem one_vector : (1 : Element c).vector = 0 := rfl
30 @[simp] theorem one_central : (1 : Element c).central = 0 := rfl
31 @[simp] theorem inv_vector (h : Element c) : h⁻¹.vector = -h.vector := rfl
32 @[simp] theorem inv_central (h : Element c) :
33     h⁻¹.central = -h.central + c h.vector h.vector := rfl
34 
35 instance instGroup : Group (Element c) where
36   mul_assoc h k l := by
37     ext <;> simp only [mul_vector, mul_central, map_add, LinearMap.add_apply]
38     · abel
39     · ring
40   one_mul h := by ext <;> simp
41   mul_one h := by ext <;> simp
42   inv_mul_cancel h := by ext <;> simp
43 
44 def i : Multiplicative K →* Element c where
45   toFun z := ⟨0, z.toAdd⟩
46   map_one' := rfl
47   map_mul' z w := by ext <;> simp
48 
49 def q : Element c →* Multiplicative V where
50   toFun h := Multiplicative.ofAdd h.vector
51   map_one' := rfl
52   map_mul' _ _ := rfl
53 
54 @[simp] theorem i_vector (z : Multiplicative K) : (i c z).vector = 0 := rfl
55 @[simp] theorem i_central (z : Multiplicative K) : (i c z).central = z.toAdd := rfl
56 @[simp] theorem q_apply (h : Element c) : (q c h).toAdd = h.vector := rfl
57 
58 /-- This is the actual short exact central extension of the additive space. -/
59 def datum : CentralExtension.Datum (Multiplicative K) (Element c) (Multiplicative V) where
60   i := i c
61   q := q c
62   i_injective := by
63     intro z w h
64     exact congrArg Multiplicative.ofAdd (congrArg Element.central h)
65   q_surjective := fun v => ⟨⟨v.toAdd, 0⟩, rfl⟩
66   range_i_eq_ker_q := by
67     ext h
68     constructor
69     · rintro ⟨z, rfl⟩
70       rfl
71     · intro hq
72       have hv : h.vector = 0 := congrArg Multiplicative.toAdd hq
73       exact ⟨Multiplicative.ofAdd h.central, by ext <;> simp [hv]⟩
74   central z h := by
75     ext <;> simp [add_comm]
76 
77 /-- The commutator is calculated from multiplication, not postulated. -/
78 theorem commutator (h k : Element c) :
79     h * k * h⁻¹ * k⁻¹ = i c (Multiplicative.ofAdd
80       (c h.vector k.vector - c k.vector h.vector)) := by
81   ext <;> simp only [mul_vector, mul_central, inv_vector, inv_central, i_vector,
82     i_central, map_add, map_neg, LinearMap.add_apply,
83     LinearMap.neg_apply]
84   · abel
85   · change _ = c h.vector k.vector - c k.vector h.vector
86     ring
87 
88 theorem centralCommutator (h k : Element c) :
89     CentralExtension.centralCommutator (datum c) h k =
90       Multiplicative.ofAdd (c h.vector k.vector - c k.vector h.vector) := by
91   apply (datum c).i_injective
92   rw [CentralExtension.i_centralCommutator]
93   exact commutator c h k
94 
95 /-- Finiteness is derived from the actual underlying coordinates. -/
96 instance instFinite [Finite K] [Finite V] : Finite (Element c) :=
97   Finite.of_injective (fun h : Element c => (h.vector, h.central))
98     (fun _ _ h => Element.ext (congrArg Prod.fst h) (congrArg Prod.snd h))
99 
100 theorem order : Nat.card (Element c) = Nat.card K * Nat.card V := by
101   have h := CentralExtension.natCard_eq (datum c)
102   change Nat.card (Element c) = Nat.card K * Nat.card V at h
103   exact h
104 
105 variable (b : LinearMap.BilinForm K V)
106 variable (hc : ∀ x y, c x y - c y x = b x y)
107 
108 include hc in
109 theorem source_commutator (h k : Element c) :
110     CentralExtension.centralCommutator (datum c) h k =
111       Multiplicative.ofAdd (b ((datum c).q h).toAdd ((datum c).q k).toAdd) := by
112   rw [centralCommutator, hc]
113   rfl
114 
115 variable [Fintype V] (hb : b.SeparatingLeft)
116 variable (ψ : AddChar K ℂ) (hψ : ψ ≠ 1)
117 include b hc hb hψ
118 
119 /-- Existence on an actual simple ideal, with dimension derived by finite
120 Stone--von Neumann.  Only the form and factor set are supplied. -/
121 theorem exists_irreducible :
122     let B : Type _ := CentralCharacter.Algebra (datum c) (SymplecticCentralExtension.scalarCharacter ψ)
123     letI : Ring B := inferInstance
124     letI : Algebra ℂ B := inferInstance
125     ∃ I : Ideal B, ∃ σ : Representation ℂ (Element c) I,
126       Representation.IsIrreducible σ ∧
127       (∀ t : K, σ (i c (Multiplicative.ofAdd t)) = ψ t •
128         (LinearMap.id : Module.End ℂ I)) ∧
129       Module.finrank ℂ I = Nat.sqrt (Fintype.card V) :=
130   SymplecticHeisenbergUniqueness.exists_irreducible
131     (datum c) b hb (source_commutator c b hc) ψ hψ
132 
133 variable {W U : Type*} [AddCommGroup W] [Module ℂ W] [AddCommGroup U] [Module ℂ U]
134 
135 /-- Uniqueness compares representations of the same specified middle group. -/
136 theorem exists_equiv (σ : Representation ℂ (Element c) W)
137     (τ : Representation ℂ (Element c) U)
138     [Representation.IsIrreducible σ] [Representation.IsIrreducible τ]
139     (hσ : ∀ t : K, σ (i c (Multiplicative.ofAdd t)) = ψ t • LinearMap.id)
140     (hτ : ∀ t : K, τ (i c (Multiplicative.ofAdd t)) = ψ t • LinearMap.id) :
141     Nonempty (Representation.Equiv σ τ) :=
142   SymplecticHeisenbergUniqueness.exists_equiv
143     (datum c) b hb (source_commutator c b hc) ψ hψ σ τ hσ hτ
144 
145 theorem finrank_sqrt (σ : Representation ℂ (Element c) W)
146     [Representation.IsIrreducible σ]
147     (hσ : ∀ t : K, σ (i c (Multiplicative.ofAdd t)) = ψ t • LinearMap.id) :
148     Module.finrank ℂ W = Nat.sqrt (Fintype.card V) :=
149   SymplecticHeisenbergUniqueness.finrank_sqrt
150     (datum c) b hb (source_commutator c b hc) ψ hψ σ hσ
151 
152 end PaperXI.BilinearHeisenberg

Back to source controls