SymplecticHeisenbergUniqueness.lean

1 import PaperXI.SymplecticCentralExtension
2 import PaperXI.CentralExtensionExistence
3 import Mathlib.Algebra.Group.TypeTags.Finite
4 
5 /-! Finite Stone–von Neumann from an actual field-valued nondegenerate
6 commutator and a nontrivial additive character. This applies to supplied actual
7 central extensions in every characteristic, without assuming scalar
8 nondegeneracy, target dimensions, or a first intertwiner. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.SymplecticHeisenbergUniqueness
12 
13 open CentralExtension SymplecticCentralExtension
14 variable {K V H W U : Type*} [Field K] [AddCommGroup V] [Module K V] [Group H]
15 variable [AddCommGroup W] [Module ℂ W] [AddCommGroup U] [Module ℂ U]
16 
17 omit [Module K V] in
18 /-- The stated additive central action is the actual unit-valued character action. -/
19 theorem central_action (D : Datum (Multiplicative K) H (Multiplicative V))
20     (ψ : AddChar K ℂ) (σ : Representation ℂ H W)
21     (hσ : ∀ t : K, σ (D.i (Multiplicative.ofAdd t)) = ψ t • LinearMap.id)
22     (z : Multiplicative K) :
23     σ (D.i z) = (scalarCharacter ψ z : ℂ) • LinearMap.id := hσ z.toAdd
24 
25 variable [Fintype V]
26 variable (D : Datum (Multiplicative K) H (Multiplicative V))
27 variable (b : LinearMap.BilinForm K V) (hb : b.SeparatingLeft)
28 variable (hcomm : ∀ h k : H, centralCommutator D h k =
29   Multiplicative.ofAdd (b (D.q h).toAdd (D.q k).toAdd))
30 variable (ψ : AddChar K ℂ) (hψ : ψ ≠ 1)
31 include D b hb hcomm ψ hψ
32 
33 /-- Finite dimensionality follows for every actual irreducible representation
34 with the prescribed nontrivial central character. -/
35 theorem finiteDimensional (σ : Representation ℂ H W) [Representation.IsIrreducible σ]
36     (hσ : ∀ t : K, σ (D.i (Multiplicative.ofAdd t)) = ψ t • LinearMap.id) :
37     FiniteDimensional ℂ W :=
38   CentralExtensionUniqueness.finiteDimensional D (scalarCharacter ψ)
39     (radical_eq_bot_scalarCharacter D b hb hcomm ψ hψ) σ (central_action D ψ σ hσ)
40 
41 /-- The dimension is the square root of the actual symplectic quotient order. -/
42 theorem finrank_sqrt (σ : Representation ℂ H W) [Representation.IsIrreducible σ]
43     (hσ : ∀ t : K, σ (D.i (Multiplicative.ofAdd t)) = ψ t • LinearMap.id) :
44     Module.finrank ℂ W = Nat.sqrt (Fintype.card V) := by
45   simpa only [Fintype.card_multiplicative] using
46     CentralExtensionUniqueness.finrank_sqrt D (scalarCharacter ψ)
47       (radical_eq_bot_scalarCharacter D b hb hcomm ψ hψ) σ (central_action D ψ σ hσ)
48 
49 /-- The first equivalence between any two such irreducibles is constructed.
50 Neither finite dimensionality nor an initial equivalence is assumed. -/
51 theorem exists_equiv (σ : Representation ℂ H W) (τ : Representation ℂ H U)
52     [Representation.IsIrreducible σ] [Representation.IsIrreducible τ]
53     (hσ : ∀ t : K, σ (D.i (Multiplicative.ofAdd t)) = ψ t • LinearMap.id)
54     (hτ : ∀ t : K, τ (D.i (Multiplicative.ofAdd t)) = ψ t • LinearMap.id) :
55     Nonempty (Representation.Equiv σ τ) :=
56   CentralExtensionUniqueness.exists_equiv D (scalarCharacter ψ)
57     (radical_eq_bot_scalarCharacter D b hb hcomm ψ hψ) σ τ
58     (central_action D ψ σ hσ) (central_action D ψ τ hτ)
59 
60 /-- The actual quotient order is a square, derived from the constructed algebra. -/
61 theorem card_eq_square : ∃ n : ℕ, 0 < n ∧ Fintype.card V = n ^ 2 := by
62   obtain ⟨n, hn, hcard⟩ := TwistedMatrix.order_square
63     (scalarCocycle D (scalarCharacter ψ)) (normalized_scalarCocycle D (scalarCharacter ψ))
64     (radical_eq_bot_scalarCharacter D b hb hcomm ψ hψ)
65   exact ⟨n, hn, by simpa only [Fintype.card_multiplicative] using hcard⟩
66 
67 /-- An actual irreducible representation exists on an actual simple ideal of
68 the constructed twisted algebra, with the source central character and dimension. -/
69 theorem exists_irreducible :
70     let B : Type _ := CentralCharacter.Algebra D (scalarCharacter ψ)
71     letI : Ring B := inferInstance
72     letI : Algebra ℂ B := inferInstance
73     ∃ I : Ideal B, ∃ σ : Representation ℂ H I,
74       Representation.IsIrreducible σ ∧
75       (∀ t : K, σ (D.i (Multiplicative.ofAdd t)) = ψ t •
76         (LinearMap.id : Module.End ℂ I)) ∧
77       Module.finrank ℂ I = Nat.sqrt (Fintype.card V) := by
78   obtain ⟨I, σ, hI, hc, hd⟩ := CentralExtensionExistence.exists_irreducible D
79     (scalarCharacter ψ) (radical_eq_bot_scalarCharacter D b hb hcomm ψ hψ)
80   refine ⟨I, σ, hI, ?_, ?_⟩
81   · intro t
82     exact hc (Multiplicative.ofAdd t)
83   · simpa only [Fintype.card_multiplicative] using hd
84 
85 end PaperXI.SymplecticHeisenbergUniqueness

Back to source controls