Physlib.Relativity.Tensors.ComplexTensor.Units.Pre

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Relativity.Tensors.ComplexTensor.Matrix.Pre
public import Physlib.Relativity.Tensors.ComplexTensor.Vector.Pre.Contraction

Unit for complex Lorentz vectors

@[expose] public section

The contra-co unit for complex lorentz vectors. Usually denoted δⁱᵢ.

def contrCoUnitVal : ContrℂModule ⊗[ℂ] CoℂModule :=
  contrCoToMatrix.symm 1

Expansion of contrCoUnitVal into basis.

lemma contrCoUnitVal_expand_tmul : contrCoUnitVal =
    complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)
    + complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)
    + complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)
    + complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) := by⊢ contrCoUnitVal =
  complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
        complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
      complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
    complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)
  simp only [contrCoUnitVal, Fin.isValue]⊢ contrCoToMatrix.symm 1 =
  complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
        complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
      complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
    complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)
  erw [contrCoToMatrix_symm_expand_tmul⊢ ∑ i, ∑ j, 1 i j • complexContrBasis i ⊗ₜ[ℂ] complexCoBasis j =
  complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
        complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
      complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
    complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)]⊢ ∑ i, ∑ j, 1 i j • complexContrBasis i ⊗ₜ[ℂ] complexCoBasis j =
  complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
        complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
      complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
    complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)
  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
    Finset.sum_singleton, Fin.sum_univ_three, ne_eq, reduceCtorEq, not_false_eq_true, one_apply_ne,
    zero_smul, add_zero, one_apply_eq, one_smul, zero_add, Sum.inr.injEq, zero_ne_one, Fin.reduceEq,
    one_ne_zero]⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
    (complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
        complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
      complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) =
  complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
        complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
      complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
    complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)
  rflAll goals completed! 🐙

lemma contrCoUnitVal_eq_sum_tmul : contrCoUnitVal =
    ∑ i, complexContrBasis i ⊗ₜ[ℂ] complexCoBasis i := by⊢ contrCoUnitVal = ∑ i, complexContrBasis i ⊗ₜ[ℂ] complexCoBasis i
  simp [contrCoUnitVal_expand_tmul, Fin.isValue, Fin.sum_univ_three]⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
        complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
      complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
    complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) =
  complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
    (complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
        complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
      complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2))
  moduleAll goals completed! 🐙

The contra-co unit for complex lorentz vectors as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo, manifesting the invariance under the SL(2, ℂ) action.


