HeisenbergTensorFactorization.lean

1 import PaperXI.HeisenbergTensor
2 import PaperXI.CentralProductCommutator
3 import PaperXI.TensorIrreducible
4 
5 /-! Finite Heisenberg tensor factorization for the actual central product.
6 All factor spaces are actual irreducible representation spaces. Their finite
7 dimensions and nontriviality are derived, including zero quotient factors and
8 the empty family. The descended tensor action is proved irreducible before
9 Stone--von Neumann uniqueness is used. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.HeisenbergTensor
13 open CentralExtension CocycleCommutator TensorProduct
14 open scoped Classical
15 
16 variable {S Z : Type*} [Fintype S] [CommGroup Z]
17 variable {H A V : S → Type*} [∀ s, Group (H s)] [∀ s, CommGroup (A s)]
18 variable [∀ s, Fintype (A s)] [∀ s, AddCommGroup (V s)] [∀ s, Module ℂ (V s)]
19 variable (D : ∀ s, Datum Z (H s) (A s)) (ζ : Z →* ℂˣ)
20 variable (hnd : ∀ s, radical (scalarCocycle (D s) ζ) = ⊥)
21 variable (σ : ∀ s, Representation ℂ (H s) (V s)) [∀ s, Representation.IsIrreducible (σ s)]
22 variable (hσ : ∀ s z, σ s ((D s).i z) = (ζ z : ℂ) • LinearMap.id)
23 include D ζ hnd σ hσ
24 
25 omit [Fintype S] in
26 /-- Each factor's finite dimensionality follows from its actual irreducible action. -/
27 theorem factor_finiteDimensional (s : S) : FiniteDimensional ℂ (V s) :=
28   CentralExtensionUniqueness.finiteDimensional (D s) ζ (hnd s) (σ s) (hσ s)
29 
30 /-- Thus the actual finite tensor product is finite-dimensional. -/
31 theorem finiteDimensional : FiniteDimensional ℂ (PiTensorProduct ℂ V) := by
32   let : ∀ s, FiniteDimensional ℂ (V s) := factor_finiteDimensional D ζ hnd σ hσ
33   infer_instance
34 
35 /-- The tensor product has the required nonzero space, also for an empty family. -/
36 theorem nontrivial : Nontrivial (PiTensorProduct ℂ V) := by
37   let : ∀ s, FiniteDimensional ℂ (V s) := factor_finiteDimensional D ζ hnd σ hσ
38   let : ∀ s, Nontrivial (V s) := fun s => GeneratedIrreducibility.nontrivial_space (σ s)
39   exact FiniteTensor.nontrivial
40 
41 /-- The actual tensor dimension squared equals the actual product quotient order. -/
42 theorem finrank_sq : Module.finrank ℂ (PiTensorProduct ℂ V) ^ 2 =
43     Fintype.card (∀ s, A s) := by
44   let : ∀ s, FiniteDimensional ℂ (V s) := factor_finiteDimensional D ζ hnd σ hσ
45   rw [FiniteTensor.finrank, ← Finset.prod_pow, Fintype.card_pi]
46   apply Finset.prod_congr rfl
47   intro s _
48   exact TensorIrreducible.finrank_sq_of_irreducible (D s) ζ (hnd s) (σ s) (hσ s)
49 
50 /-- Irreducibility of the literal quotient action on the actual finite tensor product. -/
51 theorem irreducible : Representation.IsIrreducible (descend D ζ σ hσ) := by
52   let : FiniteDimensional ℂ (PiTensorProduct ℂ V) := finiteDimensional D ζ hnd σ hσ
53   let : Nontrivial (PiTensorProduct ℂ V) := nontrivial D ζ hnd σ hσ
54   exact TensorIrreducible.irreducible (CentralProduct.datum D) ζ
55     (CentralProduct.radical_eq_bot D ζ hnd) (descend D ζ σ hσ)
56     (central D ζ σ hσ) (finrank_sq D ζ hnd σ hσ)
57 
58 variable {W : Type*} [AddCommGroup W] [Module ℂ W]
59 
60 /-- Source 15.2: equivalence of actual representations of the same total central extension. -/
61 theorem exists_factorization (τ : Representation ℂ (CentralProduct.Group D) W)
62     [Representation.IsIrreducible τ]
63     (hτ : ∀ z, τ ((CentralProduct.datum D).i z) = (ζ z : ℂ) • LinearMap.id) :
64     Nonempty (Representation.Equiv (descend D ζ σ hσ) τ) := by
65   let : Representation.IsIrreducible (descend D ζ σ hσ) := irreducible D ζ hnd σ hσ
66   exact CentralExtensionUniqueness.exists_equiv (CentralProduct.datum D) ζ
67     (CentralProduct.radical_eq_bot D ζ hnd) (descend D ζ σ hσ) τ
68     (central D ζ σ hσ) hτ
69 
70 /-- A chosen invertible intertwiner witnessing the factorization. -/
71 def factorization (τ : Representation ℂ (CentralProduct.Group D) W)
72     [Representation.IsIrreducible τ]
73     (hτ : ∀ z, τ ((CentralProduct.datum D).i z) = (ζ z : ℂ) • LinearMap.id) :
74     Representation.Equiv (descend D ζ σ hσ) τ :=
75   Classical.choice (exists_factorization D ζ hnd σ hσ τ hτ)
76 
77 /-- The chosen tensor factorization intertwines every actual total group element. -/
78 theorem factorization_intertwines (τ : Representation ℂ (CentralProduct.Group D) W)
79     [Representation.IsIrreducible τ]
80     (hτ : ∀ z, τ ((CentralProduct.datum D).i z) = (ζ z : ℂ) • LinearMap.id)
81     (g : CentralProduct.Group D) (x : PiTensorProduct ℂ V) :
82     factorization D ζ hnd σ hσ τ hτ (descend D ζ σ hσ g x) =
83       τ g (factorization D ζ hnd σ hσ τ hτ x) :=
84   Representation.IntertwiningMap.isIntertwining _ _
85     (factorization D ζ hnd σ hσ τ hτ).toIntertwiningMap g x
86 
87 end PaperXI.HeisenbergTensor

Back to source controls