Physlib.Relativity.Tensors.ComplexTensor.Vector.Pre.Contraction

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.Vector.Pre.Basic

Contraction of Lorentz vectors

@[expose] public section

The bi-linear map corresponding to contraction of a contravariant Lorentz vector with a covariant Lorentz vector.


def contrCoContrBi : ContrℂModule →ₗ[ℂ] CoℂModule →ₗ[ℂ] ℂ where
  toFun ψ := {
    toFun := fun φ => ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ,
    map_add' := byψ:ContrℂModule⊢ ∀ (x y : CoℂModule), ψ.toFin13ℂ ⬝ᵥ (x + y).toFin13ℂ = ψ.toFin13ℂ ⬝ᵥ x.toFin13ℂ + ψ.toFin13ℂ ⬝ᵥ y.toFin13ℂ
      intro φ φ'ψ:ContrℂModuleφ:CoℂModuleφ':CoℂModule⊢ ψ.toFin13ℂ ⬝ᵥ (φ + φ').toFin13ℂ = ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ + ψ.toFin13ℂ ⬝ᵥ φ'.toFin13ℂ
      simp only [map_add]ψ:ContrℂModuleφ:CoℂModuleφ':CoℂModule⊢ ψ.toFin13ℂ ⬝ᵥ (CoℂModule.toFin13ℂEquiv φ + CoℂModule.toFin13ℂEquiv φ') =
  ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ + ψ.toFin13ℂ ⬝ᵥ φ'.toFin13ℂ
      rw [dotProduct_addψ:ContrℂModuleφ:CoℂModuleφ':CoℂModule⊢ ψ.toFin13ℂ ⬝ᵥ CoℂModule.toFin13ℂEquiv φ + ψ.toFin13ℂ ⬝ᵥ CoℂModule.toFin13ℂEquiv φ' =
  ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ + ψ.toFin13ℂ ⬝ᵥ φ'.toFin13ℂAll goals completed! 🐙]All goals completed! 🐙
    map_smul' := byψ:ContrℂModule⊢ ∀ (m : ℂ) (x : CoℂModule), ψ.toFin13ℂ ⬝ᵥ (m • x).toFin13ℂ = (RingHom.id ℂ) m • (ψ.toFin13ℂ ⬝ᵥ x.toFin13ℂ)
      intro r φψ:ContrℂModuler:ℂφ:CoℂModule⊢ ψ.toFin13ℂ ⬝ᵥ (r • φ).toFin13ℂ = (RingHom.id ℂ) r • (ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ)
      simp only [LinearEquiv.map_smul]ψ:ContrℂModuler:ℂφ:CoℂModule⊢ ψ.toFin13ℂ ⬝ᵥ r • CoℂModule.toFin13ℂEquiv φ = (RingHom.id ℂ) r • (ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ)
      rw [dotProduct_smulψ:ContrℂModuler:ℂφ:CoℂModule⊢ r • (ψ.toFin13ℂ ⬝ᵥ CoℂModule.toFin13ℂEquiv φ) = (RingHom.id ℂ) r • (ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ)ψ:ContrℂModuler:ℂφ:CoℂModule⊢ r • (ψ.toFin13ℂ ⬝ᵥ CoℂModule.toFin13ℂEquiv φ) = (RingHom.id ℂ) r • (ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ)]ψ:ContrℂModuler:ℂφ:CoℂModule⊢ r • (ψ.toFin13ℂ ⬝ᵥ CoℂModule.toFin13ℂEquiv φ) = (RingHom.id ℂ) r • (ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ)
      rflAll goals completed! 🐙}
  map_add' ψ ψ':= byψ:ContrℂModuleψ':ContrℂModule⊢ { toFun := fun φ => (ψ + ψ').toFin13ℂ ⬝ᵥ φ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ } =
  { toFun := fun φ => ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ } +
    { toFun := fun φ => ψ'.toFin13ℂ ⬝ᵥ φ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ }
    refine LinearMap.ext (fun φ => ?_)ψ:ContrℂModuleψ':ContrℂModuleφ:CoℂModule⊢ { toFun := fun φ => (ψ + ψ').toFin13ℂ ⬝ᵥ φ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ } φ =
  ({ toFun := fun φ => ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun φ => ψ'.toFin13ℂ ⬝ᵥ φ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ })
    φ
    simp only [map_add, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]ψ:ContrℂModuleψ':ContrℂModuleφ:CoℂModule⊢ (ContrℂModule.toFin13ℂEquiv ψ + ContrℂModule.toFin13ℂEquiv ψ') ⬝ᵥ φ.toFin13ℂ =
  ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ + ψ'.toFin13ℂ ⬝ᵥ φ.toFin13ℂ
    rw [add_dotProductψ:ContrℂModuleψ':ContrℂModuleφ:CoℂModule⊢ ContrℂModule.toFin13ℂEquiv ψ ⬝ᵥ φ.toFin13ℂ + ContrℂModule.toFin13ℂEquiv ψ' ⬝ᵥ φ.toFin13ℂ =
  ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ + ψ'.toFin13ℂ ⬝ᵥ φ.toFin13ℂAll goals completed! 🐙]All goals completed! 🐙
  map_smul' r ψ := byr:ℂψ:ContrℂModule⊢ { toFun := fun φ => (r • ψ).toFin13ℂ ⬝ᵥ φ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ } =
  (RingHom.id ℂ) r • { toFun := fun φ => ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ }
    refine LinearMap.ext (fun φ => ?_)r:ℂψ:ContrℂModuleφ:CoℂModule⊢ { toFun := fun φ => (r • ψ).toFin13ℂ ⬝ᵥ φ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ } φ =
  ((RingHom.id ℂ) r • { toFun := fun φ => ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ }) φ
    simp only [LinearEquiv.map_smul, LinearMap.coe_mk, AddHom.coe_mk]r:ℂψ:ContrℂModuleφ:CoℂModule⊢ r • ContrℂModule.toFin13ℂEquiv ψ ⬝ᵥ φ.toFin13ℂ =
  ((RingHom.id ℂ) r • { toFun := fun φ => ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ }) φ
    rw [smul_dotProductr:ℂψ:ContrℂModuleφ:CoℂModule⊢ r • (ContrℂModule.toFin13ℂEquiv ψ ⬝ᵥ φ.toFin13ℂ) =
  ((RingHom.id ℂ) r • { toFun := fun φ => ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ }) φr:ℂψ:ContrℂModuleφ:CoℂModule⊢ r • (ContrℂModule.toFin13ℂEquiv ψ ⬝ᵥ φ.toFin13ℂ) =
  ((RingHom.id ℂ) r • { toFun := fun φ => ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ }) φ]r:ℂψ:ContrℂModuleφ:CoℂModule⊢ r • (ContrℂModule.toFin13ℂEquiv ψ ⬝ᵥ φ.toFin13ℂ) =
  ((RingHom.id ℂ) r • { toFun := fun φ => ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ }) φ
    rflAll goals completed! 🐙

The bi-linear map corresponding to contraction of a covariant Lorentz vector with a contravariant Lorentz vector.


def contrContrCoBi : CoℂModule →ₗ[ℂ] ContrℂModule →ₗ[ℂ] ℂ where
  toFun φ := {
    toFun := fun ψ => φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ,
    map_add' := byφ:CoℂModule⊢ ∀ (x y : ContrℂModule), φ.toFin13ℂ ⬝ᵥ (x + y).toFin13ℂ = φ.toFin13ℂ ⬝ᵥ x.toFin13ℂ + φ.toFin13ℂ ⬝ᵥ y.toFin13ℂ
      intro ψ ψ'φ:CoℂModuleψ:ContrℂModuleψ':ContrℂModule⊢ φ.toFin13ℂ ⬝ᵥ (ψ + ψ').toFin13ℂ = φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ + φ.toFin13ℂ ⬝ᵥ ψ'.toFin13ℂ
      simp only [map_add]φ:CoℂModuleψ:ContrℂModuleψ':ContrℂModule⊢ φ.toFin13ℂ ⬝ᵥ (ContrℂModule.toFin13ℂEquiv ψ + ContrℂModule.toFin13ℂEquiv ψ') =
  φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ + φ.toFin13ℂ ⬝ᵥ ψ'.toFin13ℂ
      rw [dotProduct_addφ:CoℂModuleψ:ContrℂModuleψ':ContrℂModule⊢ φ.toFin13ℂ ⬝ᵥ ContrℂModule.toFin13ℂEquiv ψ + φ.toFin13ℂ ⬝ᵥ ContrℂModule.toFin13ℂEquiv ψ' =
  φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ + φ.toFin13ℂ ⬝ᵥ ψ'.toFin13ℂAll goals completed! 🐙]All goals completed! 🐙
    map_smul' := byφ:CoℂModule⊢ ∀ (m : ℂ) (x : ContrℂModule), φ.toFin13ℂ ⬝ᵥ (m • x).toFin13ℂ = (RingHom.id ℂ) m • (φ.toFin13ℂ ⬝ᵥ x.toFin13ℂ)
      intro r ψφ:CoℂModuler:ℂψ:ContrℂModule⊢ φ.toFin13ℂ ⬝ᵥ (r • ψ).toFin13ℂ = (RingHom.id ℂ) r • (φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ)
      simp only [LinearEquiv.map_smul]φ:CoℂModuler:ℂψ:ContrℂModule⊢ φ.toFin13ℂ ⬝ᵥ r • ContrℂModule.toFin13ℂEquiv ψ = (RingHom.id ℂ) r • (φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ)
      rw [dotProduct_smulφ:CoℂModuler:ℂψ:ContrℂModule⊢ r • (φ.toFin13ℂ ⬝ᵥ ContrℂModule.toFin13ℂEquiv ψ) = (RingHom.id ℂ) r • (φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ)φ:CoℂModuler:ℂψ:ContrℂModule⊢ r • (φ.toFin13ℂ ⬝ᵥ ContrℂModule.toFin13ℂEquiv ψ) = (RingHom.id ℂ) r • (φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ)]φ:CoℂModuler:ℂψ:ContrℂModule⊢ r • (φ.toFin13ℂ ⬝ᵥ ContrℂModule.toFin13ℂEquiv ψ) = (RingHom.id ℂ) r • (φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ)
      rflAll goals completed! 🐙}
  map_add' φ φ' := byφ:CoℂModuleφ':CoℂModule⊢ { toFun := fun ψ => (φ + φ').toFin13ℂ ⬝ᵥ ψ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ } =
  { toFun := fun ψ => φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ } +
    { toFun := fun ψ => φ'.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ }
    refine LinearMap.ext (fun ψ => ?_)φ:CoℂModuleφ':CoℂModuleψ:ContrℂModule⊢ { toFun := fun ψ => (φ + φ').toFin13ℂ ⬝ᵥ ψ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ } ψ =
  ({ toFun := fun ψ => φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun ψ => φ'.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ })
    ψ
    simp only [map_add, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]φ:CoℂModuleφ':CoℂModuleψ:ContrℂModule⊢ (CoℂModule.toFin13ℂEquiv φ + CoℂModule.toFin13ℂEquiv φ') ⬝ᵥ ψ.toFin13ℂ =
  φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ + φ'.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ
    rw [add_dotProductφ:CoℂModuleφ':CoℂModuleψ:ContrℂModule⊢ CoℂModule.toFin13ℂEquiv φ ⬝ᵥ ψ.toFin13ℂ + CoℂModule.toFin13ℂEquiv φ' ⬝ᵥ ψ.toFin13ℂ =
  φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ + φ'.toFin13ℂ ⬝ᵥ ψ.toFin13ℂAll goals completed! 🐙]All goals completed! 🐙
  map_smul' r φ := byr:ℂφ:CoℂModule⊢ { toFun := fun ψ => (r • φ).toFin13ℂ ⬝ᵥ ψ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ } =
  (RingHom.id ℂ) r • { toFun := fun ψ => φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ }
    refine LinearMap.ext (fun ψ => ?_)r:ℂφ:CoℂModuleψ:ContrℂModule⊢ { toFun := fun ψ => (r • φ).toFin13ℂ ⬝ᵥ ψ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ } ψ =
  ((RingHom.id ℂ) r • { toFun := fun ψ => φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ }) ψ
    simp only [LinearEquiv.map_smul, LinearMap.coe_mk, AddHom.coe_mk]r:ℂφ:CoℂModuleψ:ContrℂModule⊢ r • CoℂModule.toFin13ℂEquiv φ ⬝ᵥ ψ.toFin13ℂ =
  ((RingHom.id ℂ) r • { toFun := fun ψ => φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ }) ψ
    rw [smul_dotProductr:ℂφ:CoℂModuleψ:ContrℂModule⊢ r • (CoℂModule.toFin13ℂEquiv φ ⬝ᵥ ψ.toFin13ℂ) =
  ((RingHom.id ℂ) r • { toFun := fun ψ => φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ }) ψr:ℂφ:CoℂModuleψ:ContrℂModule⊢ r • (CoℂModule.toFin13ℂEquiv φ ⬝ᵥ ψ.toFin13ℂ) =
  ((RingHom.id ℂ) r • { toFun := fun ψ => φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ }) ψ]r:ℂφ:CoℂModuleψ:ContrℂModule⊢ r • (CoℂModule.toFin13ℂEquiv φ ⬝ᵥ ψ.toFin13ℂ) =
  ((RingHom.id ℂ) r • { toFun := fun ψ => φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ, map_add' := ⋯, map_smul' := ⋯ }) ψ
    rflAll goals completed! 🐙

The linear map from complexContr ⊗ complexCo to ℂ given by summing over components of contravariant Lorentz vector and covariant Lorentz vector in the standard basis (i.e. the dot product). In terms of index notation this is the contraction is ψⁱ φᵢ.


def contrCoContraction : (ContrℂModule.SL2CRep.tprod CoℂModule.SL2CRep).IntertwiningMap
    (Representation.trivial ℂ SL(2,ℂ) ℂ) where
  toLinearMap := TensorProduct.lift contrCoContrBi
  isIntertwining' M := TensorProduct.ext' fun ψ φ => byM:SL(2, ℂ)ψ:ContrℂModuleφ:CoℂModule⊢ (TensorProduct.lift contrCoContrBi ∘ₗ (ContrℂModule.SL2CRep.tprod CoℂModule.SL2CRep) M) (ψ ⊗ₜ[ℂ] φ) =
  ((Representation.trivial ℂ SL(2, ℂ) ℂ) M ∘ₗ TensorProduct.lift contrCoContrBi) (ψ ⊗ₜ[ℂ] φ)
    change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M)) *ᵥ ψ.toFin13ℂ) ⬝ᵥ
      ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ φ.toFin13ℂ) =
        ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂM:SL(2, ℂ)ψ:ContrℂModuleφ:CoℂModule⊢ LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ ψ.toFin13ℂ ⬝ᵥ
    (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ φ.toFin13ℂ =
  ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ
    rw [dotProduct_mulVec,M:SL(2, ℂ)ψ:ContrℂModuleφ:CoℂModule⊢ (LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ ψ.toFin13ℂ) ᵥ* (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ ⬝ᵥ
    φ.toFin13ℂ =
  ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂM:SL(2, ℂ)ψ:ContrℂModuleφ:CoℂModule⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ * LorentzGroup.toComplex (SL2C.toLorentzGroup M)) *ᵥ ψ.toFin13ℂ ⬝ᵥ
    φ.toFin13ℂ =
  ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ vecMul_transpose,M:SL(2, ℂ)ψ:ContrℂModuleφ:CoℂModule⊢ (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ *ᵥ LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ ψ.toFin13ℂ ⬝ᵥ
    φ.toFin13ℂ =
  ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂM:SL(2, ℂ)ψ:ContrℂModuleφ:CoℂModule⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ * LorentzGroup.toComplex (SL2C.toLorentzGroup M)) *ᵥ ψ.toFin13ℂ ⬝ᵥ
    φ.toFin13ℂ =
  ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ mulVec_mulVecM:SL(2, ℂ)ψ:ContrℂModuleφ:CoℂModule⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ * LorentzGroup.toComplex (SL2C.toLorentzGroup M)) *ᵥ ψ.toFin13ℂ ⬝ᵥ
    φ.toFin13ℂ =
  ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂM:SL(2, ℂ)ψ:ContrℂModuleφ:CoℂModule⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ * LorentzGroup.toComplex (SL2C.toLorentzGroup M)) *ᵥ ψ.toFin13ℂ ⬝ᵥ
    φ.toFin13ℂ =
  ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ]M:SL(2, ℂ)ψ:ContrℂModuleφ:CoℂModule⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ * LorentzGroup.toComplex (SL2C.toLorentzGroup M)) *ᵥ ψ.toFin13ℂ ⬝ᵥ
    φ.toFin13ℂ =
  ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ
    rw [inv_mul_of_invertible (LorentzGroup.toComplex (SL2C.toLorentzGroup M))M:SL(2, ℂ)ψ:ContrℂModuleφ:CoℂModule⊢ 1 *ᵥ ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ = ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂM:SL(2, ℂ)ψ:ContrℂModuleφ:CoℂModule⊢ 1 *ᵥ ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ = ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ]M:SL(2, ℂ)ψ:ContrℂModuleφ:CoℂModule⊢ 1 *ᵥ ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ = ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ
    simpAll goals completed! 🐙

              lemma contrCoContraction_hom_tmul (ψ : ContrℂModule) (φ : CoℂModule) :
    contrCoContraction (ψ ⊗ₜ φ) = ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ := byψ:ContrℂModuleφ:CoℂModule⊢ contrCoContraction (ψ ⊗ₜ[ℂ] φ) = ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ
  rflAll goals completed! 🐙