def contrCoUnit : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap
    (ContrℂModule.SL2CRep.tprod CoℂModule.SL2CRep) where
  toFun := fun a =>
    let a' : ℂ := a
    a' • contrCoUnitVal
  map_add' := fun x y => byx:ℂy:ℂ⊢ (let a' := x + y;
  a' • contrCoUnitVal) =
  (let a' := x;
    a' • contrCoUnitVal) +
    let a' := y;
    a' • contrCoUnitVal
    simp only [add_smul]All goals completed! 🐙
  map_smul' := fun m x => bym:ℂx:ℂ⊢ (let a' := m • x;
  a' • contrCoUnitVal) =
  (RingHom.id ℂ) m •
    let a' := x;
    a' • contrCoUnitVal
    simp only [smul_smul]m:ℂx:ℂ⊢ (m • x) • contrCoUnitVal = ((RingHom.id ℂ) m * x) • contrCoUnitVal
    rflAll goals completed! 🐙
  isIntertwining' M := byM:SL(2, ℂ)⊢ {
      toFun := fun a =>
        let a' := a;
        a' • contrCoUnitVal,
      map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
    (Representation.trivial ℂ SL(2, ℂ) ℂ) M =
  (ContrℂModule.SL2CRep.tprod CoℂModule.SL2CRep) M ∘ₗ
    {
      toFun := fun a =>
        let a' := a;
        a' • contrCoUnitVal,
      map_add' := ⋯, map_smul' := ⋯ }
    refine LinearMap.ext fun x : ℂ => ?_M:SL(2, ℂ)x:ℂ⊢ ({
        toFun := fun a =>
          let a' := a;
          a' • contrCoUnitVal,
        map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      (Representation.trivial ℂ SL(2, ℂ) ℂ) M)
    x =
  ((ContrℂModule.SL2CRep.tprod CoℂModule.SL2CRep) M ∘ₗ
      {
        toFun := fun a =>
          let a' := a;
          a' • contrCoUnitVal,
        map_add' := ⋯, map_smul' := ⋯ })
    x
    change x • contrCoUnitVal =
      (TensorProduct.map (ContrℂModule.SL2CRep M) (CoℂModule.SL2CRep M)) (x • contrCoUnitVal)M:SL(2, ℂ)x:ℂ⊢ x • contrCoUnitVal = (TensorProduct.map (ContrℂModule.SL2CRep M) (CoℂModule.SL2CRep M)) (x • contrCoUnitVal)
    simp only [map_smul]M:SL(2, ℂ)x:ℂ⊢ x • contrCoUnitVal = x • (TensorProduct.map (ContrℂModule.SL2CRep M) (CoℂModule.SL2CRep M)) contrCoUnitVal
    apply congrArgM:SL(2, ℂ)x:ℂ⊢ contrCoUnitVal = (TensorProduct.map (ContrℂModule.SL2CRep M) (CoℂModule.SL2CRep M)) contrCoUnitVal
    simp only [contrCoUnitVal]M:SL(2, ℂ)x:ℂ⊢ contrCoToMatrix.symm 1 = (TensorProduct.map (ContrℂModule.SL2CRep M) (CoℂModule.SL2CRep M)) (contrCoToMatrix.symm 1)
    rw [contrCoToMatrix_ρ_symmM:SL(2, ℂ)x:ℂ⊢ contrCoToMatrix.symm 1 =
  contrCoToMatrix.symm
    (LorentzGroup.toComplex (SL2C.toLorentzGroup M) * 1 * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹)M:SL(2, ℂ)x:ℂ⊢ contrCoToMatrix.symm 1 =
  contrCoToMatrix.symm
    (LorentzGroup.toComplex (SL2C.toLorentzGroup M) * 1 * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹)]M:SL(2, ℂ)x:ℂ⊢ contrCoToMatrix.symm 1 =
  contrCoToMatrix.symm
    (LorentzGroup.toComplex (SL2C.toLorentzGroup M) * 1 * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹)
    apply congrArgM:SL(2, ℂ)x:ℂ⊢ 1 = LorentzGroup.toComplex (SL2C.toLorentzGroup M) * 1 * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹
    simpAll goals completed! 🐙



lemma contrCoUnit_apply_one : contrCoUnit (1 : ℂ) = contrCoUnitVal := by⊢ contrCoUnit 1 = contrCoUnitVal
  change (1 : ℂ) • contrCoUnitVal = contrCoUnitVal⊢ 1 • contrCoUnitVal = contrCoUnitVal
  rw [one_smul⊢ contrCoUnitVal = contrCoUnitValAll goals completed! 🐙]All goals completed! 🐙

The co-contra unit for complex lorentz vectors. Usually denoted δᵢⁱ.

def coContrUnitVal : CoℂModule ⊗[ℂ] ContrℂModule :=
  coContrToMatrix.symm 1

Expansion of coContrUnitVal into basis.


lemma coContrUnitVal_expand_tmul : coContrUnitVal =
    complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)
    + complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)
    + complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)
    + complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) := by⊢ coContrUnitVal =
  complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)
  simp only [coContrUnitVal, Fin.isValue]⊢ coContrToMatrix.symm 1 =
  complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)
  rw [coContrToMatrix_symm_expand_tmul⊢ ∑ i, ∑ j, 1 i j • complexCoBasis i ⊗ₜ[ℂ] complexContrBasis j =
  complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)⊢ ∑ i, ∑ j, 1 i j • complexCoBasis i ⊗ₜ[ℂ] complexContrBasis j =
  complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)]⊢ ∑ i, ∑ j, 1 i j • complexCoBasis i ⊗ₜ[ℂ] complexContrBasis j =
  complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)
  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
    Finset.sum_singleton, Fin.sum_univ_three, ne_eq, reduceCtorEq, not_false_eq_true, one_apply_ne,
    zero_smul, add_zero, one_apply_eq, one_smul, zero_add, Sum.inr.injEq, zero_ne_one, Fin.reduceEq,
    one_ne_zero]⊢ complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
    (complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
        complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
      complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) =
  complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)
  rflAll goals completed! 🐙

