Physlib

Physlib.Relativity.LorentzAlgebra.Basic

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`.

8 declarations

definition

Lorentz Algebra

The Lorentz algebra as a Lie subalgebra over R\mathbb{R} of the space of real matrices indexed by Fin 1⊕Fin 3\text{Fin } 1 \oplus \text{Fin } 3.

theorem

ATη=−ηAA^T \eta = -\eta A for A∈so(1,3)A \in \mathfrak{so}(1, 3)

For any element AA in the Lorentz algebra so(1,3)\mathfrak{so}(1, 3), the matrix representation of AA satisfies the relation ATη=−ηAA^T \eta = -\eta A, where ATA^T is the transpose of AA and η\eta is the Minkowski metric tensor.

theorem

A⊤η=−ηAA^\top \eta = -\eta A implies A∈so(1,3)A \in \mathfrak{so}(1,3)

Let AA be a real matrix indexed by Fin 1⊕Fin 3\text{Fin } 1 \oplus \text{Fin } 3. If AA satisfies the condition A⊤η=−ηAA^\top \eta = -\eta A, where η\eta is the Minkowski metric tensor, then AA is an element of the Lorentz algebra so(1,3)\mathfrak{so}(1,3).

theorem

A∈so(1,3)  ⟺  A⊤η=−ηAA \in \mathfrak{so}(1, 3) \iff A^\top \eta = -\eta A

Let AA be a real matrix indexed by Fin 1⊕Fin 3\text{Fin } 1 \oplus \text{Fin } 3. Then AA is an element of the Lorentz algebra so(1,3)\mathfrak{so}(1, 3) if and only if it satisfies the condition A⊤η=−ηAA^\top \eta = -\eta A, where η\eta is the Minkowski metric tensor.

theorem

A∈so(1,3)  ⟺  A=−ηA⊤ηA \in \mathfrak{so}(1, 3) \iff A = -\eta A^\top \eta

Let AA be a real matrix indexed by Fin 1⊕Fin 3\text{Fin } 1 \oplus \text{Fin } 3. Then AA is an element of the Lorentz algebra so(1,3)\mathfrak{so}(1, 3) if and only if it satisfies the condition A=−ηA⊤ηA = -\eta A^\top \eta, where η\eta is the Minkowski metric tensor and A⊤A^\top is the transpose of AA.

theorem

Diagonal entries of Λ∈so(1,3)\Lambda \in \mathfrak{so}(1, 3) are zero

Let Λ\Lambda be a matrix in the Lorentz algebra so(1,3)\mathfrak{so}(1, 3). For any index μ∈Fin 1⊕Fin 3\mu \in \text{Fin } 1 \oplus \text{Fin } 3, the diagonal entry of Λ\Lambda is zero, i.e., Λμμ=0\Lambda_{\mu\mu} = 0.

theorem

Λi,0=Λ0,i\Lambda_{i,0} = \Lambda_{0,i} for Λ∈so(1,3)\Lambda \in \mathfrak{so}(1, 3)

Let Λ\Lambda be a matrix in the Lorentz algebra so(1,3)\mathfrak{so}(1, 3), which is indexed by the set {0}∪{1,2,3}\{0\} \cup \{1, 2, 3\} where 00 represents the temporal dimension and {1,2,3}\{1, 2, 3\} represent the spatial dimensions. For any spatial index i∈{1,2,3}i \in \{1, 2, 3\}, the mixed temporal-spatial entries of the matrix are equal, i.e., Λi,0=Λ0,i\Lambda_{i,0} = \Lambda_{0,i}.

theorem

Λij=−Λji\Lambda_{ij} = -\Lambda_{ji} for spatial indices i,ji, j of Λ∈so(1,3)\Lambda \in \mathfrak{so}(1, 3)

Let Λ\Lambda be a matrix in the Lorentz algebra so(1,3)\mathfrak{so}(1, 3), where the indices consist of a temporal dimension and three spatial dimensions {1,2,3}\{1, 2, 3\}. For any spatial indices i,j∈{1,2,3}i, j \in \{1, 2, 3\}, the spatial components of the matrix are antisymmetric, satisfying Λij=−Λji\Lambda_{ij} = -\Lambda_{ji}.