lemma contrCoContraction_basis (i j : Fin 4) :
    contrCoContraction (complexContrBasisFin4 i ⊗ₜ complexCoBasisFin4 j) =
    if i.1 = j.1 then (1 : ℂ) else 0 := byi:Fin 4j:Fin 4⊢ contrCoContraction (complexContrBasisFin4 i ⊗ₜ[ℂ] complexCoBasisFin4 j) = if ↑i = ↑j then 1 else 0
  rw [contrCoContraction_hom_tmuli:Fin 4j:Fin 4⊢ (complexContrBasisFin4 i).toFin13ℂ ⬝ᵥ (complexCoBasisFin4 j).toFin13ℂ = if ↑i = ↑j then 1 else 0i:Fin 4j:Fin 4⊢ (complexContrBasisFin4 i).toFin13ℂ ⬝ᵥ (complexCoBasisFin4 j).toFin13ℂ = if ↑i = ↑j then 1 else 0]i:Fin 4j:Fin 4⊢ (complexContrBasisFin4 i).toFin13ℂ ⬝ᵥ (complexCoBasisFin4 j).toFin13ℂ = if ↑i = ↑j then 1 else 0
  simp only [complexContrBasisFin4, Basis.coe_reindex, Function.comp_apply,
    complexContrBasis_toFin13ℂ, complexCoBasisFin4, complexCoBasis_toFin13ℂ, dotProduct_single,
    mul_one]i:Fin 4j:Fin 4⊢ Pi.single (finSumFinEquiv.symm i) 1 (finSumFinEquiv.symm j) = if ↑i = ↑j then 1 else 0
  rw [Pi.single_applyi:Fin 4j:Fin 4⊢ (if finSumFinEquiv.symm j = finSumFinEquiv.symm i then 1 else 0) = if ↑i = ↑j then 1 else 0i:Fin 4j:Fin 4⊢ (if finSumFinEquiv.symm j = finSumFinEquiv.symm i then 1 else 0) = if ↑i = ↑j then 1 else 0]i:Fin 4j:Fin 4⊢ (if finSumFinEquiv.symm j = finSumFinEquiv.symm i then 1 else 0) = if ↑i = ↑j then 1 else 0
  refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)h₁i:Fin 4j:Fin 4⊢ (finSumFinEquiv.symm j = finSumFinEquiv.symm i) = (↑i = ↑j)
  simp only [EmbeddingLike.apply_eq_iff_eq, Fin.ext_iff, eq_comm]All goals completed! 🐙