lemma coContrUnitVal_eq_sum_tmul : coContrUnitVal =
    ∑ i, complexCoBasis i ⊗ₜ[ℂ] complexContrBasis i := by⊢ coContrUnitVal = ∑ i, complexCoBasis i ⊗ₜ[ℂ] complexContrBasis i
  simp [coContrUnitVal_expand_tmul, Fin.isValue, Fin.sum_univ_three]⊢ complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) =
  complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
    (complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
        complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
      complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2))
  moduleAll goals completed! 🐙

The co-contra unit for complex lorentz vectors as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr, manifesting the invariance under the SL(2, ℂ) action.


def coContrUnit : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap
    (CoℂModule.SL2CRep.tprod ContrℂModule.SL2CRep) where
  toFun := fun a =>
    let a' : ℂ := a
    a' • coContrUnitVal
  map_add' := fun x y => byx:ℂy:ℂ⊢ (let a' := x + y;
  a' • coContrUnitVal) =
  (let a' := x;
    a' • coContrUnitVal) +
    let a' := y;
    a' • coContrUnitVal
    simp only [add_smul]All goals completed! 🐙
  map_smul' := fun m x => bym:ℂx:ℂ⊢ (let a' := m • x;
  a' • coContrUnitVal) =
  (RingHom.id ℂ) m •
    let a' := x;
    a' • coContrUnitVal
    simp only [smul_smul]m:ℂx:ℂ⊢ (m • x) • coContrUnitVal = ((RingHom.id ℂ) m * x) • coContrUnitVal
    rflAll goals completed! 🐙
  isIntertwining' M := byM:SL(2, ℂ)⊢ {
      toFun := fun a =>
        let a' := a;
        a' • coContrUnitVal,
      map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
    (Representation.trivial ℂ SL(2, ℂ) ℂ) M =
  (CoℂModule.SL2CRep.tprod ContrℂModule.SL2CRep) M ∘ₗ
    {
      toFun := fun a =>
        let a' := a;
        a' • coContrUnitVal,
      map_add' := ⋯, map_smul' := ⋯ }
    refine LinearMap.ext fun x : ℂ => ?_M:SL(2, ℂ)x:ℂ⊢ ({
        toFun := fun a =>
          let a' := a;
          a' • coContrUnitVal,
        map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      (Representation.trivial ℂ SL(2, ℂ) ℂ) M)
    x =
  ((CoℂModule.SL2CRep.tprod ContrℂModule.SL2CRep) M ∘ₗ
      {
        toFun := fun a =>
          let a' := a;
          a' • coContrUnitVal,
        map_add' := ⋯, map_smul' := ⋯ })
    x
    change x • coContrUnitVal =
      (TensorProduct.map (CoℂModule.SL2CRep M) (ContrℂModule.SL2CRep M)) (x • coContrUnitVal)M:SL(2, ℂ)x:ℂ⊢ x • coContrUnitVal = (TensorProduct.map (CoℂModule.SL2CRep M) (ContrℂModule.SL2CRep M)) (x • coContrUnitVal)
    simp only [map_smul]M:SL(2, ℂ)x:ℂ⊢ x • coContrUnitVal = x • (TensorProduct.map (CoℂModule.SL2CRep M) (ContrℂModule.SL2CRep M)) coContrUnitVal
    apply congrArgM:SL(2, ℂ)x:ℂ⊢ coContrUnitVal = (TensorProduct.map (CoℂModule.SL2CRep M) (ContrℂModule.SL2CRep M)) coContrUnitVal
    simp only [coContrUnitVal]M:SL(2, ℂ)x:ℂ⊢ coContrToMatrix.symm 1 = (TensorProduct.map (CoℂModule.SL2CRep M) (ContrℂModule.SL2CRep M)) (coContrToMatrix.symm 1)
    rw [coContrToMatrix_ρ_symmM:SL(2, ℂ)x:ℂ⊢ coContrToMatrix.symm 1 =
  coContrToMatrix.symm
    ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ * 1 * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ)M:SL(2, ℂ)x:ℂ⊢ coContrToMatrix.symm 1 =
  coContrToMatrix.symm
    ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ * 1 * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ)]M:SL(2, ℂ)x:ℂ⊢ coContrToMatrix.symm 1 =
  coContrToMatrix.symm
    ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ * 1 * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ)
    apply congrArgM:SL(2, ℂ)x:ℂ⊢ 1 = (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ * 1 * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ
    symmM:SL(2, ℂ)x:ℂ⊢ (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ * 1 * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ = 1
    refine transpose_eq_one.mp ?h.h.h.ah.h.h.aM:SL(2, ℂ)x:ℂ⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ * 1 * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ)ᵀ = 1
    simpAll goals completed! 🐙



lemma coContrUnit_apply_one : coContrUnit (1 : ℂ) = coContrUnitVal := by⊢ coContrUnit 1 = coContrUnitVal
  change (1 : ℂ) • coContrUnitVal = coContrUnitVal⊢ 1 • coContrUnitVal = coContrUnitVal
  rw [one_smul⊢ coContrUnitVal = coContrUnitValAll goals completed! 🐙]All goals completed! 🐙

Contraction of the units

Contraction on the right with contrCoUnit does nothing.

lemma contr_contrCoUnit (x : CoℂModule) :
    (TensorProduct.lid ℂ _ <|
    coContrContraction.toLinearMap.rTensor _ <|
    (TensorProduct.assoc ℂ _ _ _).symm <|
    x ⊗ₜ[ℂ] (contrCoUnit (1 : ℂ))) = x := byx:CoℂModule⊢ (TensorProduct.lid ℂ CoℂModule)
    ((LinearMap.rTensor CoℂModule coContrContraction.toLinearMap)
      ((TensorProduct.assoc ℂ CoℂModule ContrℂModule CoℂModule).symm (x ⊗ₜ[ℂ] contrCoUnit 1))) =
  x
  obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span complexCoBasis x)x:CoℂModulec:Fin 1 ⊕ Fin 3 → ℂhc:∑ i, c i • complexCoBasis i = x⊢ (TensorProduct.lid ℂ CoℂModule)
    ((LinearMap.rTensor CoℂModule coContrContraction.toLinearMap)
      ((TensorProduct.assoc ℂ CoℂModule ContrℂModule CoℂModule).symm (x ⊗ₜ[ℂ] contrCoUnit 1))) =
  x
  subst hcc:Fin 1 ⊕ Fin 3 → ℂ⊢ (TensorProduct.lid ℂ CoℂModule)
    ((LinearMap.rTensor CoℂModule coContrContraction.toLinearMap)
      ((TensorProduct.assoc ℂ CoℂModule ContrℂModule CoℂModule).symm
        ((∑ i, c i • complexCoBasis i) ⊗ₜ[ℂ] contrCoUnit 1))) =
  ∑ i, c i • complexCoBasis i
  simp [- Fintype.sum_sum_type, map_sum, tmul_sum, smul_tmul, coContrContraction_basis',
    contrCoUnit_apply_one, contrCoUnitVal_eq_sum_tmul, sum_tmul]All goals completed! 🐙

