Modules associated with Real Lorentz vectors

We define the modules underlying real Lorentz vectors.

These definitions are preludes to the definitions of Lorentz.contr and Lorentz.co.

structure Lorentz.ContrMod (d : ℕ) : Type

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

• val : Fin 1 ⊕ Fin d → ℝ

  The underlying value as a vector Fin 1 ⊕ Fin d → ℝ.

theorem Lorentz.ContrMod.ext {d : ℕ} {ψ ψ' : ContrMod d} (h : ψ.val = ψ'.val) : ψ = ψ'

theorem Lorentz.ContrMod.ext_iff {d : ℕ} {ψ ψ' : ContrMod d} : ψ = ψ' ↔ ψ.val = ψ'.val

def Lorentz.ContrMod.toFin1dℝFun {d : ℕ} : ContrMod d ≃ (Fin 1 ⊕ Fin d → ℝ)

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

Equations

• Lorentz.ContrMod.toFin1dℝFun = { toFun := fun (v : Lorentz.ContrMod d) => v.val, invFun := fun (f : Fin 1 ⊕ Fin d → ℝ) => { val := f }, left_inv := ⋯, right_inv := ⋯ }

instance Lorentz.ContrMod.instAddCommMonoid {d : ℕ} : AddCommMonoid (ContrMod d)

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

Equations

• Lorentz.ContrMod.instAddCommMonoid = Lorentz.ContrMod.toFin1dℝFun.addCommMonoid

instance Lorentz.ContrMod.instAddCommGroup {d : ℕ} : AddCommGroup (ContrMod d)

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

Equations

• Lorentz.ContrMod.instAddCommGroup = Lorentz.ContrMod.toFin1dℝFun.addCommGroup

instance Lorentz.ContrMod.instModuleReal {d : ℕ} : Module ℝ (ContrMod d)

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

Equations

• Lorentz.ContrMod.instModuleReal = Equiv.module ℝ Lorentz.ContrMod.toFin1dℝFun

@[simp]

theorem Lorentz.ContrMod.val_add {d : ℕ} (ψ ψ' : ContrMod d) : (ψ + ψ').val = ψ.val + ψ'.val

@[simp]

theorem Lorentz.ContrMod.val_smul {d : ℕ} (r : ℝ) (ψ : ContrMod d) : (r • ψ).val = r • ψ.val

def Lorentz.ContrMod.toFin1dℝEquiv {d : ℕ} : ContrMod d ≃ₗ[ℝ] Fin 1 ⊕ Fin d → ℝ

The linear equivalence between ContrℝModule and (Fin 1 ⊕ Fin d → ℝ).

Equations

• Lorentz.ContrMod.toFin1dℝEquiv = Equiv.linearEquiv ℝ Lorentz.ContrMod.toFin1dℝFun

@[reducible, inline]

abbrev Lorentz.ContrMod.toFin1dℝ {d : ℕ} (ψ : ContrMod d) : Fin 1 ⊕ Fin d → ℝ

The underlying element of Fin 1 ⊕ Fin d → ℝ of a element in ContrℝModule defined through the linear equivalence toFin1dℝEquiv.

Equations

• ψ.toFin1dℝ = Lorentz.ContrMod.toFin1dℝEquiv ψ

theorem Lorentz.ContrMod.toFin1dℝ_eq_val {d : ℕ} (ψ : ContrMod d) : ψ.toFin1dℝ = ψ.val

The standard basis.

def Lorentz.ContrMod.stdBasis {d : ℕ} : Basis (Fin 1 ⊕ Fin d) ℝ (ContrMod d)

The standard basis of ContrℝModule indexed by Fin 1 ⊕ Fin d.

Equations

• Lorentz.ContrMod.stdBasis = Basis.ofEquivFun Lorentz.ContrMod.toFin1dℝEquiv

@[simp]

theorem Lorentz.ContrMod.stdBasis_repr_symm_apply_val {d : ℕ} (a✝ : Fin 1 ⊕ Fin d →₀ ℝ) (a✝¹ : Fin 1 ⊕ Fin d) : (stdBasis.repr.symm a✝).val a✝¹ = a✝ a✝¹

@[simp]

theorem Lorentz.ContrMod.stdBasis_repr_apply_toFun {d : ℕ} (a✝ : ContrMod d) (a✝¹ : Fin 1 ⊕ Fin d) : (stdBasis.repr a✝) a✝¹ = toFin1dℝEquiv a✝ a✝¹

@[simp]

theorem Lorentz.ContrMod.stdBasis_repr_apply_support_val {d : ℕ} (a✝ : ContrMod d) : (stdBasis.repr a✝).support.val = Multiset.map Subtype.val Finset.univ.val

@[simp]

theorem Lorentz.ContrMod.stdBasis_toFin1dℝEquiv_apply_same {d : ℕ} (μ : Fin 1 ⊕ Fin d) : toFin1dℝEquiv (stdBasis μ) μ = 1

@[simp]

theorem Lorentz.ContrMod.stdBasis_apply_same {d : ℕ} (μ : Fin 1 ⊕ Fin d) : (stdBasis μ).val μ = 1

theorem Lorentz.ContrMod.stdBasis_toFin1dℝEquiv_apply_ne {d : ℕ} {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) : toFin1dℝEquiv (stdBasis μ) ν = 0

@[simp]

theorem Lorentz.ContrMod.stdBasis_inl_apply_inr {d : ℕ} (i : Fin d) : (stdBasis (Sum.inl 0)).val (Sum.inr i) = 0

theorem Lorentz.ContrMod.stdBasis_apply {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) : (stdBasis μ).val ν = if μ = ν then 1 else 0

theorem Lorentz.ContrMod.stdBasis_decomp {d : ℕ} (v : ContrMod d) : v = ∑ i : Fin 1 ⊕ Fin d, v.toFin1dℝ i • stdBasis i

Decomposition of a contravariant Lorentz vector into the standard basis.

mulVec

@[reducible, inline]

abbrev Lorentz.ContrMod.mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) : ContrMod d

