221 lines
8 KiB
Text
221 lines
8 KiB
Text
/-
|
||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Joseph Tooby-Smith
|
||
-/
|
||
import HepLean.SpaceTime.LorentzGroup.Basic
|
||
import Mathlib.RepresentationTheory.Basic
|
||
import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
|
||
import HepLean.SpaceTime.LorentzGroup.Restricted
|
||
import HepLean.Meta.Informal
|
||
/-!
|
||
# 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.
|
||
|
||
-/
|
||
namespace SpaceTime
|
||
|
||
open Matrix
|
||
open MatrixGroups
|
||
open Complex
|
||
|
||
namespace SL2C
|
||
|
||
open SpaceTime
|
||
|
||
noncomputable section
|
||
|
||
/-!
|
||
|
||
## Some basic properties about SL(2, ℂ)
|
||
|
||
Possibly to be moved to mathlib at some point.
|
||
-/
|
||
|
||
lemma inverse_coe (M : SL(2, ℂ)) : M.1⁻¹ = (M⁻¹).1 := by
|
||
apply Matrix.inv_inj
|
||
simp only [SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq, one_ne_zero, not_false_eq_true,
|
||
nonsing_inv_nonsing_inv, SpecialLinearGroup.coe_inv]
|
||
have h1 : IsUnit M.1.det := by
|
||
simp
|
||
rw [Matrix.inv_adjugate M.1 h1]
|
||
· simp
|
||
· simp
|
||
|
||
lemma transpose_coe (M : SL(2, ℂ)) : M.1ᵀ = (M.transpose).1 := rfl
|
||
/-!
|
||
|
||
## 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.
|
||
|
||
-/
|
||
|
||
/-- Given an element `M ∈ SL(2, ℂ)` the linear map from `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` to
|
||
itself defined by `A ↦ M * A * Mᴴ`. -/
|
||
@[simps!]
|
||
def toLinearMapSelfAdjointMatrix (M : SL(2, ℂ)) :
|
||
selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) →ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where
|
||
toFun A := ⟨M.1 * A.1 * Matrix.conjTranspose M,
|
||
by
|
||
noncomm_ring [selfAdjoint.mem_iff, star_eq_conjTranspose,
|
||
conjTranspose_mul, conjTranspose_conjTranspose,
|
||
(star_eq_conjTranspose A.1).symm.trans $ selfAdjoint.mem_iff.mp A.2]⟩
|
||
map_add' A B := by
|
||
simp only [AddSubgroup.coe_add, AddMemClass.mk_add_mk, Subtype.mk.injEq]
|
||
noncomm_ring [AddSubmonoid.coe_add, AddSubgroup.coe_toAddSubmonoid, AddSubmonoid.mk_add_mk,
|
||
Subtype.mk.injEq]
|
||
map_smul' r A := by
|
||
noncomm_ring [selfAdjoint.val_smul, Algebra.mul_smul_comm, Algebra.smul_mul_assoc,
|
||
RingHom.id_apply]
|
||
|
||
/-- The representation of `SL(2, ℂ)` on `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` given by
|
||
`M A ↦ M * A * Mᴴ`. -/
|
||
@[simps!]
|
||
def repSelfAdjointMatrix : Representation ℝ SL(2, ℂ) $ selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where
|
||
toFun := toLinearMapSelfAdjointMatrix
|
||
map_one' := by
|
||
noncomm_ring [toLinearMapSelfAdjointMatrix, SpecialLinearGroup.coe_one, one_mul,
|
||
conjTranspose_one, mul_one, Subtype.coe_eta]
|
||
map_mul' M N := by
|
||
ext x i j : 3
|
||
noncomm_ring [toLinearMapSelfAdjointMatrix, SpecialLinearGroup.coe_mul, mul_assoc,
|
||
conjTranspose_mul, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.mul_apply]
|
||
|
||
/-- The representation of `SL(2, ℂ)` on `spaceTime` obtained from `toSelfAdjointMatrix` and
|
||
`repSelfAdjointMatrix`. -/
|
||
def repLorentzVector : Representation ℝ SL(2, ℂ) (LorentzVector 3) where
|
||
toFun M := toSelfAdjointMatrix.symm.comp ((repSelfAdjointMatrix M).comp
|
||
toSelfAdjointMatrix.toLinearMap)
|
||
map_one' := by
|
||
ext
|
||
simp
|
||
map_mul' M N := by
|
||
ext x : 3
|
||
simp
|
||
|
||
/-!
|
||
|
||
## Homomorphism to the Lorentz group
|
||
|
||
There is a group homomorphism from `SL(2, ℂ)` to the Lorentz group `𝓛`.
|
||
The purpose of this section is to define this homomorphism.
|
||
In the next section we will restrict this homomorphism to the restricted Lorentz group.
|
||
|
||
-/
|
||
|
||
lemma iff_det_selfAdjoint (Λ : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) : Λ ∈ LorentzGroup 3 ↔
|
||
∀ (x : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)),
|
||
det ((toSelfAdjointMatrix ∘
|
||
toLin LorentzVector.stdBasis LorentzVector.stdBasis Λ ∘ toSelfAdjointMatrix.symm) x).1
|
||
= det x.1 := by
|
||
rw [LorentzGroup.mem_iff_norm]
|
||
refine Iff.intro (fun h x => ?_) (fun h x => ?_)
|
||
· simpa [← det_eq_ηLin] using congrArg ofReal $ h (toSelfAdjointMatrix.symm x)
|
||
· simpa [det_eq_ηLin] using h (toSelfAdjointMatrix x)
|
||
|
||
/-- Given an element `M ∈ SL(2, ℂ)` the corresponding element of the Lorentz group. -/
|
||
@[simps!]
|
||
def toLorentzGroupElem (M : SL(2, ℂ)) : LorentzGroup 3 :=
|
||
⟨LinearMap.toMatrix LorentzVector.stdBasis LorentzVector.stdBasis (repLorentzVector M),
|
||
by simp [repLorentzVector, iff_det_selfAdjoint]⟩
|
||
|
||
/-- The group homomorphism from ` SL(2, ℂ)` to the Lorentz group `𝓛`. -/
|
||
@[simps!]
|
||
def toLorentzGroup : SL(2, ℂ) →* LorentzGroup 3 where
|
||
toFun := toLorentzGroupElem
|
||
map_one' := by
|
||
simp only [toLorentzGroupElem, _root_.map_one, LinearMap.toMatrix_one]
|
||
rfl
|
||
map_mul' M N := by
|
||
apply Subtype.eq
|
||
simp only [toLorentzGroupElem, _root_.map_mul, LinearMap.toMatrix_mul,
|
||
lorentzGroupIsGroup_mul_coe]
|
||
|
||
lemma toLorentzGroup_eq_σSAL (M : SL(2, ℂ)) :
|
||
toLorentzGroup M = LinearMap.toMatrix
|
||
PauliMatrix.σSAL PauliMatrix.σSAL (repSelfAdjointMatrix M) := by
|
||
rfl
|
||
|
||
lemma toLorentzGroup_eq_stdBasis (M : SL(2, ℂ)) :
|
||
toLorentzGroup M = LinearMap.toMatrix LorentzVector.stdBasis LorentzVector.stdBasis
|
||
(repLorentzVector M) := by rfl
|
||
|
||
lemma repLorentzVector_apply_eq_mulVec (v : LorentzVector 3) :
|
||
SL2C.repLorentzVector M v = (SL2C.toLorentzGroup M).1 *ᵥ v := by
|
||
simp only [toLorentzGroup, MonoidHom.coe_mk, OneHom.coe_mk, toLorentzGroupElem_coe]
|
||
have hv : v = (Finsupp.linearEquivFunOnFinite ℝ ℝ (Fin 1 ⊕ Fin 3))
|
||
(LorentzVector.stdBasis.repr v) := by rfl
|
||
nth_rewrite 2 [hv]
|
||
change _ = toLorentzGroup M *ᵥ (LorentzVector.stdBasis.repr v)
|
||
rw [toLorentzGroup_eq_stdBasis, LinearMap.toMatrix_mulVec_repr]
|
||
rfl
|
||
|
||
lemma repSelfAdjointMatrix_basis (i : Fin 1 ⊕ Fin 3) :
|
||
SL2C.repSelfAdjointMatrix M (PauliMatrix.σSAL i) =
|
||
∑ j, (toLorentzGroup M).1 j i •
|
||
PauliMatrix.σSAL j := by
|
||
rw [toLorentzGroup_eq_σSAL]
|
||
simp only [LinearMap.toMatrix_apply, Finset.univ_unique,
|
||
Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton]
|
||
nth_rewrite 1 [← (Basis.sum_repr PauliMatrix.σSAL
|
||
((repSelfAdjointMatrix M) (PauliMatrix.σSAL i)))]
|
||
rfl
|
||
|
||
lemma repSelfAdjointMatrix_σSA (i : Fin 1 ⊕ Fin 3) :
|
||
SL2C.repSelfAdjointMatrix M (PauliMatrix.σSA i) =
|
||
∑ j, (toLorentzGroup M⁻¹).1 i j • PauliMatrix.σSA j := by
|
||
have h1 : (toLorentzGroup M⁻¹).1 = minkowskiMatrix.dual (toLorentzGroup M).1 := by
|
||
simp
|
||
simp only [h1]
|
||
rw [PauliMatrix.σSA_minkowskiMetric_σSAL, _root_.map_smul]
|
||
rw [repSelfAdjointMatrix_basis]
|
||
rw [Finset.smul_sum]
|
||
apply congrArg
|
||
funext j
|
||
rw [smul_smul, PauliMatrix.σSA_minkowskiMetric_σSAL, smul_smul]
|
||
apply congrFun
|
||
apply congrArg
|
||
exact Eq.symm (minkowskiMatrix.dual_apply_minkowskiMatrix ((toLorentzGroup M).1) i j)
|
||
|
||
lemma repLorentzVector_stdBasis (i : Fin 1 ⊕ Fin 3) :
|
||
SL2C.repLorentzVector M (LorentzVector.stdBasis i) =
|
||
∑ j, (toLorentzGroup M).1 j i • LorentzVector.stdBasis j := by
|
||
simp only [repLorentzVector, MonoidHom.coe_mk, OneHom.coe_mk, LinearMap.coe_comp,
|
||
LinearEquiv.coe_coe, Function.comp_apply]
|
||
rw [toSelfAdjointMatrix_stdBasis]
|
||
rw [repSelfAdjointMatrix_basis]
|
||
rw [map_sum]
|
||
apply congrArg
|
||
funext j
|
||
simp
|
||
|
||
/-!
|
||
|
||
## 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.
|
||
|
||
-/
|
||
|
||
informal_lemma toLorentzGroup_det_one where
|
||
math :≈ "The determinant of the image of `SL(2, ℂ)` in the Lorentz group is one."
|
||
deps :≈ [``toLorentzGroup]
|
||
|
||
informal_lemma toLorentzGroup_timeComp_nonneg where
|
||
math :≈ "The time coponent of the image of `SL(2, ℂ)` in the Lorentz group is non-negative."
|
||
deps :≈ [``toLorentzGroup, ``LorentzGroup.timeComp]
|
||
|
||
informal_lemma toRestrictedLorentzGroup where
|
||
math :≈ "The homomorphism from `SL(2, ℂ)` to the restricted Lorentz group."
|
||
deps :≈ [``toLorentzGroup, ``toLorentzGroup_det_one, ``toLorentzGroup_timeComp_nonneg,
|
||
``LorentzGroup.Restricted]
|
||
|
||
/-! TODO: Define homomorphism from `SL(2, ℂ)` to the restricted Lorentz group. -/
|
||
end
|
||
end SL2C
|
||
|
||
end SpaceTime
|