Contraction on the right with coContrUnit.

lemma contr_coContrUnit (x : ContrℂModule) :
    (TensorProduct.lid ℂ _ <|
    contrCoContraction.toLinearMap.rTensor _ <|
    (TensorProduct.assoc ℂ _ _ _).symm <|
    x ⊗ₜ[ℂ] (coContrUnit (1 : ℂ))) = x := byx:ContrℂModule⊢ (TensorProduct.lid ℂ ContrℂModule)
    ((LinearMap.rTensor ContrℂModule contrCoContraction.toLinearMap)
      ((TensorProduct.assoc ℂ ContrℂModule CoℂModule ContrℂModule).symm (x ⊗ₜ[ℂ] coContrUnit 1))) =
  x
  obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun ℂ).mp
    (Basis.mem_span complexContrBasis x)x:ContrℂModulec:Fin 1 ⊕ Fin 3 → ℂhc:∑ i, c i • complexContrBasis i = x⊢ (TensorProduct.lid ℂ ContrℂModule)
    ((LinearMap.rTensor ContrℂModule contrCoContraction.toLinearMap)
      ((TensorProduct.assoc ℂ ContrℂModule CoℂModule ContrℂModule).symm (x ⊗ₜ[ℂ] coContrUnit 1))) =
  x
  subst hcc:Fin 1 ⊕ Fin 3 → ℂ⊢ (TensorProduct.lid ℂ ContrℂModule)
    ((LinearMap.rTensor ContrℂModule contrCoContraction.toLinearMap)
      ((TensorProduct.assoc ℂ ContrℂModule CoℂModule ContrℂModule).symm
        ((∑ i, c i • complexContrBasis i) ⊗ₜ[ℂ] coContrUnit 1))) =
  ∑ i, c i • complexContrBasis i
  simp [- Fintype.sum_sum_type, map_sum, tmul_sum, smul_tmul, contrCoContraction_basis',
    coContrUnit_apply_one, coContrUnitVal_eq_sum_tmul, sum_tmul]All goals completed! 🐙