Multiplication of a matrix with a vector in ContrMod.

Equations

• Lorentz.ContrMod.mulVec M v = ((Matrix.toLinAlgEquiv Lorentz.ContrMod.stdBasis) M) v

def Lorentz.«term_*ᵥ_» : Lean.TrailingParserDescr

Multiplication of a matrix with a vector in ContrMod.

Equations

• Lorentz.«term_*ᵥ_» = Lean.ParserDescr.trailingNode `Lorentz.«term_*ᵥ_» 73 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " *ᵥ ") (Lean.ParserDescr.cat `term 73))

@[simp]

theorem Lorentz.ContrMod.mulVec_toFin1dℝ {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) : (mulVec M v).toFin1dℝ = M.mulVec v.toFin1dℝ

@[simp]

theorem Lorentz.ContrMod.mulVec_val {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) : (mulVec M v).val = M.mulVec v.val

theorem Lorentz.ContrMod.mulVec_sub {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v w : ContrMod d) : mulVec M (v - w) = mulVec M v - mulVec M w

theorem Lorentz.ContrMod.sub_mulVec {d : ℕ} (M N : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) : mulVec (M - N) v = mulVec M v - mulVec N v

theorem Lorentz.ContrMod.mulVec_add {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v w : ContrMod d) : mulVec M (v + w) = mulVec M v + mulVec M w

@[simp]

theorem Lorentz.ContrMod.one_mulVec {d : ℕ} (v : ContrMod d) : mulVec 1 v = v

theorem Lorentz.ContrMod.mulVec_mulVec {d : ℕ} (M N : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) : mulVec M (mulVec N v) = mulVec (M * N) v

The norm

(Not the Minkowski norm, but the norm of a vector in ContrℝModule d.)

def Lorentz.ContrMod.norm {d : ℕ} : NormedAddCommGroup (ContrMod d)

A NormedAddCommGroup structure on ContrMod. This is not an instance, as we don't want it to be applied always.

Equations

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

def Lorentz.ContrMod.toSpace {d : ℕ} (v : ContrMod d) : EuclideanSpace ℝ (Fin d)

The underlying space part of a ContrMod formed by removing the first element. A better name for this might be tail.

Equations

• v.toSpace = v.val ∘ Sum.inr

The representation.

def Lorentz.ContrMod.rep {d : ℕ} : Representation ℝ (↑(LorentzGroup d)) (ContrMod d)

The representation of the Lorentz group acting on ContrℝModule d.

Equations

• Lorentz.ContrMod.rep = { toFun := fun (g : ↑(LorentzGroup d)) => (Matrix.toLinAlgEquiv Lorentz.ContrMod.stdBasis) ↑g, map_one' := ⋯, map_mul' := ⋯ }

theorem Lorentz.ContrMod.rep_apply_toFin1dℝ {d : ℕ} (g : ↑(LorentzGroup d)) (ψ : ContrMod d) : ((rep g) ψ).toFin1dℝ = (↑g).mulVec ψ.toFin1dℝ

To Self-Adjoint Matrix

def Lorentz.ContrMod.toSelfAdjoint : ContrMod 3 ≃ₗ[ℝ] ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))

