Physlib.Relativity.Tensors.ComplexTensor.Vector.Pre.Basic

Imports

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

public import Physlib.Relativity.Tensors.ComplexTensor.Vector.Pre.Modules

Complex Lorentz vectors

We define complex Lorentz vectors in 4d space-time as representations of SL(2, C).

@[expose] public section

The standard basis of complex contravariant Lorentz vectors.

def complexContrBasis : Basis (Fin 1 ⊕ Fin 3) ℂ ContrℂModule :=
  Basis.ofEquivFun ContrℂModule.toFin13ℂEquiv

              @[simp]
lemma complexContrBasis_toFin13ℂ (i :Fin 1 ⊕ Fin 3) :
    (complexContrBasis i).toFin13ℂ = Pi.single i 1 := byi:Fin 1 ⊕ Fin 3⊢ (complexContrBasis i).toFin13ℂ = Pi.single i 1
  simp only [complexContrBasis, Basis.coe_ofEquivFun]i:Fin 1 ⊕ Fin 3⊢ (ContrℂModule.toFin13ℂEquiv.symm (Pi.single i 1)).toFin13ℂ = Pi.single i 1
  rflAll goals completed! 🐙

@[simp]
lemma complexContrBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 1 ⊕ Fin 3) :
    (LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) i j =
    (LorentzGroup.toComplex (SL2C.toLorentzGroup M)) i j := byM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (LinearMap.toMatrix complexContrBasis complexContrBasis) (ContrℂModule.SL2CRep M) i j =
  LorentzGroup.toComplex (SL2C.toLorentzGroup M) i j
  rw [LinearMap.toMatrix_applyM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (complexContrBasis.repr ((ContrℂModule.SL2CRep M) (complexContrBasis j))) i =
  LorentzGroup.toComplex (SL2C.toLorentzGroup M) i jM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (complexContrBasis.repr ((ContrℂModule.SL2CRep M) (complexContrBasis j))) i =
  LorentzGroup.toComplex (SL2C.toLorentzGroup M) i j]M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (complexContrBasis.repr ((ContrℂModule.SL2CRep M) (complexContrBasis j))) i =
  LorentzGroup.toComplex (SL2C.toLorentzGroup M) i j
  simp only [complexContrBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply]M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ ContrℂModule.toFin13ℂEquiv ((ContrℂModule.SL2CRep M) (ContrℂModule.toFin13ℂEquiv.symm (Pi.single j 1))) i =
  LorentzGroup.toComplex (SL2C.toLorentzGroup M) i j
  change (((LorentzGroup.toComplex (SL2C.toLorentzGroup M))) *ᵥ (Pi.single j 1)) i = _M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ Pi.single j 1) i = LorentzGroup.toComplex (SL2C.toLorentzGroup M) i j
  simpAll goals completed! 🐙lemma complexContrBasis_ρ_val (M : SL(2,ℂ)) (v : ContrℂModule) :
    ((ContrℂModule.SL2CRep M) v).val =
    LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ v.val := byM:SL(2, ℂ)v:ContrℂModule⊢ ((ContrℂModule.SL2CRep M) v).val = LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ v.val
  rflAll goals completed! 🐙

The standard basis of complex contravariant Lorentz vectors indexed by Fin 4.

def complexContrBasisFin4 : Basis (Fin 4) ℂ ContrℂModule :=
  Basis.reindex complexContrBasis finSumFinEquiv

              lemma complexContrBasisFin4_eq_reindex :
    complexContrBasisFin4 = complexContrBasis.reindex finSumFinEquiv :=
  rfllemma complexContrBasis_reindex_apply_eq_fin4 (j : Fin 4) :
    (complexContrBasis.reindex finSumFinEquiv) j = complexContrBasisFin4 j :=
  rfl@[simp]
lemma complexContrBasisFin4_apply_zero :
    complexContrBasisFin4 0 = complexContrBasis (Sum.inl 0) := by⊢ complexContrBasisFin4 0 = complexContrBasis (Sum.inl 0)
  simp only [complexContrBasisFin4, Basis.reindex_apply]⊢ complexContrBasis (finSumFinEquiv.symm 0) = complexContrBasis (Sum.inl 0)
  rflAll goals completed! 🐙@[simp]
lemma complexContrBasisFin4_apply_one :
    complexContrBasisFin4 1 = complexContrBasis (Sum.inr 0) := by⊢ complexContrBasisFin4 1 = complexContrBasis (Sum.inr 0)
  simp only [complexContrBasisFin4, Basis.reindex_apply]⊢ complexContrBasis (finSumFinEquiv.symm 1) = complexContrBasis (Sum.inr 0)
  rflAll goals completed! 🐙@[simp]
lemma complexContrBasisFin4_apply_two :
    complexContrBasisFin4 2 = complexContrBasis (Sum.inr 1) := by⊢ complexContrBasisFin4 2 = complexContrBasis (Sum.inr 1)
  simp only [complexContrBasisFin4, Basis.reindex_apply]⊢ complexContrBasis (finSumFinEquiv.symm 2) = complexContrBasis (Sum.inr 1)
  rflAll goals completed! 🐙@[simp]
