The group SL(2, ℂ) and it's relation to the Lorentz group

The aim of this file is to give the relationship between SL(2, ℂ) and the Lorentz group.

Some basic properties about SL(2, ℂ)

Possibly to be moved to mathlib at some point.

theorem Lorentz.SL2C.inverse_coe (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (↑M)⁻¹ = ↑M⁻¹

theorem Lorentz.SL2C.transpose_coe (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (↑M).transpose = ↑M.transpose

Representation of SL(2, ℂ) on spacetime

Through the correspondence between spacetime and self-adjoint matrices, we can define a representation a representation of SL(2, ℂ) on spacetime.

def Lorentz.SL2C.toSelfAdjointMap (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) →ₗ[ℝ] ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))

Given an element M ∈ SL(2, ℂ) the linear map from selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) to itself defined by A ↦ M * A * Mᴴ.

Equations

• Lorentz.SL2C.toSelfAdjointMap M = { toFun := fun (A : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) => ⟨↑M * ↑A * (↑M).conjTranspose, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Lorentz.SL2C.toSelfAdjointMap_apply_coe (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) (A : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) : ↑((toSelfAdjointMap M) A) = ↑M * ↑A * (↑M).conjTranspose

theorem Lorentz.SL2C.toSelfAdjointMap_apply_det (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) (A : ↥(selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))) : (↑((toSelfAdjointMap M) A)).det = (↑A).det

theorem Lorentz.SL2C.toSelfAdjointMap_apply_σSAL_inl (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (toSelfAdjointMap M) (PauliMatrix.σSAL (Sum.inl 0)) = ((‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • PauliMatrix.σSAL (Sum.inl 0) + -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re) • PauliMatrix.σSAL (Sum.inr 0) + (-(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re) • PauliMatrix.σSAL (Sum.inr 1) + ((-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • PauliMatrix.σSAL (Sum.inr 2)

def Lorentz.SL2C.toMatrix : Matrix.SpecialLinearGroup (Fin 2) ℂ →* Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ

The monoid homomorphisms from SL(2, ℂ) to matrices indexed by Fin 1 ⊕ Fin 3 formed by the action M A Mᴴ.

Equations

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

theorem Lorentz.SL2C.toMatrix_apply_contrMod (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) (v : ContrMod 3) : ContrMod.mulVec (toMatrix M) v = ContrMod.toSelfAdjoint.symm ((toSelfAdjointMap M) (ContrMod.toSelfAdjoint v))

theorem Lorentz.SL2C.toMatrix_mem_lorentzGroup (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : toMatrix M ∈ LorentzGroup 3

def Lorentz.SL2C.toLorentzGroup : Matrix.SpecialLinearGroup (Fin 2) ℂ →* ↑(LorentzGroup 3)

The group homomorphism from SL(2, ℂ) to the Lorentz group 𝓛.

Equations

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

@[simp]

theorem Lorentz.SL2C.toLorentzGroup_apply_coe (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : ↑(toLorentzGroup M) = toMatrix M

theorem Lorentz.SL2C.toLorentzGroup_eq_σSAL (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : ↑(toLorentzGroup M) = (LinearMap.toMatrix PauliMatrix.σSAL PauliMatrix.σSAL) (toSelfAdjointMap M)

theorem Lorentz.SL2C.toSelfAdjointMap_basis {M : Matrix.SpecialLinearGroup (Fin 2) ℂ} (i : Fin 1 ⊕ Fin 3) : (toSelfAdjointMap M) (PauliMatrix.σSAL i) = ∑ j : Fin 1 ⊕ Fin 3, ↑(toLorentzGroup M) j i • PauliMatrix.σSAL j

theorem Lorentz.SL2C.toSelfAdjointMap_σSA {M : Matrix.SpecialLinearGroup (Fin 2) ℂ} (i : Fin 1 ⊕ Fin 3) : (toSelfAdjointMap M) (PauliMatrix.σSA i) = ∑ j : Fin 1 ⊕ Fin 3, ↑(toLorentzGroup M⁻¹) i j • PauliMatrix.σSA j

theorem Lorentz.SL2C.toLorentzGroup_fst_col (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (fun (μ : Fin 1 ⊕ Fin 3) => ↑(toLorentzGroup M) μ (Sum.inl 0)) = fun (μ : Fin 1 ⊕ Fin 3) => match μ with | Sum.inl 0 => (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2 | Sum.inr 0 => -((↑M 0 1).re * (↑M 1 1).re + (↑M 0 1).im * (↑M 1 1).im + (↑M 0 0).im * (↑M 1 0).im + (↑M 0 0).re * (↑M 1 0).re) | Sum.inr 1 => -(↑M 0 0).re * (↑M 1 0).im + (↑M 1 0).re * (↑M 0 0).im - (↑M 0 1).re * (↑M 1 1).im + (↑M 0 1).im * (↑M 1 1).re | Sum.inr 2 => (-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2

The first column of the Lorentz matrix formed from an element of SL(2, ℂ).

theorem Lorentz.SL2C.toLorentzGroup_inl_inl (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : ↑(toLorentzGroup M) (Sum.inl 0) (Sum.inl 0) = (‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2

The first element of the image of SL(2, ℂ) in the Lorentz group.

theorem Lorentz.SL2C.toLorentzGroup_isOrthochronous (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : LorentzGroup.IsOrthochronous (toLorentzGroup M)

The image of SL(2, ℂ) in the Lorentz group is orthochronous.

Homomorphism to the restricted Lorentz group

The homomorphism toLorentzGroup restricts to a homomorphism to the restricted Lorentz group. In this section we will define this homomorphism.

theorem Lorentz.SL2C.toLorentzGroup_det_one (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (↑(toLorentzGroup M)).det = 1

The determinant of the image of SL(2, ℂ) in the Lorentz group is one.

def Lorentz.SL2C.toRestrictedLorentzGroup : InformalLemma

The homomorphism from SL(2, ℂ) to the restricted Lorentz group.

Equations

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