Imports
/-
Copyright (c) 2025 Matteo Cipollina. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Matteo Cipollina
-/
module
public import Physlib.Mathematics.DataStructures.Matrix.LieTrace
public import Physlib.Relativity.LorentzAlgebra.Basic
public import Physlib.Relativity.LorentzGroup.Restricted.BasicExponential 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.
@[expose] public sectionattribute [local instance] Matrix.linftyOpNormedAlgebraattribute [local instance] Matrix.linftyOpNormedRingattribute [local instance] Matrix.instCompleteSpace
A key property of a Lorentz algebra element A is that its transpose
is related to its conjugation by the Minkowski metric η.
All goals completed! 🐙
_ = - (η * A.1 * η) := A:↥lorentzAlgebrah:(↑A)ᵀ * η = -η * ↑A⊢ -η * ↑A * η = -(η * ↑A * η) All goals completed! 🐙
The exponential of the transpose of a Lorentz algebra element.
This connects exp(Aᵀ) to a conjugation of exp(-A).
A:↥lorentzAlgebraP_gl:GL (Fin 1 ⊕ Fin 3) ℝ := { val := η, inv := η, val_inv := ⋯, inv_val := ⋯ }⊢ NormedSpace.exp (η * -↑A * η) = η * NormedSpace.exp (-↑A) * η
erw [A:↥lorentzAlgebraP_gl:GL (Fin 1 ⊕ Fin 3) ℝ := { val := η, inv := η, val_inv := ⋯, inv_val := ⋯ }⊢ ↑P_gl * NormedSpace.exp (-↑A) * ↑P_gl⁻¹ = η * NormedSpace.exp (-↑A) * ηA:↥lorentzAlgebraP_gl:GL (Fin 1 ⊕ Fin 3) ℝ := { val := η, inv := η, val_inv := ⋯, inv_val := ⋯ }⊢ ↑P_gl * NormedSpace.exp (-↑A) * ↑P_gl⁻¹ = η * NormedSpace.exp (-↑A) * η
All goals completed! 🐙The exponential of an element of the Lorentz algebra is a member of the Lorentz group.
set_option backward.isDefEq.respectTransparency false inAll goals completed! 🐙attribute [local instance] Matrix.linftyOpNormedAlgebrainstance [UniformSpace 𝕂] : UniformSpace (Matrix m n 𝕂) := 𝕂:Type ?u.5m:Type ?u.10n:Type ?u.9inst✝:UniformSpace 𝕂⊢ UniformSpace (Matrix m n 𝕂) 𝕂:Type ?u.5m:Type ?u.10n:Type ?u.9inst✝:UniformSpace 𝕂⊢ UniformSpace (m → n → 𝕂); All goals completed! 🐙The trace of a matrix equals the sum of its diagonal elements.
lemma trace_eq_sum_diagonal (A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) :
trace A = ∑ i, A i i := rflThe trace of any element of the Lorentz algebra is zero.
A:↥lorentzAlgebra⊢ ∑ i, ↑A i i = 0
A:↥lorentzAlgebrah_diag_zero:∀ (μ : Fin 1 ⊕ Fin 3), ↑A μ μ = 0⊢ ∑ i, ↑A i i = 0
All goals completed! 🐙@[simp]
lemma trace_reindex [Semiring R] [Fintype ι] (e : n ≃ ι) (A : Matrix n n R) :
trace (A.submatrix e.symm e.symm) = trace A := n:Type u_1R:Type u_2ι:Type u_3inst✝²:Fintype ninst✝¹:Semiring Rinst✝:Fintype ιe:n ≃ ιA:Matrix n n R⊢ (A.submatrix ⇑e.symm ⇑e.symm).trace = A.trace
n:Type u_1R:Type u_2ι:Type u_3inst✝²:Fintype ninst✝¹:Semiring Rinst✝:Fintype ιe:n ≃ ιA:Matrix n n R⊢ ∑ x, A (e.symm x) (e.symm x) = ∑ x, A x x
All goals completed! 🐙@[simp]
lemma exp_reindex {k : Type*}
[RCLike k] [Fintype ι] [DecidableEq ι] (e : n ≃ ι) (A : Matrix n n k) :
NormedSpace.exp (A.submatrix e.symm e.symm) = reindex e e (NormedSpace.exp A) := n:Type u_4ι:Type u_6inst✝⁴:Fintype ninst✝³:DecidableEq nk:Type u_7inst✝²:RCLike kinst✝¹:Fintype ιinst✝:DecidableEq ιe:n ≃ ιA:Matrix n n k⊢ NormedSpace.exp (A.submatrix ⇑e.symm ⇑e.symm) = (reindex e e) (NormedSpace.exp A)
n:Type u_4ι:Type u_6inst✝⁴:Fintype ninst✝³:DecidableEq nk:Type u_7inst✝²:RCLike kinst✝¹:Fintype ιinst✝:DecidableEq ιe:n ≃ ιA:Matrix n n kf:Matrix n n k ≃ₐ[k] Matrix ι ι k := reindexAlgEquiv k k e⊢ NormedSpace.exp (A.submatrix ⇑e.symm ⇑e.symm) = (reindex e e) (NormedSpace.exp A)
n:Type u_4ι:Type u_6inst✝⁴:Fintype ninst✝³:DecidableEq nk:Type u_7inst✝²:RCLike kinst✝¹:Fintype ιinst✝:DecidableEq ιe:n ≃ ιA:Matrix n n kf:Matrix n n k ≃ₐ[k] Matrix ι ι k := reindexAlgEquiv k k eh_cont:Continuous ⇑f⊢ NormedSpace.exp (A.submatrix ⇑e.symm ⇑e.symm) = (reindex e e) (NormedSpace.exp A)
All goals completed! 🐙attribute [local instance] Matrix.linftyOpNormedAlgebraThe exponential of an element of the Lorentz algebra is proper (has determinant 1).
A:↥lorentzAlgebrae:Fin 1 ⊕ Fin 3 ≃ Fin 4 := finSumFinEquiv⊢ (NormedSpace.exp ((↑A).submatrix ⇑e.symm ⇑e.symm)).det = 1
A:↥lorentzAlgebrae:Fin 1 ⊕ Fin 3 ≃ Fin 4 := finSumFinEquiv⊢ 1 = Real.exp ((reindex e e) ↑A).trace
erw [A:↥lorentzAlgebrae:Fin 1 ⊕ Fin 3 ≃ Fin 4 := finSumFinEquiv⊢ 1 = Real.exp A.1.trace A:↥lorentzAlgebrae:Fin 1 ⊕ Fin 3 ≃ Fin 4 := finSumFinEquiv⊢ 1 = Real.exp 0 A:↥lorentzAlgebrae:Fin 1 ⊕ Fin 3 ≃ Fin 4 := finSumFinEquiv⊢ 1 = 1All goals completed! 🐙The exponential of an element of the Lorentz algebra is orthochronous.
A:↥lorentzAlgebraγ:Path 0 A := { toFun := fun t => ↑t • A, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }exp_γ:Path 1 ⟨NormedSpace.exp ↑A, ⋯⟩ := { toFun := fun t => ⟨NormedSpace.exp ↑(γ t), ⋯⟩, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }h_joined:Joined 1 ⟨NormedSpace.exp ↑A, ⋯⟩h_connected:⟨NormedSpace.exp ↑A, ⋯⟩ ∈ connectedComponent 1⊢ LorentzGroup.IsOrthochronous 1
All goals completed! 🐙The exponential of an element of the Lorentz algebra is a member of the restricted Lorentz group.
theorem exp_mem_restricted_lorentzGroup (A : lorentzAlgebra) :
(⟨NormedSpace.exp A.1, exp_mem_lorentzGroup A⟩ : LorentzGroup 3) ∈
LorentzGroup.restricted 3 := A:↥lorentzAlgebra⊢ ⟨NormedSpace.exp ↑A, ⋯⟩ ∈ LorentzGroup.restricted 3
All goals completed! 🐙