lemma contrCoContraction_basis' (i j : Fin 1 ⊕ Fin 3) :
    contrCoContraction (complexContrBasis i ⊗ₜ complexCoBasis j) =
    if i = j then (1 : ℂ) else 0 := byi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ contrCoContraction (complexContrBasis i ⊗ₜ[ℂ] complexCoBasis j) = if i = j then 1 else 0
  rw [contrCoContraction_hom_tmuli:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (complexContrBasis i).toFin13ℂ ⬝ᵥ (complexCoBasis j).toFin13ℂ = if i = j then 1 else 0i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (complexContrBasis i).toFin13ℂ ⬝ᵥ (complexCoBasis j).toFin13ℂ = if i = j then 1 else 0]i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (complexContrBasis i).toFin13ℂ ⬝ᵥ (complexCoBasis j).toFin13ℂ = if i = j then 1 else 0
  simp only [complexContrBasis_toFin13ℂ, complexCoBasis_toFin13ℂ, dotProduct_single, mul_one]i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 j = if i = j then 1 else 0
  rw [Pi.single_applyi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (if j = i then 1 else 0) = if i = j then 1 else 0i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (if j = i then 1 else 0) = if i = j then 1 else 0]i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (if j = i then 1 else 0) = if i = j then 1 else 0
  refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)h₁i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (j = i) = (i = j)
  exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)All goals completed! 🐙