The linear equivalence between the vector-space ContrMod 3 and self-adjoint 2×2-complex matrices.

Equations

• Lorentz.ContrMod.toSelfAdjoint = Lorentz.ContrMod.toFin1dℝEquiv ≪≫ₗ (Finsupp.linearEquivFunOnFinite ℝ ℝ (Fin 1 ⊕ Fin 3)).symm ≪≫ₗ PauliMatrix.σSAL.repr.symm

theorem Lorentz.ContrMod.toSelfAdjoint_apply (x : ContrMod 3) : toSelfAdjoint x = x.toFin1dℝ (Sum.inl 0) • ⟨PauliMatrix.σ0, PauliMatrix.σ0_selfAdjoint⟩ - x.toFin1dℝ (Sum.inr 0) • ⟨PauliMatrix.σ1, PauliMatrix.σ1_selfAdjoint⟩ - x.toFin1dℝ (Sum.inr 1) • ⟨PauliMatrix.σ2, PauliMatrix.σ2_selfAdjoint⟩ - x.toFin1dℝ (Sum.inr 2) • ⟨PauliMatrix.σ3, PauliMatrix.σ3_selfAdjoint⟩

theorem Lorentz.ContrMod.toSelfAdjoint_apply_coe (x : ContrMod 3) : ↑(toSelfAdjoint x) = x.toFin1dℝ (Sum.inl 0) • PauliMatrix.σ0 - x.toFin1dℝ (Sum.inr 0) • PauliMatrix.σ1 - x.toFin1dℝ (Sum.inr 1) • PauliMatrix.σ2 - x.toFin1dℝ (Sum.inr 2) • PauliMatrix.σ3

theorem Lorentz.ContrMod.toSelfAdjoint_stdBasis (i : Fin 1 ⊕ Fin 3) : toSelfAdjoint (stdBasis i) = PauliMatrix.σSAL i

@[simp]

theorem Lorentz.ContrMod.toSelfAdjoint_symm_basis (i : Fin 1 ⊕ Fin 3) : toSelfAdjoint.symm (PauliMatrix.σSAL i) = stdBasis i

Topology

instance Lorentz.ContrMod.instTopologicalSpace {d : ℕ} : TopologicalSpace (ContrMod d)

The type ContrMod d carries an instance of a topological group, induced by it's equivalence to Fin 1 ⊕ Fin d → ℝ.

Equations

• Lorentz.ContrMod.instTopologicalSpace = TopologicalSpace.induced (⇑Lorentz.ContrMod.toFin1dℝEquiv) Pi.topologicalSpace

theorem Lorentz.ContrMod.toFin1dℝEquiv_isInducing {d : ℕ} : Topology.IsInducing ⇑toFin1dℝEquiv

theorem Lorentz.ContrMod.toFin1dℝEquiv_symm_isInducing {d : ℕ} : Topology.IsInducing ⇑toFin1dℝEquiv.symm

structure Lorentz.CoMod (d : ℕ) : Type

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

• val : Fin 1 ⊕ Fin d → ℝ

  The underlying value as a vector Fin 1 ⊕ Fin d → ℝ.

theorem Lorentz.CoMod.ext {d : ℕ} {ψ ψ' : CoMod d} (h : ψ.val = ψ'.val) : ψ = ψ'

