Merge pull request #178 from HEPLean/ComplexLorentz
feat: Complex Lorentz vectors
This commit is contained in:
Joseph Tooby-Smith
GitHub
commit
47d9649c44
5 changed files with 292 additions and 18 deletions
|
|
@ -81,9 +81,11 @@ import HepLean.SpaceTime.LorentzTensor.Real.Basic
|
|||
import HepLean.SpaceTime.LorentzTensor.Real.IndexNotation
|
||||
import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
|
||||
import HepLean.SpaceTime.LorentzVector.Basic
|
||||
import HepLean.SpaceTime.LorentzVector.Complex
|
||||
import HepLean.SpaceTime.LorentzVector.Contraction
|
||||
import HepLean.SpaceTime.LorentzVector.Covariant
|
||||
import HepLean.SpaceTime.LorentzVector.LorentzAction
|
||||
import HepLean.SpaceTime.LorentzVector.Modules
|
||||
import HepLean.SpaceTime.LorentzVector.NormOne
|
||||
import HepLean.SpaceTime.MinkowskiMetric
|
||||
import HepLean.SpaceTime.SL2C.Basic
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ open Matrix
|
|||
open MatrixGroups
|
||||
open Complex
|
||||
|
||||
/-- A 2×2-complex matrix formed from a space-time point. -/
|
||||
/-- A 2×2-complex matrix formed from a Lorentz vector point. -/
|
||||
@[simp]
|
||||
def toMatrix (x : LorentzVector 3) : Matrix (Fin 2) (Fin 2) ℂ :=
|
||||
!![x.time + x.space 2, x.space 0 - x.space 1 * I; x.space 0 + x.space 1 * I, x.time - x.space 2]
|
||||
|
|
@ -34,12 +34,12 @@ lemma toMatrix_isSelfAdjoint (x : LorentzVector 3) : IsSelfAdjoint (toMatrix x)
|
|||
simp [toMatrix, conj_ofReal]
|
||||
rfl
|
||||
|
||||
/-- A self-adjoint matrix formed from a space-time point. -/
|
||||
/-- A self-adjoint matrix formed from a Lorentz vector point. -/
|
||||
@[simps!]
|
||||
def toSelfAdjointMatrix' (x : LorentzVector 3) : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) :=
|
||||
⟨toMatrix x, toMatrix_isSelfAdjoint x⟩
|
||||
|
||||
/-- A self-adjoint matrix formed from a space-time point. -/
|
||||
/-- A self-adjoint matrix formed from a Lorentz vector point. -/
|
||||
@[simp]
|
||||
noncomputable def fromSelfAdjointMatrix' (x : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
|
||||
LorentzVector 3 := fun i =>
|
||||
|
|
|
|||
39
HepLean/SpaceTime/LorentzVector/Complex.lean
Normal file
39
HepLean/SpaceTime/LorentzVector/Complex.lean
Normal file
|
|
@ -0,0 +1,39 @@
|
|||
/-
|
||||
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 Mathlib.Data.Complex.Exponential
|
||||
import Mathlib.Analysis.InnerProductSpace.PiL2
|
||||
import HepLean.SpaceTime.SL2C.Basic
|
||||
import HepLean.SpaceTime.LorentzVector.Modules
|
||||
import HepLean.Meta.Informal
|
||||
import Mathlib.RepresentationTheory.Rep
|
||||
import HepLean.Tensors.Basic
|
||||
/-!
|
||||
|
||||
# Complex Lorentz vectors
|
||||
|
||||
We define complex Lorentz vectors in 4d space-time as representations of SL(2, C).
|
||||
|
||||
-/
|
||||
|
||||
noncomputable section
|
||||
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
open TensorProduct
|
||||
|
||||
namespace Lorentz
|
||||
|
||||
/-- The representation of `SL(2, ℂ)` on complex vectors corresponding to contravariant
|
||||
Lorentz vectors. -/
|
||||
def complexContr : Rep ℂ SL(2, ℂ) := Rep.of ContrℂModule.SL2CRep
|
||||
|
||||
/-- The representation of `SL(2, ℂ)` on complex vectors corresponding to contravariant
|
||||
Lorentz vectors. -/
|
||||
def complexCo : Rep ℂ SL(2, ℂ) := Rep.of CoℂModule.SL2CRep
|
||||
|
||||
end Lorentz
|
||||
end
|
||||
162
HepLean/SpaceTime/LorentzVector/Modules.lean
Normal file
162
HepLean/SpaceTime/LorentzVector/Modules.lean
Normal file
|
|
@ -0,0 +1,162 @@
|
|||
/-
|
||||
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.Meta.Informal
|
||||
import HepLean.SpaceTime.SL2C.Basic
|
||||
import Mathlib.RepresentationTheory.Rep
|
||||
import HepLean.Tensors.Basic
|
||||
import Mathlib.Logic.Equiv.TransferInstance
|
||||
/-!
|
||||
|
||||
## Modules associated with Lorentz vectors
|
||||
|
||||
These have not yet been fully-implmented.
|
||||
|
||||
We define these modules to prevent casting between different types of Lorentz vectors.
|
||||
|
||||
-/
|
||||
|
||||
namespace Lorentz
|
||||
|
||||
noncomputable section
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
|
||||
/-- The module for contravariant (up-index) complex Lorentz vectors. -/
|
||||
structure ContrℂModule where
|
||||
/-- The underlying value as a vector `Fin 1 ⊕ Fin 3 → ℂ`. -/
|
||||
val : Fin 1 ⊕ Fin 3 → ℂ
|
||||
|
||||
namespace ContrℂModule
|
||||
|
||||
/-- The equivalence between `ContrℂModule` and `Fin 1 ⊕ Fin 3 → ℂ`. -/
|
||||
def toFin13ℂFun : ContrℂModule ≃ (Fin 1 ⊕ Fin 3 → ℂ) where
|
||||
toFun v := v.val
|
||||
invFun f := ⟨f⟩
|
||||
left_inv _ := rfl
|
||||
right_inv _ := rfl
|
||||
|
||||
/-- The instance of `AddCommMonoid` on `ContrℂModule` defined via its equivalence
|
||||
with `Fin 1 ⊕ Fin 3 → ℂ`. -/
|
||||
instance : AddCommMonoid ContrℂModule := Equiv.addCommMonoid toFin13ℂFun
|
||||
|
||||
/-- The instance of `AddCommGroup` on `ContrℂModule` defined via its equivalence
|
||||
with `Fin 1 ⊕ Fin 3 → ℂ`. -/
|
||||
instance : AddCommGroup ContrℂModule := Equiv.addCommGroup toFin13ℂFun
|
||||
|
||||
/-- The instance of `Module` on `ContrℂModule` defined via its equivalence
|
||||
with `Fin 1 ⊕ Fin 3 → ℂ`. -/
|
||||
instance : Module ℂ ContrℂModule := Equiv.module ℂ toFin13ℂFun
|
||||
|
||||
/-- The linear equivalence between `ContrℂModule` and `(Fin 1 ⊕ Fin 3 → ℂ)`. -/
|
||||
@[simps!]
|
||||
def toFin13ℂEquiv : ContrℂModule ≃ₗ[ℂ] (Fin 1 ⊕ Fin 3 → ℂ) where
|
||||
toFun := toFin13ℂFun
|
||||
map_add' := fun _ _ => rfl
|
||||
map_smul' := fun _ _ => rfl
|
||||
invFun := toFin13ℂFun.symm
|
||||
left_inv := fun _ => rfl
|
||||
right_inv := fun _ => rfl
|
||||
|
||||
/-- The underlying element of `Fin 1 ⊕ Fin 3 → ℂ` of a element in `ContrℂModule` defined
|
||||
through the linear equivalence `toFin13ℂEquiv`. -/
|
||||
abbrev toFin13ℂ (ψ : ContrℂModule) := toFin13ℂEquiv ψ
|
||||
|
||||
/-- The representation of the Lorentz group on `ContrℂModule`. -/
|
||||
def lorentzGroupRep : Representation ℂ (LorentzGroup 3) ContrℂModule where
|
||||
toFun M := {
|
||||
toFun := fun v => toFin13ℂEquiv.symm ((M.1.map ofReal) *ᵥ v.toFin13ℂ),
|
||||
map_add' := by
|
||||
intro ψ ψ'
|
||||
simp [mulVec_add]
|
||||
map_smul' := by
|
||||
intro r ψ
|
||||
simp [mulVec_smul]}
|
||||
map_one' := by
|
||||
ext i
|
||||
simp
|
||||
map_mul' M N := by
|
||||
ext i
|
||||
simp
|
||||
|
||||
/-- The representation of the SL(2, ℂ) on `ContrℂModule` induced by the representation of the
|
||||
Lorentz group. -/
|
||||
def SL2CRep : Representation ℂ SL(2, ℂ) ContrℂModule :=
|
||||
MonoidHom.comp lorentzGroupRep SpaceTime.SL2C.toLorentzGroup
|
||||
|
||||
end ContrℂModule
|
||||
|
||||
/-- The module for covariant (up-index) complex Lorentz vectors. -/
|
||||
structure CoℂModule where
|
||||
/-- The underlying value as a vector `Fin 1 ⊕ Fin 3 → ℂ`. -/
|
||||
val : Fin 1 ⊕ Fin 3 → ℂ
|
||||
|
||||
namespace CoℂModule
|
||||
|
||||
/-- The equivalence between `CoℂModule` and `Fin 1 ⊕ Fin 3 → ℂ`. -/
|
||||
def toFin13ℂFun : CoℂModule ≃ (Fin 1 ⊕ Fin 3 → ℂ) where
|
||||
toFun v := v.val
|
||||
invFun f := ⟨f⟩
|
||||
left_inv _ := rfl
|
||||
right_inv _ := rfl
|
||||
|
||||
/-- The instance of `AddCommMonoid` on `CoℂModule` defined via its equivalence
|
||||
with `Fin 1 ⊕ Fin 3 → ℂ`. -/
|
||||
instance : AddCommMonoid CoℂModule := Equiv.addCommMonoid toFin13ℂFun
|
||||
|
||||
/-- The instance of `AddCommGroup` on `CoℂModule` defined via its equivalence
|
||||
with `Fin 1 ⊕ Fin 3 → ℂ`. -/
|
||||
instance : AddCommGroup CoℂModule := Equiv.addCommGroup toFin13ℂFun
|
||||
|
||||
/-- The instance of `Module` on `CoℂModule` defined via its equivalence
|
||||
with `Fin 1 ⊕ Fin 3 → ℂ`. -/
|
||||
instance : Module ℂ CoℂModule := Equiv.module ℂ toFin13ℂFun
|
||||
|
||||
/-- The linear equivalence between `CoℂModule` and `(Fin 1 ⊕ Fin 3 → ℂ)`. -/
|
||||
@[simps!]
|
||||
def toFin13ℂEquiv : CoℂModule ≃ₗ[ℂ] (Fin 1 ⊕ Fin 3 → ℂ) where
|
||||
toFun := toFin13ℂFun
|
||||
map_add' := fun _ _ => rfl
|
||||
map_smul' := fun _ _ => rfl
|
||||
invFun := toFin13ℂFun.symm
|
||||
left_inv := fun _ => rfl
|
||||
right_inv := fun _ => rfl
|
||||
|
||||
/-- The underlying element of `Fin 1 ⊕ Fin 3 → ℂ` of a element in `CoℂModule` defined
|
||||
through the linear equivalence `toFin13ℂEquiv`. -/
|
||||
abbrev toFin13ℂ (ψ : CoℂModule) := toFin13ℂEquiv ψ
|
||||
|
||||
/-- The representation of the Lorentz group on `CoℂModule`. -/
|
||||
def lorentzGroupRep : Representation ℂ (LorentzGroup 3) CoℂModule where
|
||||
toFun M := {
|
||||
toFun := fun v => toFin13ℂEquiv.symm ((M.1.map ofReal)⁻¹ᵀ *ᵥ v.toFin13ℂ),
|
||||
map_add' := by
|
||||
intro ψ ψ'
|
||||
simp [mulVec_add]
|
||||
map_smul' := by
|
||||
intro r ψ
|
||||
simp [mulVec_smul]}
|
||||
map_one' := by
|
||||
ext i
|
||||
simp
|
||||
map_mul' M N := by
|
||||
ext1 x
|
||||
simp only [SpecialLinearGroup.coe_mul, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.mul_apply,
|
||||
LinearEquiv.apply_symm_apply, mulVec_mulVec, EmbeddingLike.apply_eq_iff_eq]
|
||||
refine (congrFun (congrArg _ ?_) _)
|
||||
simp only [lorentzGroupIsGroup_mul_coe, Matrix.map_mul]
|
||||
rw [Matrix.mul_inv_rev]
|
||||
exact transpose_mul _ _
|
||||
|
||||
/-- The representation of the SL(2, ℂ) on `ContrℂModule` induced by the representation of the
|
||||
Lorentz group. -/
|
||||
def SL2CRep : Representation ℂ SL(2, ℂ) CoℂModule :=
|
||||
MonoidHom.comp lorentzGroupRep SpaceTime.SL2C.toLorentzGroup
|
||||
|
||||
end CoℂModule
|
||||
|
||||
end
|
||||
end Lorentz
|
||||
|
|
@ -9,6 +9,7 @@ import Mathlib.CategoryTheory.Monoidal.Category
|
|||
import Mathlib.CategoryTheory.Comma.Over
|
||||
import Mathlib.CategoryTheory.Core
|
||||
import HepLean.SpaceTime.WeylFermion.Basic
|
||||
import HepLean.SpaceTime.LorentzVector.Complex
|
||||
/-!
|
||||
|
||||
## Category over color
|
||||
|
|
@ -49,8 +50,85 @@ lemma toEquiv_symm_apply (m : f ⟶ g) (i : g.left) :
|
|||
f.hom ((toEquiv m).symm i) = g.hom i := by
|
||||
simpa [toEquiv, types_comp] using congrFun m.inv.w i
|
||||
|
||||
lemma toEquiv_comp_hom (m : f ⟶ g) : g.hom ∘ (toEquiv m) = f.hom := by
|
||||
ext x
|
||||
simpa [types_comp, toEquiv] using congrFun m.hom.w x
|
||||
|
||||
end Hom
|
||||
|
||||
instance (C : Type) : MonoidalCategoryStruct (OverColor C) where
|
||||
tensorObj f g := Over.mk (Sum.elim f.hom g.hom)
|
||||
tensorUnit := Over.mk Empty.elim
|
||||
whiskerLeft X Y1 Y2 m := Over.isoMk (Equiv.sumCongr (Equiv.refl X.left) (Hom.toEquiv m)).toIso
|
||||
(by
|
||||
ext x
|
||||
simp only [Functor.id_obj, Functor.const_obj_obj, Over.mk_left, Equiv.toIso_hom, Over.mk_hom,
|
||||
types_comp_apply, Equiv.sumCongr_apply, Equiv.coe_refl]
|
||||
rw [Sum.elim_map, Hom.toEquiv_comp_hom]
|
||||
rfl)
|
||||
whiskerRight m X := Over.isoMk (Equiv.sumCongr (Hom.toEquiv m) (Equiv.refl X.left)).toIso
|
||||
(by
|
||||
ext x
|
||||
simp only [Functor.id_obj, Functor.const_obj_obj, Over.mk_left, Equiv.toIso_hom, Over.mk_hom,
|
||||
types_comp_apply, Equiv.sumCongr_apply, Equiv.coe_refl]
|
||||
rw [Sum.elim_map, Hom.toEquiv_comp_hom]
|
||||
rfl)
|
||||
associator X Y Z := {
|
||||
hom := Over.isoMk (Equiv.sumAssoc X.left Y.left Z.left).toIso (by
|
||||
simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Functor.const_obj_obj, Equiv.sumAssoc,
|
||||
Equiv.toIso_hom, Equiv.coe_fn_mk, types_comp]
|
||||
ext x
|
||||
simp only [Function.comp_apply]
|
||||
cases x with
|
||||
| inl val =>
|
||||
cases val with
|
||||
| inl val_1 => simp_all only [Sum.elim_inl]
|
||||
| inr val_2 => simp_all only [Sum.elim_inl, Sum.elim_inr, Function.comp_apply]
|
||||
| inr val_1 => simp_all only [Sum.elim_inr, Function.comp_apply]),
|
||||
inv := (Over.isoMk (Equiv.sumAssoc X.left Y.left Z.left).toIso (by
|
||||
simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Functor.const_obj_obj, Equiv.sumAssoc,
|
||||
Equiv.toIso_hom, Equiv.coe_fn_mk, types_comp]
|
||||
ext x
|
||||
simp only [Function.comp_apply]
|
||||
cases x with
|
||||
| inl val =>
|
||||
cases val with
|
||||
| inl val_1 => simp_all only [Sum.elim_inl]
|
||||
| inr val_2 => simp_all only [Sum.elim_inl, Sum.elim_inr, Function.comp_apply]
|
||||
| inr val_1 => simp_all only [Sum.elim_inr, Function.comp_apply])).symm,
|
||||
hom_inv_id := by
|
||||
apply CategoryTheory.Iso.ext
|
||||
erw [CategoryTheory.Iso.trans_hom]
|
||||
simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.hom_inv_id]
|
||||
rfl,
|
||||
inv_hom_id := by
|
||||
apply CategoryTheory.Iso.ext
|
||||
erw [CategoryTheory.Iso.trans_hom]
|
||||
simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.inv_hom_id]
|
||||
rfl}
|
||||
leftUnitor X := {
|
||||
hom := Over.isoMk (Equiv.emptySum Empty X.left).toIso
|
||||
inv := (Over.isoMk (Equiv.emptySum Empty X.left).toIso).symm
|
||||
hom_inv_id := by
|
||||
apply CategoryTheory.Iso.ext
|
||||
erw [CategoryTheory.Iso.trans_hom]
|
||||
simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.hom_inv_id]
|
||||
rfl,
|
||||
inv_hom_id := by
|
||||
apply CategoryTheory.Iso.ext
|
||||
erw [CategoryTheory.Iso.trans_hom]}
|
||||
rightUnitor X := {
|
||||
hom := Over.isoMk (Equiv.sumEmpty X.left Empty).toIso
|
||||
inv := (Over.isoMk (Equiv.sumEmpty X.left Empty).toIso).symm
|
||||
hom_inv_id := by
|
||||
apply CategoryTheory.Iso.ext
|
||||
erw [CategoryTheory.Iso.trans_hom]
|
||||
simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.hom_inv_id]
|
||||
rfl,
|
||||
inv_hom_id := by
|
||||
apply CategoryTheory.Iso.ext
|
||||
erw [CategoryTheory.Iso.trans_hom]}
|
||||
|
||||
end OverColor
|
||||
|
||||
end IndexNotation
|
||||
|
|
@ -72,6 +150,8 @@ inductive Color
|
|||
| downL : Color
|
||||
| upR : Color
|
||||
| downR : Color
|
||||
| up : Color
|
||||
| down : Color
|
||||
|
||||
/-- The corresponding representations associated with a color. -/
|
||||
def colorToRep (c : Color) : Rep ℂ SL(2, ℂ) :=
|
||||
|
|
@ -80,6 +160,8 @@ def colorToRep (c : Color) : Rep ℂ SL(2, ℂ) :=
|
|||
| Color.downL => leftHanded
|
||||
| Color.upR => altRightHanded
|
||||
| Color.downR => rightHanded
|
||||
| Color.up => Lorentz.complexContr
|
||||
| Color.down => Lorentz.complexCo
|
||||
|
||||
/-- The linear equivalence between `colorToRep c1` and `colorToRep c2` when `c1 = c2`. -/
|
||||
def colorToRepCongr {c1 c2 : Color} (h : c1 = c2) : colorToRep c1 ≃ₗ[ℂ] colorToRep c2 where
|
||||
|
|
@ -172,41 +254,30 @@ def colorFun : OverColor Color ⥤ Rep ℂ SL(2, ℂ) where
|
|||
obj := colorFun.obj'
|
||||
map := colorFun.map'
|
||||
map_id f := by
|
||||
simp only
|
||||
ext x
|
||||
refine PiTensorProduct.induction_on' x ?_ (by
|
||||
intro x y hx hy
|
||||
refine PiTensorProduct.induction_on' x (fun r x => ?_) (fun x y hx hy => by
|
||||
simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp,
|
||||
Function.comp_apply, hy])
|
||||
intro r x
|
||||
simp only [CategoryTheory.Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod,
|
||||
_root_.map_smul, Action.id_hom, ModuleCat.id_apply]
|
||||
apply congrArg
|
||||
rw [colorFun.map']
|
||||
erw [colorFun.mapToLinearEquiv'_tprod]
|
||||
apply congrArg
|
||||
funext i
|
||||
rfl
|
||||
exact congrArg _ (funext (fun i => rfl))
|
||||
map_comp {X Y Z} f g := by
|
||||
simp only
|
||||
ext x
|
||||
refine PiTensorProduct.induction_on' x ?_ (by
|
||||
intro x y hx hy
|
||||
refine PiTensorProduct.induction_on' x (fun r x => ?_) (fun x y hx hy => by
|
||||
simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp,
|
||||
Function.comp_apply, hy])
|
||||
intro r x
|
||||
simp only [Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod, _root_.map_smul,
|
||||
Action.comp_hom, ModuleCat.coe_comp, Function.comp_apply]
|
||||
apply congrArg
|
||||
rw [colorFun.map', colorFun.map', colorFun.map']
|
||||
simp only
|
||||
change (colorFun.mapToLinearEquiv' (CategoryTheory.CategoryStruct.comp f g))
|
||||
((PiTensorProduct.tprod ℂ) x) =
|
||||
(colorFun.mapToLinearEquiv' g) ((colorFun.mapToLinearEquiv' f) ((PiTensorProduct.tprod ℂ) x))
|
||||
rw [colorFun.mapToLinearEquiv'_tprod, colorFun.mapToLinearEquiv'_tprod]
|
||||
erw [colorFun.mapToLinearEquiv'_tprod]
|
||||
apply congrArg
|
||||
funext i
|
||||
refine congrArg _ (funext (fun i => ?_))
|
||||
simp only [colorToRepCongr, Function.comp_apply, Equiv.cast_symm, LinearEquiv.coe_mk,
|
||||
Equiv.cast_apply, cast_cast, cast_inj]
|
||||
rfl
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue