The Restricted Lorentz Group

This file is currently a stub.

def LorentzGroup.restricted (d : ℕ) : Subgroup ↑(LorentzGroup d)

The restricted Lorentz group comprises the proper and orthochronous elements of the Lorentz group.

Equations

• LorentzGroup.restricted d = { carrier := {Λ : ↑(LorentzGroup d) | LorentzGroup.IsProper Λ ∧ LorentzGroup.IsOrthochronous Λ}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem LorentzGroup.restricted_normal_subgroup {d : ℕ} : (restricted d).Normal

The restricted Lorentz group is a normal subgroup of the Lorentz group.

theorem LorentzGroup.restricted_eq_identity_component_of_isConnected {d : ℕ} (h1 : IsConnected ↑(restricted d)) : ↑(restricted d) = connectedComponent 1

Given the hypothesis that the restricted Lorentz group is connected, the proof that the restricted lorentz group is equal to the connected component of the identity.