HeisenbergTensorComparison.lean

1 import PaperXI.HeisenbergTensorFactorization
2 import PaperXI.CentralExtensionComparison
3 
4 /-! Tensor factorization transported along an actual equivalence to a declared
5 full central extension. The comparisons intertwine actual group actions, not
6 only vector-space dimensions. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.HeisenbergTensor
10 open CentralExtension CocycleCommutator
11 open scoped Classical
12 
13 variable {S Z : Type*} [Fintype S] [CommGroup Z]
14 variable {H A V : S → Type*} [∀ s, Group (H s)] [∀ s, CommGroup (A s)]
15 variable [∀ s, Fintype (A s)] [∀ s, AddCommGroup (V s)] [∀ s, Module ℂ (V s)]
16 variable (D : ∀ s, Datum Z (H s) (A s)) (ζ : Z →* ℂˣ)
17 variable (hnd : ∀ s, radical (scalarCocycle (D s) ζ) = ⊥)
18 variable (σ : ∀ s, Representation ℂ (H s) (V s)) [∀ s, Representation.IsIrreducible (σ s)]
19 variable (hσ : ∀ s z, σ s ((D s).i z) = (ζ z : ℂ) • LinearMap.id)
20 variable {G W : Type*} [Group G] [AddCommGroup W] [Module ℂ W]
21 
22 /-- The total representation is compared through an actual central-extension equivalence. -/
23 def factorizationAlong (e : CentralProduct.Group D ≃* G)
24     (τ : Representation ℂ G W) [Representation.IsIrreducible τ]
25     (hτ : ∀ z, τ (e ((CentralProduct.datum D).i z)) = (ζ z : ℂ) • LinearMap.id) :
26     Representation.Equiv (descend D ζ σ hσ) (HeisenbergTransport.pullback e τ) := by
27   let : Representation.IsIrreducible (descend D ζ σ hσ) := irreducible D ζ hnd σ hσ
28   exact CentralExtensionComparison.equivAlong (CentralProduct.datum D) ζ
29     (CentralProduct.radical_eq_bot D ζ hnd) e (descend D ζ σ hσ) τ
30     (central D ζ σ hσ) hτ
31 
32 /-- Actual covariance of the tensor comparison along the declared group equivalence. -/
33 theorem factorizationAlong_intertwines (e : CentralProduct.Group D ≃* G)
34     (τ : Representation ℂ G W) [Representation.IsIrreducible τ]
35     (hτ : ∀ z, τ (e ((CentralProduct.datum D).i z)) = (ζ z : ℂ) • LinearMap.id)
36     (g : CentralProduct.Group D) (x : PiTensorProduct ℂ V) :
37     factorizationAlong D ζ hnd σ hσ e τ hτ (descend D ζ σ hσ g x) =
38       τ (e g) (factorizationAlong D ζ hnd σ hσ e τ hτ x) :=
39   Representation.IntertwiningMap.isIntertwining _ _
40     (factorizationAlong D ζ hnd σ hσ e τ hτ).toIntertwiningMap g x
41 
42 /-- The actual tensor action as a representation of the full declared group. -/
43 def onFullEnvelope (e : CentralProduct.Group D ≃* G) :
44     Representation ℂ G (PiTensorProduct ℂ V) :=
45   (descend D ζ σ hσ).comp e.symm.toMonoidHom
46 
47 /-- Factorization as an equivalence of representations of the very same full group. -/
48 def fullEnvelopeFactorization (e : CentralProduct.Group D ≃* G)
49     (τ : Representation ℂ G W) [Representation.IsIrreducible τ]
50     (hτ : ∀ z, τ (e ((CentralProduct.datum D).i z)) = (ζ z : ℂ) • LinearMap.id) :
51     Representation.Equiv (onFullEnvelope D ζ σ hσ e) τ := by
52   let U := (factorizationAlong D ζ hnd σ hσ e τ hτ).toLinearEquiv
53   let F : Representation.IntertwiningMap (onFullEnvelope D ζ σ hσ e) τ :=
54     ⟨U.toLinearMap, fun g => LinearMap.ext (fun x => by
55       have h := factorizationAlong_intertwines D ζ hnd σ hσ e τ hτ (e.symm g) x
56       simpa [onFullEnvelope, U] using h)⟩
57   exact F.ofBijective U.bijective
58 
59 /-- Every full-envelope operator is intertwined by the constructed factorization. -/
60 theorem fullEnvelopeFactorization_intertwines (e : CentralProduct.Group D ≃* G)
61     (τ : Representation ℂ G W) [Representation.IsIrreducible τ]
62     (hτ : ∀ z, τ (e ((CentralProduct.datum D).i z)) = (ζ z : ℂ) • LinearMap.id)
63     (g : G) (x : PiTensorProduct ℂ V) :
64     fullEnvelopeFactorization D ζ hnd σ hσ e τ hτ
65         (onFullEnvelope D ζ σ hσ e g x) =
66       τ g (fullEnvelopeFactorization D ζ hnd σ hσ e τ hτ x) :=
67   Representation.IntertwiningMap.isIntertwining _ _
68     (fullEnvelopeFactorization D ζ hnd σ hσ e τ hτ).toIntertwiningMap g x
69 
70 end PaperXI.HeisenbergTensor

Back to source controls