HeisenbergTensor.lean

1 import PaperXI.FiniteTensor
2 import PaperXI.CentralProduct
3 import Mathlib.Analysis.Complex.Basic
4 
5 /-! The actual tensor action descends from the direct product, with one retained
6 central factor, to the balanced central product. Its central character occurs once. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.HeisenbergTensor
10 open TensorProduct
11 
12 variable {S Z : Type*} [Fintype S] [CommGroup Z]
13 variable {H A V : S → Type*} [∀ s, Group (H s)] [∀ s, CommGroup (A s)]
14 variable [∀ s, AddCommGroup (V s)] [∀ s, Module ℂ (V s)]
15 
16 /-- The central coordinate acts once, in addition to the external tensor action. -/
17 def ambient (ζ : Z →* ℂˣ) (σ : ∀ s, Representation ℂ (H s) (V s)) :
18     Representation ℂ (Z × (∀ s, H s)) (PiTensorProduct ℂ V) where
19   toFun x := (ζ x.1 : ℂ) • FiniteTensor.representation σ x.2
20   map_one' := by simp
21   map_mul' x y := by
22     simp only [Prod.fst_mul, Prod.snd_mul, map_mul, Units.val_mul,
23       smul_mul_assoc, mul_smul_comm, smul_smul]
24     rw [mul_comm (ζ x.1 : ℂ) (ζ y.1 : ℂ)]
25 
26 omit [Fintype S] in
27 @[simp] theorem ambient_apply (ζ : Z →* ℂˣ)
28     (σ : ∀ s, Representation ℂ (H s) (V s)) (z : Z) (h : ∀ s, H s)
29     (x : PiTensorProduct ℂ V) :
30     ambient ζ σ (z, h) x = (ζ z : ℂ) • FiniteTensor.representation σ h x := rfl
31 
32 omit [Fintype S] in
33 @[simp] theorem ambient_tprod (ζ : Z →* ℂˣ)
34     (σ : ∀ s, Representation ℂ (H s) (V s)) (z : Z) (h : ∀ s, H s)
35     (v : ∀ s, V s) :
36     ambient ζ σ (z, h) (PiTensorProduct.tprod ℂ v) =
37       (ζ z : ℂ) • PiTensorProduct.tprod ℂ (fun s => σ s (h s) (v s)) := by
38   simp
39 
40 /-- The balancing relations act trivially, permitting actual quotient descent. -/
41 theorem ambient_balanced (D : ∀ s, CentralExtension.Datum Z (H s) (A s))
42     (ζ : Z →* ℂˣ) (σ : ∀ s, Representation ℂ (H s) (V s))
43     (hσ : ∀ s z, σ s ((D s).i z) = (ζ z : ℂ) • LinearMap.id)
44     (z : S → Z) : ambient ζ σ (CentralProduct.balanced D z) = 1 := by
45   change (ζ ((∏ s, z s)⁻¹) : ℂ) •
46       PiTensorProduct.map (fun s => σ s ((D s).i (z s))) = 1
47   simp only [hσ, FiniteTensor.scalar_map, smul_smul]
48   have hp : (∏ s, (ζ (z s) : ℂ)) = (ζ (∏ s, z s) : ℂ) := by
49     simp
50   rw [hp]
51   rw [map_inv, ← Units.val_mul, inv_mul_cancel, Units.val_one, one_smul]
52   rfl
53 
54 /-- Representation of the genuine central quotient, on the actual finite tensor space. -/
55 def descend (D : ∀ s, CentralExtension.Datum Z (H s) (A s))
56     (ζ : Z →* ℂˣ) (σ : ∀ s, Representation ℂ (H s) (V s))
57     (hσ : ∀ s z, σ s ((D s).i z) = (ζ z : ℂ) • LinearMap.id) :
58     Representation ℂ (CentralProduct.Group D) (PiTensorProduct ℂ V) :=
59   CentralProduct.descend D (ambient ζ σ) (ambient_balanced D ζ σ hσ)
60 
61 @[simp] theorem descend_mk (D : ∀ s, CentralExtension.Datum Z (H s) (A s))
62     (ζ : Z →* ℂˣ) (σ : ∀ s, Representation ℂ (H s) (V s))
63     (hσ : ∀ s z, σ s ((D s).i z) = (ζ z : ℂ) • LinearMap.id)
64     (x : Z × (∀ s, H s)) :
65     descend D ζ σ hσ (CentralProduct.mk D x) = ambient ζ σ x := rfl
66 
67 /-- Formula on pure tensors for representatives of every element of the quotient. -/
68 theorem descend_tprod (D : ∀ s, CentralExtension.Datum Z (H s) (A s))
69     (ζ : Z →* ℂˣ) (σ : ∀ s, Representation ℂ (H s) (V s))
70     (hσ : ∀ s z, σ s ((D s).i z) = (ζ z : ℂ) • LinearMap.id)
71     (z : Z) (h : ∀ s, H s) (v : ∀ s, V s) :
72     descend D ζ σ hσ (CentralProduct.mk D (z, h)) (PiTensorProduct.tprod ℂ v) =
73       (ζ z : ℂ) • PiTensorProduct.tprod ℂ (fun s => σ s (h s) (v s)) := by
74   simp
75 
76 /-- The total distinguished center has the prescribed character, to the first power. -/
77 theorem central (D : ∀ s, CentralExtension.Datum Z (H s) (A s))
78     (ζ : Z →* ℂˣ) (σ : ∀ s, Representation ℂ (H s) (V s))
79     (hσ : ∀ s z, σ s ((D s).i z) = (ζ z : ℂ) • LinearMap.id) (z : Z) :
80     descend D ζ σ hσ ((CentralProduct.datum D).i z) =
81       (ζ z : ℂ) • LinearMap.id := by
82   change ambient ζ σ (z, 1) = _
83   change (ζ z : ℂ) • FiniteTensor.representation σ 1 = _
84   rw [map_one]
85   rfl
86 
87 /-- In an empty family, the tensor unit still carries the central character. -/
88 theorem empty_central [IsEmpty S]
89     (D : ∀ s, CentralExtension.Datum Z (H s) (A s))
90     (ζ : Z →* ℂˣ) (σ : ∀ s, Representation ℂ (H s) (V s))
91     (hσ : ∀ s z, σ s ((D s).i z) = (ζ z : ℂ) • LinearMap.id)
92     (z : Z) (x : PiTensorProduct ℂ V) :
93     PiTensorProduct.isEmptyEquiv S
94         (descend D ζ σ hσ ((CentralProduct.datum D).i z) x) =
95       (ζ z : ℂ) * PiTensorProduct.isEmptyEquiv S x := by
96   rw [central]
97   simp
98 
99 end PaperXI.HeisenbergTensor

Back to source controls