Symmetry properties of the units



lemma contrCoUnit_symm :
    contrCoUnit (1 : ℂ) = LinearMap.lTensor _ (LinearEquiv.refl _ _).toLinearMap
      (TensorProduct.comm ℂ _ _ (coContrUnit (1 : ℂ))) := by⊢ contrCoUnit 1 =
  (LinearMap.lTensor ContrℂModule ↑(LinearEquiv.refl ℂ CoℂModule))
    ((TensorProduct.comm ℂ CoℂModule ContrℂModule) (coContrUnit 1))
  rw [contrCoUnit_apply_one,⊢ contrCoUnitVal =
  (LinearMap.lTensor ContrℂModule ↑(LinearEquiv.refl ℂ CoℂModule))
    ((TensorProduct.comm ℂ CoℂModule ContrℂModule) (coContrUnit 1))⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
        complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
      complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
    complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) =
  (LinearMap.lTensor ContrℂModule ↑(LinearEquiv.refl ℂ CoℂModule))
    ((TensorProduct.comm ℂ CoℂModule ContrℂModule) (coContrUnit 1)) contrCoUnitVal_expand_tmul⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
        complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
      complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
    complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) =
  (LinearMap.lTensor ContrℂModule ↑(LinearEquiv.refl ℂ CoℂModule))
    ((TensorProduct.comm ℂ CoℂModule ContrℂModule) (coContrUnit 1))⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
        complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
      complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
    complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) =
  (LinearMap.lTensor ContrℂModule ↑(LinearEquiv.refl ℂ CoℂModule))
    ((TensorProduct.comm ℂ CoℂModule ContrℂModule) (coContrUnit 1))]⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
        complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
      complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
    complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) =
  (LinearMap.lTensor ContrℂModule ↑(LinearEquiv.refl ℂ CoℂModule))
    ((TensorProduct.comm ℂ CoℂModule ContrℂModule) (coContrUnit 1))
  rw [coContrUnit_apply_one,⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
        complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
      complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
    complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) =
  (LinearMap.lTensor ContrℂModule ↑(LinearEquiv.refl ℂ CoℂModule))
    ((TensorProduct.comm ℂ CoℂModule ContrℂModule) coContrUnitVal)⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
        complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
      complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
    complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) =
  (LinearMap.lTensor ContrℂModule ↑(LinearEquiv.refl ℂ CoℂModule))
    ((TensorProduct.comm ℂ CoℂModule ContrℂModule)
      (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
            complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
          complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
        complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2))) coContrUnitVal_expand_tmul⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
        complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
      complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
    complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) =
  (LinearMap.lTensor ContrℂModule ↑(LinearEquiv.refl ℂ CoℂModule))
    ((TensorProduct.comm ℂ CoℂModule ContrℂModule)
      (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
            complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
          complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
        complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)))⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
        complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
      complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
    complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) =
  (LinearMap.lTensor ContrℂModule ↑(LinearEquiv.refl ℂ CoℂModule))
    ((TensorProduct.comm ℂ CoℂModule ContrℂModule)
      (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
            complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
          complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
        complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)))]⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
        complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
      complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
    complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) =
  (LinearMap.lTensor ContrℂModule ↑(LinearEquiv.refl ℂ CoℂModule))
    ((TensorProduct.comm ℂ CoℂModule ContrℂModule)
      (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
            complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
          complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
        complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)))
  rflAll goals completed! 🐙



