The Lorentz Algebra

We define

• Define lorentzAlgebra via LieAlgebra.Orthogonal.so' as a subalgebra of Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ.
• In mem_iff prove that a matrix is in the Lorentz algebra if and only if it satisfies the condition Aᵀ * η = - η * A.

def lorentzAlgebra : LieSubalgebra ℝ (Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ)

The Lorentz algebra as a subalgebra of Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ.

Equations

• lorentzAlgebra = LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ

theorem lorentzAlgebra.transpose_eta (A : ↥lorentzAlgebra) : (↑A).transpose * minkowskiMatrix = -minkowskiMatrix * ↑A

theorem lorentzAlgebra.mem_of_transpose_eta_eq_eta_mul_self {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ} (h : A.transpose * minkowskiMatrix = -minkowskiMatrix * A) : A ∈ lorentzAlgebra

theorem lorentzAlgebra.mem_iff {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ} : A ∈ lorentzAlgebra ↔ A.transpose * minkowskiMatrix = -minkowskiMatrix * A

theorem lorentzAlgebra.mem_iff' (A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) : A ∈ lorentzAlgebra ↔ A = -minkowskiMatrix * A.transpose * minkowskiMatrix

theorem lorentzAlgebra.diag_comp (Λ : ↥lorentzAlgebra) (μ : Fin 1 ⊕ Fin 3) : ↑Λ μ μ = 0

theorem lorentzAlgebra.time_comps (Λ : ↥lorentzAlgebra) (i : Fin 3) : ↑Λ (Sum.inr i) (Sum.inl 0) = ↑Λ (Sum.inl 0) (Sum.inr i)

theorem lorentzAlgebra.space_comps (Λ : ↥lorentzAlgebra) (i j : Fin 3) : ↑Λ (Sum.inr i) (Sum.inr j) = -↑Λ (Sum.inr j) (Sum.inr i)