1. Physlib
  2. Relativity
  3. Tensors
  4. ComplexTensor
  5. Vector
  6. Pre
  7. Modules
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.SL2C.Basic

Modules associated with complex Lorentz vectors

We define the modules underlying complex Lorentz vectors. These definitions are preludes to the definitions of Lorentz.complexContr and Lorentz.complexCo.

@[expose] public section

The module for contravariant (up-index) complex Lorentz vectors.

The underlying value as a vector Fin 1 ⊕ Fin 3 → ℂ.

structure ContrℂModule where val : Fin 1 ⊕ Fin 3 → ℂ

The equivalence between ContrℂModule and Fin 1 ⊕ Fin 3 → ℂ.

def toFin13ℂFun : ContrℂModule ≃ (Fin 1 ⊕ Fin 3 → ℂ) where toFun v := v.val invFun f := ⟨f⟩ left_inv _ := rfl right_inv _ := rfl

The instance of AddCommMonoid on ContrℂModule defined via its equivalence with Fin 1 ⊕ Fin 3 → ℂ.

instance : AddCommMonoid ContrℂModule := Equiv.addCommMonoid toFin13ℂFun

The instance of AddCommGroup on ContrℂModule defined via its equivalence with Fin 1 ⊕ Fin 3 → ℂ.

instance : AddCommGroup ContrℂModule := Equiv.addCommGroup toFin13ℂFun

The instance of Module on ContrℂModule defined via its equivalence with Fin 1 ⊕ Fin 3 → ℂ.