The linear map from complexCo ⊗ complexContr to ℂ given by summing over components of covariant Lorentz vector and contravariant Lorentz vector in the standard basis (i.e. the dot product). In terms of index notation this is the contraction is φᵢ ψⁱ.


def coContrContraction : (CoℂModule.SL2CRep.tprod ContrℂModule.SL2CRep).IntertwiningMap
    (Representation.trivial ℂ SL(2,ℂ) ℂ) where
  toLinearMap := TensorProduct.lift contrContrCoBi
  isIntertwining' M := TensorProduct.ext' fun φ ψ => byM:SL(2, ℂ)φ:CoℂModuleψ:ContrℂModule⊢ (TensorProduct.lift contrContrCoBi ∘ₗ (CoℂModule.SL2CRep.tprod ContrℂModule.SL2CRep) M) (φ ⊗ₜ[ℂ] ψ) =
  ((Representation.trivial ℂ SL(2, ℂ) ℂ) M ∘ₗ TensorProduct.lift contrContrCoBi) (φ ⊗ₜ[ℂ] ψ)
    change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ φ.toFin13ℂ) ⬝ᵥ
      ((LorentzGroup.toComplex (SL2C.toLorentzGroup M)) *ᵥ ψ.toFin13ℂ) = φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂM:SL(2, ℂ)φ:CoℂModuleψ:ContrℂModule⊢ (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ φ.toFin13ℂ ⬝ᵥ
    LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ ψ.toFin13ℂ =
  φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ
    rw [dotProduct_mulVec,M:SL(2, ℂ)φ:CoℂModuleψ:ContrℂModule⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ φ.toFin13ℂ) ᵥ* LorentzGroup.toComplex (SL2C.toLorentzGroup M) ⬝ᵥ
    ψ.toFin13ℂ =
  φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂM:SL(2, ℂ)φ:CoℂModuleψ:ContrℂModule⊢ φ.toFin13ℂ ᵥ* ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ * LorentzGroup.toComplex (SL2C.toLorentzGroup M)) ⬝ᵥ
    ψ.toFin13ℂ =
  φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ mulVec_transpose,M:SL(2, ℂ)φ:CoℂModuleψ:ContrℂModule⊢ φ.toFin13ℂ ᵥ* (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ ᵥ* LorentzGroup.toComplex (SL2C.toLorentzGroup M) ⬝ᵥ
    ψ.toFin13ℂ =
  φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂM:SL(2, ℂ)φ:CoℂModuleψ:ContrℂModule⊢ φ.toFin13ℂ ᵥ* ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ * LorentzGroup.toComplex (SL2C.toLorentzGroup M)) ⬝ᵥ
    ψ.toFin13ℂ =
  φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ vecMul_vecMulM:SL(2, ℂ)φ:CoℂModuleψ:ContrℂModule⊢ φ.toFin13ℂ ᵥ* ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ * LorentzGroup.toComplex (SL2C.toLorentzGroup M)) ⬝ᵥ
    ψ.toFin13ℂ =
  φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂM:SL(2, ℂ)φ:CoℂModuleψ:ContrℂModule⊢ φ.toFin13ℂ ᵥ* ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ * LorentzGroup.toComplex (SL2C.toLorentzGroup M)) ⬝ᵥ
    ψ.toFin13ℂ =
  φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ]M:SL(2, ℂ)φ:CoℂModuleψ:ContrℂModule⊢ φ.toFin13ℂ ᵥ* ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ * LorentzGroup.toComplex (SL2C.toLorentzGroup M)) ⬝ᵥ
    ψ.toFin13ℂ =
  φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ
    rw [inv_mul_of_invertible (LorentzGroup.toComplex (SL2C.toLorentzGroup M))M:SL(2, ℂ)φ:CoℂModuleψ:ContrℂModule⊢ φ.toFin13ℂ ᵥ* 1 ⬝ᵥ ψ.toFin13ℂ = φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂM:SL(2, ℂ)φ:CoℂModuleψ:ContrℂModule⊢ φ.toFin13ℂ ᵥ* 1 ⬝ᵥ ψ.toFin13ℂ = φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ]M:SL(2, ℂ)φ:CoℂModuleψ:ContrℂModule⊢ φ.toFin13ℂ ᵥ* 1 ⬝ᵥ ψ.toFin13ℂ = φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ
    simpAll goals completed! 🐙

              lemma coContrContraction_hom_tmul (φ : CoℂModule) (ψ : ContrℂModule) :
    coContrContraction (φ ⊗ₜ ψ) = φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ := byφ:CoℂModuleψ:ContrℂModule⊢ coContrContraction (φ ⊗ₜ[ℂ] ψ) = φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ
  rflAll goals completed! 🐙

