refactor: Move complex vec
This commit is contained in:
jstoobysmith
parent
e3ad445866
commit
236e99bd33
13 changed files with 23 additions and 23 deletions
|
|
@ -3,7 +3,7 @@ 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.MinkowskiMatrix
|
||||
import HepLean.Lorentz.MinkowskiMatrix
|
||||
import Mathlib.Algebra.Lie.Classical
|
||||
import HepLean.Lorentz.RealVector.Basic
|
||||
/-!
|
||||
|
|
|
|||
155
HepLean/Lorentz/ComplexVector/Basic.lean
Normal file
155
HepLean/Lorentz/ComplexVector/Basic.lean
Normal file
|
|
@ -0,0 +1,155 @@
|
|||
/-
|
||||
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.Lorentz.ComplexVector.Modules
|
||||
import HepLean.Meta.Informal
|
||||
import Mathlib.RepresentationTheory.Rep
|
||||
import HepLean.SpaceTime.PauliMatrices.SelfAdjoint
|
||||
/-!
|
||||
|
||||
# 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
|
||||
open SpaceTime
|
||||
|
||||
namespace Lorentz
|
||||
|
||||
/-- The representation of `SL(2, ℂ)` on complex vectors corresponding to contravariant
|
||||
Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
|
||||
def complexContr : Rep ℂ SL(2, ℂ) := Rep.of ContrℂModule.SL2CRep
|
||||
|
||||
/-- The representation of `SL(2, ℂ)` on complex vectors corresponding to contravariant
|
||||
Lorentz vectors. In index notation these have a down index `ψⁱ`. -/
|
||||
def complexCo : Rep ℂ SL(2, ℂ) := Rep.of CoℂModule.SL2CRep
|
||||
|
||||
/-- The standard basis of complex contravariant Lorentz vectors. -/
|
||||
def complexContrBasis : Basis (Fin 1 ⊕ Fin 3) ℂ complexContr :=
|
||||
Basis.ofEquivFun ContrℂModule.toFin13ℂEquiv
|
||||
|
||||
@[simp]
|
||||
lemma complexContrBasis_toFin13ℂ (i :Fin 1 ⊕ Fin 3) :
|
||||
(complexContrBasis i).toFin13ℂ = Pi.single i 1 := by
|
||||
simp only [complexContrBasis, Basis.coe_ofEquivFun]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma complexContrBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 1 ⊕ Fin 3) :
|
||||
(LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M) i j =
|
||||
(LorentzGroup.toComplex (SL2C.toLorentzGroup M)) i j := by
|
||||
rw [LinearMap.toMatrix_apply]
|
||||
simp only [complexContrBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply, transpose_apply]
|
||||
change (((LorentzGroup.toComplex (SL2C.toLorentzGroup M))) *ᵥ (Pi.single j 1)) i = _
|
||||
simp only [mulVec_single, transpose_apply, mul_one]
|
||||
|
||||
lemma complexContrBasis_ρ_val (M : SL(2,ℂ)) (v : complexContr) :
|
||||
((complexContr.ρ M) v).val =
|
||||
LorentzGroup.toComplex (SL2C.toLorentzGroup M) *ᵥ v.val := by
|
||||
rfl
|
||||
|
||||
/-- The standard basis of complex contravariant Lorentz vectors indexed by `Fin 4`. -/
|
||||
def complexContrBasisFin4 : Basis (Fin 4) ℂ complexContr :=
|
||||
Basis.reindex complexContrBasis finSumFinEquiv
|
||||
|
||||
/-- The standard basis of complex covariant Lorentz vectors. -/
|
||||
def complexCoBasis : Basis (Fin 1 ⊕ Fin 3) ℂ complexCo :=
|
||||
Basis.ofEquivFun CoℂModule.toFin13ℂEquiv
|
||||
|
||||
@[simp]
|
||||
lemma complexCoBasis_toFin13ℂ (i :Fin 1 ⊕ Fin 3) : (complexCoBasis i).toFin13ℂ = Pi.single i 1 := by
|
||||
simp only [complexCoBasis, Basis.coe_ofEquivFun]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma complexCoBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 1 ⊕ Fin 3) :
|
||||
(LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M) i j =
|
||||
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ i j := by
|
||||
rw [LinearMap.toMatrix_apply]
|
||||
simp only [complexCoBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply, transpose_apply]
|
||||
change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ (Pi.single j 1)) i = _
|
||||
simp only [mulVec_single, transpose_apply, mul_one]
|
||||
|
||||
/-- The standard basis of complex covariant Lorentz vectors indexed by `Fin 4`. -/
|
||||
def complexCoBasisFin4 : Basis (Fin 4) ℂ complexCo :=
|
||||
Basis.reindex complexCoBasis finSumFinEquiv
|
||||
|
||||
/-!
|
||||
|
||||
## Relation to real
|
||||
|
||||
-/
|
||||
|
||||
/-- The semilinear map including real Lorentz vectors into complex contravariant
|
||||
lorentz vectors. -/
|
||||
def inclCongrRealLorentz : ContrMod 3 →ₛₗ[Complex.ofRealHom] complexContr where
|
||||
toFun v := {val := ofReal ∘ v.toFin1dℝ}
|
||||
map_add' x y := by
|
||||
apply Lorentz.ContrℂModule.ext
|
||||
rw [Lorentz.ContrℂModule.val_add]
|
||||
funext i
|
||||
simp only [Function.comp_apply, ofRealHom_eq_coe, Pi.add_apply, map_add]
|
||||
simp only [ofRealHom_eq_coe, ofReal_add]
|
||||
map_smul' c x := by
|
||||
apply Lorentz.ContrℂModule.ext
|
||||
rw [Lorentz.ContrℂModule.val_smul]
|
||||
funext i
|
||||
simp only [Function.comp_apply, ofRealHom_eq_coe, Pi.smul_apply, _root_.map_smul]
|
||||
simp only [smul_eq_mul, ofRealHom_eq_coe, ofReal_mul]
|
||||
|
||||
lemma inclCongrRealLorentz_val (v : ContrMod 3) :
|
||||
(inclCongrRealLorentz v).val = ofRealHom ∘ v.toFin1dℝ := rfl
|
||||
|
||||
lemma complexContrBasis_of_real (i : Fin 1 ⊕ Fin 3) :
|
||||
(complexContrBasis i) = inclCongrRealLorentz (ContrMod.stdBasis i) := by
|
||||
apply Lorentz.ContrℂModule.ext
|
||||
simp only [complexContrBasis, Basis.coe_ofEquivFun, inclCongrRealLorentz,
|
||||
LinearMap.coe_mk, AddHom.coe_mk]
|
||||
ext j
|
||||
simp only [Function.comp_apply]
|
||||
change (Pi.single i 1) j = _
|
||||
by_cases h : i = j
|
||||
· subst h
|
||||
rw [ContrMod.toFin1dℝ, ContrMod.stdBasis_toFin1dℝEquiv_apply_same]
|
||||
simp
|
||||
· rw [ContrMod.toFin1dℝ, ContrMod.stdBasis_toFin1dℝEquiv_apply_ne h]
|
||||
simp [h]
|
||||
|
||||
lemma inclCongrRealLorentz_ρ (M : SL(2, ℂ)) (v : ContrMod 3) :
|
||||
(complexContr.ρ M) (inclCongrRealLorentz v) =
|
||||
inclCongrRealLorentz ((Contr 3).ρ (SL2C.toLorentzGroup M) v) := by
|
||||
apply Lorentz.ContrℂModule.ext
|
||||
rw [complexContrBasis_ρ_val, inclCongrRealLorentz_val, inclCongrRealLorentz_val]
|
||||
rw [LorentzGroup.toComplex_mulVec_ofReal]
|
||||
apply congrArg
|
||||
simp only [SL2C.toLorentzGroup_apply_coe]
|
||||
change _ = ContrMod.toFin1dℝ ((SL2C.toLorentzGroup M) *ᵥ v)
|
||||
simp only [SL2C.toLorentzGroup_apply_coe, ContrMod.mulVec_toFin1dℝ]
|
||||
|
||||
/-! TODO: Rename.-/
|
||||
lemma SL2CRep_ρ_basis (M : SL(2, ℂ)) (i : Fin 1 ⊕ Fin 3) :
|
||||
(complexContr.ρ M) (complexContrBasis i) =
|
||||
∑ j, (SL2C.toLorentzGroup M).1 j i •
|
||||
complexContrBasis j := by
|
||||
rw [complexContrBasis_of_real, inclCongrRealLorentz_ρ]
|
||||
rw [Contr.ρ_stdBasis, map_sum]
|
||||
apply congrArg
|
||||
funext j
|
||||
simp only [LinearMap.map_smulₛₗ, ofRealHom_eq_coe, coe_smul]
|
||||
rw [complexContrBasis_of_real]
|
||||
|
||||
/-! TODO: Include relation to real Lorentz vectors.-/
|
||||
end Lorentz
|
||||
end
|
||||
166
HepLean/Lorentz/ComplexVector/Contraction.lean
Normal file
166
HepLean/Lorentz/ComplexVector/Contraction.lean
Normal file
|
|
@ -0,0 +1,166 @@
|
|||
/-
|
||||
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.Lorentz.ComplexVector.Basic
|
||||
/-!
|
||||
|
||||
# Contraction of Lorentz vectors
|
||||
|
||||
-/
|
||||
|
||||
noncomputable section
|
||||
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
open TensorProduct
|
||||
open SpaceTime
|
||||
open CategoryTheory.MonoidalCategory
|
||||
namespace Lorentz
|
||||
|
||||
/-- The bi-linear map corresponding to contraction of a contravariant Lorentz vector with a
|
||||
covariant Lorentz vector. -/
|
||||
def contrCoContrBi : complexContr →ₗ[ℂ] complexCo →ₗ[ℂ] ℂ where
|
||||
toFun ψ := {
|
||||
toFun := fun φ => ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ,
|
||||
map_add' := by
|
||||
intro φ φ'
|
||||
simp only [map_add]
|
||||
rw [dotProduct_add]
|
||||
map_smul' := by
|
||||
intro r φ
|
||||
simp only [LinearEquiv.map_smul]
|
||||
rw [dotProduct_smul]
|
||||
rfl}
|
||||
map_add' ψ ψ':= by
|
||||
refine LinearMap.ext (fun φ => ?_)
|
||||
simp only [map_add, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]
|
||||
rw [add_dotProduct]
|
||||
map_smul' r ψ := by
|
||||
refine LinearMap.ext (fun φ => ?_)
|
||||
simp only [LinearEquiv.map_smul, LinearMap.coe_mk, AddHom.coe_mk]
|
||||
rw [smul_dotProduct]
|
||||
rfl
|
||||
|
||||
/-- The bi-linear map corresponding to contraction of a covariant Lorentz vector with a
|
||||
contravariant Lorentz vector. -/
|
||||
def contrContrCoBi : complexCo →ₗ[ℂ] complexContr →ₗ[ℂ] ℂ where
|
||||
toFun φ := {
|
||||
toFun := fun ψ => φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ,
|
||||
map_add' := by
|
||||
intro ψ ψ'
|
||||
simp only [map_add]
|
||||
rw [dotProduct_add]
|
||||
map_smul' := by
|
||||
intro r ψ
|
||||
simp only [LinearEquiv.map_smul]
|
||||
rw [dotProduct_smul]
|
||||
rfl}
|
||||
map_add' φ φ' := by
|
||||
refine LinearMap.ext (fun ψ => ?_)
|
||||
simp only [map_add, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]
|
||||
rw [add_dotProduct]
|
||||
map_smul' r φ := by
|
||||
refine LinearMap.ext (fun ψ => ?_)
|
||||
simp only [LinearEquiv.map_smul, LinearMap.coe_mk, AddHom.coe_mk]
|
||||
rw [smul_dotProduct]
|
||||
rfl
|
||||
|
||||
/-- The linear map from complexContr ⊗ complexCo to ℂ given by
|
||||
summing over components of contravariant Lorentz vector and
|
||||
covariant Lorentz vector in the
|
||||
standard basis (i.e. the dot product).
|
||||
In terms of index notation this is the contraction is ψⁱ φᵢ. -/
|
||||
def contrCoContraction : complexContr ⊗ complexCo ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
|
||||
hom := TensorProduct.lift contrCoContrBi
|
||||
comm M := TensorProduct.ext' fun ψ φ => by
|
||||
change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M)) *ᵥ ψ.toFin13ℂ) ⬝ᵥ
|
||||
((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ φ.toFin13ℂ) = ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ
|
||||
rw [dotProduct_mulVec, vecMul_transpose, mulVec_mulVec]
|
||||
rw [inv_mul_of_invertible (LorentzGroup.toComplex (SL2C.toLorentzGroup M))]
|
||||
simp
|
||||
|
||||
lemma contrCoContraction_hom_tmul (ψ : complexContr) (φ : complexCo) :
|
||||
contrCoContraction.hom (ψ ⊗ₜ φ) = ψ.toFin13ℂ ⬝ᵥ φ.toFin13ℂ := by
|
||||
rfl
|
||||
|
||||
lemma contrCoContraction_basis (i j : Fin 4) :
|
||||
contrCoContraction.hom (complexContrBasisFin4 i ⊗ₜ complexCoBasisFin4 j) =
|
||||
if i.1 = j.1 then (1 : ℂ) else 0 := by
|
||||
rw [contrCoContraction_hom_tmul]
|
||||
simp only [Action.instMonoidalCategory_tensorUnit_V, complexContrBasisFin4, Basis.coe_reindex,
|
||||
Function.comp_apply, complexContrBasis_toFin13ℂ, complexCoBasisFin4, complexCoBasis_toFin13ℂ,
|
||||
dotProduct_single, mul_one]
|
||||
rw [Pi.single_apply]
|
||||
refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
|
||||
simp only [EmbeddingLike.apply_eq_iff_eq, Fin.ext_iff, eq_iff_iff, eq_comm]
|
||||
|
||||
lemma contrCoContraction_basis' (i j : Fin 1 ⊕ Fin 3) :
|
||||
contrCoContraction.hom (complexContrBasis i ⊗ₜ complexCoBasis j) =
|
||||
if i = j then (1 : ℂ) else 0 := by
|
||||
rw [contrCoContraction_hom_tmul]
|
||||
simp only [Action.instMonoidalCategory_tensorUnit_V, complexContrBasisFin4, Basis.coe_reindex,
|
||||
Function.comp_apply, complexContrBasis_toFin13ℂ, complexCoBasisFin4, complexCoBasis_toFin13ℂ,
|
||||
dotProduct_single, mul_one]
|
||||
rw [Pi.single_apply]
|
||||
refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
|
||||
exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
|
||||
|
||||
/-- The linear map from complexCo ⊗ complexContr to ℂ given by
|
||||
summing over components of covariant Lorentz vector and
|
||||
contravariant Lorentz vector in the
|
||||
standard basis (i.e. the dot product).
|
||||
In terms of index notation this is the contraction is φᵢ ψⁱ. -/
|
||||
def coContrContraction : complexCo ⊗ complexContr ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
|
||||
hom := TensorProduct.lift contrContrCoBi
|
||||
comm M := TensorProduct.ext' fun φ ψ => by
|
||||
change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ φ.toFin13ℂ) ⬝ᵥ
|
||||
((LorentzGroup.toComplex (SL2C.toLorentzGroup M)) *ᵥ ψ.toFin13ℂ) = φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ
|
||||
rw [dotProduct_mulVec, mulVec_transpose, vecMul_vecMul]
|
||||
rw [inv_mul_of_invertible (LorentzGroup.toComplex (SL2C.toLorentzGroup M))]
|
||||
simp
|
||||
|
||||
lemma coContrContraction_hom_tmul (φ : complexCo) (ψ : complexContr) :
|
||||
coContrContraction.hom (φ ⊗ₜ ψ) = φ.toFin13ℂ ⬝ᵥ ψ.toFin13ℂ := by
|
||||
rfl
|
||||
|
||||
lemma coContrContraction_basis (i j : Fin 4) :
|
||||
coContrContraction.hom (complexCoBasisFin4 i ⊗ₜ complexContrBasisFin4 j) =
|
||||
if i.1 = j.1 then (1 : ℂ) else 0 := by
|
||||
rw [coContrContraction_hom_tmul]
|
||||
simp only [Action.instMonoidalCategory_tensorUnit_V, complexCoBasisFin4, Basis.coe_reindex,
|
||||
Function.comp_apply, complexCoBasis_toFin13ℂ, complexContrBasisFin4, complexContrBasis_toFin13ℂ,
|
||||
dotProduct_single, mul_one]
|
||||
rw [Pi.single_apply]
|
||||
refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
|
||||
simp only [EmbeddingLike.apply_eq_iff_eq, Fin.ext_iff, eq_iff_iff, eq_comm]
|
||||
|
||||
lemma coContrContraction_basis' (i j : Fin 1 ⊕ Fin 3) :
|
||||
coContrContraction.hom (complexCoBasis i ⊗ₜ complexContrBasis j) =
|
||||
if i = j then (1 : ℂ) else 0 := by
|
||||
rw [coContrContraction_hom_tmul]
|
||||
simp only [Action.instMonoidalCategory_tensorUnit_V, complexCoBasisFin4, Basis.coe_reindex,
|
||||
Function.comp_apply, complexCoBasis_toFin13ℂ, complexContrBasisFin4, complexContrBasis_toFin13ℂ,
|
||||
dotProduct_single, mul_one]
|
||||
rw [Pi.single_apply]
|
||||
refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
|
||||
simp only [EmbeddingLike.apply_eq_iff_eq, Fin.ext_iff, eq_iff_iff, eq_comm]
|
||||
|
||||
/-!
|
||||
|
||||
## Symmetry
|
||||
|
||||
-/
|
||||
|
||||
lemma contrCoContraction_tmul_symm (φ : complexContr) (ψ : complexCo) :
|
||||
contrCoContraction.hom (φ ⊗ₜ ψ) = coContrContraction.hom (ψ ⊗ₜ φ) := by
|
||||
rw [contrCoContraction_hom_tmul, coContrContraction_hom_tmul, dotProduct_comm]
|
||||
|
||||
lemma coContrContraction_tmul_symm (φ : complexCo) (ψ : complexContr) :
|
||||
coContrContraction.hom (φ ⊗ₜ ψ) = contrCoContraction.hom (ψ ⊗ₜ φ) := by
|
||||
rw [contrCoContraction_tmul_symm]
|
||||
|
||||
end Lorentz
|
||||
end
|
||||
192
HepLean/Lorentz/ComplexVector/Metric.lean
Normal file
192
HepLean/Lorentz/ComplexVector/Metric.lean
Normal file
|
|
@ -0,0 +1,192 @@
|
|||
/-
|
||||
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.Lorentz.ComplexVector.Two
|
||||
import HepLean.Lorentz.MinkowskiMatrix
|
||||
import HepLean.Lorentz.ComplexVector.Contraction
|
||||
import HepLean.Lorentz.ComplexVector.Unit
|
||||
/-!
|
||||
|
||||
# Metric for complex Lorentz vectors
|
||||
|
||||
-/
|
||||
noncomputable section
|
||||
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
open TensorProduct
|
||||
open SpaceTime
|
||||
open CategoryTheory.MonoidalCategory
|
||||
namespace Lorentz
|
||||
|
||||
/-- The metric `ηᵃᵃ` as an element of `(complexContr ⊗ complexContr).V`. -/
|
||||
def contrMetricVal : (complexContr ⊗ complexContr).V :=
|
||||
contrContrToMatrix.symm ((@minkowskiMatrix 3).map ofRealHom)
|
||||
|
||||
/-- The expansion of `contrMetricVal` into basis vectors. -/
|
||||
lemma contrMetricVal_expand_tmul : contrMetricVal =
|
||||
complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)
|
||||
- complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)
|
||||
- complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)
|
||||
- complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) := by
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, contrMetricVal, Fin.isValue]
|
||||
erw [contrContrToMatrix_symm_expand_tmul]
|
||||
simp only [map_apply, ofRealHom_eq_coe, coe_smul, Fintype.sum_sum_type, Finset.univ_unique,
|
||||
Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton, Fin.sum_univ_three, ne_eq, reduceCtorEq,
|
||||
not_false_eq_true, minkowskiMatrix.off_diag_zero, zero_smul, add_zero, zero_add, Sum.inr.injEq,
|
||||
zero_ne_one, Fin.reduceEq, one_ne_zero]
|
||||
rw [minkowskiMatrix.inl_0_inl_0, minkowskiMatrix.inr_i_inr_i,
|
||||
minkowskiMatrix.inr_i_inr_i, minkowskiMatrix.inr_i_inr_i]
|
||||
simp only [Fin.isValue, one_smul, neg_smul]
|
||||
rfl
|
||||
|
||||
/-- The metric `ηᵃᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexContr`,
|
||||
making its invariance under the action of `SL(2,ℂ)`. -/
|
||||
def contrMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexContr where
|
||||
hom := {
|
||||
toFun := fun a =>
|
||||
let a' : ℂ := a
|
||||
a' • contrMetricVal,
|
||||
map_add' := fun x y => by
|
||||
simp only [add_smul],
|
||||
map_smul' := fun m x => by
|
||||
simp only [smul_smul]
|
||||
rfl}
|
||||
comm M := by
|
||||
ext x : 2
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
|
||||
Function.comp_apply]
|
||||
let x' : ℂ := x
|
||||
change x' • contrMetricVal =
|
||||
(TensorProduct.map (complexContr.ρ M) (complexContr.ρ M)) (x' • contrMetricVal)
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
|
||||
apply congrArg
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, contrMetricVal]
|
||||
erw [contrContrToMatrix_ρ_symm]
|
||||
apply congrArg
|
||||
simp only [LorentzGroup.toComplex_mul_minkowskiMatrix_mul_transpose]
|
||||
|
||||
lemma contrMetric_apply_one : contrMetric.hom (1 : ℂ) = contrMetricVal := by
|
||||
change contrMetric.hom.toFun (1 : ℂ) = contrMetricVal
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
contrMetric, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
|
||||
|
||||
/-- The metric `ηᵢᵢ` as an element of `(complexCo ⊗ complexCo).V`. -/
|
||||
def coMetricVal : (complexCo ⊗ complexCo).V :=
|
||||
coCoToMatrix.symm ((@minkowskiMatrix 3).map ofRealHom)
|
||||
|
||||
/-- The expansion of `coMetricVal` into basis vectors. -/
|
||||
lemma coMetricVal_expand_tmul : coMetricVal =
|
||||
complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)
|
||||
- complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)
|
||||
- complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)
|
||||
- complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) := by
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, coMetricVal, Fin.isValue]
|
||||
erw [coCoToMatrix_symm_expand_tmul]
|
||||
simp only [map_apply, ofRealHom_eq_coe, coe_smul, Fintype.sum_sum_type, Finset.univ_unique,
|
||||
Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton, Fin.sum_univ_three, ne_eq, reduceCtorEq,
|
||||
not_false_eq_true, minkowskiMatrix.off_diag_zero, zero_smul, add_zero, zero_add, Sum.inr.injEq,
|
||||
zero_ne_one, Fin.reduceEq, one_ne_zero]
|
||||
rw [minkowskiMatrix.inl_0_inl_0, minkowskiMatrix.inr_i_inr_i,
|
||||
minkowskiMatrix.inr_i_inr_i, minkowskiMatrix.inr_i_inr_i]
|
||||
simp only [Fin.isValue, one_smul, neg_smul]
|
||||
rfl
|
||||
|
||||
/-- The metric `ηᵢᵢ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexCo`,
|
||||
making its invariance under the action of `SL(2,ℂ)`. -/
|
||||
def coMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexCo where
|
||||
hom := {
|
||||
toFun := fun a =>
|
||||
let a' : ℂ := a
|
||||
a' • coMetricVal,
|
||||
map_add' := fun x y => by
|
||||
simp only [add_smul],
|
||||
map_smul' := fun m x => by
|
||||
simp only [smul_smul]
|
||||
rfl}
|
||||
comm M := by
|
||||
ext x : 2
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
|
||||
Function.comp_apply]
|
||||
let x' : ℂ := x
|
||||
change x' • coMetricVal =
|
||||
(TensorProduct.map (complexCo.ρ M) (complexCo.ρ M)) (x' • coMetricVal)
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
|
||||
apply congrArg
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, coMetricVal]
|
||||
erw [coCoToMatrix_ρ_symm]
|
||||
apply congrArg
|
||||
rw [LorentzGroup.toComplex_inv]
|
||||
simp only [lorentzGroupIsGroup_inv, SL2C.toLorentzGroup_apply_coe,
|
||||
LorentzGroup.toComplex_transpose_mul_minkowskiMatrix_mul_self]
|
||||
|
||||
lemma coMetric_apply_one : coMetric.hom (1 : ℂ) = coMetricVal := by
|
||||
change coMetric.hom.toFun (1 : ℂ) = coMetricVal
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
coMetric, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
|
||||
|
||||
/-!
|
||||
|
||||
## Contraction of metrics
|
||||
|
||||
-/
|
||||
|
||||
lemma contrCoContraction_apply_metric : (β_ complexContr complexCo).hom.hom
|
||||
((complexContr.V ◁ (λ_ complexCo.V).hom)
|
||||
((complexContr.V ◁ contrCoContraction.hom ▷ complexCo.V)
|
||||
((complexContr.V ◁ (α_ complexContr.V complexCo.V complexCo.V).inv)
|
||||
((α_ complexContr.V complexContr.V (complexCo.V ⊗ complexCo.V)).hom
|
||||
(contrMetric.hom (1 : ℂ) ⊗ₜ[ℂ] coMetric.hom (1 : ℂ)))))) =
|
||||
coContrUnit.hom (1 : ℂ) := by
|
||||
rw [contrMetric_apply_one, coMetric_apply_one]
|
||||
rw [contrMetricVal_expand_tmul, coMetricVal_expand_tmul]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Fin.isValue, tmul_sub, add_tmul, neg_tmul, map_sub, map_add, map_neg, tmul_sub, sub_tmul]
|
||||
have h1 (x1 x2 : complexContr) (y1 y2 :complexCo) :
|
||||
(complexContr.V ◁ (λ_ complexCo.V).hom)
|
||||
((complexContr.V ◁ contrCoContraction.hom ▷ complexCo.V) (((complexContr.V ◁
|
||||
(α_ complexContr.V complexCo.V complexCo.V).inv)
|
||||
((α_ complexContr.V complexContr.V (complexCo.V ⊗ complexCo.V)).hom
|
||||
((x1 ⊗ₜ[ℂ] x2) ⊗ₜ[ℂ] y1 ⊗ₜ[ℂ] y2)))))
|
||||
= x1 ⊗ₜ[ℂ] ((λ_ complexCo.V).hom ((contrCoContraction.hom (x2 ⊗ₜ[ℂ] y1)) ⊗ₜ[ℂ] y2)) := rfl
|
||||
repeat rw (config := { transparency := .instances }) [h1]
|
||||
repeat rw [contrCoContraction_basis']
|
||||
simp only [Fin.isValue, ↓reduceIte, ModuleCat.MonoidalCategory.leftUnitor_hom_apply, one_smul,
|
||||
reduceCtorEq, zero_tmul, map_zero, tmul_zero, sub_zero, zero_sub, Sum.inr.injEq, one_ne_zero,
|
||||
Fin.reduceEq, sub_neg_eq_add, zero_ne_one, sub_self]
|
||||
erw [coContrUnit_apply_one, coContrUnitVal_expand_tmul]
|
||||
rfl
|
||||
|
||||
lemma coContrContraction_apply_metric : (β_ complexCo complexContr).hom.hom
|
||||
((complexCo.V ◁ (λ_ complexContr.V).hom)
|
||||
((complexCo.V ◁ coContrContraction.hom ▷ complexContr.V)
|
||||
((complexCo.V ◁ (α_ complexCo.V complexContr.V complexContr.V).inv)
|
||||
((α_ complexCo.V complexCo.V (complexContr.V ⊗ complexContr.V)).hom
|
||||
(coMetric.hom (1 : ℂ) ⊗ₜ[ℂ] contrMetric.hom (1 : ℂ)))))) =
|
||||
contrCoUnit.hom (1 : ℂ) := by
|
||||
rw [coMetric_apply_one, contrMetric_apply_one]
|
||||
rw [coMetricVal_expand_tmul, contrMetricVal_expand_tmul]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Fin.isValue, tmul_sub, add_tmul, neg_tmul, map_sub, map_add, map_neg, tmul_sub, sub_tmul]
|
||||
have h1 (x1 x2 : complexCo) (y1 y2 :complexContr) :
|
||||
(complexCo.V ◁ (λ_ complexContr.V).hom)
|
||||
((complexCo.V ◁ coContrContraction.hom ▷ complexContr.V) (((complexCo.V ◁
|
||||
(α_ complexCo.V complexContr.V complexContr.V).inv)
|
||||
((α_ complexCo.V complexCo.V (complexContr.V ⊗ complexContr.V)).hom
|
||||
((x1 ⊗ₜ[ℂ] x2) ⊗ₜ[ℂ] y1 ⊗ₜ[ℂ] y2)))))
|
||||
= x1 ⊗ₜ[ℂ] ((λ_ complexContr.V).hom ((coContrContraction.hom (x2 ⊗ₜ[ℂ] y1)) ⊗ₜ[ℂ] y2)) := rfl
|
||||
repeat rw (config := { transparency := .instances }) [h1]
|
||||
repeat rw [coContrContraction_basis']
|
||||
simp only [Fin.isValue, ↓reduceIte, ModuleCat.MonoidalCategory.leftUnitor_hom_apply, one_smul,
|
||||
reduceCtorEq, zero_tmul, map_zero, tmul_zero, sub_zero, zero_sub, Sum.inr.injEq, one_ne_zero,
|
||||
Fin.reduceEq, sub_neg_eq_add, zero_ne_one, sub_self]
|
||||
erw [contrCoUnit_apply_one, contrCoUnitVal_expand_tmul]
|
||||
rfl
|
||||
|
||||
end Lorentz
|
||||
end
|
||||
164
HepLean/Lorentz/ComplexVector/Modules.lean
Normal file
164
HepLean/Lorentz/ComplexVector/Modules.lean
Normal file
|
|
@ -0,0 +1,164 @@
|
|||
/-
|
||||
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 Mathlib.Logic.Equiv.TransferInstance
|
||||
/-!
|
||||
|
||||
## Modules associated with complex Lorentz vectors
|
||||
|
||||
We define the modules underlying complex Lorentz vectors.
|
||||
These definitions are preludes to the definitions of
|
||||
`Lorentz.complexContr` and `Lorentz.complexCo`.
|
||||
|
||||
-/
|
||||
|
||||
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
|
||||
|
||||
@[ext]
|
||||
lemma ext (ψ ψ' : ContrℂModule) (h : ψ.val = ψ'.val) : ψ = ψ' := by
|
||||
cases ψ
|
||||
cases ψ'
|
||||
subst h
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma val_add (ψ ψ' : ContrℂModule) : (ψ + ψ').val = ψ.val + ψ'.val := rfl
|
||||
|
||||
@[simp]
|
||||
lemma val_smul (r : ℂ) (ψ : ContrℂModule) : (r • ψ).val = r • ψ.val := rfl
|
||||
|
||||
/-- The linear equivalence between `ContrℂModule` and `(Fin 1 ⊕ Fin 3 → ℂ)`. -/
|
||||
@[simps!]
|
||||
def toFin13ℂEquiv : ContrℂModule ≃ₗ[ℂ] (Fin 1 ⊕ Fin 3 → ℂ) :=
|
||||
Equiv.linearEquiv ℂ toFin13ℂFun
|
||||
|
||||
/-- 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 (LorentzGroup.toComplex M *ᵥ 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 → ℂ) :=
|
||||
Equiv.linearEquiv ℂ toFin13ℂFun
|
||||
|
||||
/-- 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 ((LorentzGroup.toComplex M)⁻¹ᵀ *ᵥ 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 [_root_.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
|
||||
319
HepLean/Lorentz/ComplexVector/Two.lean
Normal file
319
HepLean/Lorentz/ComplexVector/Two.lean
Normal file
|
|
@ -0,0 +1,319 @@
|
|||
/-
|
||||
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.Lorentz.ComplexVector.Basic
|
||||
import Mathlib.LinearAlgebra.TensorProduct.Matrix
|
||||
/-!
|
||||
|
||||
# Tensor products of two complex Lorentz vectors
|
||||
|
||||
-/
|
||||
noncomputable section
|
||||
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
open TensorProduct
|
||||
open SpaceTime
|
||||
open CategoryTheory.MonoidalCategory
|
||||
namespace Lorentz
|
||||
|
||||
/-- Equivalence of `complexContr ⊗ complexContr` to `4 x 4` complex matrices. -/
|
||||
def contrContrToMatrix : (complexContr ⊗ complexContr).V ≃ₗ[ℂ]
|
||||
Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ :=
|
||||
(Basis.tensorProduct complexContrBasis complexContrBasis).repr ≪≫ₗ
|
||||
Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ
|
||||
LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)
|
||||
|
||||
/-- Expanding `contrContrToMatrix` in terms of the standard basis. -/
|
||||
lemma contrContrToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) :
|
||||
contrContrToMatrix.symm M =
|
||||
∑ i, ∑ j, M i j • (complexContrBasis i ⊗ₜ[ℂ] complexContrBasis j) := by
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, contrContrToMatrix, LinearEquiv.trans_symm,
|
||||
LinearEquiv.trans_apply, Basis.repr_symm_apply]
|
||||
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
|
||||
· erw [Finset.sum_product]
|
||||
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
|
||||
erw [Basis.tensorProduct_apply complexContrBasis complexContrBasis i j]
|
||||
rfl
|
||||
· simp
|
||||
|
||||
/-- Equivalence of `complexCo ⊗ complexCo` to `4 x 4` complex matrices. -/
|
||||
def coCoToMatrix : (complexCo ⊗ complexCo).V ≃ₗ[ℂ]
|
||||
Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ :=
|
||||
(Basis.tensorProduct complexCoBasis complexCoBasis).repr ≪≫ₗ
|
||||
Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ
|
||||
LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)
|
||||
|
||||
/-- Expanding `coCoToMatrix` in terms of the standard basis. -/
|
||||
lemma coCoToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) :
|
||||
coCoToMatrix.symm M = ∑ i, ∑ j, M i j • (complexCoBasis i ⊗ₜ[ℂ] complexCoBasis j) := by
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, coCoToMatrix, LinearEquiv.trans_symm,
|
||||
LinearEquiv.trans_apply, Basis.repr_symm_apply]
|
||||
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
|
||||
· erw [Finset.sum_product]
|
||||
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
|
||||
erw [Basis.tensorProduct_apply complexCoBasis complexCoBasis i j]
|
||||
rfl
|
||||
· simp
|
||||
|
||||
/-- Equivalence of `complexContr ⊗ complexCo` to `4 x 4` complex matrices. -/
|
||||
def contrCoToMatrix : (complexContr ⊗ complexCo).V ≃ₗ[ℂ]
|
||||
Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ :=
|
||||
(Basis.tensorProduct complexContrBasis complexCoBasis).repr ≪≫ₗ
|
||||
Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ
|
||||
LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)
|
||||
|
||||
/-- Expansion of `contrCoToMatrix` in terms of the standard basis. -/
|
||||
lemma contrCoToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) :
|
||||
contrCoToMatrix.symm M = ∑ i, ∑ j, M i j • (complexContrBasis i ⊗ₜ[ℂ] complexCoBasis j) := by
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, contrCoToMatrix, LinearEquiv.trans_symm,
|
||||
LinearEquiv.trans_apply, Basis.repr_symm_apply]
|
||||
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
|
||||
· erw [Finset.sum_product]
|
||||
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
|
||||
erw [Basis.tensorProduct_apply complexContrBasis complexCoBasis i j]
|
||||
rfl
|
||||
· simp
|
||||
|
||||
/-- Equivalence of `complexCo ⊗ complexContr` to `4 x 4` complex matrices. -/
|
||||
def coContrToMatrix : (complexCo ⊗ complexContr).V ≃ₗ[ℂ]
|
||||
Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ :=
|
||||
(Basis.tensorProduct complexCoBasis complexContrBasis).repr ≪≫ₗ
|
||||
Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ
|
||||
LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)
|
||||
|
||||
/-- Expansion of `coContrToMatrix` in terms of the standard basis. -/
|
||||
lemma coContrToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) :
|
||||
coContrToMatrix.symm M = ∑ i, ∑ j, M i j • (complexCoBasis i ⊗ₜ[ℂ] complexContrBasis j) := by
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, coContrToMatrix, LinearEquiv.trans_symm,
|
||||
LinearEquiv.trans_apply, Basis.repr_symm_apply]
|
||||
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
|
||||
· erw [Finset.sum_product]
|
||||
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
|
||||
erw [Basis.tensorProduct_apply complexCoBasis complexContrBasis i j]
|
||||
rfl
|
||||
· simp
|
||||
|
||||
/-!
|
||||
|
||||
## Group actions
|
||||
|
||||
-/
|
||||
|
||||
lemma contrContrToMatrix_ρ (v : (complexContr ⊗ complexContr).V) (M : SL(2,ℂ)) :
|
||||
contrContrToMatrix (TensorProduct.map (complexContr.ρ M) (complexContr.ρ M) v) =
|
||||
(LorentzGroup.toComplex (SL2C.toLorentzGroup M)) * contrContrToMatrix v *
|
||||
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ := by
|
||||
nth_rewrite 1 [contrContrToMatrix]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
|
||||
trans (LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)) ((LinearMap.toMatrix
|
||||
(complexContrBasis.tensorProduct complexContrBasis)
|
||||
(complexContrBasis.tensorProduct complexContrBasis)
|
||||
(TensorProduct.map (complexContr.ρ M) (complexContr.ρ M)))
|
||||
*ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)))
|
||||
((complexContrBasis.tensorProduct complexContrBasis).repr v)))
|
||||
· apply congrArg
|
||||
have h1 := (LinearMap.toMatrix_mulVec_repr (complexContrBasis.tensorProduct complexContrBasis)
|
||||
(complexContrBasis.tensorProduct complexContrBasis)
|
||||
(TensorProduct.map (complexContr.ρ M) (complexContr.ρ M)) v)
|
||||
erw [h1]
|
||||
rfl
|
||||
rw [TensorProduct.toMatrix_map]
|
||||
funext i j
|
||||
change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
|
||||
((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M))
|
||||
((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M)) (i, j) k)
|
||||
* contrContrToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
|
||||
have h1 : ∑ x, (∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 *
|
||||
contrContrToMatrix v x1 x) * LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
|
||||
= ∑ x, ∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1
|
||||
* contrContrToMatrix v x1 x) * LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x := by
|
||||
congr
|
||||
funext x
|
||||
rw [Finset.sum_mul]
|
||||
erw [h1]
|
||||
rw [Finset.sum_comm]
|
||||
congr
|
||||
funext x
|
||||
congr
|
||||
funext x1
|
||||
simp only [complexContrBasis_ρ_apply, transpose_apply, Action.instMonoidalCategory_tensorObj_V]
|
||||
ring
|
||||
|
||||
lemma coCoToMatrix_ρ (v : (complexCo ⊗ complexCo).V) (M : SL(2,ℂ)) :
|
||||
coCoToMatrix (TensorProduct.map (complexCo.ρ M) (complexCo.ρ M) v) =
|
||||
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ * coCoToMatrix v *
|
||||
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ := by
|
||||
nth_rewrite 1 [coCoToMatrix]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
|
||||
trans (LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)) ((LinearMap.toMatrix
|
||||
(complexCoBasis.tensorProduct complexCoBasis)
|
||||
(complexCoBasis.tensorProduct complexCoBasis)
|
||||
(TensorProduct.map (complexCo.ρ M) (complexCo.ρ M))
|
||||
*ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)))
|
||||
((complexCoBasis.tensorProduct complexCoBasis).repr v))))
|
||||
· apply congrArg
|
||||
have h1 := (LinearMap.toMatrix_mulVec_repr (complexCoBasis.tensorProduct complexCoBasis)
|
||||
(complexCoBasis.tensorProduct complexCoBasis)
|
||||
(TensorProduct.map (complexCo.ρ M) (complexCo.ρ M)) v)
|
||||
erw [h1]
|
||||
rfl
|
||||
rw [TensorProduct.toMatrix_map]
|
||||
funext i j
|
||||
change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
|
||||
((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M))
|
||||
((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M)) (i, j) k)
|
||||
* coCoToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
|
||||
have h1 : ∑ x, (∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i *
|
||||
coCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
|
||||
= ∑ x, ∑ x1, ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i
|
||||
* coCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j := by
|
||||
congr
|
||||
funext x
|
||||
rw [Finset.sum_mul]
|
||||
erw [h1]
|
||||
rw [Finset.sum_comm]
|
||||
congr
|
||||
funext x
|
||||
congr
|
||||
funext x1
|
||||
simp only [complexCoBasis_ρ_apply, transpose_apply, Action.instMonoidalCategory_tensorObj_V]
|
||||
ring
|
||||
|
||||
lemma contrCoToMatrix_ρ (v : (complexContr ⊗ complexCo).V) (M : SL(2,ℂ)) :
|
||||
contrCoToMatrix (TensorProduct.map (complexContr.ρ M) (complexCo.ρ M) v) =
|
||||
(LorentzGroup.toComplex (SL2C.toLorentzGroup M)) * contrCoToMatrix v *
|
||||
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ := by
|
||||
nth_rewrite 1 [contrCoToMatrix]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
|
||||
trans (LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)) ((LinearMap.toMatrix
|
||||
(complexContrBasis.tensorProduct complexCoBasis)
|
||||
(complexContrBasis.tensorProduct complexCoBasis)
|
||||
(TensorProduct.map (complexContr.ρ M) (complexCo.ρ M))
|
||||
*ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)))
|
||||
((complexContrBasis.tensorProduct complexCoBasis).repr v))))
|
||||
· apply congrArg
|
||||
have h1 := (LinearMap.toMatrix_mulVec_repr (complexContrBasis.tensorProduct complexCoBasis)
|
||||
(complexContrBasis.tensorProduct complexCoBasis)
|
||||
(TensorProduct.map (complexContr.ρ M) (complexCo.ρ M)) v)
|
||||
erw [h1]
|
||||
rfl
|
||||
rw [TensorProduct.toMatrix_map]
|
||||
funext i j
|
||||
change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
|
||||
((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M))
|
||||
((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M)) (i, j) k)
|
||||
* contrCoToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply]
|
||||
have h1 : ∑ x, (∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 *
|
||||
contrCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
|
||||
= ∑ x, ∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1
|
||||
* contrCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j := by
|
||||
congr
|
||||
funext x
|
||||
rw [Finset.sum_mul]
|
||||
erw [h1]
|
||||
rw [Finset.sum_comm]
|
||||
congr
|
||||
funext x
|
||||
congr
|
||||
funext x1
|
||||
simp only [complexContrBasis_ρ_apply, complexCoBasis_ρ_apply, transpose_apply,
|
||||
Action.instMonoidalCategory_tensorObj_V]
|
||||
ring
|
||||
|
||||
lemma coContrToMatrix_ρ (v : (complexCo ⊗ complexContr).V) (M : SL(2,ℂ)) :
|
||||
coContrToMatrix (TensorProduct.map (complexCo.ρ M) (complexContr.ρ M) v) =
|
||||
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ * coContrToMatrix v *
|
||||
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ := by
|
||||
nth_rewrite 1 [coContrToMatrix]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
|
||||
trans (LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)) ((LinearMap.toMatrix
|
||||
(complexCoBasis.tensorProduct complexContrBasis)
|
||||
(complexCoBasis.tensorProduct complexContrBasis)
|
||||
(TensorProduct.map (complexCo.ρ M) (complexContr.ρ M))
|
||||
*ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)))
|
||||
((complexCoBasis.tensorProduct complexContrBasis).repr v))))
|
||||
· apply congrArg
|
||||
have h1 := (LinearMap.toMatrix_mulVec_repr (complexCoBasis.tensorProduct complexContrBasis)
|
||||
(complexCoBasis.tensorProduct complexContrBasis)
|
||||
(TensorProduct.map (complexCo.ρ M) (complexContr.ρ M)) v)
|
||||
erw [h1]
|
||||
rfl
|
||||
rw [TensorProduct.toMatrix_map]
|
||||
funext i j
|
||||
change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
|
||||
((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M))
|
||||
((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M)) (i, j) k)
|
||||
* coContrToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
|
||||
have h1 : ∑ x, (∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i *
|
||||
coContrToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M)) j x
|
||||
= ∑ x, ∑ x1, ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i
|
||||
* coContrToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M)) j x := by
|
||||
congr
|
||||
funext x
|
||||
rw [Finset.sum_mul]
|
||||
erw [h1]
|
||||
rw [Finset.sum_comm]
|
||||
congr
|
||||
funext x
|
||||
congr
|
||||
funext x1
|
||||
simp only [complexCoBasis_ρ_apply, complexContrBasis_ρ_apply, transpose_apply,
|
||||
Action.instMonoidalCategory_tensorObj_V]
|
||||
ring
|
||||
|
||||
/-!
|
||||
|
||||
## The symm version of the group actions.
|
||||
|
||||
-/
|
||||
|
||||
lemma contrContrToMatrix_ρ_symm (v : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) (M : SL(2,ℂ)) :
|
||||
TensorProduct.map (complexContr.ρ M) (complexContr.ρ M) (contrContrToMatrix.symm v) =
|
||||
contrContrToMatrix.symm ((LorentzGroup.toComplex (SL2C.toLorentzGroup M)) * v *
|
||||
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ) := by
|
||||
have h1 := contrContrToMatrix_ρ (contrContrToMatrix.symm v) M
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
|
||||
rw [← h1]
|
||||
simp
|
||||
|
||||
lemma coCoToMatrix_ρ_symm (v : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) (M : SL(2,ℂ)) :
|
||||
TensorProduct.map (complexCo.ρ M) (complexCo.ρ M) (coCoToMatrix.symm v) =
|
||||
coCoToMatrix.symm ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ * v *
|
||||
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹) := by
|
||||
have h1 := coCoToMatrix_ρ (coCoToMatrix.symm v) M
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
|
||||
rw [← h1]
|
||||
simp
|
||||
|
||||
lemma contrCoToMatrix_ρ_symm (v : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) (M : SL(2,ℂ)) :
|
||||
TensorProduct.map (complexContr.ρ M) (complexCo.ρ M) (contrCoToMatrix.symm v) =
|
||||
contrCoToMatrix.symm ((LorentzGroup.toComplex (SL2C.toLorentzGroup M)) * v *
|
||||
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹) := by
|
||||
have h1 := contrCoToMatrix_ρ (contrCoToMatrix.symm v) M
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
|
||||
rw [← h1]
|
||||
simp
|
||||
|
||||
lemma coContrToMatrix_ρ_symm (v : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) (M : SL(2,ℂ)) :
|
||||
TensorProduct.map (complexCo.ρ M) (complexContr.ρ M) (coContrToMatrix.symm v) =
|
||||
coContrToMatrix.symm ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ * v *
|
||||
(LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ) := by
|
||||
have h1 := coContrToMatrix_ρ (coContrToMatrix.symm v) M
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
|
||||
rw [← h1]
|
||||
simp
|
||||
|
||||
end Lorentz
|
||||
end
|
||||
223
HepLean/Lorentz/ComplexVector/Unit.lean
Normal file
223
HepLean/Lorentz/ComplexVector/Unit.lean
Normal file
|
|
@ -0,0 +1,223 @@
|
|||
/-
|
||||
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.Lorentz.ComplexVector.Two
|
||||
import HepLean.Lorentz.ComplexVector.Contraction
|
||||
/-!
|
||||
|
||||
# Unit for complex Lorentz vectors
|
||||
|
||||
-/
|
||||
noncomputable section
|
||||
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
open TensorProduct
|
||||
open SpaceTime
|
||||
open CategoryTheory.MonoidalCategory
|
||||
namespace Lorentz
|
||||
|
||||
/-- The contra-co unit for complex lorentz vectors. Usually denoted `δⁱᵢ`. -/
|
||||
def contrCoUnitVal : (complexContr ⊗ complexCo).V :=
|
||||
contrCoToMatrix.symm 1
|
||||
|
||||
/-- Expansion of `contrCoUnitVal` into basis. -/
|
||||
lemma contrCoUnitVal_expand_tmul : contrCoUnitVal =
|
||||
complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)
|
||||
+ complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)
|
||||
+ complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)
|
||||
+ complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) := by
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, contrCoUnitVal, Fin.isValue]
|
||||
erw [contrCoToMatrix_symm_expand_tmul]
|
||||
simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
|
||||
Finset.sum_singleton, Fin.sum_univ_three, ne_eq, reduceCtorEq, not_false_eq_true, one_apply_ne,
|
||||
zero_smul, add_zero, one_apply_eq, one_smul, zero_add, Sum.inr.injEq, zero_ne_one, Fin.reduceEq,
|
||||
one_ne_zero]
|
||||
rfl
|
||||
|
||||
/-- The contra-co unit for complex lorentz vectors as a morphism
|
||||
`𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo`, manifesting the invaraince under
|
||||
the `SL(2, ℂ)` action. -/
|
||||
def contrCoUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo where
|
||||
hom := {
|
||||
toFun := fun a =>
|
||||
let a' : ℂ := a
|
||||
a' • contrCoUnitVal,
|
||||
map_add' := fun x y => by
|
||||
simp only [add_smul],
|
||||
map_smul' := fun m x => by
|
||||
simp only [smul_smul]
|
||||
rfl}
|
||||
comm M := by
|
||||
ext x : 2
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
|
||||
Function.comp_apply]
|
||||
let x' : ℂ := x
|
||||
change x' • contrCoUnitVal =
|
||||
(TensorProduct.map (complexContr.ρ M) (complexCo.ρ M)) (x' • contrCoUnitVal)
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
|
||||
apply congrArg
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, contrCoUnitVal]
|
||||
erw [contrCoToMatrix_ρ_symm]
|
||||
apply congrArg
|
||||
simp
|
||||
|
||||
lemma contrCoUnit_apply_one : contrCoUnit.hom (1 : ℂ) = contrCoUnitVal := by
|
||||
change contrCoUnit.hom.toFun (1 : ℂ) = contrCoUnitVal
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
contrCoUnit, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
|
||||
|
||||
/-- The co-contra unit for complex lorentz vectors. Usually denoted `δᵢⁱ`. -/
|
||||
def coContrUnitVal : (complexCo ⊗ complexContr).V :=
|
||||
coContrToMatrix.symm 1
|
||||
|
||||
/-- Expansion of `coContrUnitVal` into basis. -/
|
||||
lemma coContrUnitVal_expand_tmul : coContrUnitVal =
|
||||
complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)
|
||||
+ complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)
|
||||
+ complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)
|
||||
+ complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) := by
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, coContrUnitVal, Fin.isValue]
|
||||
erw [coContrToMatrix_symm_expand_tmul]
|
||||
simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
|
||||
Finset.sum_singleton, Fin.sum_univ_three, ne_eq, reduceCtorEq, not_false_eq_true, one_apply_ne,
|
||||
zero_smul, add_zero, one_apply_eq, one_smul, zero_add, Sum.inr.injEq, zero_ne_one, Fin.reduceEq,
|
||||
one_ne_zero]
|
||||
rfl
|
||||
|
||||
/-- The co-contra unit for complex lorentz vectors as a morphism
|
||||
`𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr`, manifesting the invaraince under
|
||||
the `SL(2, ℂ)` action. -/
|
||||
def coContrUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexContr where
|
||||
hom := {
|
||||
toFun := fun a =>
|
||||
let a' : ℂ := a
|
||||
a' • coContrUnitVal,
|
||||
map_add' := fun x y => by
|
||||
simp only [add_smul],
|
||||
map_smul' := fun m x => by
|
||||
simp only [smul_smul]
|
||||
rfl}
|
||||
comm M := by
|
||||
ext x : 2
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
|
||||
Function.comp_apply]
|
||||
let x' : ℂ := x
|
||||
change x' • coContrUnitVal =
|
||||
(TensorProduct.map (complexCo.ρ M) (complexContr.ρ M)) (x' • coContrUnitVal)
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
|
||||
apply congrArg
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, coContrUnitVal]
|
||||
erw [coContrToMatrix_ρ_symm]
|
||||
apply congrArg
|
||||
symm
|
||||
refine transpose_eq_one.mp ?h.h.h.a
|
||||
simp
|
||||
|
||||
lemma coContrUnit_apply_one : coContrUnit.hom (1 : ℂ) = coContrUnitVal := by
|
||||
change coContrUnit.hom.toFun (1 : ℂ) = coContrUnitVal
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
coContrUnit, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
|
||||
/-!
|
||||
|
||||
## Contraction of the units
|
||||
|
||||
-/
|
||||
|
||||
/-- Contraction on the right with `contrCoUnit` does nothing. -/
|
||||
lemma contr_contrCoUnit (x : complexCo) :
|
||||
(λ_ complexCo).hom.hom
|
||||
((coContrContraction ▷ complexCo).hom
|
||||
((α_ _ _ complexCo).inv.hom
|
||||
(x ⊗ₜ[ℂ] contrCoUnit.hom (1 : ℂ)))) = x := by
|
||||
obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span complexCoBasis x)
|
||||
subst hc
|
||||
rw [contrCoUnit_apply_one, contrCoUnitVal_expand_tmul]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.instMonoidalCategory_leftUnitor_hom_hom, Action.instMonoidalCategory_whiskerRight_hom,
|
||||
Action.instMonoidalCategory_associator_inv_hom, CategoryTheory.Equivalence.symm_inverse,
|
||||
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
|
||||
Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
|
||||
Finset.sum_singleton, Fin.sum_univ_three, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add,
|
||||
_root_.map_smul]
|
||||
have h1' (x y : CoeSort.coe complexCo) (z : CoeSort.coe complexContr) :
|
||||
(α_ complexCo.V complexContr.V complexCo.V).inv (x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y) = (x ⊗ₜ[ℂ] z) ⊗ₜ[ℂ] y := rfl
|
||||
repeat rw [h1']
|
||||
have h1'' (y : CoeSort.coe complexCo)
|
||||
(z : CoeSort.coe complexCo ⊗[ℂ] CoeSort.coe complexContr) :
|
||||
(coContrContraction.hom ▷ complexCo.V) (z ⊗ₜ[ℂ] y) = (coContrContraction.hom z) ⊗ₜ[ℂ] y := rfl
|
||||
repeat rw (config := { transparency := .instances }) [h1'']
|
||||
repeat rw [coContrContraction_basis']
|
||||
simp only [Fin.isValue, leftUnitor, ModuleCat.MonoidalCategory.leftUnitor, ModuleCat.of_coe,
|
||||
CategoryTheory.Iso.trans_hom, LinearEquiv.toModuleIso_hom, ModuleCat.ofSelfIso_hom,
|
||||
CategoryTheory.Category.comp_id, Action.instMonoidalCategory_tensorUnit_V, ↓reduceIte,
|
||||
reduceCtorEq, zero_tmul, map_zero, smul_zero, add_zero, Sum.inr.injEq, one_ne_zero,
|
||||
Fin.reduceEq, zero_add, zero_ne_one]
|
||||
erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul, TensorProduct.lid_tmul,
|
||||
TensorProduct.lid_tmul]
|
||||
simp only [Fin.isValue, one_smul]
|
||||
repeat rw [add_assoc]
|
||||
|
||||
/-- Contraction on the right with `coContrUnit`. -/
|
||||
lemma contr_coContrUnit (x : complexContr) :
|
||||
(λ_ complexContr).hom.hom
|
||||
((contrCoContraction ▷ complexContr).hom
|
||||
((α_ _ _ complexContr).inv.hom
|
||||
(x ⊗ₜ[ℂ] coContrUnit.hom (1 : ℂ)))) = x := by
|
||||
obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span complexContrBasis x)
|
||||
subst hc
|
||||
rw [coContrUnit_apply_one, coContrUnitVal_expand_tmul]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.instMonoidalCategory_leftUnitor_hom_hom, Action.instMonoidalCategory_whiskerRight_hom,
|
||||
Action.instMonoidalCategory_associator_inv_hom, CategoryTheory.Equivalence.symm_inverse,
|
||||
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
|
||||
Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
|
||||
Finset.sum_singleton, Fin.sum_univ_three, tmul_add, add_tmul, smul_tmul, tmul_smul, map_add,
|
||||
_root_.map_smul]
|
||||
have h1' (x y : CoeSort.coe complexContr) (z : CoeSort.coe complexCo) :
|
||||
(α_ complexContr.V complexCo.V complexContr.V).inv
|
||||
(x ⊗ₜ[ℂ] z ⊗ₜ[ℂ] y) = (x ⊗ₜ[ℂ] z) ⊗ₜ[ℂ] y := rfl
|
||||
repeat rw [h1']
|
||||
have h1'' (y : CoeSort.coe complexContr)
|
||||
(z : CoeSort.coe complexContr ⊗[ℂ] CoeSort.coe complexCo) :
|
||||
(contrCoContraction.hom ▷ complexContr.V) (z ⊗ₜ[ℂ] y) =
|
||||
(contrCoContraction.hom z) ⊗ₜ[ℂ] y := rfl
|
||||
repeat rw (config := { transparency := .instances }) [h1'']
|
||||
repeat rw [contrCoContraction_basis']
|
||||
simp only [Fin.isValue, Action.instMonoidalCategory_tensorUnit_V, ↓reduceIte, reduceCtorEq,
|
||||
zero_tmul, map_zero, smul_zero, add_zero, Sum.inr.injEq, one_ne_zero, Fin.reduceEq, zero_add,
|
||||
zero_ne_one]
|
||||
erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul, TensorProduct.lid_tmul,
|
||||
TensorProduct.lid_tmul]
|
||||
simp only [Fin.isValue, one_smul]
|
||||
repeat rw [add_assoc]
|
||||
|
||||
/-!
|
||||
|
||||
## Symmetry properties of the units
|
||||
|
||||
-/
|
||||
|
||||
open CategoryTheory
|
||||
|
||||
lemma contrCoUnit_symm :
|
||||
(contrCoUnit.hom (1 : ℂ)) = (complexContr ◁ 𝟙 _).hom ((β_ complexCo complexContr).hom.hom
|
||||
(coContrUnit.hom (1 : ℂ))) := by
|
||||
rw [contrCoUnit_apply_one, contrCoUnitVal_expand_tmul]
|
||||
rw [coContrUnit_apply_one, coContrUnitVal_expand_tmul]
|
||||
rfl
|
||||
|
||||
lemma coContrUnit_symm :
|
||||
(coContrUnit.hom (1 : ℂ)) = (complexCo ◁ 𝟙 _).hom ((β_ complexContr complexCo).hom.hom
|
||||
(contrCoUnit.hom (1 : ℂ))) := by
|
||||
rw [coContrUnit_apply_one, coContrUnitVal_expand_tmul]
|
||||
rw [contrCoUnit_apply_one, contrCoUnitVal_expand_tmul]
|
||||
rfl
|
||||
|
||||
end Lorentz
|
||||
end
|
||||
|
|
@ -3,7 +3,7 @@ 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.MinkowskiMatrix
|
||||
import HepLean.Lorentz.MinkowskiMatrix
|
||||
/-!
|
||||
# The Lorentz Group
|
||||
|
||||
|
|
|
|||
152
HepLean/Lorentz/MinkowskiMatrix.lean
Normal file
152
HepLean/Lorentz/MinkowskiMatrix.lean
Normal file
|
|
@ -0,0 +1,152 @@
|
|||
/-
|
||||
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 Mathlib.Algebra.Lie.Classical
|
||||
/-!
|
||||
|
||||
# The Minkowski matrix
|
||||
|
||||
|
||||
-/
|
||||
|
||||
open Matrix
|
||||
open InnerProductSpace
|
||||
/-!
|
||||
|
||||
# The definition of the Minkowski Matrix
|
||||
|
||||
-/
|
||||
/-- The `d.succ`-dimensional real matrix of the form `diag(1, -1, -1, -1, ...)`. -/
|
||||
def minkowskiMatrix {d : ℕ} : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ :=
|
||||
LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin d) ℝ
|
||||
|
||||
namespace minkowskiMatrix
|
||||
|
||||
variable {d : ℕ}
|
||||
|
||||
/-- Notation for `minkowskiMatrix`. -/
|
||||
scoped[minkowskiMatrix] notation "η" => minkowskiMatrix
|
||||
|
||||
@[simp]
|
||||
lemma sq : @minkowskiMatrix d * minkowskiMatrix = 1 := by
|
||||
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_mul_diagonal]
|
||||
ext1 i j
|
||||
rcases i with i | i <;> rcases j with j | j
|
||||
· simp only [diagonal, of_apply, Sum.inl.injEq, Sum.elim_inl, mul_one]
|
||||
split
|
||||
· rename_i h
|
||||
subst h
|
||||
simp_all only [one_apply_eq]
|
||||
· simp_all only [ne_eq, Sum.inl.injEq, not_false_eq_true, one_apply_ne]
|
||||
· rfl
|
||||
· rfl
|
||||
· simp only [diagonal, of_apply, Sum.inr.injEq, Sum.elim_inr, mul_neg, mul_one, neg_neg]
|
||||
split
|
||||
· rename_i h
|
||||
subst h
|
||||
simp_all only [one_apply_eq]
|
||||
· simp_all only [ne_eq, Sum.inr.injEq, not_false_eq_true, one_apply_ne]
|
||||
|
||||
@[simp]
|
||||
lemma eq_transpose : minkowskiMatrixᵀ = @minkowskiMatrix d := by
|
||||
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_transpose]
|
||||
|
||||
@[simp]
|
||||
lemma det_eq_neg_one_pow_d : (@minkowskiMatrix d).det = (- 1) ^ d := by
|
||||
simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
|
||||
|
||||
@[simp]
|
||||
lemma η_apply_mul_η_apply_diag (μ : Fin 1 ⊕ Fin d) : η μ μ * η μ μ = 1 := by
|
||||
match μ with
|
||||
| Sum.inl _ => simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
|
||||
| Sum.inr _ => simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
|
||||
|
||||
lemma as_block : @minkowskiMatrix d =
|
||||
Matrix.fromBlocks (1 : Matrix (Fin 1) (Fin 1) ℝ) 0 0 (-1 : Matrix (Fin d) (Fin d) ℝ) := by
|
||||
rw [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, ← fromBlocks_diagonal]
|
||||
refine fromBlocks_inj.mpr ?_
|
||||
simp only [diagonal_one, true_and]
|
||||
funext i j
|
||||
rw [← diagonal_neg]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma off_diag_zero {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) : η μ ν = 0 := by
|
||||
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
|
||||
exact diagonal_apply_ne _ h
|
||||
|
||||
lemma inl_0_inl_0 : @minkowskiMatrix d (Sum.inl 0) (Sum.inl 0) = 1 := by
|
||||
rfl
|
||||
|
||||
lemma inr_i_inr_i (i : Fin d) : @minkowskiMatrix d (Sum.inr i) (Sum.inr i) = -1 := by
|
||||
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
|
||||
simp_all only [diagonal_apply_eq, Sum.elim_inr]
|
||||
|
||||
@[simp]
|
||||
lemma mulVec_inl_0 (v : (Fin 1 ⊕ Fin d) → ℝ) :
|
||||
(η *ᵥ v) (Sum.inl 0)= v (Sum.inl 0) := by
|
||||
simp only [mulVec, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mulVec_diagonal]
|
||||
simp only [Fin.isValue, diagonal_dotProduct, Sum.elim_inl, one_mul]
|
||||
|
||||
@[simp]
|
||||
lemma mulVec_inr_i (v : (Fin 1 ⊕ Fin d) → ℝ) (i : Fin d) :
|
||||
(η *ᵥ v) (Sum.inr i)= - v (Sum.inr i) := by
|
||||
simp only [mulVec, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mulVec_diagonal]
|
||||
simp only [diagonal_dotProduct, Sum.elim_inr, neg_mul, one_mul]
|
||||
|
||||
|
||||
variable (Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
|
||||
|
||||
/-- The dual of a matrix with respect to the Minkowski metric. -/
|
||||
def dual : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ := η * Λᵀ * η
|
||||
|
||||
@[simp]
|
||||
lemma dual_id : @dual d 1 = 1 := by
|
||||
simpa only [dual, transpose_one, mul_one] using minkowskiMatrix.sq
|
||||
|
||||
@[simp]
|
||||
lemma dual_mul : dual (Λ * Λ') = dual Λ' * dual Λ := by
|
||||
simp only [dual, transpose_mul]
|
||||
trans η * Λ'ᵀ * (η * η) * Λᵀ * η
|
||||
· noncomm_ring [minkowskiMatrix.sq]
|
||||
· noncomm_ring
|
||||
|
||||
@[simp]
|
||||
lemma dual_dual : dual (dual Λ) = Λ := by
|
||||
simp only [dual, transpose_mul, transpose_transpose, eq_transpose]
|
||||
trans (η * η) * Λ * (η * η)
|
||||
· noncomm_ring
|
||||
· noncomm_ring [minkowskiMatrix.sq]
|
||||
|
||||
@[simp]
|
||||
lemma dual_eta : @dual d η = η := by
|
||||
simp only [dual, eq_transpose]
|
||||
noncomm_ring [minkowskiMatrix.sq]
|
||||
|
||||
@[simp]
|
||||
lemma dual_transpose : dual Λᵀ = (dual Λ)ᵀ := by
|
||||
simp only [dual, transpose_transpose, transpose_mul, eq_transpose]
|
||||
noncomm_ring
|
||||
|
||||
@[simp]
|
||||
lemma det_dual : (dual Λ).det = Λ.det := by
|
||||
simp only [dual, det_mul, minkowskiMatrix.det_eq_neg_one_pow_d, det_transpose]
|
||||
group
|
||||
norm_cast
|
||||
simp
|
||||
|
||||
lemma dual_apply (μ ν : Fin 1 ⊕ Fin d) :
|
||||
dual Λ μ ν = η μ μ * Λ ν μ * η ν ν := by
|
||||
simp only [dual, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mul_diagonal,
|
||||
diagonal_mul, transpose_apply, diagonal_apply_eq]
|
||||
|
||||
lemma dual_apply_minkowskiMatrix (μ ν : Fin 1 ⊕ Fin d) :
|
||||
dual Λ μ ν * η ν ν = η μ μ * Λ ν μ := by
|
||||
rw [dual_apply, mul_assoc]
|
||||
simp
|
||||
|
||||
end minkowskiMatrix
|
||||
Loading…
Add table
Add a link
Reference in a new issue