theorem Lorentz.CoMod.ext_iff {d : ℕ} {ψ ψ' : CoMod d} : ψ = ψ' ↔ ψ.val = ψ'.val

def Lorentz.CoMod.toFin1dℝFun {d : ℕ} : CoMod d ≃ (Fin 1 ⊕ Fin d → ℝ)

The equivalence between CoℝModule and Fin 1 ⊕ Fin d → ℝ.

Equations

• Lorentz.CoMod.toFin1dℝFun = { toFun := fun (v : Lorentz.CoMod d) => v.val, invFun := fun (f : Fin 1 ⊕ Fin d → ℝ) => { val := f }, left_inv := ⋯, right_inv := ⋯ }

instance Lorentz.CoMod.instAddCommMonoid {d : ℕ} : AddCommMonoid (CoMod d)

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

Equations

• Lorentz.CoMod.instAddCommMonoid = Lorentz.CoMod.toFin1dℝFun.addCommMonoid

instance Lorentz.CoMod.instAddCommGroup {d : ℕ} : AddCommGroup (CoMod d)

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

Equations

• Lorentz.CoMod.instAddCommGroup = Lorentz.CoMod.toFin1dℝFun.addCommGroup

instance Lorentz.CoMod.instModuleReal {d : ℕ} : Module ℝ (CoMod d)

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

Equations

• Lorentz.CoMod.instModuleReal = Equiv.module ℝ Lorentz.CoMod.toFin1dℝFun

def Lorentz.CoMod.toFin1dℝEquiv {d : ℕ} : CoMod d ≃ₗ[ℝ] Fin 1 ⊕ Fin d → ℝ

The linear equivalence between CoℝModule and (Fin 1 ⊕ Fin d → ℝ).

Equations

• Lorentz.CoMod.toFin1dℝEquiv = Equiv.linearEquiv ℝ Lorentz.CoMod.toFin1dℝFun

@[reducible, inline]

abbrev Lorentz.CoMod.toFin1dℝ {d : ℕ} (ψ : CoMod d) : Fin 1 ⊕ Fin d → ℝ

The underlying element of Fin 1 ⊕ Fin d → ℝ of a element in CoℝModule defined through the linear equivalence toFin1dℝEquiv.

Equations

• ψ.toFin1dℝ = Lorentz.CoMod.toFin1dℝEquiv ψ

The standard basis.

def Lorentz.CoMod.stdBasis {d : ℕ} : Basis (Fin 1 ⊕ Fin d) ℝ (CoMod d)

The standard basis of CoℝModule indexed by Fin 1 ⊕ Fin d.

Equations

• Lorentz.CoMod.stdBasis = Basis.ofEquivFun Lorentz.CoMod.toFin1dℝEquiv

@[simp]

theorem Lorentz.CoMod.stdBasis_repr_apply_support_val {d : ℕ} (a✝ : CoMod d) : (stdBasis.repr a✝).support.val = Multiset.map Subtype.val Finset.univ.val

@[simp]

theorem Lorentz.CoMod.stdBasis_repr_apply_toFun {d : ℕ} (a✝ : CoMod d) (a✝¹ : Fin 1 ⊕ Fin d) : (stdBasis.repr a✝) a✝¹ = toFin1dℝEquiv a✝ a✝¹

@[simp]

theorem Lorentz.CoMod.stdBasis_repr_symm_apply_val {d : ℕ} (a✝ : Fin 1 ⊕ Fin d →₀ ℝ) (a✝¹ : Fin 1 ⊕ Fin d) : (stdBasis.repr.symm a✝).val a✝¹ = a✝ a✝¹

@[simp]

theorem Lorentz.CoMod.stdBasis_toFin1dℝEquiv_apply_same {d : ℕ} (μ : Fin 1 ⊕ Fin d) : toFin1dℝEquiv (stdBasis μ) μ = 1

@[simp]

theorem Lorentz.CoMod.stdBasis_apply_same {d : ℕ} (μ : Fin 1 ⊕ Fin d) : (stdBasis μ).val μ = 1

theorem Lorentz.CoMod.stdBasis_toFin1dℝEquiv_apply_ne {d : ℕ} {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) : toFin1dℝEquiv (stdBasis μ) ν = 0

theorem Lorentz.CoMod.stdBasis_apply {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) : (stdBasis μ).val ν = if μ = ν then 1 else 0

theorem Lorentz.CoMod.stdBasis_decomp {d : ℕ} (v : CoMod d) : v = ∑ i : Fin 1 ⊕ Fin d, v.toFin1dℝ i • stdBasis i

Decomposition of a covariant Lorentz vector into the standard basis.

mulVec

@[reducible, inline]

abbrev Lorentz.CoMod.mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : CoMod d) : CoMod d

Multiplication of a matrix with a vector in CoMod.

Equations

• Lorentz.CoMod.mulVec M v = ((Matrix.toLinAlgEquiv Lorentz.CoMod.stdBasis) M) v

def Lorentz.«term_*ᵥ__1» : Lean.TrailingParserDescr

Multiplication of a matrix with a vector in CoMod.

Equations

• Lorentz.«term_*ᵥ__1» = Lean.ParserDescr.trailingNode `Lorentz.«term_*ᵥ__1» 73 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " *ᵥ ") (Lean.ParserDescr.cat `term 73))

@[simp]

theorem Lorentz.CoMod.mulVec_toFin1dℝ {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : CoMod d) : (mulVec M v).toFin1dℝ = M.mulVec v.toFin1dℝ

The representation

def Lorentz.CoMod.rep {d : ℕ} : Representation ℝ (↑(LorentzGroup d)) (CoMod d)

The representation of the Lorentz group acting on CoℝModule d.

Equations

• Lorentz.CoMod.rep = { toFun := fun (g : ↑(LorentzGroup d)) => (Matrix.toLinAlgEquiv Lorentz.CoMod.stdBasis) ↑(LorentzGroup.transpose g⁻¹), map_one' := ⋯, map_mul' := ⋯ }