1. Physlib
  2. Relativity
  3. LorentzGroup
  4. Restricted
  5. FromBoostRotation
Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Relativity.LorentzGroup.Rotations public import Physlib.Relativity.LorentzGroup.Boosts.Generalized

The construction of an element of the Lorentz group from a boost and a rotation

The main result of this module is the homeomorphism toBoostRotation from the restricted Lorentz group to the product of Lorentz velocities and rotations.

The inverse of this homeomorphism writes elements of the restricted Lorentz group as a product of a generalized boost and a rotation.

@[expose] public section

The Lorentz velocity obtained from toVector Λ where Λ is an element of the restricted Lorentz group.

d:ℕΛ:↥(restricted d)h:1 ≤ ↑↑Λ (Sum.inl 0) (Sum.inl 0)⊢ 0 < ↑↑Λ (Sum.inl 0) (Sum.inl 0) All goals completed! 🐙⟩
@[fun_prop] lemma toVelocity_continuous {d} : Continuous (toVelocity : LorentzGroup.restricted d → Lorentz.Velocity d) := d:ℕ⊢ Continuous toVelocity d:ℕ⊢ Continuous fun x => toVector ↑x All goals completed! 🐙

A map from the restricted Lorentz group to rotations.

d:ℕΛ:↥(restricted d)⊢ IsProper (generalizedBoost (toVelocity Λ) 0) All goals completed! 🐙⟩
@[fun_prop] lemma toRotation_continuous {d} : Continuous (toRotation : LorentzGroup.restricted d → Rotations d) := d:ℕ⊢ Continuous toRotation d:ℕ⊢ Continuous fun x => (generalizedBoost 0 (toVelocity x))⁻¹ * ↑x d:ℕ⊢ Continuous fun x => (generalizedBoost 0 (toVelocity x))⁻¹ * ↑x All goals completed! 🐙

The homeomorphism from the restricted Lorentz group to the product of Lorentz.Velocity d and Matrix.specialOrthogonalGroup (Fin d) ℝ. The inverse of this map writes an element of the restricted Lorentz group as a product of a boost and a rotation.

d:ℕp:↑(Lorentz.Velocity d) × ↥(specialOrthogonalGroup (Fin d) ℝ)v:Lorentz.Vector dhv:v ∈ Lorentz.Velocity dR:↥(specialOrthogonalGroup (Fin d) ℝ)h0:toVector (generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R)) = v⊢ ⟨(generalizedBoost 0 (toVelocity ⟨generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R), ⋯⟩))⁻¹ * ↑⟨generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R), ⋯⟩, ⋯⟩ = ofSpecialOrthogonal R d:ℕp:↑(Lorentz.Velocity d) × ↥(specialOrthogonalGroup (Fin d) ℝ)v:Lorentz.Vector dhv:v ∈ Lorentz.Velocity dR:↥(specialOrthogonalGroup (Fin d) ℝ)h0:toVector (generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R)) = v⊢ ↑⟨(generalizedBoost 0 (toVelocity ⟨generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R), ⋯⟩))⁻¹ * ↑⟨generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R), ⋯⟩, ⋯⟩ = ↑(ofSpecialOrthogonal R) d:ℕp:↑(Lorentz.Velocity d) × ↥(specialOrthogonalGroup (Fin d) ℝ)v:Lorentz.Vector dhv:v ∈ Lorentz.Velocity dR:↥(specialOrthogonalGroup (Fin d) ℝ)h0:toVector (generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R)) = v⊢ (generalizedBoost 0 (toVelocity ⟨generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R), ⋯⟩))⁻¹ * (generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R)) = ↑(ofSpecialOrthogonal R) d:ℕp:↑(Lorentz.Velocity d) × ↥(specialOrthogonalGroup (Fin d) ℝ)v:Lorentz.Vector dhv:v ∈ Lorentz.Velocity dR:↥(specialOrthogonalGroup (Fin d) ℝ)h0:toVector (generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R)) = v⊢ (generalizedBoost 0 (toVelocity ⟨generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R), ⋯⟩))⁻¹ * (generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R)) = (generalizedBoost 0 ⟨v, hv⟩)⁻¹ * (generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R))d:ℕp:↑(Lorentz.Velocity d) × ↥(specialOrthogonalGroup (Fin d) ℝ)v:Lorentz.Vector dhv:v ∈ Lorentz.Velocity dR:↥(specialOrthogonalGroup (Fin d) ℝ)h0:toVector (generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R)) = v⊢ (generalizedBoost 0 ⟨v, hv⟩)⁻¹ * (generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R)) = ↑(ofSpecialOrthogonal R) d:ℕp:↑(Lorentz.Velocity d) × ↥(specialOrthogonalGroup (Fin d) ℝ)v:Lorentz.Vector dhv:v ∈ Lorentz.Velocity dR:↥(specialOrthogonalGroup (Fin d) ℝ)h0:toVector (generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R)) = v⊢ (generalizedBoost 0 (toVelocity ⟨generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R), ⋯⟩))⁻¹ * (generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R)) = (generalizedBoost 0 ⟨v, hv⟩)⁻¹ * (generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R)) d:ℕp:↑(Lorentz.Velocity d) × ↥(specialOrthogonalGroup (Fin d) ℝ)v:Lorentz.Vector dhv:v ∈ Lorentz.Velocity dR:↥(specialOrthogonalGroup (Fin d) ℝ)h0:toVector (generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R)) = v⊢ toVelocity ⟨generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R), ⋯⟩ = ⟨v, hv⟩ d:ℕp:↑(Lorentz.Velocity d) × ↥(specialOrthogonalGroup (Fin d) ℝ)v:Lorentz.Vector dhv:v ∈ Lorentz.Velocity dR:↥(specialOrthogonalGroup (Fin d) ℝ)h0:toVector (generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R)) = v⊢ ↑(toVelocity ⟨generalizedBoost 0 ⟨v, hv⟩ * ↑(ofSpecialOrthogonal R), ⋯⟩) = ↑⟨v, hv⟩ All goals completed! 🐙 All goals completed! 🐙 continuous_toFun := d:ℕ⊢ Continuous fun Λ => (toVelocity Λ, ofSpecialOrthogonal.symm (toRotation Λ)) All goals completed! 🐙 continuous_invFun := d:ℕ⊢ Continuous fun p => ⟨generalizedBoost 0 p.1 * ↑(ofSpecialOrthogonal p.2), ⋯⟩ All goals completed! 🐙

Every element of the restricted Lorentz group can be written as a product of a generalized boost and a rotation.

All goals completed! 🐙⟩