lemma coContrContraction_basis (i j : Fin 4) :
    coContrContraction (complexCoBasisFin4 i ⊗ₜ complexContrBasisFin4 j) =
    if i.1 = j.1 then (1 : ℂ) else 0 := byi:Fin 4j:Fin 4⊢ coContrContraction (complexCoBasisFin4 i ⊗ₜ[ℂ] complexContrBasisFin4 j) = if ↑i = ↑j then 1 else 0
  rw [coContrContraction_hom_tmuli:Fin 4j:Fin 4⊢ (complexCoBasisFin4 i).toFin13ℂ ⬝ᵥ (complexContrBasisFin4 j).toFin13ℂ = if ↑i = ↑j then 1 else 0i:Fin 4j:Fin 4⊢ (complexCoBasisFin4 i).toFin13ℂ ⬝ᵥ (complexContrBasisFin4 j).toFin13ℂ = if ↑i = ↑j then 1 else 0]i:Fin 4j:Fin 4⊢ (complexCoBasisFin4 i).toFin13ℂ ⬝ᵥ (complexContrBasisFin4 j).toFin13ℂ = if ↑i = ↑j then 1 else 0
  simp only [complexCoBasisFin4, Basis.coe_reindex, Function.comp_apply, complexCoBasis_toFin13ℂ,
    complexContrBasisFin4, complexContrBasis_toFin13ℂ, dotProduct_single, mul_one]i:Fin 4j:Fin 4⊢ Pi.single (finSumFinEquiv.symm i) 1 (finSumFinEquiv.symm j) = if ↑i = ↑j then 1 else 0
  rw [Pi.single_applyi:Fin 4j:Fin 4⊢ (if finSumFinEquiv.symm j = finSumFinEquiv.symm i then 1 else 0) = if ↑i = ↑j then 1 else 0i:Fin 4j:Fin 4⊢ (if finSumFinEquiv.symm j = finSumFinEquiv.symm i then 1 else 0) = if ↑i = ↑j then 1 else 0]i:Fin 4j:Fin 4⊢ (if finSumFinEquiv.symm j = finSumFinEquiv.symm i then 1 else 0) = if ↑i = ↑j then 1 else 0
  refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)h₁i:Fin 4j:Fin 4⊢ (finSumFinEquiv.symm j = finSumFinEquiv.symm i) = (↑i = ↑j)
  simp only [eq_comm, EmbeddingLike.apply_eq_iff_eq, Fin.ext_iff]All goals completed! 🐙

