PhysLean.Relativity.Lorentz.ComplexVector.Modules

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.

source

structure Lorentz.ContrℂModule :

Type

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

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

Instances For

source

def Lorentz.ContrℂModule.toFin13ℂFun :

ContrℂModule ≃ (Fin 1 ⊕ Fin 3 → ℂ)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance Lorentz.ContrℂModule.instAddCommMonoid :

AddCommMonoid ContrℂModule

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

Equations

Lorentz.ContrℂModule.instAddCommMonoid = Lorentz.ContrℂModule.toFin13ℂFun.addCommMonoid

source

instance Lorentz.ContrℂModule.instAddCommGroup :

AddCommGroup ContrℂModule

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

Equations

Lorentz.ContrℂModule.instAddCommGroup = Lorentz.ContrℂModule.toFin13ℂFun.addCommGroup

source

instance Lorentz.ContrℂModule.instModuleComplex :

Module ℂ ContrℂModule

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

Equations

Lorentz.ContrℂModule.instModuleComplex = Equiv.module ℂ Lorentz.ContrℂModule.toFin13ℂFun

source

theorem Lorentz.ContrℂModule.ext (ψ ψ' : ContrℂModule) (h : ψ.val = ψ'.val) :

ψ = ψ'

source

@[simp]

theorem Lorentz.ContrℂModule.val_add (ψ ψ' : ContrℂModule) :

(ψ + ψ').val = ψ.val + ψ'.val

source

@[simp]

theorem Lorentz.ContrℂModule.val_smul (r : ℂ) (ψ : ContrℂModule) :

(r • ψ).val = r • ψ.val

source

def Lorentz.ContrℂModule.toFin13ℂEquiv :

ContrℂModule ≃ₗ[ℂ ] Fin 1 ⊕ Fin 3 → ℂ

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

Equations

Lorentz.ContrℂModule.toFin13ℂEquiv = Equiv.linearEquiv ℂ Lorentz.ContrℂModule.toFin13ℂFun

Instances For

source

@[simp]

theorem Lorentz.ContrℂModule.toFin13ℂEquiv_symm_apply_val (a✝ : Fin 1 ⊕ Fin 3 → ℂ) (a✝¹ : Fin 1 ⊕ Fin 3) :

(toFin13ℂEquiv.symm a✝).val a✝¹ = a✝ a✝¹

source

@[simp]

theorem Lorentz.ContrℂModule.toFin13ℂEquiv_apply (a✝ : ContrℂModule) (a✝¹ : Fin 1 ⊕ Fin 3) :

toFin13ℂEquiv a✝ a✝¹ = toFin13ℂFun a✝ a✝¹

source

@[reducible, inline]

abbrev Lorentz.ContrℂModule.toFin13ℂ (ψ : ContrℂModule) :

Fin 1 ⊕ Fin 3 → ℂ

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

Equations

ψ.toFin13ℂ = Lorentz.ContrℂModule.toFin13ℂEquiv ψ

Instances For

source

def Lorentz.ContrℂModule.lorentzGroupRep :

Representation ℂ (↑(LorentzGroup 3)) ContrℂModule

The representation of the Lorentz group on ContrℂModule.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lorentz.ContrℂModule.SL2CRep :

Representation ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ) ContrℂModule

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

Equations

Lorentz.ContrℂModule.SL2CRep = MonoidHom.comp Lorentz.ContrℂModule.lorentzGroupRep Lorentz.SL2C.toLorentzGroup

Instances For

source

structure Lorentz.CoℂModule :

Type

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

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

Instances For

source

def Lorentz.CoℂModule.toFin13ℂFun :

CoℂModule ≃ (Fin 1 ⊕ Fin 3 → ℂ)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance Lorentz.CoℂModule.instAddCommMonoid :

AddCommMonoid CoℂModule

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

Equations

Lorentz.CoℂModule.instAddCommMonoid = Lorentz.CoℂModule.toFin13ℂFun.addCommMonoid

source

instance Lorentz.CoℂModule.instAddCommGroup :

AddCommGroup CoℂModule

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

Equations

Lorentz.CoℂModule.instAddCommGroup = Lorentz.CoℂModule.toFin13ℂFun.addCommGroup

source

instance Lorentz.CoℂModule.instModuleComplex :

Module ℂ CoℂModule

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

Equations

Lorentz.CoℂModule.instModuleComplex = Equiv.module ℂ Lorentz.CoℂModule.toFin13ℂFun

source

def Lorentz.CoℂModule.toFin13ℂEquiv :

CoℂModule ≃ₗ[ℂ ] Fin 1 ⊕ Fin 3 → ℂ

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

Equations

Lorentz.CoℂModule.toFin13ℂEquiv = Equiv.linearEquiv ℂ Lorentz.CoℂModule.toFin13ℂFun

Instances For

source

@[simp]

theorem Lorentz.CoℂModule.toFin13ℂEquiv_apply (a✝ : CoℂModule) (a✝¹ : Fin 1 ⊕ Fin 3) :

toFin13ℂEquiv a✝ a✝¹ = toFin13ℂFun a✝ a✝¹

source

@[simp]

theorem Lorentz.CoℂModule.toFin13ℂEquiv_symm_apply_val (a✝ : Fin 1 ⊕ Fin 3 → ℂ) (a✝¹ : Fin 1 ⊕ Fin 3) :

(toFin13ℂEquiv.symm a✝).val a✝¹ = a✝ a✝¹

source

@[reducible, inline]

abbrev Lorentz.CoℂModule.toFin13ℂ (ψ : CoℂModule) :

Fin 1 ⊕ Fin 3 → ℂ

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

Equations

ψ.toFin13ℂ = Lorentz.CoℂModule.toFin13ℂEquiv ψ

Instances For

source

def Lorentz.CoℂModule.lorentzGroupRep :

Representation ℂ (↑(LorentzGroup 3)) CoℂModule

The representation of the Lorentz group on CoℂModule.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lorentz.CoℂModule.SL2CRep :

Representation ℂ (Matrix.SpecialLinearGroup (Fin 2) ℂ) CoℂModule

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

Equations

Lorentz.CoℂModule.SL2CRep = MonoidHom.comp Lorentz.CoℂModule.lorentzGroupRep Lorentz.SL2C.toLorentzGroup

Instances For