PhysLean Documentation

PhysLean.Relativity.LorentzGroup.Restricted.FromBoostRotation

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.

def LorentzGroup.toVelocity {d : } (Λ : (restricted d)) :

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

Equations
Instances For
    def LorentzGroup.toRotation {d : } (Λ : (restricted d)) :
    (Rotations d)

    A map from the restricted Lorentz group to rotations.

    Equations
    Instances For

      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.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For