lemma coContrUnit_symm :
    (coContrUnit (1 : ℂ)) = LinearMap.lTensor _ (LinearEquiv.refl _ _).toLinearMap
      (TensorProduct.comm ℂ _ _ (contrCoUnit (1 : ℂ))) := by⊢ coContrUnit 1 =
  (LinearMap.lTensor CoℂModule ↑(LinearEquiv.refl ℂ ContrℂModule))
    ((TensorProduct.comm ℂ ContrℂModule CoℂModule) (contrCoUnit 1))
  rw [coContrUnit_apply_one,⊢ coContrUnitVal =
  (LinearMap.lTensor CoℂModule ↑(LinearEquiv.refl ℂ ContrℂModule))
    ((TensorProduct.comm ℂ ContrℂModule CoℂModule) (contrCoUnit 1))⊢ complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) =
  (LinearMap.lTensor CoℂModule ↑(LinearEquiv.refl ℂ ContrℂModule))
    ((TensorProduct.comm ℂ ContrℂModule CoℂModule) (contrCoUnit 1)) coContrUnitVal_expand_tmul⊢ complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) =
  (LinearMap.lTensor CoℂModule ↑(LinearEquiv.refl ℂ ContrℂModule))
    ((TensorProduct.comm ℂ ContrℂModule CoℂModule) (contrCoUnit 1))⊢ complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) =
  (LinearMap.lTensor CoℂModule ↑(LinearEquiv.refl ℂ ContrℂModule))
    ((TensorProduct.comm ℂ ContrℂModule CoℂModule) (contrCoUnit 1))]⊢ complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) =
  (LinearMap.lTensor CoℂModule ↑(LinearEquiv.refl ℂ ContrℂModule))
    ((TensorProduct.comm ℂ ContrℂModule CoℂModule) (contrCoUnit 1))
  rw [contrCoUnit_apply_one,⊢ complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) =
  (LinearMap.lTensor CoℂModule ↑(LinearEquiv.refl ℂ ContrℂModule))
    ((TensorProduct.comm ℂ ContrℂModule CoℂModule) contrCoUnitVal)⊢ complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) =
  (LinearMap.lTensor CoℂModule ↑(LinearEquiv.refl ℂ ContrℂModule))
    ((TensorProduct.comm ℂ ContrℂModule CoℂModule)
      (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
            complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
          complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
        complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2))) contrCoUnitVal_expand_tmul⊢ complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) =
  (LinearMap.lTensor CoℂModule ↑(LinearEquiv.refl ℂ ContrℂModule))
    ((TensorProduct.comm ℂ ContrℂModule CoℂModule)
      (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
            complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
          complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
        complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)))⊢ complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) =
  (LinearMap.lTensor CoℂModule ↑(LinearEquiv.refl ℂ ContrℂModule))
    ((TensorProduct.comm ℂ ContrℂModule CoℂModule)
      (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
            complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
          complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
        complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)))]⊢ complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) +
        complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) +
      complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) +
    complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) =
  (LinearMap.lTensor CoℂModule ↑(LinearEquiv.refl ℂ ContrℂModule))
    ((TensorProduct.comm ℂ ContrℂModule CoℂModule)
      (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) +
            complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) +
          complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) +
        complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)))
  rflAll goals completed! 🐙