lemma coContrContraction_basis' (i j : Fin 1 ⊕ Fin 3) :
    coContrContraction (complexCoBasis i ⊗ₜ complexContrBasis j) =
    if i = j then (1 : ℂ) else 0 := byi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ coContrContraction (complexCoBasis i ⊗ₜ[ℂ] complexContrBasis j) = if i = j then 1 else 0
  rw [coContrContraction_hom_tmuli:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (complexCoBasis i).toFin13ℂ ⬝ᵥ (complexContrBasis j).toFin13ℂ = if i = j then 1 else 0i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (complexCoBasis i).toFin13ℂ ⬝ᵥ (complexContrBasis j).toFin13ℂ = if i = j then 1 else 0]i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (complexCoBasis i).toFin13ℂ ⬝ᵥ (complexContrBasis j).toFin13ℂ = if i = j then 1 else 0
  simp only [complexCoBasis_toFin13ℂ, complexContrBasis_toFin13ℂ, dotProduct_single, mul_one]i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 j = if i = j then 1 else 0
  rw [Pi.single_applyi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (if j = i then 1 else 0) = if i = j then 1 else 0i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (if j = i then 1 else 0) = if i = j then 1 else 0]i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (if j = i then 1 else 0) = if i = j then 1 else 0
  refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)h₁i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (j = i) = (i = j)
  simp only [eq_comm]All goals completed! 🐙