lemma complexContrBasisFin4_apply_three :
    complexContrBasisFin4 3 = complexContrBasis (Sum.inr 2) := by⊢ complexContrBasisFin4 3 = complexContrBasis (Sum.inr 2)
  simp only [complexContrBasisFin4, Basis.reindex_apply]⊢ complexContrBasis (finSumFinEquiv.symm 3) = complexContrBasis (Sum.inr 2)
  rflAll goals completed! 🐙@[simp]
lemma complexContrBasisFin4_apply_succ (i : Fin 3) :
    complexContrBasisFin4 i.succ = complexContrBasis (Sum.inr i) := byi:Fin 3⊢ complexContrBasisFin4 i.succ = complexContrBasis (Sum.inr i)
  simp only [complexContrBasisFin4, Basis.reindex_apply]i:Fin 3⊢ complexContrBasis (finSumFinEquiv.symm i.succ) = complexContrBasis (Sum.inr i)
  congr 1e_6i:Fin 3⊢ finSumFinEquiv.symm i.succ = Sum.inr i
  fin_cases ie_6.«0»⊢ finSumFinEquiv.symm ((fun i => i) ⟨0, ⋯⟩).succ = Sum.inr ((fun i => i) ⟨0, ⋯⟩)e_6.«1»⊢ finSumFinEquiv.symm ((fun i => i) ⟨1, ⋯⟩).succ = Sum.inr ((fun i => i) ⟨1, ⋯⟩)e_6.«2»⊢ finSumFinEquiv.symm ((fun i => i) ⟨2, ⋯⟩).succ = Sum.inr ((fun i => i) ⟨2, ⋯⟩) <;>e_6.«0»⊢ finSumFinEquiv.symm ((fun i => i) ⟨0, ⋯⟩).succ = Sum.inr ((fun i => i) ⟨0, ⋯⟩)e_6.«1»⊢ finSumFinEquiv.symm ((fun i => i) ⟨1, ⋯⟩).succ = Sum.inr ((fun i => i) ⟨1, ⋯⟩)e_6.«2»⊢ finSumFinEquiv.symm ((fun i => i) ⟨2, ⋯⟩).succ = Sum.inr ((fun i => i) ⟨2, ⋯⟩) decideAll goals completed! 🐙

The standard basis of complex covariant Lorentz vectors.

def complexCoBasis : Basis (Fin 1 ⊕ Fin 3) ℂ CoℂModule :=
  Basis.ofEquivFun CoℂModule.toFin13ℂEquiv

              @[simp]
lemma complexCoBasis_toFin13ℂ (i :Fin 1 ⊕ Fin 3) : (complexCoBasis i).toFin13ℂ = Pi.single i 1 := byi:Fin 1 ⊕ Fin 3⊢ (complexCoBasis i).toFin13ℂ = Pi.single i 1
  simp only [complexCoBasis, Basis.coe_ofEquivFun]i:Fin 1 ⊕ Fin 3⊢ (CoℂModule.toFin13ℂEquiv.symm (Pi.single i 1)).toFin13ℂ = Pi.single i 1
  rflAll goals completed! 🐙