instance : Module ℂ ContrℂModule := Equiv.module ℂ toFin13ℂFun
@[ext] lemma ext (ψ ψ' : ContrℂModule) (h : ψ.val = ψ'.val) : ψ = ψ' := ψ:ContrℂModuleψ':ContrℂModuleh:ψ.val = ψ'.val⊢ ψ = ψ' ψ':ContrℂModuleval✝:Fin 1 ⊕ Fin 3 → ℂh:{ val := val✝ }.val = ψ'.val⊢ { val := val✝ } = ψ' val✝¹:Fin 1 ⊕ Fin 3 → ℂval✝:Fin 1 ⊕ Fin 3 → ℂh:{ val := val✝¹ }.val = { val := val✝ }.val⊢ { val := val✝¹ } = { val := val✝ } val✝:Fin 1 ⊕ Fin 3 → ℂ⊢ { val := val✝ } = { val := { val := val✝ }.val } All goals completed! 🐙@[simp] lemma val_add (ψ ψ' : ContrℂModule) : (ψ + ψ').val = ψ.val + ψ'.val := rfl@[simp] lemma val_smul (r : ℂ) (ψ : ContrℂModule) : (r • ψ).val = r • ψ.val := rfl

The linear equivalence between ContrℂModule and (Fin 1 ⊕ Fin 3 → ℂ).

@[simps!] def toFin13ℂEquiv : ContrℂModule ≃ₗ[ℂ] (Fin 1 ⊕ Fin 3 → ℂ) := Equiv.linearEquiv ℂ toFin13ℂFun

The underlying element of Fin 1 ⊕ Fin 3 → ℂ of a element in ContrℂModule defined through the linear equivalence toFin13ℂEquiv.

abbrev toFin13ℂ (ψ : ContrℂModule) := toFin13ℂEquiv ψ

The representation of the Lorentz group on ContrℂModule.

def lorentzGroupRep : Representation ℂ (LorentzGroup 3) ContrℂModule where toFun M := { toFun := fun v => toFin13ℂEquiv.symm (LorentzGroup.toComplex M *ᵥ v.toFin13ℂ), map_add' := M:↑(LorentzGroup 3)⊢ ∀ (x y : ContrℂModule), toFin13ℂEquiv.symm (LorentzGroup.toComplex M *ᵥ (x + y).toFin13ℂ) = toFin13ℂEquiv.symm (LorentzGroup.toComplex M *ᵥ x.toFin13ℂ) + toFin13ℂEquiv.symm (LorentzGroup.toComplex M *ᵥ y.toFin13ℂ) M:↑(LorentzGroup 3)ψ:ContrℂModuleψ':ContrℂModule⊢ toFin13ℂEquiv.symm (LorentzGroup.toComplex M *ᵥ (ψ + ψ').toFin13ℂ) = toFin13ℂEquiv.symm (LorentzGroup.toComplex M *ᵥ ψ.toFin13ℂ) + toFin13ℂEquiv.symm (LorentzGroup.toComplex M *ᵥ ψ'.toFin13ℂ) All goals completed! 🐙 map_smul' := M:↑(LorentzGroup 3)⊢ ∀ (m : ℂ) (x : ContrℂModule), toFin13ℂEquiv.symm (LorentzGroup.toComplex M *ᵥ (m • x).toFin13ℂ) = (RingHom.id ℂ) m • toFin13ℂEquiv.symm (LorentzGroup.toComplex M *ᵥ x.toFin13ℂ) M:↑(LorentzGroup 3)r:ℂψ:ContrℂModule⊢ toFin13ℂEquiv.symm (LorentzGroup.toComplex M *ᵥ (r • ψ).toFin13ℂ) = (RingHom.id ℂ) r • toFin13ℂEquiv.symm (LorentzGroup.toComplex M *ᵥ ψ.toFin13ℂ) All goals completed! 🐙} map_one' := ⊢ { toFun := fun v => toFin13ℂEquiv.symm (LorentzGroup.toComplex 1 *ᵥ v.toFin13ℂ), map_add' := ⋯, map_smul' := ⋯ } = 1 i:ContrℂModulex✝:Fin 1 ⊕ Fin 3⊢ ({ toFun := fun v => toFin13ℂEquiv.symm (LorentzGroup.toComplex 1 *ᵥ v.toFin13ℂ), map_add' := ⋯, map_smul' := ⋯ } i).val x✝ = (1 i).val x✝ All goals completed! 🐙 map_mul' M N := M:↑(LorentzGroup 3)N:↑(LorentzGroup 3)⊢ { toFun := fun v => toFin13ℂEquiv.symm (LorentzGroup.toComplex (M * N) *ᵥ v.toFin13ℂ), map_add' := ⋯, map_smul' := ⋯ } = { toFun := fun v => toFin13ℂEquiv.symm (LorentzGroup.toComplex M *ᵥ v.toFin13ℂ), map_add' := ⋯, map_smul' := ⋯ } * { toFun := fun v => toFin13ℂEquiv.symm (LorentzGroup.toComplex N *ᵥ v.toFin13ℂ), map_add' := ⋯, map_smul' := ⋯ } M:↑(LorentzGroup 3)N:↑(LorentzGroup 3)i:ContrℂModulex✝:Fin 1 ⊕ Fin 3⊢ ({ toFun := fun v => toFin13ℂEquiv.symm (LorentzGroup.toComplex (M * N) *ᵥ v.toFin13ℂ), map_add' := ⋯, map_smul' := ⋯ } i).val x✝ = (({ toFun := fun v => toFin13ℂEquiv.symm (LorentzGroup.toComplex M *ᵥ v.toFin13ℂ), map_add' := ⋯, map_smul' := ⋯ } * { toFun := fun v => toFin13ℂEquiv.symm (LorentzGroup.toComplex N *ᵥ v.toFin13ℂ), map_add' := ⋯, map_smul' := ⋯ }) i).val x✝ All goals completed! 🐙

The representation of the SL(2, ℂ) on ContrℂModule induced by the representation of the Lorentz group.

def SL2CRep : Representation ℂ SL(2, ℂ) ContrℂModule := MonoidHom.comp lorentzGroupRep Lorentz.SL2C.toLorentzGroup

The module for covariant (up-index) complex Lorentz vectors.

The underlying value as a vector Fin 1 ⊕ Fin 3 → ℂ.

structure CoℂModule where val : Fin 1 ⊕ Fin 3 → ℂ

The equivalence between CoℂModule and Fin 1 ⊕ Fin 3 → ℂ.

def toFin13ℂFun : CoℂModule ≃ (Fin 1 ⊕ Fin 3 → ℂ) where toFun v := v.val invFun f := ⟨f⟩ left_inv _ := rfl right_inv _ := rfl

The instance of AddCommMonoid on CoℂModule defined via its equivalence with Fin 1 ⊕ Fin 3 → ℂ.

instance : AddCommMonoid CoℂModule := Equiv.addCommMonoid toFin13ℂFun

The instance of AddCommGroup on CoℂModule defined via its equivalence with Fin 1 ⊕ Fin 3 → ℂ.

instance : AddCommGroup CoℂModule := Equiv.addCommGroup toFin13ℂFun

The instance of Module on CoℂModule defined via its equivalence with Fin 1 ⊕ Fin 3 → ℂ.

instance : Module ℂ CoℂModule := Equiv.module ℂ toFin13ℂFun
@[ext] lemma ext (ψ ψ' : CoℂModule) (h : ψ.val = ψ'.val) : ψ = ψ' := ψ:CoℂModuleψ':CoℂModuleh:ψ.val = ψ'.val⊢ ψ = ψ' ψ':CoℂModuleval✝:Fin 1 ⊕ Fin 3 → ℂh:{ val := val✝ }.val = ψ'.val⊢ { val := val✝ } = ψ' val✝¹:Fin 1 ⊕ Fin 3 → ℂval✝:Fin 1 ⊕ Fin 3 → ℂh:{ val := val✝¹ }.val = { val := val✝ }.val⊢ { val := val✝¹ } = { val := val✝ } val✝:Fin 1 ⊕ Fin 3 → ℂ⊢ { val := val✝ } = { val := { val := val✝ }.val } All goals completed! 🐙@[simp] lemma val_add (ψ ψ' : CoℂModule) : (ψ + ψ').val = ψ.val + ψ'.val := rfl@[simp] lemma val_smul (r : ℂ) (ψ : CoℂModule) : (r • ψ).val = r • ψ.val := rfl

The linear equivalence between CoℂModule and (Fin 1 ⊕ Fin 3 → ℂ).

@[simps!] def toFin13ℂEquiv : CoℂModule ≃ₗ[ℂ] (Fin 1 ⊕ Fin 3 → ℂ) := Equiv.linearEquiv ℂ toFin13ℂFun

The underlying element of Fin 1 ⊕ Fin 3 → ℂ of a element in CoℂModule defined through the linear equivalence toFin13ℂEquiv.

abbrev toFin13ℂ (ψ : CoℂModule) := toFin13ℂEquiv ψ

The representation of the Lorentz group on CoℂModule.

M:↑(LorentzGroup 3)N:↑(LorentzGroup 3)x:CoℂModule⊢ ((LorentzGroup.toComplex N)⁻¹ * (LorentzGroup.toComplex M)⁻¹)ᵀ = (LorentzGroup.toComplex M)⁻¹ᵀ * (LorentzGroup.toComplex N)⁻¹ᵀ All goals completed! 🐙

The representation of the SL(2, ℂ) on ContrℂModule induced by the representation of the Lorentz group.

def SL2CRep : Representation ℂ SL(2, ℂ) CoℂModule := MonoidHom.comp lorentzGroupRep Lorentz.SL2C.toLorentzGroup