Rotations

This file describes the embedding of SO(3) into LorentzGroup 3.

def LorentzGroup.SO3ToMatrix (A : GroupTheory.SO3) : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ

Given a element of SO(3) the matrix corresponding to a space-time rotation.

Equations

• LorentzGroup.SO3ToMatrix A = Matrix.fromBlocks 1 0 0 ↑A

theorem LorentzGroup.SO3ToMatrix_in_LorentzGroup (A : GroupTheory.SO3) : SO3ToMatrix A ∈ LorentzGroup 3

theorem LorentzGroup.SO3ToMatrix_injective : Function.Injective SO3ToMatrix

def LorentzGroup.SO3ToLorentz : GroupTheory.SO3 →* ↑(LorentzGroup 3)

Given a element of SO(3) the element of the Lorentz group corresponding to a space-time rotation.

Equations

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