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.

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

A key property of a Lorentz algebra element A is that its transpose is related to its conjugation by the Minkowski metric η.

theorem lorentzAlgebra.exp_transpose_of_mem_algebra (A : ↥lorentzAlgebra) : NormedSpace.exp ℝ (↑A).transpose = minkowskiMatrix * NormedSpace.exp ℝ (-↑A) * minkowskiMatrix

The exponential of the transpose of a Lorentz algebra element. This connects exp(Aᵀ) to a conjugation of exp(-A).

theorem lorentzAlgebra.exp_mem_lorentzGroup (A : ↥lorentzAlgebra) : NormedSpace.exp ℝ ↑A ∈ LorentzGroup 3

The exponential of an element of the Lorentz algebra is a member of the Lorentz group.

instance lorentzAlgebra.instUniformSpaceMatrix {𝕂 : Type u_1} {m : Type u_2} {n : Type u_3} [UniformSpace 𝕂] : UniformSpace (Matrix m n 𝕂)

Equations

• lorentzAlgebra.instUniformSpaceMatrix = id inferInstance

theorem lorentzAlgebra.trace_eq_sum_diagonal (A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) : A.trace = ∑ i : Fin 1 ⊕ Fin 3, A i i

The trace of a matrix equals the sum of its diagonal elements.

theorem lorentzAlgebra.trace_of_mem_is_zero (A : ↥lorentzAlgebra) : (↑A).trace = 0

The trace of any element of the Lorentz algebra is zero.

@[simp]

theorem lorentzAlgebra.Matrix.trace_reindex {n : Type u_1} {R : Type u_2} {ι : Type u_3} [Fintype n] [Semiring R] [Fintype ι] (e : n ≃ ι) (A : Matrix n n R) : (A.submatrix ⇑e.symm ⇑e.symm).trace = A.trace

@[simp]

theorem lorentzAlgebra.Matrix.exp_reindex {n : Type u_4} {ι : Type u_6} [Fintype n] [DecidableEq n] {k : Type u_7} [RCLike k] [Fintype ι] [DecidableEq ι] (e : n ≃ ι) (A : Matrix n n k) : NormedSpace.exp k (A.submatrix ⇑e.symm ⇑e.symm) = (Matrix.reindex e e) (NormedSpace.exp k A)

theorem lorentzAlgebra.exp_isProper (A : ↥lorentzAlgebra) : LorentzGroup.IsProper ⟨NormedSpace.exp ℝ ↑A, ⋯⟩

The exponential of an element of the Lorentz algebra is proper (has determinant 1).

theorem lorentzAlgebra.exp_isOrthochronous (A : ↥lorentzAlgebra) : LorentzGroup.IsOrthochronous ⟨NormedSpace.exp ℝ ↑A, ⋯⟩

The exponential of an element of the Lorentz algebra is orthochronous.

theorem lorentzAlgebra.exp_mem_restricted_lorentzGroup (A : ↥lorentzAlgebra) : ⟨NormedSpace.exp ℝ ↑A, ⋯⟩ ∈ LorentzGroup.restricted 3

The exponential of an element of the Lorentz algebra is a member of the restricted Lorentz group.