Physlib.Relativity.LorentzAlgebra.ExponentialMap

Exponential map from the Lorentz algebra to the restricted Lorentz group

In 1+3 Minkowski space with metric η, the Lie algebra `lorentzAlgebra` exponentiates onto the proper orthochronous Lorentz group (`LorentzGroup.restricted 3`). We prove: * exp_mem_lorentzGroup : `NormedSpace.exp ℝ A.1 ∈ LorentzGroup 3` (η-preserving). * exp_transpose_of_mem_algebra : `exp (A.1ᵀ) = η * exp (−A.1) * η`. * exp_isProper : `det (exp A) = 1`. * exp_isOrthochronous : `(exp A)₀₀ ≥ 1`. Hence `exp A ∈ LorentzGroup.restricted 3`.

11 declarations

theorem

$A^T = -\eta A \eta$ for $A \in \mathfrak{so}(1, 3)$

#transpose_eq_neg_eta_conj

Let $A$ be an element of the Lorentz algebra $\mathfrak{so}(1, 3)$ and let $\eta$ denote the Minkowski metric tensor. The transpose of the matrix representation of $A$ , denoted $A^T$ , satisfies the relation $A^T = -\eta A \eta$ .

theorem

$\exp(A^T) = \eta \exp(-A) \eta$ for $A \in \mathfrak{so}(1, 3)$

#exp_transpose_of_mem_algebra

Let $A$ be an element of the Lorentz algebra $\mathfrak{so}(1, 3)$ and let $\eta$ denote the Minkowski metric matrix. Then the matrix exponential of the transpose of $A$ satisfies the identity: $\exp(A^T) = \eta \exp(-A) \eta$

theorem

$\exp(A) \in O(1, 3)$ for $A \in \mathfrak{so}(1, 3)$

#exp_mem_lorentzGroup

Let $A$ be an element of the Lorentz algebra $\mathfrak{so}(1, 3)$ . Then the matrix exponential of $A$ , denoted $\exp(A)$ , is an element of the Lorentz group $O(1, 3)$ .

instance

Uniform space structure on matrices

#instUniformSpaceMatrix

Given that $\mathbb{K}$ is a uniform space, the space of $m \times n$ matrices over $\mathbb{K}$ is also equipped with a uniform space structure.

theorem

Trace of a Matrix Equals the Sum of its Diagonal Elements

#trace_eq_sum_diagonal

For any real matrix $A$ with rows and columns indexed by $\text{Fin } 1 \oplus \text{Fin } 3$ , the trace of $A$ equals the sum of its diagonal elements, i.e., $\operatorname{trace}(A) = \sum_i A_{ii}$ .

theorem

$\operatorname{tr}(A) = 0$ for $A \in \mathfrak{so}(1, 3)$

#trace_of_mem_is_zero

For any element $A$ of the Lorentz algebra $\mathfrak{so}(1, 3)$ (the Lie algebra of the Lorentz group in 1+3 Minkowski space), the trace of its matrix representation is zero, i.e., $\operatorname{tr}(A) = 0$ .

theorem

Invariance of Matrix Trace under Reindexing

#trace_reindex

For any semiring $R$ , finite types $n$ and $\iota$ , a bijection $e : n \simeq \iota$ , and an $n \times n$ matrix $A$ over $R$ , the trace of the matrix obtained by reindexing the rows and columns of $A$ using the inverse bijection $e^{-1}$ is equal to the trace of $A$ .

theorem

Commutativity of Matrix Exponential and Reindexing

#exp_reindex

For any real or complex-like field $k$ , finite types $n$ and $\iota$ , a bijection $e : n \simeq \iota$ , and an $n \times n$ matrix $A$ over $k$ , the matrix exponential of the matrix obtained by reindexing the rows and columns of $A$ using the inverse bijection $e^{-1}$ is equal to the matrix obtained by reindexing the rows and columns of the matrix exponential of $A$ using $e$ .

theorem

$\det(\exp A) = 1$ for $A \in \mathfrak{so}(1, 3)$

#exp_isProper

For any element $A$ of the Lorentz algebra $\mathfrak{so}(1, 3)$ , the matrix exponential $\exp(A)$ is a proper Lorentz transformation, meaning its determinant is equal to $1$ .

theorem

$\exp(A)$ is orthochronous for $A \in \mathfrak{so}(1, 3)$

#exp_isOrthochronous

For any element $A$ of the Lorentz algebra $\mathfrak{so}(1, 3)$ , its matrix exponential $\exp(A)$ is orthochronous. Specifically, the $(0,0)$ -component of the resulting Lorentz transformation matrix satisfies $(\exp A)_{00} \geq 1$ .

theorem

$\exp(A) \in SO^+(1, 3)$ for $A \in \mathfrak{so}(1, 3)$

#exp_mem_restricted_lorentzGroup

For any element $A$ of the Lorentz algebra $\mathfrak{so}(1, 3)$ , its matrix exponential $\exp(A)$ is an element of the restricted Lorentz group $SO^+(1, 3)$ .

Physlib.Relativity.LorentzAlgebra.ExponentialMap

Exponential map from the Lorentz algebra to the restricted Lorentz group

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

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

exp⁡(A)∈O(1,3)\exp(A) \in O(1, 3)exp(A)∈O(1,3) for A∈so(1,3)A \in \mathfrak{so}(1, 3)A∈so(1,3)

Uniform space structure on matrices

Trace of a Matrix Equals the Sum of its Diagonal Elements

tr⁡(A)=0\operatorname{tr}(A) = 0tr(A)=0 for A∈so(1,3)A \in \mathfrak{so}(1, 3)A∈so(1,3)

Invariance of Matrix Trace under Reindexing

Commutativity of Matrix Exponential and Reindexing

det⁡(exp⁡A)=1\det(\exp A) = 1det(expA)=1 for A∈so(1,3)A \in \mathfrak{so}(1, 3)A∈so(1,3)

exp⁡(A)\exp(A)exp(A) is orthochronous for A∈so(1,3)A \in \mathfrak{so}(1, 3)A∈so(1,3)

exp⁡(A)∈SO+(1,3)\exp(A) \in SO^+(1, 3)exp(A)∈SO+(1,3) for A∈so(1,3)A \in \mathfrak{so}(1, 3)A∈so(1,3)

$A^T = -\eta A \eta$ for $A \in \mathfrak{so}(1, 3)$

$\exp(A^T) = \eta \exp(-A) \eta$ for $A \in \mathfrak{so}(1, 3)$

$\exp(A) \in O(1, 3)$ for $A \in \mathfrak{so}(1, 3)$

$\operatorname{tr}(A) = 0$ for $A \in \mathfrak{so}(1, 3)$

$\det(\exp A) = 1$ for $A \in \mathfrak{so}(1, 3)$

$\exp(A)$ is orthochronous for $A \in \mathfrak{so}(1, 3)$

$\exp(A) \in SO^+(1, 3)$ for $A \in \mathfrak{so}(1, 3)$