Symmetry



lemma contrCoContraction_tmul_symm (φ : ContrℂModule) (ψ : CoℂModule) :
    contrCoContraction (φ ⊗ₜ ψ) = coContrContraction (ψ ⊗ₜ φ) := byφ:ContrℂModuleψ:CoℂModule⊢ contrCoContraction (φ ⊗ₜ[ℂ] ψ) = coContrContraction (ψ ⊗ₜ[ℂ] φ)
  rw [contrCoContraction_hom_tmul,φ:ContrℂModuleψ:CoℂModule⊢ φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ = coContrContraction (ψ ⊗ₜ[ℂ] φ)All goals completed! 🐙 coContrContraction_hom_tmul,φ:ContrℂModuleψ:CoℂModule⊢ φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ = ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂAll goals completed! 🐙 dotProduct_commφ:ContrℂModuleψ:CoℂModule⊢ ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ = ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂAll goals completed! 🐙]All goals completed! 🐙



lemma coContrContraction_tmul_symm (φ : CoℂModule) (ψ : ContrℂModule) :
    coContrContraction (φ ⊗ₜ ψ) = contrCoContraction (ψ ⊗ₜ φ) := byφ:CoℂModuleψ:ContrℂModule⊢ coContrContraction (φ ⊗ₜ[ℂ] ψ) = contrCoContraction (ψ ⊗ₜ[ℂ] φ)
  rw [contrCoContraction_tmul_symmφ:CoℂModuleψ:ContrℂModule⊢ coContrContraction (φ ⊗ₜ[ℂ] ψ) = coContrContraction (φ ⊗ₜ[ℂ] ψ)All goals completed! 🐙]All goals completed! 🐙