PhysLean Documentation

PhysLean.Relativity.LorentzGroup.ToVector

Vectors from Lorentz group elements #

Every element of the Lorentz group defines a Lorentz vector, but it's first column.

source
def LorentzGroup.toVector {d : ℕ} (Λ : ↑(LorentzGroup d)) :
Lorentz.Vector d

The Lorentz vector obtained by acting the Lorentz group element Λ on basis (Sum.inl 0).

Equations
Instances For
    source
    theorem LorentzGroup.toVector_mul {d : ℕ} (Λ₁ Λ₂ : ↑(LorentzGroup d)) :
    toVector (Λ₁ * Λ₂) = Λ₁ • toVector Λ₂
    source
    theorem LorentzGroup.toVector_neg {d : ℕ} (Λ : ↑(LorentzGroup d)) :
    toVector (-Λ) = -toVector Λ
    source
    @[simp]
    theorem LorentzGroup.toVector_apply {d : ℕ} (Λ : ↑(LorentzGroup d)) (i : Fin 1 ⊕ Fin d) :
    toVector Λ i = ↑Λ i (Sum.inl 0)
    source
    theorem LorentzGroup.toVector_eq_fun {d : ℕ} (Λ : ↑(LorentzGroup d)) :
    toVector Λ = fun (i : Fin 1 ⊕ Fin d) => ↑Λ i (Sum.inl 0)
    source
    theorem LorentzGroup.toVector_continuous {d : ℕ} :
    Continuous toVector
    source
    theorem LorentzGroup.toVector_timeComponent {d : ℕ} (Λ : ↑(LorentzGroup d)) :
    (toVector Λ).timeComponent = ↑Λ (Sum.inl 0) (Sum.inl 0)
    source
    @[simp]
    theorem LorentzGroup.toVector_minkowskiProduct_self {d : ℕ} (Λ : ↑(LorentzGroup d)) :
    (Lorentz.Vector.minkowskiProduct (toVector Λ)) (toVector Λ) = 1
    source
    theorem LorentzGroup.one_le_abs_timeComponent {d : ℕ} (Λ : ↑(LorentzGroup d)) :
    1 ≤ |↑Λ (Sum.inl 0) (Sum.inl 0)|
    source
    theorem LorentzGroup.toVector_eq_basis_iff_timeComponent_eq_one {d : ℕ} (Λ : ↑(LorentzGroup d)) :
    toVector Λ = Lorentz.Vector.basis (Sum.inl 0) ↔ ↑Λ (Sum.inl 0) (Sum.inl 0) = 1
    source
    theorem LorentzGroup.smul_timeComponent_eq_toVector_minkowskiProduct {d : ℕ} (Λ : ↑(LorentzGroup d)) (v : Lorentz.Vector d) :
    (Λ • v).timeComponent = (Lorentz.Vector.minkowskiProduct (toVector Λ⁻¹)) v