CompactTypeTensorNormalizer58.lean

1 import PaperXI.CompactTypeTensor58
2 
3 /-!
4 # Lifting a prescribed normalizer intertwiner through the quotient tensor factor
5 
6 When an actual normalizer automorphism acts trivially on the quotient, its
7 invertible intertwiner on the prescribed first factor supplies an invertible
8 intertwiner on the literal compact tensor action. The latter covariance is a
9 conclusion, not a hypothesis.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.CompactTypeTensorNormalizer58
14 
15 open Representation
16 open scoped TensorProduct
17 
18 variable {J Q W U : Type*} [Group J] [Group Q]
19 variable [AddCommGroup W] [Module ℂ W] [AddCommGroup U] [Module ℂ U]
20 variable (q : J →* Q) (κ : Representation ℂ J W) (σ : Representation ℂ Q U)
21 variable (a : J ≃* J) (hq : ∀ j, q (a j) = q j)
22 variable (A : W ≃ₗ[ℂ] W)
23 variable (hA : ∀ j w, A (κ j w) = κ (a j) (A w))
24 
25 /-- The invertible operator on the exact tensor space is constructed from A. -/
26 def tensorOperator : W ⊗[ℂ] U ≃ₗ[ℂ] W ⊗[ℂ] U :=
27   TensorProduct.congr A (LinearEquiv.refl ℂ U)
28 
29 @[simp] theorem tensorOperator_tmul (w : W) (u : U) :
30     tensorOperator (U := U) A (w ⊗ₜ[ℂ] u) = A w ⊗ₜ[ℂ] u := rfl
31 
32 include hq hA in
33 /-- Quotient-triviality and first-factor covariance imply whole-type covariance. -/
34 theorem tensorOperator_covariance (j : J) (x : W ⊗[ℂ] U) :
35     tensorOperator A (CompactTypeTensor58.action q κ σ j x) =
36       CompactTypeTensor58.action q κ σ (a j) (tensorOperator A x) := by
37   induction x using TensorProduct.induction_on with
38   | zero => simp
39   | add x y hx hy => simp only [map_add, hx, hy]
40   | tmul w u => simp [CompactTypeTensor58.action, hA, hq]
41 
42 /-- The actual equivalent actions, with the specified tensor normalizer operator. -/
43 def normalizerEquiv : Representation.Equiv (CompactTypeTensor58.action q κ σ)
44     ((CompactTypeTensor58.action q κ σ).comp a.toMonoidHom) :=
45   Representation.Equiv.mk (tensorOperator A) (by
46     intro j
47     apply LinearMap.ext
48     intro x
49     exact tensorOperator_covariance q κ σ a hq A hA j x)
50 
51 @[simp] theorem normalizerEquiv_linear :
52     (normalizerEquiv q κ σ a hq A hA).toLinearEquiv = tensorOperator A := rfl
53 
54 end PaperXI.CompactTypeTensorNormalizer58

Back to source controls