@[simp]
lemma complexCoBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 1 ⊕ Fin 3) :
    (LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) i j =
    (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ i j := byM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (LinearMap.toMatrix complexCoBasis complexCoBasis) (CoℂModule.SL2CRep M) i j =
  (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ i j
  rw [LinearMap.toMatrix_applyM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (complexCoBasis.repr ((CoℂModule.SL2CRep M) (complexCoBasis j))) i =
  (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ i jM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (complexCoBasis.repr ((CoℂModule.SL2CRep M) (complexCoBasis j))) i =
  (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ i j]M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (complexCoBasis.repr ((CoℂModule.SL2CRep M) (complexCoBasis j))) i =
  (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ i j
  simp only [complexCoBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply, transpose_apply]M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ CoℂModule.toFin13ℂEquiv ((CoℂModule.SL2CRep M) (CoℂModule.toFin13ℂEquiv.symm (Pi.single j 1))) i =
  (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ j i
  change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ (Pi.single j 1)) i = _M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ Pi.single j 1) i =
  (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ j i
  simpAll goals completed! 🐙lemma CoℂModule.SL2CRep_val (M : SL(2,ℂ)) (v : CoℂModule) :
    ((CoℂModule.SL2CRep M) v).val =
    (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ v.val := byM:SL(2, ℂ)v:CoℂModule⊢ ((SL2CRep M) v).val = (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ v.val
  rflAll goals completed! 🐙

The standard basis of complex covariant Lorentz vectors indexed by Fin 4.

def complexCoBasisFin4 : Basis (Fin 4) ℂ CoℂModule :=
  Basis.reindex complexCoBasis finSumFinEquiv

              lemma complexCoBasisFin4_eq_reindex :
    complexCoBasisFin4 = complexCoBasis.reindex finSumFinEquiv :=
  rfllemma complexCoBasis_reindex_apply_eq_fin4 (j : Fin 4) :
    (complexCoBasis.reindex finSumFinEquiv) j = complexCoBasisFin4 j :=
  rfl@[simp]
lemma complexCoBasisFin4_apply_zero :
    complexCoBasisFin4 0 = complexCoBasis (Sum.inl 0) := by⊢ complexCoBasisFin4 0 = complexCoBasis (Sum.inl 0)
  simp only [complexCoBasisFin4, Basis.reindex_apply]⊢ complexCoBasis (finSumFinEquiv.symm 0) = complexCoBasis (Sum.inl 0)
  rflAll goals completed! 🐙@[simp]
lemma complexCoBasisFin4_apply_one :
    complexCoBasisFin4 1 = complexCoBasis (Sum.inr 0) := by⊢ complexCoBasisFin4 1 = complexCoBasis (Sum.inr 0)
  simp only [complexCoBasisFin4, Basis.reindex_apply]⊢ complexCoBasis (finSumFinEquiv.symm 1) = complexCoBasis (Sum.inr 0)
  rflAll goals completed! 🐙@[simp]
lemma complexCoBasisFin4_apply_two :
    complexCoBasisFin4 2 = complexCoBasis (Sum.inr 1) := by⊢ complexCoBasisFin4 2 = complexCoBasis (Sum.inr 1)
  simp only [complexCoBasisFin4, Basis.reindex_apply]⊢ complexCoBasis (finSumFinEquiv.symm 2) = complexCoBasis (Sum.inr 1)
  rflAll goals completed! 🐙@[simp]
lemma complexCoBasisFin4_apply_three :
    complexCoBasisFin4 3 = complexCoBasis (Sum.inr 2) := by⊢ complexCoBasisFin4 3 = complexCoBasis (Sum.inr 2)
  simp only [complexCoBasisFin4, Basis.reindex_apply]⊢ complexCoBasis (finSumFinEquiv.symm 3) = complexCoBasis (Sum.inr 2)
  rflAll goals completed! 🐙

Relation to real

The semilinear map including real Lorentz vectors into complex contravariant lorentz vectors.


def inclCongrRealLorentz : ContrMod 3 →ₛₗ[Complex.ofRealHom] ContrℂModule where
  toFun v := {val := ofReal ∘ v.toFin1dℝ}
  map_add' x y := byx:ContrMod 3y:ContrMod 3⊢ { val := ofReal ∘ (x + y).toFin1dℝ } = { val := ofReal ∘ x.toFin1dℝ } + { val := ofReal ∘ y.toFin1dℝ }
    apply Lorentz.ContrℂModule.extx:ContrMod 3y:ContrMod 3⊢ { val := ofReal ∘ (x + y).toFin1dℝ }.val = ({ val := ofReal ∘ x.toFin1dℝ } + { val := ofReal ∘ y.toFin1dℝ }).val
    rw [Lorentz.ContrℂModule.val_addx:ContrMod 3y:ContrMod 3⊢ { val := ofReal ∘ (x + y).toFin1dℝ }.val = { val := ofReal ∘ x.toFin1dℝ }.val + { val := ofReal ∘ y.toFin1dℝ }.valx:ContrMod 3y:ContrMod 3⊢ { val := ofReal ∘ (x + y).toFin1dℝ }.val = { val := ofReal ∘ x.toFin1dℝ }.val + { val := ofReal ∘ y.toFin1dℝ }.val]x:ContrMod 3y:ContrMod 3⊢ { val := ofReal ∘ (x + y).toFin1dℝ }.val = { val := ofReal ∘ x.toFin1dℝ }.val + { val := ofReal ∘ y.toFin1dℝ }.val
    funext ix:ContrMod 3y:ContrMod 3i:Fin 1 ⊕ Fin 3⊢ { val := ofReal ∘ (x + y).toFin1dℝ }.val i = ({ val := ofReal ∘ x.toFin1dℝ }.val + { val := ofReal ∘ y.toFin1dℝ }.val) i
    simp only [Function.comp_apply, Pi.add_apply, map_add]x:ContrMod 3y:ContrMod 3i:Fin 1 ⊕ Fin 3⊢ ↑(ContrMod.toFin1dℝEquiv x i + ContrMod.toFin1dℝEquiv y i) = ↑(x.toFin1dℝ i) + ↑(y.toFin1dℝ i)
    simp only [ofReal_add]All goals completed! 🐙
  map_smul' c x := byc:ℝx:ContrMod 3⊢ { val := ofReal ∘ (c • x).toFin1dℝ } = ofRealHom c • { val := ofReal ∘ x.toFin1dℝ }
    apply Lorentz.ContrℂModule.extc:ℝx:ContrMod 3⊢ { val := ofReal ∘ (c • x).toFin1dℝ }.val = (ofRealHom c • { val := ofReal ∘ x.toFin1dℝ }).val
    rw [Lorentz.ContrℂModule.val_smulc:ℝx:ContrMod 3⊢ { val := ofReal ∘ (c • x).toFin1dℝ }.val = ofRealHom c • { val := ofReal ∘ x.toFin1dℝ }.valc:ℝx:ContrMod 3⊢ { val := ofReal ∘ (c • x).toFin1dℝ }.val = ofRealHom c • { val := ofReal ∘ x.toFin1dℝ }.val]c:ℝx:ContrMod 3⊢ { val := ofReal ∘ (c • x).toFin1dℝ }.val = ofRealHom c • { val := ofReal ∘ x.toFin1dℝ }.val
    funext ic:ℝx:ContrMod 3i:Fin 1 ⊕ Fin 3⊢ { val := ofReal ∘ (c • x).toFin1dℝ }.val i = (ofRealHom c • { val := ofReal ∘ x.toFin1dℝ }.val) i
    simp only [Function.comp_apply, ofRealHom_eq_coe, Pi.smul_apply, _root_.map_smul]c:ℝx:ContrMod 3i:Fin 1 ⊕ Fin 3⊢ ↑(c • ContrMod.toFin1dℝEquiv x i) = ↑c • ↑(x.toFin1dℝ i)
    simp only [smul_eq_mul, ofReal_mul]All goals completed! 🐙

              lemma inclCongrRealLorentz_val (v : ContrMod 3) :
    (inclCongrRealLorentz v).val = ofRealHom ∘ v.toFin1dℝ := rfl

lemma complexContrBasis_of_real (i : Fin 1 ⊕ Fin 3) :
    (complexContrBasis i) = inclCongrRealLorentz (ContrMod.stdBasis i) := byi:Fin 1 ⊕ Fin 3⊢ complexContrBasis i = inclCongrRealLorentz (ContrMod.stdBasis i)
  apply Lorentz.ContrℂModule.exti:Fin 1 ⊕ Fin 3⊢ (complexContrBasis i).val = (inclCongrRealLorentz (ContrMod.stdBasis i)).val
  simp only [complexContrBasis, Basis.coe_ofEquivFun, inclCongrRealLorentz,
    LinearMap.coe_mk, AddHom.coe_mk]i:Fin 1 ⊕ Fin 3⊢ (ContrℂModule.toFin13ℂEquiv.symm (Pi.single i 1)).val = ofReal ∘ (ContrMod.stdBasis i).toFin1dℝ
  ext ji:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (ContrℂModule.toFin13ℂEquiv.symm (Pi.single i 1)).val j = (ofReal ∘ (ContrMod.stdBasis i).toFin1dℝ) j
  simp only [Function.comp_apply]i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (ContrℂModule.toFin13ℂEquiv.symm (Pi.single i 1)).val j = ↑((ContrMod.stdBasis i).toFin1dℝ j)
  change (Pi.single i 1) j = _i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 j = ↑((ContrMod.stdBasis i).toFin1dℝ j)
  by_cases h : i = jposi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:i = j⊢ Pi.single i 1 j = ↑((ContrMod.stdBasis i).toFin1dℝ j)negi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:¬i = j⊢ Pi.single i 1 j = ↑((ContrMod.stdBasis i).toFin1dℝ j)
  ·posi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:i = j⊢ Pi.single i 1 j = ↑((ContrMod.stdBasis i).toFin1dℝ j) subst hposi:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 i = ↑((ContrMod.stdBasis i).toFin1dℝ i)
    rw [ContrMod.toFin1dℝ,posi:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 i = ↑(ContrMod.toFin1dℝEquiv (ContrMod.stdBasis i) i)posi:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 i = ↑1 ContrMod.stdBasis_toFin1dℝEquiv_apply_sameposi:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 i = ↑1posi:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 i = ↑1]posi:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 i = ↑1
    simpAll goals completed! 🐙
  ·negi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:¬i = j⊢ Pi.single i 1 j = ↑((ContrMod.stdBasis i).toFin1dℝ j) rw [ContrMod.toFin1dℝ,negi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:¬i = j⊢ Pi.single i 1 j = ↑(ContrMod.toFin1dℝEquiv (ContrMod.stdBasis i) j)negi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:¬i = j⊢ Pi.single i 1 j = ↑0 ContrMod.stdBasis_toFin1dℝEquiv_apply_ne hnegi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:¬i = j⊢ Pi.single i 1 j = ↑0negi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:¬i = j⊢ Pi.single i 1 j = ↑0]negi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:¬i = j⊢ Pi.single i 1 j = ↑0
    simp [h]All goals completed! 🐙

lemma inclCongrRealLorentz_ρ (M : SL(2, ℂ)) (v : ContrMod 3) :
    (ContrℂModule.SL2CRep M) (inclCongrRealLorentz v) =
    inclCongrRealLorentz (ContrMod.rep (SL2C.toLorentzGroup M) v) := byM:SL(2, ℂ)v:ContrMod 3⊢ (ContrℂModule.SL2CRep M) (inclCongrRealLorentz v) = inclCongrRealLorentz ((ContrMod.rep (SL2C.toLorentzGroup M)) v)
  apply Lorentz.ContrℂModule.extM:SL(2, ℂ)v:ContrMod 3⊢ ((ContrℂModule.SL2CRep M) (inclCongrRealLorentz v)).val =
  (inclCongrRealLorentz ((ContrMod.rep (SL2C.toLorentzGroup M)) v)).val
  rw [complexContrBasis_ρ_val,M:SL(2, ℂ)v:ContrMod 3⊢ LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ (inclCongrRealLorentz v).val =
  (inclCongrRealLorentz ((ContrMod.rep (SL2C.toLorentzGroup M)) v)).valM:SL(2, ℂ)v:ContrMod 3⊢ LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ =
  ⇑ofRealHom ∘ ((ContrMod.rep (SL2C.toLorentzGroup M)) v).toFin1dℝ inclCongrRealLorentz_val,M:SL(2, ℂ)v:ContrMod 3⊢ LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ =
  (inclCongrRealLorentz ((ContrMod.rep (SL2C.toLorentzGroup M)) v)).valM:SL(2, ℂ)v:ContrMod 3⊢ LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ =
  ⇑ofRealHom ∘ ((ContrMod.rep (SL2C.toLorentzGroup M)) v).toFin1dℝ inclCongrRealLorentz_valM:SL(2, ℂ)v:ContrMod 3⊢ LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ =
  ⇑ofRealHom ∘ ((ContrMod.rep (SL2C.toLorentzGroup M)) v).toFin1dℝM:SL(2, ℂ)v:ContrMod 3⊢ LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ =
  ⇑ofRealHom ∘ ((ContrMod.rep (SL2C.toLorentzGroup M)) v).toFin1dℝ]M:SL(2, ℂ)v:ContrMod 3⊢ LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ =
  ⇑ofRealHom ∘ ((ContrMod.rep (SL2C.toLorentzGroup M)) v).toFin1dℝ
  rw [LorentzGroup.toComplex_mulVec_ofRealM:SL(2, ℂ)v:ContrMod 3⊢ ⇑ofRealHom ∘ (↑(SL2C.toLorentzGroup M) *ᵥ v.toFin1dℝ) = ⇑ofRealHom ∘ ((ContrMod.rep (SL2C.toLorentzGroup M)) v).toFin1dℝM:SL(2, ℂ)v:ContrMod 3⊢ ⇑ofRealHom ∘ (↑(SL2C.toLorentzGroup M) *ᵥ v.toFin1dℝ) = ⇑ofRealHom ∘ ((ContrMod.rep (SL2C.toLorentzGroup M)) v).toFin1dℝ]M:SL(2, ℂ)v:ContrMod 3⊢ ⇑ofRealHom ∘ (↑(SL2C.toLorentzGroup M) *ᵥ v.toFin1dℝ) = ⇑ofRealHom ∘ ((ContrMod.rep (SL2C.toLorentzGroup M)) v).toFin1dℝ
  rflAll goals completed! 🐙

lemma SL2CRep_ρ_basis (M : SL(2, ℂ)) (i : Fin 1 ⊕ Fin 3) :
    (ContrℂModule.SL2CRep M) (complexContrBasis i) =
    ∑ j, (SL2C.toLorentzGroup M).1 j i •
    complexContrBasis j := byM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ (ContrℂModule.SL2CRep M) (complexContrBasis i) = ∑ j, ↑(SL2C.toLorentzGroup M) j i • complexContrBasis j
  rw [complexContrBasis_of_real,M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ (ContrℂModule.SL2CRep M) (inclCongrRealLorentz (ContrMod.stdBasis i)) =
  ∑ j, ↑(SL2C.toLorentzGroup M) j i • complexContrBasis jM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ inclCongrRealLorentz ((ContrMod.rep (SL2C.toLorentzGroup M)) (ContrMod.stdBasis i)) =
  ∑ j, ↑(SL2C.toLorentzGroup M) j i • complexContrBasis j inclCongrRealLorentz_ρM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ inclCongrRealLorentz ((ContrMod.rep (SL2C.toLorentzGroup M)) (ContrMod.stdBasis i)) =
  ∑ j, ↑(SL2C.toLorentzGroup M) j i • complexContrBasis jM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ inclCongrRealLorentz ((ContrMod.rep (SL2C.toLorentzGroup M)) (ContrMod.stdBasis i)) =
  ∑ j, ↑(SL2C.toLorentzGroup M) j i • complexContrBasis j]M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ inclCongrRealLorentz ((ContrMod.rep (SL2C.toLorentzGroup M)) (ContrMod.stdBasis i)) =
  ∑ j, ↑(SL2C.toLorentzGroup M) j i • complexContrBasis j
  rw [Contr.ρ_stdBasis,M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ inclCongrRealLorentz (∑ j, ↑(SL2C.toLorentzGroup M) j i • ContrMod.stdBasis j) =
  ∑ j, ↑(SL2C.toLorentzGroup M) j i • complexContrBasis jM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ ∑ x, inclCongrRealLorentz (↑(SL2C.toLorentzGroup M) x i • ContrMod.stdBasis x) =
  ∑ j, ↑(SL2C.toLorentzGroup M) j i • complexContrBasis j map_sumM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ ∑ x, inclCongrRealLorentz (↑(SL2C.toLorentzGroup M) x i • ContrMod.stdBasis x) =
  ∑ j, ↑(SL2C.toLorentzGroup M) j i • complexContrBasis jM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ ∑ x, inclCongrRealLorentz (↑(SL2C.toLorentzGroup M) x i • ContrMod.stdBasis x) =
  ∑ j, ↑(SL2C.toLorentzGroup M) j i • complexContrBasis j]M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ ∑ x, inclCongrRealLorentz (↑(SL2C.toLorentzGroup M) x i • ContrMod.stdBasis x) =
  ∑ j, ↑(SL2C.toLorentzGroup M) j i • complexContrBasis j
  apply congrArgM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3⊢ (fun x => inclCongrRealLorentz (↑(SL2C.toLorentzGroup M) x i • ContrMod.stdBasis x)) = fun j =>
  ↑(SL2C.toLorentzGroup M) j i • complexContrBasis j
  funext jM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ inclCongrRealLorentz (↑(SL2C.toLorentzGroup M) j i • ContrMod.stdBasis j) =
  ↑(SL2C.toLorentzGroup M) j i • complexContrBasis j
  simp only [LinearMap.map_smulₛₗ, ofRealHom_eq_coe, coe_smul]M:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ ↑(SL2C.toLorentzGroup M) j i • inclCongrRealLorentz (ContrMod.stdBasis j) =
  ↑(SL2C.toLorentzGroup M) j i • complexContrBasis j
  rw [complexContrBasis_of_realM:SL(2, ℂ)i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ ↑(SL2C.toLorentzGroup M) j i • inclCongrRealLorentz (ContrMod.stdBasis j) =
  ↑(SL2C.toLorentzGroup M) j i • inclCongrRealLorentz (ContrMod.stdBasis j)All goals completed! 🐙]All goals completed! 🐙

The semilinear map including real Lorentz co-vectors into complex covariant Lorentz vectors.


def inclCoRealLorentz : CoMod 3 →ₛₗ[Complex.ofRealHom] CoℂModule where
  toFun v := { val := ofReal ∘ v.toFin1dℝ }
  map_add' x y := byx:CoMod 3y:CoMod 3⊢ { val := ofReal ∘ (x + y).toFin1dℝ } = { val := ofReal ∘ x.toFin1dℝ } + { val := ofReal ∘ y.toFin1dℝ }
    ext ix:CoMod 3y:CoMod 3i:Fin 1 ⊕ Fin 3⊢ { val := ofReal ∘ (x + y).toFin1dℝ }.val i = ({ val := ofReal ∘ x.toFin1dℝ } + { val := ofReal ∘ y.toFin1dℝ }).val i
    rw [CoℂModule.val_addx:CoMod 3y:CoMod 3i:Fin 1 ⊕ Fin 3⊢ { val := ofReal ∘ (x + y).toFin1dℝ }.val i = ({ val := ofReal ∘ x.toFin1dℝ }.val + { val := ofReal ∘ y.toFin1dℝ }.val) ix:CoMod 3y:CoMod 3i:Fin 1 ⊕ Fin 3⊢ { val := ofReal ∘ (x + y).toFin1dℝ }.val i = ({ val := ofReal ∘ x.toFin1dℝ }.val + { val := ofReal ∘ y.toFin1dℝ }.val) i]x:CoMod 3y:CoMod 3i:Fin 1 ⊕ Fin 3⊢ { val := ofReal ∘ (x + y).toFin1dℝ }.val i = ({ val := ofReal ∘ x.toFin1dℝ }.val + { val := ofReal ∘ y.toFin1dℝ }.val) i
    simp only [Function.comp_apply, Pi.add_apply, map_add]x:CoMod 3y:CoMod 3i:Fin 1 ⊕ Fin 3⊢ ↑(CoMod.toFin1dℝEquiv x i + CoMod.toFin1dℝEquiv y i) = ↑(x.toFin1dℝ i) + ↑(y.toFin1dℝ i)
    simp only [ofReal_add]All goals completed! 🐙
  map_smul' c x := byc:ℝx:CoMod 3⊢ { val := ofReal ∘ (c • x).toFin1dℝ } = ofRealHom c • { val := ofReal ∘ x.toFin1dℝ }
    ext ic:ℝx:CoMod 3i:Fin 1 ⊕ Fin 3⊢ { val := ofReal ∘ (c • x).toFin1dℝ }.val i = (ofRealHom c • { val := ofReal ∘ x.toFin1dℝ }).val i
    rw [CoℂModule.val_smulc:ℝx:CoMod 3i:Fin 1 ⊕ Fin 3⊢ { val := ofReal ∘ (c • x).toFin1dℝ }.val i = (ofRealHom c • { val := ofReal ∘ x.toFin1dℝ }.val) ic:ℝx:CoMod 3i:Fin 1 ⊕ Fin 3⊢ { val := ofReal ∘ (c • x).toFin1dℝ }.val i = (ofRealHom c • { val := ofReal ∘ x.toFin1dℝ }.val) i]c:ℝx:CoMod 3i:Fin 1 ⊕ Fin 3⊢ { val := ofReal ∘ (c • x).toFin1dℝ }.val i = (ofRealHom c • { val := ofReal ∘ x.toFin1dℝ }.val) i
    simp only [Function.comp_apply, ofRealHom_eq_coe, Pi.smul_apply, _root_.map_smul]c:ℝx:CoMod 3i:Fin 1 ⊕ Fin 3⊢ ↑(c • CoMod.toFin1dℝEquiv x i) = ↑c • ↑(x.toFin1dℝ i)
    simp only [smul_eq_mul, ofReal_mul]All goals completed! 🐙

              lemma inclCoRealLorentz_val (v : CoMod 3) :
    (inclCoRealLorentz v).val = ofRealHom ∘ v.toFin1dℝ := rfl

lemma complexCoBasis_of_real (i : Fin 1 ⊕ Fin 3) :
    (complexCoBasis i) = inclCoRealLorentz (CoMod.stdBasis i) := byi:Fin 1 ⊕ Fin 3⊢ complexCoBasis i = inclCoRealLorentz (CoMod.stdBasis i)
  apply CoℂModule.exti:Fin 1 ⊕ Fin 3⊢ (complexCoBasis i).val = (inclCoRealLorentz (CoMod.stdBasis i)).val
  simp only [complexCoBasis, Basis.coe_ofEquivFun, inclCoRealLorentz,
    LinearMap.coe_mk, AddHom.coe_mk]i:Fin 1 ⊕ Fin 3⊢ (CoℂModule.toFin13ℂEquiv.symm (Pi.single i 1)).val = ofReal ∘ (CoMod.stdBasis i).toFin1dℝ
  ext ji:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (CoℂModule.toFin13ℂEquiv.symm (Pi.single i 1)).val j = (ofReal ∘ (CoMod.stdBasis i).toFin1dℝ) j
  simp only [Function.comp_apply]i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ (CoℂModule.toFin13ℂEquiv.symm (Pi.single i 1)).val j = ↑((CoMod.stdBasis i).toFin1dℝ j)
  change (Pi.single i 1) j = _i:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 j = ↑((CoMod.stdBasis i).toFin1dℝ j)
  by_cases h : i = jposi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:i = j⊢ Pi.single i 1 j = ↑((CoMod.stdBasis i).toFin1dℝ j)negi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:¬i = j⊢ Pi.single i 1 j = ↑((CoMod.stdBasis i).toFin1dℝ j)
  ·posi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:i = j⊢ Pi.single i 1 j = ↑((CoMod.stdBasis i).toFin1dℝ j) subst hposi:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 i = ↑((CoMod.stdBasis i).toFin1dℝ i)
    rw [CoMod.toFin1dℝ,posi:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 i = ↑(CoMod.toFin1dℝEquiv (CoMod.stdBasis i) i)posi:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 i = ↑1 CoMod.stdBasis_toFin1dℝEquiv_apply_sameposi:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 i = ↑1posi:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 i = ↑1]posi:Fin 1 ⊕ Fin 3⊢ Pi.single i 1 i = ↑1
    simpAll goals completed! 🐙
  ·negi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:¬i = j⊢ Pi.single i 1 j = ↑((CoMod.stdBasis i).toFin1dℝ j) rw [CoMod.toFin1dℝ,negi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:¬i = j⊢ Pi.single i 1 j = ↑(CoMod.toFin1dℝEquiv (CoMod.stdBasis i) j)negi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:¬i = j⊢ Pi.single i 1 j = ↑0 CoMod.stdBasis_toFin1dℝEquiv_apply_ne hnegi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:¬i = j⊢ Pi.single i 1 j = ↑0negi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:¬i = j⊢ Pi.single i 1 j = ↑0]negi:Fin 1 ⊕ Fin 3j:Fin 1 ⊕ Fin 3h:¬i = j⊢ Pi.single i 1 j = ↑0
    simp [h]All goals completed! 🐙

lemma inclCoRealLorentz_ρ (M : SL(2, ℂ)) (v : CoMod 3) :
    (CoℂModule.SL2CRep M) (inclCoRealLorentz v) =
    inclCoRealLorentz (CoMod.rep (SL2C.toLorentzGroup M) v) := byM:SL(2, ℂ)v:CoMod 3⊢ (CoℂModule.SL2CRep M) (inclCoRealLorentz v) = inclCoRealLorentz ((CoMod.rep (SL2C.toLorentzGroup M)) v)
  ext iM:SL(2, ℂ)v:CoMod 3i:Fin 1 ⊕ Fin 3⊢ ((CoℂModule.SL2CRep M) (inclCoRealLorentz v)).val i = (inclCoRealLorentz ((CoMod.rep (SL2C.toLorentzGroup M)) v)).val i
  rw [CoℂModule.SL2CRep_val,M:SL(2, ℂ)v:CoMod 3i:Fin 1 ⊕ Fin 3⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ (inclCoRealLorentz v).val) i =
  (inclCoRealLorentz ((CoMod.rep (SL2C.toLorentzGroup M)) v)).val iM:SL(2, ℂ)v:CoMod 3i:Fin 1 ⊕ Fin 3⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ) i =
  (⇑ofRealHom ∘ ((CoMod.rep (SL2C.toLorentzGroup M)) v).toFin1dℝ) i inclCoRealLorentz_val,M:SL(2, ℂ)v:CoMod 3i:Fin 1 ⊕ Fin 3⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ) i =
  (inclCoRealLorentz ((CoMod.rep (SL2C.toLorentzGroup M)) v)).val iM:SL(2, ℂ)v:CoMod 3i:Fin 1 ⊕ Fin 3⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ) i =
  (⇑ofRealHom ∘ ((CoMod.rep (SL2C.toLorentzGroup M)) v).toFin1dℝ) i inclCoRealLorentz_valM:SL(2, ℂ)v:CoMod 3i:Fin 1 ⊕ Fin 3⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ) i =
  (⇑ofRealHom ∘ ((CoMod.rep (SL2C.toLorentzGroup M)) v).toFin1dℝ) iM:SL(2, ℂ)v:CoMod 3i:Fin 1 ⊕ Fin 3⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ) i =
  (⇑ofRealHom ∘ ((CoMod.rep (SL2C.toLorentzGroup M)) v).toFin1dℝ) i]M:SL(2, ℂ)v:CoMod 3i:Fin 1 ⊕ Fin 3⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ) i =
  (⇑ofRealHom ∘ ((CoMod.rep (SL2C.toLorentzGroup M)) v).toFin1dℝ) i
  change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ
      (ofRealHom ∘ v.toFin1dℝ)) i =
    (ofRealHom ∘ ((LorentzGroup.transpose (SL2C.toLorentzGroup M)⁻¹).1 *ᵥ
      v.toFin1dℝ)) iM:SL(2, ℂ)v:CoMod 3i:Fin 1 ⊕ Fin 3⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ) i =
  (⇑ofRealHom ∘ (↑(LorentzGroup.transpose (SL2C.toLorentzGroup M)⁻¹) *ᵥ v.toFin1dℝ)) i
  rw [LorentzGroup.toComplex_invM:SL(2, ℂ)v:CoMod 3i:Fin 1 ⊕ Fin 3⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M)⁻¹)ᵀ *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ) i =
  (⇑ofRealHom ∘ (↑(LorentzGroup.transpose (SL2C.toLorentzGroup M)⁻¹) *ᵥ v.toFin1dℝ)) iM:SL(2, ℂ)v:CoMod 3i:Fin 1 ⊕ Fin 3⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M)⁻¹)ᵀ *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ) i =
  (⇑ofRealHom ∘ (↑(LorentzGroup.transpose (SL2C.toLorentzGroup M)⁻¹) *ᵥ v.toFin1dℝ)) i]M:SL(2, ℂ)v:CoMod 3i:Fin 1 ⊕ Fin 3⊢ ((LorentzGroup.toComplex (SL2C.toLorentzGroup M)⁻¹)ᵀ *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ) i =
  (⇑ofRealHom ∘ (↑(LorentzGroup.transpose (SL2C.toLorentzGroup M)⁻¹) *ᵥ v.toFin1dℝ)) i
  change (LorentzGroup.toComplex (LorentzGroup.transpose (SL2C.toLorentzGroup M)⁻¹) *ᵥ
      (ofRealHom ∘ v.toFin1dℝ)) i =
    (ofRealHom ∘ ((LorentzGroup.transpose (SL2C.toLorentzGroup M)⁻¹).1 *ᵥ
      v.toFin1dℝ)) iM:SL(2, ℂ)v:CoMod 3i:Fin 1 ⊕ Fin 3⊢ (LorentzGroup.toComplex (LorentzGroup.transpose (SL2C.toLorentzGroup M)⁻¹) *ᵥ ⇑ofRealHom ∘ v.toFin1dℝ) i =
  (⇑ofRealHom ∘ (↑(LorentzGroup.transpose (SL2C.toLorentzGroup M)⁻¹) *ᵥ v.toFin1dℝ)) i
  rw [LorentzGroup.toComplex_mulVec_ofRealM:SL(2, ℂ)v:CoMod 3i:Fin 1 ⊕ Fin 3⊢ (⇑ofRealHom ∘ (↑(LorentzGroup.transpose (SL2C.toLorentzGroup M)⁻¹) *ᵥ v.toFin1dℝ)) i =
  (⇑ofRealHom ∘ (↑(LorentzGroup.transpose (SL2C.toLorentzGroup M)⁻¹) *ᵥ v.toFin1dℝ)) iAll goals completed! 🐙]All goals completed! 🐙