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_pauliBasis'_inl (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : (toSelfAdjointMap M) (PauliMatrix.pauliBasis' (Sum.inl 0)) = ((‖↑M 0 0‖ ^ 2 + ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • PauliMatrix.pauliBasis' (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.pauliBasis' (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.pauliBasis' (Sum.inr 1) + ((-‖↑M 0 0‖ ^ 2 - ‖↑M 0 1‖ ^ 2 + ‖↑M 1 0‖ ^ 2 + ‖↑M 1 1‖ ^ 2) / 2) • PauliMatrix.pauliBasis' (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_pauliBasis' (M : Matrix.SpecialLinearGroup (Fin 2) ℂ) : ↑(toLorentzGroup M) = (LinearMap.toMatrix PauliMatrix.pauliBasis' PauliMatrix.pauliBasis') (toSelfAdjointMap M)

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

theorem Lorentz.SL2C.toSelfAdjointMap_pauliBasis {M : Matrix.SpecialLinearGroup (Fin 2) ℂ} (i : Fin 1 ⊕ Fin 3) : (toSelfAdjointMap M) (PauliMatrix.pauliBasis i) = ∑ j : Fin 1 ⊕ Fin 3, ↑(toLorentzGroup M⁻¹) i j • PauliMatrix.pauliBasis 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 : Matrix.SpecialLinearGroup (Fin 2) ℂ →* ↥(LorentzGroup.restricted 3)

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

Equations

• Lorentz.SL2C.toRestrictedLorentzGroup = Lorentz.SL2C.toLorentzGroup.codRestrict (LorentzGroup.restricted 3) Lorentz.SL2C.toRestrictedLorentzGroup._proof_2

@[simp]

theorem Lorentz.SL2C.toRestrictedLorentzGroup_apply_coe_coe (n : Matrix.SpecialLinearGroup (Fin 2) ℂ) : ↑↑(toRestrictedLorentzGroup n) = toMatrix n