refactor: Major refactor of Lorentz vecs
This commit is contained in:
jstoobysmith
parent
3eb5da875f
commit
5cc188146f
20 changed files with 494 additions and 1005 deletions
|
|
@ -79,21 +79,16 @@ import HepLean.SpaceTime.LorentzGroup.Orthochronous
|
|||
import HepLean.SpaceTime.LorentzGroup.Proper
|
||||
import HepLean.SpaceTime.LorentzGroup.Restricted
|
||||
import HepLean.SpaceTime.LorentzGroup.Rotations
|
||||
import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
|
||||
import HepLean.SpaceTime.LorentzVector.Basic
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Basic
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Contraction
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Metric
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Modules
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Two
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Unit
|
||||
import HepLean.SpaceTime.LorentzVector.LorentzAction
|
||||
import HepLean.SpaceTime.LorentzVector.NormOne
|
||||
import HepLean.SpaceTime.LorentzVector.Real.Basic
|
||||
import HepLean.SpaceTime.LorentzVector.Real.Contraction
|
||||
import HepLean.SpaceTime.LorentzVector.Real.Modules
|
||||
import HepLean.SpaceTime.MinkowskiMatrix
|
||||
import HepLean.SpaceTime.MinkowskiMetric
|
||||
import HepLean.SpaceTime.PauliMatrices.AsTensor
|
||||
import HepLean.SpaceTime.PauliMatrices.Basic
|
||||
import HepLean.SpaceTime.PauliMatrices.SelfAdjoint
|
||||
|
|
|
|||
|
|
@ -3,8 +3,9 @@ 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.MinkowskiMetric
|
||||
import HepLean.SpaceTime.MinkowskiMatrix
|
||||
import Mathlib.Algebra.Lie.Classical
|
||||
import HepLean.SpaceTime.LorentzVector.Real.Basic
|
||||
/-!
|
||||
# The Lorentz Algebra
|
||||
|
||||
|
|
@ -84,22 +85,4 @@ lemma space_comps (Λ : lorentzAlgebra) (i j : Fin 3) :
|
|||
|
||||
end lorentzAlgebra
|
||||
|
||||
@[simps!]
|
||||
instance lorentzVectorAsLieRingModule : LieRingModule lorentzAlgebra (LorentzVector 3) where
|
||||
bracket Λ x := Λ.1.mulVec x
|
||||
add_lie Λ1 Λ2 x := by
|
||||
simp [add_mulVec]
|
||||
lie_add Λ x1 x2 := by
|
||||
simp only
|
||||
exact mulVec_add _ _ _
|
||||
leibniz_lie Λ1 Λ2 x := by
|
||||
simp [mulVec_add, Bracket.bracket, sub_mulVec]
|
||||
|
||||
@[simps!]
|
||||
instance spaceTimeAsLieModule : LieModule ℝ lorentzAlgebra (LorentzVector 3) where
|
||||
smul_lie r Λ x := smul_mulVec_assoc r Λ.1 x
|
||||
lie_smul r Λ x := by
|
||||
simp only [Bracket.bracket]
|
||||
rw [mulVec_smul]
|
||||
|
||||
end SpaceTime
|
||||
|
|
|
|||
|
|
@ -35,21 +35,19 @@ variable {d : ℕ}
|
|||
|
||||
/-- An auxillary linear map used in the definition of a generalised boost. -/
|
||||
def genBoostAux₁ (u v : FuturePointing d) : ContrMod d →ₗ[ℝ] ContrMod d where
|
||||
toFun x := (2 * toField d ⟪x, u.val.val⟫ₘ) • v.1.1
|
||||
toFun x := (2 * ⟪x, u.val.val⟫ₘ) • v.1.1
|
||||
map_add' x y := by
|
||||
simp [map_add, LinearMap.add_apply, tmul_add, add_tmul, mul_add, add_smul]
|
||||
map_smul' c x := by
|
||||
simp only [toField, Action.instMonoidalCategory_tensorObj_V,
|
||||
simp only [ Action.instMonoidalCategory_tensorObj_V,
|
||||
Action.instMonoidalCategory_tensorUnit_V, CategoryTheory.Equivalence.symm_inverse,
|
||||
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
|
||||
smul_tmul, tmul_smul, map_smul, smul_eq_mul, RingHom.id_apply]
|
||||
erw [LinearMap.id_apply]
|
||||
rw [← mul_assoc, mul_comm 2 c, mul_assoc, mul_smul]
|
||||
rfl
|
||||
|
||||
/-- An auxillary linear map used in the definition of a genearlised boost. -/
|
||||
def genBoostAux₂ (u v : FuturePointing d) : ContrMod d →ₗ[ℝ] ContrMod d where
|
||||
toFun x := - (toField d ⟪x, u.1.1 + v.1.1⟫ₘ / (1 + toField d ⟪u.1.1, v.1.1⟫ₘ)) • (u.1.1 + v.1.1)
|
||||
toFun x := - (⟪x, u.1.1 + v.1.1⟫ₘ / (1 + ⟪u.1.1, v.1.1⟫ₘ)) • (u.1.1 + v.1.1)
|
||||
map_add' x y := by
|
||||
simp only
|
||||
rw [← add_smul]
|
||||
|
|
@ -62,7 +60,7 @@ def genBoostAux₂ (u v : FuturePointing d) : ContrMod d →ₗ[ℝ] ContrMod d
|
|||
rw [map_smul]
|
||||
conv =>
|
||||
lhs; lhs; rhs; lhs
|
||||
change (c * toField d (contrContrContract.hom (x ⊗ₜ[ℝ] (u.val.val + v.val.val))))
|
||||
change (c * (contrContrContractField (x ⊗ₜ[ℝ] (u.val.val + v.val.val))))
|
||||
rw [mul_div_assoc, neg_mul_eq_mul_neg, smul_smul]
|
||||
rfl
|
||||
|
||||
|
|
@ -75,21 +73,47 @@ lemma genBoostAux₂_self (u : FuturePointing d) : genBoostAux₂ u u = - genBoo
|
|||
rw [smul_smul]
|
||||
congr 1
|
||||
rw [u.1.2]
|
||||
simp [toField]
|
||||
conv => lhs; lhs; rhs; rhs; change 1
|
||||
rw [show 1 + (1 : ℝ) = (2 : ℝ ) by ring]
|
||||
simp only [isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
|
||||
IsUnit.div_mul_cancel]
|
||||
rw [← (two_smul ℝ u.val.val)]
|
||||
simp only [tmul_smul, map_smul, smul_eq_mul]
|
||||
rfl
|
||||
|
||||
|
||||
/-- An generalised boost. This is a Lorentz transformation which takes the four velocity `u`
|
||||
to `v`. -/
|
||||
def genBoost (u v : FuturePointing d) : ContrMod d →ₗ[ℝ] ContrMod d :=
|
||||
LinearMap.id + genBoostAux₁ u v + genBoostAux₂ u v
|
||||
|
||||
lemma genBoost_mul_one_plus_contr (u v : FuturePointing d) (x : Contr d) :
|
||||
(1 + ⟪u.1.1, v.1.1⟫ₘ) • genBoost u v x =
|
||||
(1 + ⟪u.1.1, v.1.1⟫ₘ) • x +
|
||||
(2 * ⟪x, u.val.val⟫ₘ * (1 + ⟪u.1.1, v.1.1⟫ₘ)) • v.1.1
|
||||
- (⟪x, u.1.1 + v.1.1⟫ₘ) • (u.1.1 + v.1.1) := by
|
||||
simp only [genBoost, LinearMap.add_apply, LinearMap.id_apply, id_eq]
|
||||
rw [smul_add, smul_add]
|
||||
trans (1 + ⟪u.1.1, v.1.1⟫ₘ) • x +
|
||||
(2 * ⟪x, u.val.val⟫ₘ * (1 + ⟪u.1.1, v.1.1⟫ₘ)) • v.1.1
|
||||
+ (- ⟪x, u.1.1 + v.1.1⟫ₘ) • (u.1.1 + v.1.1)
|
||||
· congr 1
|
||||
· congr 1
|
||||
rw [genBoostAux₁]
|
||||
simp
|
||||
rw [smul_smul]
|
||||
congr 1
|
||||
ring
|
||||
· rw [genBoostAux₂]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
CategoryTheory.Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, neg_smul, LinearMap.coe_mk,
|
||||
AddHom.coe_mk, smul_neg]
|
||||
rw [smul_smul]
|
||||
congr
|
||||
have h1 := FuturePointing.one_add_metric_non_zero u v
|
||||
field_simp
|
||||
· rw [neg_smul]
|
||||
rfl
|
||||
|
||||
namespace genBoost
|
||||
|
||||
/--
|
||||
|
|
@ -110,7 +134,7 @@ lemma toMatrix_mulVec (u v : FuturePointing d) (x : Contr d) :
|
|||
(toMatrix u v) *ᵥ x = genBoost u v x :=
|
||||
ContrMod.ext (LinearMap.toMatrix_mulVec_repr ContrMod.stdBasis ContrMod.stdBasis (genBoost u v) x)
|
||||
|
||||
open minkowskiMatrix LorentzVector in
|
||||
open minkowskiMatrix in
|
||||
@[simp]
|
||||
lemma toMatrix_apply (u v : FuturePointing d) (μ ν : Fin 1 ⊕ Fin d) :
|
||||
(toMatrix u v) μ ν = η μ μ * (toField d ⟪ContrMod.stdBasis μ, ContrMod.stdBasis ν⟫ₘ + 2 *
|
||||
|
|
@ -118,31 +142,39 @@ lemma toMatrix_apply (u v : FuturePointing d) (μ ν : Fin 1 ⊕ Fin d) :
|
|||
- toField d ⟪ContrMod.stdBasis μ, u.val.val + v.val.val⟫ₘ *
|
||||
toField d ⟪ContrMod.stdBasis ν, u.val.val + v.val.val⟫ₘ /
|
||||
(1 + toField d ⟪u.val.val, v.val.val⟫ₘ)) := by
|
||||
sorry
|
||||
rw [matrix_apply_stdBasis (toMatrix u v) μ ν, toMatrix_mulVec]
|
||||
rw [contrContrContractField.matrix_apply_stdBasis (Λ := toMatrix u v) μ ν, toMatrix_mulVec]
|
||||
simp only [genBoost, genBoostAux₁, genBoostAux₂, map_add, smul_add, neg_smul, LinearMap.add_apply,
|
||||
LinearMap.id_apply, LinearMap.coe_mk, AddHom.coe_mk, basis_left, map_smul, smul_eq_mul, map_neg,
|
||||
mul_eq_mul_left_iff]
|
||||
LinearMap.id_apply, LinearMap.coe_mk, AddHom.coe_mk, contrContrContractField.basis_left, map_smul, smul_eq_mul, map_neg,
|
||||
mul_eq_mul_left_iff, toField_apply]
|
||||
ring_nf
|
||||
exact (true_or (η μ μ = 0)).mpr trivial
|
||||
simp only [Pi.add_apply, Action.instMonoidalCategory_tensorObj_V,
|
||||
Action.instMonoidalCategory_tensorUnit_V, CategoryTheory.Equivalence.symm_inverse,
|
||||
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
|
||||
Pi.smul_apply, smul_eq_mul, Pi.sub_apply, Pi.neg_apply]
|
||||
apply Or.inl
|
||||
ring
|
||||
|
||||
open minkowskiMatrix LorentzVector in
|
||||
open minkowskiMatrix in
|
||||
lemma toMatrix_continuous (u : FuturePointing d) : Continuous (toMatrix u) := by
|
||||
refine continuous_matrix ?_
|
||||
intro i j
|
||||
simp only [toMatrix_apply]
|
||||
refine (continuous_mul_left (η i i)).comp' ?_
|
||||
refine Continuous.sub ?_ ?_
|
||||
· refine .comp' (continuous_add_left (minkowskiMetric (e i) (e j))) ?_
|
||||
refine .comp' (continuous_mul_left (2 * ⟪e j, u⟫ₘ)) ?_
|
||||
· refine .comp' (continuous_add_left _) ?_
|
||||
refine .comp' (continuous_mul_left _) ?_
|
||||
exact FuturePointing.metric_continuous _
|
||||
refine .mul ?_ ?_
|
||||
· refine .mul ?_ ?_
|
||||
· simp only [(minkowskiMetric _).map_add]
|
||||
· simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
CategoryTheory.Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, tmul_add, map_add]
|
||||
refine .comp' ?_ ?_
|
||||
· exact continuous_add_left ((minkowskiMetric (stdBasis i)) ↑u)
|
||||
· exact continuous_add_left _
|
||||
· exact FuturePointing.metric_continuous _
|
||||
· simp only [(minkowskiMetric _).map_add]
|
||||
· simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
CategoryTheory.Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, tmul_add, map_add]
|
||||
refine .comp' ?_ ?_
|
||||
· exact continuous_add_left _
|
||||
· exact FuturePointing.metric_continuous _
|
||||
|
|
@ -150,17 +182,28 @@ lemma toMatrix_continuous (u : FuturePointing d) : Continuous (toMatrix u) := by
|
|||
· refine .comp' (continuous_add_left 1) (FuturePointing.metric_continuous _)
|
||||
exact fun x => FuturePointing.one_add_metric_non_zero u x
|
||||
|
||||
lemma toMatrix_in_lorentzGroup (u v : FuturePointing d) : (toMatrix u v) ∈ LorentzGroup d:= by
|
||||
lemma toMatrix_in_lorentzGroup (u v : FuturePointing d) : (toMatrix u v) ∈ LorentzGroup d := by
|
||||
rw [LorentzGroup.mem_iff_invariant]
|
||||
intro x y
|
||||
rw [toMatrix_mulVec, toMatrix_mulVec, genBoost, genBoostAux₁, genBoostAux₂]
|
||||
have h1 : (1 + (minkowskiMetric ↑u) ↑v.1.1) ≠ 0 := FuturePointing.one_add_metric_non_zero u v
|
||||
simp only [map_add, smul_add, neg_smul, LinearMap.add_apply, LinearMap.id_coe,
|
||||
id_eq, LinearMap.coe_mk, AddHom.coe_mk, LinearMapClass.map_smul, map_neg, LinearMap.smul_apply,
|
||||
smul_eq_mul, LinearMap.neg_apply]
|
||||
field_simp
|
||||
rw [u.1.2, v.1.2, minkowskiMetric.symm v.1.1 u, minkowskiMetric.symm u y,
|
||||
minkowskiMetric.symm v y]
|
||||
ring
|
||||
rw [toMatrix_mulVec, toMatrix_mulVec]
|
||||
have h1 : (((1 + ⟪u.1.1, v.1.1⟫ₘ)) * (1 + ⟪u.1.1, v.1.1⟫ₘ)) •
|
||||
(contrContrContractField ((genBoost u v) y ⊗ₜ[ℝ] (genBoost u v) x))
|
||||
= (((1 + ⟪u.1.1, v.1.1⟫ₘ)) * (1 + ⟪u.1.1, v.1.1⟫ₘ)) • ⟪y, x⟫ₘ := by
|
||||
conv_lhs =>
|
||||
erw [← map_smul]
|
||||
rw [← smul_smul]
|
||||
rw [← tmul_smul, ← smul_tmul, ← tmul_smul, genBoost_mul_one_plus_contr,
|
||||
genBoost_mul_one_plus_contr]
|
||||
simp only [add_smul, one_smul, tmul_add, map_add, smul_add, tmul_sub, sub_tmul, add_tmul,
|
||||
smul_tmul, tmul_smul, map_sub, map_smul, smul_eq_mul, contr_self, mul_one]
|
||||
rw [contrContrContractField.symm v.1.1 u, contrContrContractField.symm v.1.1 x,
|
||||
contrContrContractField.symm u.1.1 x]
|
||||
simp
|
||||
ring
|
||||
have hn (a : ℝ ) {b c : ℝ} (h : a ≠ 0) (hab : a * b = a * c ) : b = c := by
|
||||
simp_all only [smul_eq_mul, ne_eq, mul_eq_mul_left_iff, or_false]
|
||||
refine hn _ ?_ h1
|
||||
simpa using (FuturePointing.one_add_metric_non_zero u v)
|
||||
|
||||
/-- A generalised boost as an element of the Lorentz Group. -/
|
||||
def toLorentz (u v : FuturePointing d) : LorentzGroup d :=
|
||||
|
|
|
|||
|
|
@ -24,7 +24,6 @@ namespace LorentzGroup
|
|||
|
||||
variable {d : ℕ}
|
||||
variable (Λ : LorentzGroup d)
|
||||
open LorentzVector
|
||||
open Lorentz.Contr
|
||||
|
||||
/-- A Lorentz transformation is `orthochronous` if its `0 0` element is non-negative. -/
|
||||
|
|
|
|||
|
|
@ -25,8 +25,6 @@ open ComplexConjugate
|
|||
|
||||
namespace LorentzGroup
|
||||
|
||||
open minkowskiMetric
|
||||
|
||||
informal_definition Restricted where
|
||||
math :≈ "The subgroup of the Lorentz group consisting of elements which
|
||||
are proper and orthochronous."
|
||||
|
|
|
|||
|
|
@ -1,107 +0,0 @@
|
|||
/-
|
||||
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.MinkowskiMetric
|
||||
import HepLean.SpaceTime.PauliMatrices.SelfAdjoint
|
||||
import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
|
||||
import Mathlib.Tactic.Polyrith
|
||||
/-!
|
||||
# Lorentz vector as a self-adjoint matrix
|
||||
|
||||
There is a linear equivalence between the vector space of space-time points
|
||||
and the vector space of 2×2-complex self-adjoint matrices.
|
||||
|
||||
In this file we define this linear equivalence in `toSelfAdjointMatrix`.
|
||||
|
||||
-/
|
||||
/-! TODO: Generalize rep of Lorentz vector as a self-adjoint matrix to arbitrary dimension. -/
|
||||
namespace SpaceTime
|
||||
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
noncomputable section
|
||||
|
||||
/-- The linear equivalence between the vector-space `spaceTime` and self-adjoint
|
||||
`2×2`-complex matrices. -/
|
||||
def toSelfAdjointMatrix : LorentzVector 3 ≃ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) :=
|
||||
(Finsupp.linearEquivFunOnFinite ℝ ℝ (Fin 1 ⊕ Fin 3)).symm ≪≫ₗ PauliMatrix.σSAL.repr.symm
|
||||
|
||||
lemma toSelfAdjointMatrix_apply (x : LorentzVector 3) : toSelfAdjointMatrix x =
|
||||
x (Sum.inl 0) • ⟨PauliMatrix.σ0, PauliMatrix.σ0_selfAdjoint⟩
|
||||
- x (Sum.inr 0) • ⟨PauliMatrix.σ1, PauliMatrix.σ1_selfAdjoint⟩
|
||||
- x (Sum.inr 1) • ⟨PauliMatrix.σ2, PauliMatrix.σ2_selfAdjoint⟩
|
||||
- x (Sum.inr 2) • ⟨PauliMatrix.σ3, PauliMatrix.σ3_selfAdjoint⟩ := by
|
||||
simp only [toSelfAdjointMatrix, PauliMatrix.σSAL, LinearEquiv.trans_apply, Basis.repr_symm_apply,
|
||||
Basis.coe_mk, Fin.isValue]
|
||||
rw [Finsupp.linearCombination_apply_of_mem_supported ℝ (s := Finset.univ)]
|
||||
· change (∑ i : Fin 1 ⊕ Fin 3, x i • PauliMatrix.σSAL' i) = _
|
||||
simp only [PauliMatrix.σSAL', Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
|
||||
Fin.isValue, Finset.sum_singleton, Fin.sum_univ_three]
|
||||
apply Subtype.ext
|
||||
simp only [Fin.isValue, AddSubgroup.coe_add, selfAdjoint.val_smul, smul_neg,
|
||||
AddSubgroupClass.coe_sub]
|
||||
simp only [neg_add, add_assoc, sub_eq_add_neg]
|
||||
· simp_all only [Finset.coe_univ, Finsupp.supported_univ, Submodule.mem_top]
|
||||
|
||||
lemma toSelfAdjointMatrix_apply_coe (x : LorentzVector 3) : (toSelfAdjointMatrix x).1 =
|
||||
x (Sum.inl 0) • PauliMatrix.σ0
|
||||
- x (Sum.inr 0) • PauliMatrix.σ1
|
||||
- x (Sum.inr 1) • PauliMatrix.σ2
|
||||
- x (Sum.inr 2) • PauliMatrix.σ3 := by
|
||||
rw [toSelfAdjointMatrix_apply]
|
||||
rfl
|
||||
|
||||
lemma toSelfAdjointMatrix_stdBasis (i : Fin 1 ⊕ Fin 3) :
|
||||
toSelfAdjointMatrix (LorentzVector.stdBasis i) = PauliMatrix.σSAL i := by
|
||||
rw [toSelfAdjointMatrix_apply]
|
||||
match i with
|
||||
| Sum.inl 0 =>
|
||||
simp only [LorentzVector.stdBasis, Fin.isValue]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp [PauliMatrix.σSAL, PauliMatrix.σSAL']
|
||||
| Sum.inr 0 =>
|
||||
simp only [LorentzVector.stdBasis, Fin.isValue]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp only [Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul,
|
||||
Pi.single_eq_same, one_smul, zero_sub, Sum.inr.injEq, one_ne_zero, sub_zero, Fin.reduceEq,
|
||||
PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL']
|
||||
rfl
|
||||
| Sum.inr 1 =>
|
||||
simp only [LorentzVector.stdBasis, Fin.isValue]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp only [Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul,
|
||||
Sum.inr.injEq, zero_ne_one, sub_self, Pi.single_eq_same, one_smul, zero_sub, Fin.reduceEq,
|
||||
sub_zero, PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL']
|
||||
rfl
|
||||
| Sum.inr 2 =>
|
||||
simp only [LorentzVector.stdBasis, Fin.isValue]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp only [Fin.isValue, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul,
|
||||
Sum.inr.injEq, Fin.reduceEq, sub_self, Pi.single_eq_same, one_smul, zero_sub,
|
||||
PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL']
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma toSelfAdjointMatrix_symm_basis (i : Fin 1 ⊕ Fin 3) :
|
||||
toSelfAdjointMatrix.symm (PauliMatrix.σSAL i) = (LorentzVector.stdBasis i) := by
|
||||
refine (LinearEquiv.symm_apply_eq toSelfAdjointMatrix).mpr ?_
|
||||
rw [toSelfAdjointMatrix_stdBasis]
|
||||
|
||||
open minkowskiMetric in
|
||||
lemma det_eq_ηLin (x : LorentzVector 3) : det (toSelfAdjointMatrix x).1 = ⟪x, x⟫ₘ := by
|
||||
rw [toSelfAdjointMatrix_apply_coe]
|
||||
simp only [Fin.isValue, eq_time_minus_inner_prod, LorentzVector.time, LorentzVector.space,
|
||||
PiLp.inner_apply, Function.comp_apply, RCLike.inner_apply, conj_trivial, Fin.sum_univ_three,
|
||||
ofReal_sub, ofReal_mul, ofReal_add]
|
||||
simp only [Fin.isValue, PauliMatrix.σ0, smul_of, smul_cons, real_smul, mul_one, smul_zero,
|
||||
smul_empty, PauliMatrix.σ1, of_sub_of, sub_cons, head_cons, sub_zero, tail_cons, zero_sub,
|
||||
sub_self, zero_empty, PauliMatrix.σ2, smul_neg, sub_neg_eq_add, PauliMatrix.σ3, det_fin_two_of]
|
||||
ring_nf
|
||||
simp only [Fin.isValue, I_sq, mul_neg, mul_one]
|
||||
ring
|
||||
|
||||
end
|
||||
end SpaceTime
|
||||
|
|
@ -1,137 +0,0 @@
|
|||
/-
|
||||
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
|
||||
/-!
|
||||
|
||||
# Lorentz vectors
|
||||
|
||||
(aka 4-vectors)
|
||||
|
||||
In this file we define a Lorentz vector (in 4d, this is more often called a 4-vector).
|
||||
|
||||
One of the most important example of a Lorentz vector is SpaceTime.
|
||||
|
||||
We will define the group action of the Lorentz group on Lorentz vectors in
|
||||
`HepLean.SpaceTime.LorentzVector.LorentzAction` in such a way that `LorentzVector`
|
||||
corresponds to contravariant Lorentz tensors.
|
||||
|
||||
-/
|
||||
|
||||
/- The number of space dimensions . -/
|
||||
variable (d : ℕ)
|
||||
|
||||
/-- The type of Lorentz Vectors in `d`-space dimensions.
|
||||
This is very weak definition of a Lorentz vector. -/
|
||||
def LorentzVector : Type := (Fin 1 ⊕ Fin d) → ℝ
|
||||
|
||||
/-- An instance of an additive commutative monoid on `LorentzVector`. -/
|
||||
instance : AddCommMonoid (LorentzVector d) := Pi.addCommMonoid
|
||||
|
||||
/-- An instance of a module on `LorentzVector`. -/
|
||||
noncomputable instance : Module ℝ (LorentzVector d) := Pi.module _ _ _
|
||||
|
||||
instance : AddCommGroup (LorentzVector d) := Pi.addCommGroup
|
||||
|
||||
/-- The structure of a topological space `LorentzVector d`. -/
|
||||
instance : TopologicalSpace (LorentzVector d) :=
|
||||
haveI : NormedAddCommGroup (LorentzVector d) := Pi.normedAddCommGroup
|
||||
UniformSpace.toTopologicalSpace
|
||||
|
||||
namespace LorentzVector
|
||||
|
||||
variable {d : ℕ} (v : LorentzVector d)
|
||||
|
||||
/-- The space components. -/
|
||||
@[simp]
|
||||
def space : EuclideanSpace ℝ (Fin d) := v ∘ Sum.inr
|
||||
|
||||
/-- The time component. -/
|
||||
@[simp]
|
||||
def time : ℝ := v (Sum.inl 0)
|
||||
|
||||
/-!
|
||||
|
||||
# The standard basis
|
||||
|
||||
-/
|
||||
|
||||
/-- The standard basis of `LorentzVector` indexed by `Fin 1 ⊕ Fin d`. -/
|
||||
@[simps!]
|
||||
noncomputable def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (LorentzVector d) := Pi.basisFun ℝ _
|
||||
|
||||
/-- Notation for `stdBasis`. -/
|
||||
scoped[LorentzVector] notation "e" => stdBasis
|
||||
|
||||
lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : e μ ν = if μ = ν then 1 else 0 := by
|
||||
erw [stdBasis, Pi.basisFun_apply, Pi.single_apply]
|
||||
refine Eq.symm (ite_congr ?h₁ (congrFun rfl) (congrFun rfl))
|
||||
exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
|
||||
|
||||
lemma decomp_stdBasis (v : LorentzVector d) : ∑ i, v i • e i = v := by
|
||||
funext ν
|
||||
rw [Finset.sum_apply]
|
||||
rw [Finset.sum_eq_single_of_mem ν]
|
||||
· simp only [HSMul.hSMul, SMul.smul, stdBasis]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp only [Pi.single_eq_same, mul_one]
|
||||
· exact Finset.mem_univ ν
|
||||
· intros b _ hbi
|
||||
simp only [HSMul.hSMul, SMul.smul, stdBasis, mul_eq_zero]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp only [Pi.single]
|
||||
apply Or.inr $ Function.update_noteq (id (Ne.symm hbi)) 1 0
|
||||
|
||||
@[simp]
|
||||
lemma decomp_stdBasis' (v : LorentzVector d) :
|
||||
v (Sum.inl 0) • e (Sum.inl 0) + ∑ a₂ : Fin d, v (Sum.inr a₂) • e (Sum.inr a₂) = v := by
|
||||
trans ∑ i, v i • e i
|
||||
· simp only [Fin.isValue, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
|
||||
Finset.sum_singleton]
|
||||
· exact decomp_stdBasis v
|
||||
|
||||
/-- The standard unit time vector. -/
|
||||
noncomputable abbrev timeVec : (LorentzVector d) := e (Sum.inl 0)
|
||||
|
||||
lemma timeVec_space : (@timeVec d).space = 0 := by
|
||||
funext i
|
||||
simp only [space, Function.comp_apply, stdBasis_apply, Fin.isValue, reduceCtorEq, ↓reduceIte,
|
||||
PiLp.zero_apply]
|
||||
|
||||
lemma timeVec_time: (@timeVec d).time = 1 := by
|
||||
simp only [time, Fin.isValue, stdBasis_apply, ↓reduceIte]
|
||||
|
||||
/-!
|
||||
|
||||
# Reflection of space
|
||||
|
||||
-/
|
||||
|
||||
/-- The reflection of space as a linear map. -/
|
||||
@[simps!]
|
||||
def spaceReflectionLin : LorentzVector d →ₗ[ℝ] LorentzVector d where
|
||||
toFun x := Sum.elim (x ∘ Sum.inl) (- x ∘ Sum.inr)
|
||||
map_add' x y := by
|
||||
funext i
|
||||
rcases i with i | i
|
||||
· rfl
|
||||
· simp only [Sum.elim_inr, Pi.neg_apply]
|
||||
apply neg_add
|
||||
map_smul' c x := by
|
||||
funext i
|
||||
rcases i with i | i
|
||||
· rfl
|
||||
· simp [HSMul.hSMul, SMul.smul]
|
||||
|
||||
/-- The reflection of space. -/
|
||||
@[simp]
|
||||
def spaceReflection : LorentzVector d := spaceReflectionLin v
|
||||
|
||||
lemma spaceReflection_space : v.spaceReflection.space = - v.space := rfl
|
||||
|
||||
lemma spaceReflection_time : v.spaceReflection.time = v.time := rfl
|
||||
|
||||
end LorentzVector
|
||||
|
|
@ -94,57 +94,62 @@ def complexCoBasisFin4 : Basis (Fin 4) ℂ complexCo :=
|
|||
|
||||
/-- The semilinear map including real Lorentz vectors into complex contravariant
|
||||
lorentz vectors. -/
|
||||
def inclCongrRealLorentz : LorentzVector 3 →ₛₗ[Complex.ofRealHom] complexContr where
|
||||
toFun v := {val := ofReal ∘ v}
|
||||
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]
|
||||
change ofReal (x i + y 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]
|
||||
change ofReal (c • x 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 : LorentzVector 3) :
|
||||
(inclCongrRealLorentz v).val = ofRealHom ∘ v := rfl
|
||||
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 (LorentzVector.stdBasis i) := by
|
||||
(complexContrBasis i) = inclCongrRealLorentz (ContrMod.stdBasis i) := by
|
||||
apply Lorentz.ContrℂModule.ext
|
||||
simp only [complexContrBasis, Basis.coe_ofEquivFun, inclCongrRealLorentz, LorentzVector.stdBasis,
|
||||
simp only [complexContrBasis, Basis.coe_ofEquivFun, inclCongrRealLorentz,
|
||||
LinearMap.coe_mk, AddHom.coe_mk]
|
||||
ext j
|
||||
simp only [Function.comp_apply, ofRealHom_eq_coe]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp
|
||||
change (Pi.single i 1) j = _
|
||||
exact Eq.symm (Pi.apply_single (fun _ => ofRealHom) (congrFun rfl) 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 : LorentzVector 3) :
|
||||
lemma inclCongrRealLorentz_ρ (M : SL(2, ℂ)) (v : ContrMod 3) :
|
||||
(complexContr.ρ M) (inclCongrRealLorentz v) =
|
||||
inclCongrRealLorentz (SL2C.repLorentzVector M v) := by
|
||||
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]
|
||||
rw [SL2C.repLorentzVector_apply_eq_mulVec]
|
||||
rfl
|
||||
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_ρ, SL2C.repLorentzVector_stdBasis, map_sum]
|
||||
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
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Two
|
||||
import HepLean.SpaceTime.MinkowskiMetric
|
||||
import HepLean.SpaceTime.MinkowskiMatrix
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Contraction
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Unit
|
||||
/-!
|
||||
|
|
|
|||
|
|
@ -1,41 +0,0 @@
|
|||
/-
|
||||
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.LorentzVector.Basic
|
||||
import HepLean.SpaceTime.LorentzGroup.Basic
|
||||
import Mathlib.RepresentationTheory.Basic
|
||||
/-!
|
||||
|
||||
# Lorentz group action on Lorentz vectors.
|
||||
|
||||
-/
|
||||
noncomputable section
|
||||
|
||||
namespace LorentzVector
|
||||
|
||||
variable {d : ℕ} (v : LorentzVector d)
|
||||
|
||||
/-- The contravariant action of the Lorentz group on a Lorentz vector. -/
|
||||
def rep : Representation ℝ (LorentzGroup d) (LorentzVector d) where
|
||||
toFun g := Matrix.toLinAlgEquiv e g
|
||||
map_one' := (MulEquivClass.map_eq_one_iff (Matrix.toLinAlgEquiv e)).mpr rfl
|
||||
map_mul' x y := by
|
||||
simp only [lorentzGroupIsGroup_mul_coe, map_mul]
|
||||
|
||||
open Matrix in
|
||||
lemma rep_apply (g : LorentzGroup d) : rep g v = g *ᵥ v := rfl
|
||||
|
||||
lemma rep_apply_stdBasis (g : LorentzGroup d) (μ : Fin 1 ⊕ Fin d) :
|
||||
rep g (stdBasis μ) = ∑ ν, g.1.transpose μ ν • stdBasis ν := by
|
||||
simp only [rep_apply, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
|
||||
Finset.sum_singleton, decomp_stdBasis']
|
||||
funext ν
|
||||
simp only [stdBasis, Matrix.transpose_apply]
|
||||
erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
|
||||
rfl
|
||||
|
||||
end LorentzVector
|
||||
|
||||
end
|
||||
|
|
@ -1,287 +0,0 @@
|
|||
/-
|
||||
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.LorentzVector.Basic
|
||||
import HepLean.SpaceTime.MinkowskiMetric
|
||||
/-!
|
||||
|
||||
# Lorentz vectors with norm one
|
||||
|
||||
-/
|
||||
|
||||
open minkowskiMetric
|
||||
|
||||
/-- The set of Lorentz vectors with norm 1. -/
|
||||
@[simp]
|
||||
def NormOneLorentzVector (d : ℕ) : Set (LorentzVector d) :=
|
||||
fun x => ⟪x, x⟫ₘ = 1
|
||||
|
||||
instance : TopologicalSpace (NormOneLorentzVector d) := instTopologicalSpaceSubtype
|
||||
|
||||
namespace NormOneLorentzVector
|
||||
|
||||
variable {d : ℕ}
|
||||
|
||||
section
|
||||
variable (v w : NormOneLorentzVector d)
|
||||
|
||||
lemma mem_iff {x : LorentzVector d} : x ∈ NormOneLorentzVector d ↔ ⟪x, x⟫ₘ = 1 := by
|
||||
rfl
|
||||
|
||||
/-- The negative of a `NormOneLorentzVector` as a `NormOneLorentzVector`. -/
|
||||
def neg : NormOneLorentzVector d := ⟨- v, by
|
||||
rw [mem_iff]
|
||||
simp only [map_neg, LinearMap.neg_apply, neg_neg]
|
||||
exact v.2⟩
|
||||
|
||||
lemma time_sq : v.1.time ^ 2 = 1 + ‖v.1.space‖ ^ 2 := by
|
||||
rw [time_sq_eq_metric_add_space, v.2]
|
||||
|
||||
lemma abs_time_ge_one : 1 ≤ |v.1.time| := by
|
||||
have h1 := leq_time_sq v.1
|
||||
rw [v.2] at h1
|
||||
exact (one_le_sq_iff_one_le_abs _).mp h1
|
||||
|
||||
lemma norm_space_le_abs_time : ‖v.1.space‖ < |v.1.time| := by
|
||||
rw [(abs_norm _).symm, ← @sq_lt_sq, time_sq]
|
||||
exact lt_one_add (‖(v.1).space‖ ^ 2)
|
||||
|
||||
lemma norm_space_leq_abs_time : ‖v.1.space‖ ≤ |v.1.time| :=
|
||||
le_of_lt (norm_space_le_abs_time v)
|
||||
|
||||
lemma time_le_minus_one_or_ge_one : v.1.time ≤ -1 ∨ 1 ≤ v.1.time :=
|
||||
le_abs'.mp (abs_time_ge_one v)
|
||||
|
||||
lemma time_nonpos_iff : v.1.time ≤ 0 ↔ v.1.time ≤ - 1 := by
|
||||
apply Iff.intro
|
||||
· intro h
|
||||
cases' time_le_minus_one_or_ge_one v with h1 h1
|
||||
· exact h1
|
||||
· linarith
|
||||
· intro h
|
||||
linarith
|
||||
|
||||
lemma time_nonneg_iff : 0 ≤ v.1.time ↔ 1 ≤ v.1.time := by
|
||||
apply Iff.intro
|
||||
· intro h
|
||||
cases' time_le_minus_one_or_ge_one v with h1 h1
|
||||
· linarith
|
||||
· exact h1
|
||||
· intro h
|
||||
linarith
|
||||
|
||||
lemma time_pos_iff : 0 < v.1.time ↔ 1 ≤ v.1.time := by
|
||||
refine Iff.intro (fun h => ?_) (fun h => ?_)
|
||||
· exact (time_nonneg_iff v).mp (le_of_lt h)
|
||||
· linarith
|
||||
|
||||
lemma time_abs_sub_space_norm :
|
||||
0 ≤ |v.1.time| * |w.1.time| - ‖v.1.space‖ * ‖w.1.space‖ := by
|
||||
apply sub_nonneg.mpr
|
||||
apply mul_le_mul (norm_space_leq_abs_time v) (norm_space_leq_abs_time w) ?_ ?_
|
||||
· exact norm_nonneg w.1.space
|
||||
· exact abs_nonneg (v.1 _)
|
||||
|
||||
/-!
|
||||
|
||||
# Future pointing norm one Lorentz vectors
|
||||
|
||||
-/
|
||||
|
||||
/-- The future pointing Lorentz vectors with Norm one. -/
|
||||
def FuturePointing (d : ℕ) : Set (NormOneLorentzVector d) :=
|
||||
fun x => 0 < x.1.time
|
||||
|
||||
instance : TopologicalSpace (FuturePointing d) := instTopologicalSpaceSubtype
|
||||
|
||||
namespace FuturePointing
|
||||
|
||||
section
|
||||
variable (f f' : FuturePointing d)
|
||||
|
||||
lemma mem_iff : v ∈ FuturePointing d ↔ 0 < v.1.time := by
|
||||
rfl
|
||||
|
||||
lemma mem_iff_time_nonneg : v ∈ FuturePointing d ↔ 0 ≤ v.1.time := by
|
||||
refine Iff.intro (fun h => le_of_lt h) (fun h => ?_)
|
||||
rw [time_nonneg_iff] at h
|
||||
rw [mem_iff]
|
||||
linarith
|
||||
|
||||
lemma not_mem_iff : v ∉ FuturePointing d ↔ v.1.time ≤ 0 := by
|
||||
refine Iff.intro (fun h => ?_) (fun h => ?_)
|
||||
· exact le_of_not_lt ((mem_iff v).mp.mt h)
|
||||
· have h1 := (mem_iff v).mp.mt
|
||||
simp only [LorentzVector.time, Fin.isValue, not_lt] at h1
|
||||
exact h1 h
|
||||
|
||||
lemma not_mem_iff_neg : v ∉ FuturePointing d ↔ neg v ∈ FuturePointing d := by
|
||||
rw [not_mem_iff, mem_iff_time_nonneg]
|
||||
simp only [Fin.isValue, neg]
|
||||
change _ ↔ 0 ≤ - v.1 _
|
||||
exact Iff.symm neg_nonneg
|
||||
|
||||
lemma time_nonneg : 0 ≤ f.1.1.time := le_of_lt f.2
|
||||
|
||||
lemma abs_time : |f.1.1.time| = f.1.1.time := abs_of_nonneg (time_nonneg f)
|
||||
|
||||
lemma time_eq_sqrt : f.1.1.time = √(1 + ‖f.1.1.space‖ ^ 2) := by
|
||||
symm
|
||||
rw [Real.sqrt_eq_cases]
|
||||
apply Or.inl
|
||||
rw [← time_sq, sq]
|
||||
exact ⟨rfl, time_nonneg f⟩
|
||||
|
||||
/-!
|
||||
|
||||
# The sign of ⟪v, w.1⟫ₘ different v and w
|
||||
|
||||
-/
|
||||
|
||||
lemma metric_nonneg : 0 ≤ ⟪f, f'.1.1⟫ₘ := by
|
||||
apply le_trans (time_abs_sub_space_norm f f'.1)
|
||||
rw [abs_time f, abs_time f']
|
||||
exact ge_sub_norm f.1.1 f'.1.1
|
||||
|
||||
lemma one_add_metric_non_zero : 1 + ⟪f, f'.1.1⟫ₘ ≠ 0 := by
|
||||
linarith [metric_nonneg f f']
|
||||
|
||||
/-!
|
||||
|
||||
# The sign of ⟪v, w.1.spaceReflection⟫ₘ different v and w
|
||||
|
||||
-/
|
||||
|
||||
section
|
||||
variable {v w : NormOneLorentzVector d}
|
||||
open InnerProductSpace
|
||||
|
||||
lemma metric_reflect_mem_mem (h : v ∈ FuturePointing d) (hw : w ∈ FuturePointing d) :
|
||||
0 ≤ ⟪v.1, w.1.spaceReflection⟫ₘ := by
|
||||
apply le_trans (time_abs_sub_space_norm v w)
|
||||
rw [abs_time ⟨v, h⟩, abs_time ⟨w, hw⟩, sub_eq_add_neg, right_spaceReflection]
|
||||
apply (add_le_add_iff_left _).mpr
|
||||
rw [neg_le]
|
||||
apply le_trans (neg_le_abs _ : _ ≤ |⟪(v.1).space, (w.1).space⟫_ℝ|) ?_
|
||||
exact abs_real_inner_le_norm (v.1).space (w.1).space
|
||||
|
||||
lemma metric_reflect_not_mem_not_mem (h : v ∉ FuturePointing d) (hw : w ∉ FuturePointing d) :
|
||||
0 ≤ ⟪v.1, w.1.spaceReflection⟫ₘ := by
|
||||
have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h) ((not_mem_iff_neg w).mp hw)
|
||||
apply le_of_le_of_eq h1 ?_
|
||||
simp [neg]
|
||||
|
||||
lemma metric_reflect_mem_not_mem (h : v ∈ FuturePointing d) (hw : w ∉ FuturePointing d) :
|
||||
⟪v.1, w.1.spaceReflection⟫ₘ ≤ 0 := by
|
||||
rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, le_neg]
|
||||
have h1 := metric_reflect_mem_mem h ((not_mem_iff_neg w).mp hw)
|
||||
apply le_of_le_of_eq h1 ?_
|
||||
simp [neg]
|
||||
|
||||
lemma metric_reflect_not_mem_mem (h : v ∉ FuturePointing d) (hw : w ∈ FuturePointing d) :
|
||||
⟪v.1, w.1.spaceReflection⟫ₘ ≤ 0 := by
|
||||
rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, le_neg]
|
||||
have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h) hw
|
||||
apply le_of_le_of_eq h1 ?_
|
||||
simp [neg]
|
||||
|
||||
end
|
||||
end
|
||||
|
||||
end FuturePointing
|
||||
end
|
||||
|
||||
namespace FuturePointing
|
||||
/-!
|
||||
|
||||
# Topology
|
||||
|
||||
-/
|
||||
open LorentzVector
|
||||
|
||||
/-- The `FuturePointing d` which has all space components zero. -/
|
||||
@[simps!]
|
||||
noncomputable def timeVecNormOneFuture : FuturePointing d := ⟨⟨timeVec, by
|
||||
rw [NormOneLorentzVector.mem_iff, on_timeVec]⟩, by
|
||||
rw [mem_iff, timeVec_time]; exact Real.zero_lt_one⟩
|
||||
|
||||
/-- A continuous path from `timeVecNormOneFuture` to any other. -/
|
||||
noncomputable def pathFromTime (u : FuturePointing d) : Path timeVecNormOneFuture u where
|
||||
toFun t := ⟨
|
||||
⟨fun i => match i with
|
||||
| Sum.inl 0 => √(1 + t ^ 2 * ‖u.1.1.space‖ ^ 2)
|
||||
| Sum.inr i => t * u.1.1.space i,
|
||||
by
|
||||
rw [NormOneLorentzVector.mem_iff, minkowskiMetric.eq_time_minus_inner_prod]
|
||||
simp only [time, space, Function.comp_apply, PiLp.inner_apply, RCLike.inner_apply, map_mul,
|
||||
conj_trivial]
|
||||
rw [Real.mul_self_sqrt, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply]
|
||||
· simp only [Function.comp_apply, RCLike.inner_apply, conj_trivial]
|
||||
refine Eq.symm (eq_sub_of_add_eq (congrArg (HAdd.hAdd 1) ?_))
|
||||
rw [Finset.mul_sum]
|
||||
apply Finset.sum_congr rfl
|
||||
intro i _
|
||||
ring
|
||||
· exact Right.add_nonneg (zero_le_one' ℝ) $ mul_nonneg (sq_nonneg _) (sq_nonneg _)⟩,
|
||||
by
|
||||
simp only [space, Function.comp_apply, mem_iff_time_nonneg, time, Real.sqrt_pos]
|
||||
exact Real.sqrt_nonneg _⟩
|
||||
continuous_toFun := by
|
||||
refine Continuous.subtype_mk ?_ _
|
||||
refine Continuous.subtype_mk ?_ _
|
||||
apply (continuous_pi_iff).mpr
|
||||
intro i
|
||||
match i with
|
||||
| Sum.inl 0 =>
|
||||
continuity
|
||||
| Sum.inr i =>
|
||||
continuity
|
||||
source' := by
|
||||
ext
|
||||
funext i
|
||||
match i with
|
||||
| Sum.inl 0 =>
|
||||
simp only [Set.Icc.coe_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, space,
|
||||
zero_mul, add_zero, Real.sqrt_one, Fin.isValue, timeVecNormOneFuture_coe_coe]
|
||||
exact Eq.symm timeVec_time
|
||||
| Sum.inr i =>
|
||||
simp only [Set.Icc.coe_zero, space, Function.comp_apply, zero_mul,
|
||||
timeVecNormOneFuture_coe_coe]
|
||||
change _ = timeVec.space i
|
||||
rw [timeVec_space]
|
||||
rfl
|
||||
target' := by
|
||||
ext
|
||||
funext i
|
||||
match i with
|
||||
| Sum.inl 0 =>
|
||||
simp only [Set.Icc.coe_one, one_pow, space, one_mul, Fin.isValue]
|
||||
exact (time_eq_sqrt u).symm
|
||||
| Sum.inr i =>
|
||||
simp only [Set.Icc.coe_one, one_pow, space, one_mul, Fin.isValue]
|
||||
exact rfl
|
||||
|
||||
lemma isPathConnected : IsPathConnected (@Set.univ (FuturePointing d)) := by
|
||||
use timeVecNormOneFuture
|
||||
apply And.intro trivial ?_
|
||||
intro y a
|
||||
use pathFromTime y
|
||||
exact fun _ => a
|
||||
|
||||
lemma metric_continuous (u : LorentzVector d) :
|
||||
Continuous (fun (a : FuturePointing d) => ⟪u, a.1.1⟫ₘ) := by
|
||||
simp only [minkowskiMetric.eq_time_minus_inner_prod]
|
||||
refine Continuous.add ?_ ?_
|
||||
· refine Continuous.comp' (continuous_mul_left _) $ Continuous.comp'
|
||||
(continuous_apply (Sum.inl 0))
|
||||
(Continuous.comp' continuous_subtype_val continuous_subtype_val)
|
||||
· refine Continuous.comp' continuous_neg $ Continuous.inner
|
||||
(Continuous.comp' (Pi.continuous_precomp Sum.inr) continuous_const)
|
||||
(Continuous.comp' (Pi.continuous_precomp Sum.inr) (Continuous.comp'
|
||||
continuous_subtype_val continuous_subtype_val))
|
||||
|
||||
end FuturePointing
|
||||
|
||||
end NormOneLorentzVector
|
||||
|
|
@ -30,9 +30,30 @@ open minkowskiMatrix
|
|||
Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
|
||||
def Contr (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of ContrMod.rep
|
||||
|
||||
instance : TopologicalSpace (Contr d) :=
|
||||
haveI : NormedAddCommGroup (Contr d) := ContrMod.norm
|
||||
UniformSpace.toTopologicalSpace
|
||||
instance : TopologicalSpace (Contr d) := TopologicalSpace.induced
|
||||
ContrMod.toFin1dℝEquiv (Pi.topologicalSpace)
|
||||
|
||||
instance : TopologicalSpace (ContrMod d) := TopologicalSpace.induced
|
||||
ContrMod.toFin1dℝEquiv (Pi.topologicalSpace)
|
||||
|
||||
lemma toFin1dℝEquiv_isInducing : IsInducing (@ContrMod.toFin1dℝEquiv d) := by
|
||||
exact { eq_induced := rfl }
|
||||
|
||||
lemma toFin1dℝEquiv_symm_isInducing : IsInducing ((@ContrMod.toFin1dℝEquiv d).symm) := by
|
||||
let x := Equiv.toHomeomorphOfIsInducing (@ContrMod.toFin1dℝEquiv d).toEquiv
|
||||
toFin1dℝEquiv_isInducing
|
||||
exact Homeomorph.isInducing x.symm
|
||||
|
||||
lemma continuous_contr {T : Type} [TopologicalSpace T] (f : T → Contr d)
|
||||
(h : Continuous (fun i => (f i).toFin1dℝ)) : Continuous f := by
|
||||
exact continuous_induced_rng.mpr h
|
||||
|
||||
lemma contr_continuous {T : Type} [TopologicalSpace T] (f : Contr d → T)
|
||||
(h : Continuous (f ∘ (@ContrMod.toFin1dℝEquiv d).symm)): Continuous f := by
|
||||
let x := Equiv.toHomeomorphOfIsInducing (@ContrMod.toFin1dℝEquiv d).toEquiv
|
||||
toFin1dℝEquiv_isInducing
|
||||
rw [← Homeomorph.comp_continuous_iff' x.symm]
|
||||
exact h
|
||||
|
||||
/-- The representation of `LorentzGroup d` on real vectors corresponding to covariant
|
||||
Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
|
||||
|
|
@ -42,6 +63,7 @@ open CategoryTheory.MonoidalCategory
|
|||
|
||||
def toField (d : ℕ) : (𝟙_ (Rep ℝ ↑(LorentzGroup d))) →ₗ[ℝ] ℝ := LinearMap.id
|
||||
|
||||
lemma toField_apply {d : ℕ} (a : 𝟙_ (Rep ℝ ↑(LorentzGroup d))) : toField d a = a := rfl
|
||||
/-!
|
||||
|
||||
## Isomorphism between contravariant and covariant Lorentz vectors
|
||||
|
|
@ -108,5 +130,21 @@ def contrIsoCo (d : ℕ) : Contr d ≅ Co d where
|
|||
rw [LinearEquiv.apply_symm_apply, mulVec_mulVec, minkowskiMatrix.sq]
|
||||
simp
|
||||
|
||||
/-!
|
||||
|
||||
## Other properties
|
||||
|
||||
-/
|
||||
namespace Contr
|
||||
|
||||
open Lorentz
|
||||
lemma ρ_stdBasis (μ : Fin 1 ⊕ Fin 3) (Λ : LorentzGroup 3) :
|
||||
(Contr 3).ρ Λ (ContrMod.stdBasis μ) = ∑ j, Λ.1 j μ • ContrMod.stdBasis j := by
|
||||
change Λ *ᵥ ContrMod.stdBasis μ = ∑ j, Λ.1 j μ • ContrMod.stdBasis j
|
||||
apply ContrMod.ext
|
||||
simp only [toLinAlgEquiv_self, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
|
||||
Fin.isValue, Finset.sum_singleton, ContrMod.val_add, ContrMod.val_smul]
|
||||
|
||||
end Contr
|
||||
end Lorentz
|
||||
end
|
||||
|
|
|
|||
|
|
@ -141,13 +141,18 @@ open CategoryTheory
|
|||
def contrContrContract : Contr d ⊗ Contr d ⟶ 𝟙_ (Rep ℝ (LorentzGroup d)) :=
|
||||
(Contr d ◁ Contr.toCo d) ≫ contrCoContract
|
||||
|
||||
/-- Notation for `contrContrContract` acting on a tmul. -/
|
||||
scoped[Lorentz] notation "⟪" ψ "," φ "⟫ₘ" => contrContrContract.hom (ψ ⊗ₜ φ)
|
||||
/-- The linear map from Contr d ⊗ Contr d to ℝ induced by the homomorphism
|
||||
`Contr.toCo` and the contraction `contrCoContract`. -/
|
||||
def contrContrContractField : (Contr d).V ⊗[ℝ] (Contr d).V →ₗ[ℝ] ℝ :=
|
||||
contrContrContract.hom
|
||||
|
||||
/-- Notation for `contrContrContractField` acting on a tmul. -/
|
||||
scoped[Lorentz] notation "⟪" ψ "," φ "⟫ₘ" => contrContrContractField (ψ ⊗ₜ φ)
|
||||
|
||||
lemma contrContrContract_hom_tmul (φ : Contr d) (ψ : Contr d) :
|
||||
⟪φ, ψ⟫ₘ = φ.toFin1dℝ ⬝ᵥ η *ᵥ ψ.toFin1dℝ:= by
|
||||
simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
|
||||
contrContrContract, Action.comp_hom, Action.instMonoidalCategory_whiskerLeft_hom,
|
||||
contrContrContractField, Action.comp_hom, Action.instMonoidalCategory_whiskerLeft_hom,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Function.comp_apply,
|
||||
ModuleCat.MonoidalCategory.whiskerLeft_apply]
|
||||
|
|
@ -176,10 +181,10 @@ lemma coCoContract_hom_tmul (φ : Co d) (ψ : Co d) :
|
|||
|
||||
## Lemmas related to contraction.
|
||||
|
||||
We derive the lemmas in main for `contrContrContract`.
|
||||
We derive the lemmas in main for `contrContrContractField`.
|
||||
|
||||
-/
|
||||
namespace contrContrContract
|
||||
namespace contrContrContractField
|
||||
|
||||
variable (x y : Contr d)
|
||||
|
||||
|
|
@ -354,7 +359,7 @@ lemma _root_.LorentzGroup.mem_iff_norm : Λ ∈ LorentzGroup d ↔
|
|||
-/
|
||||
|
||||
lemma inl_sq_eq (v : Contr d) : v.val (Sum.inl 0) ^ 2 =
|
||||
(toField d ⟪v, v⟫ₘ) + ∑ i, v.val (Sum.inr i) ^ 2:= by
|
||||
(⟪v, v⟫ₘ) + ∑ i, v.val (Sum.inr i) ^ 2:= by
|
||||
rw [as_sum]
|
||||
apply sub_eq_iff_eq_add.mp
|
||||
congr
|
||||
|
|
@ -362,7 +367,7 @@ lemma inl_sq_eq (v : Contr d) : v.val (Sum.inl 0) ^ 2 =
|
|||
· funext i
|
||||
exact pow_two (v.val (Sum.inr i))
|
||||
|
||||
lemma le_inl_sq (v : Contr d) : toField d ⟪v, v⟫ₘ ≤ v.val (Sum.inl 0) ^ 2 := by
|
||||
lemma le_inl_sq (v : Contr d) : ⟪v, v⟫ₘ ≤ v.val (Sum.inl 0) ^ 2 := by
|
||||
rw [inl_sq_eq]
|
||||
apply (le_add_iff_nonneg_right _).mpr
|
||||
refine Fintype.sum_nonneg ?hf
|
||||
|
|
@ -380,7 +385,70 @@ lemma ge_sub_norm (v w : Contr d) : v.val (Sum.inl 0) * w.val (Sum.inl 0) -
|
|||
rw [sub_le_sub_iff_left]
|
||||
exact norm_inner_le_norm v.toSpace w.toSpace
|
||||
|
||||
end contrContrContract
|
||||
|
||||
/-!
|
||||
|
||||
# The Minkowski metric and the standard basis
|
||||
|
||||
-/
|
||||
|
||||
@[simp]
|
||||
lemma basis_left {v : Contr d} (μ : Fin 1 ⊕ Fin d) :
|
||||
⟪ ContrMod.stdBasis μ, v⟫ₘ = η μ μ * v.toFin1dℝ μ := by
|
||||
rw [as_sum]
|
||||
rcases μ with μ | μ
|
||||
· fin_cases μ
|
||||
simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
|
||||
rfl
|
||||
· simp only [Action.instMonoidalCategory_tensorUnit_V, Fin.isValue, ContrMod.stdBasis_apply,
|
||||
reduceCtorEq, ↓reduceIte, zero_mul, Sum.inr.injEq, ite_mul, one_mul, Finset.sum_ite_eq,
|
||||
Finset.mem_univ, zero_sub, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal,
|
||||
diagonal_apply_eq, Sum.elim_inr, neg_mul, neg_inj]
|
||||
rfl
|
||||
|
||||
lemma on_basis_mulVec (μ ν : Fin 1 ⊕ Fin d) : ⟪ContrMod.stdBasis μ, Λ *ᵥ ContrMod.stdBasis ν⟫ₘ = η μ μ * Λ μ ν := by
|
||||
rw [basis_left]
|
||||
rw [@ContrMod.mulVec_toFin1dℝ]
|
||||
simp [basis_left, mulVec, dotProduct, ContrMod.stdBasis_apply, ContrMod.toFin1dℝ_eq_val]
|
||||
|
||||
|
||||
lemma on_basis (μ ν : Fin 1 ⊕ Fin d) : ⟪ContrMod.stdBasis μ, ContrMod.stdBasis ν⟫ₘ = η μ ν := by
|
||||
trans ⟪ContrMod.stdBasis μ, 1 *ᵥ ContrMod.stdBasis ν⟫ₘ
|
||||
· rw [ContrMod.one_mulVec]
|
||||
rw [on_basis_mulVec]
|
||||
by_cases h : μ = ν
|
||||
· subst h
|
||||
simp
|
||||
· simp only [Action.instMonoidalCategory_tensorUnit_V, ne_eq, h, not_false_eq_true, one_apply_ne,
|
||||
mul_zero, off_diag_zero]
|
||||
|
||||
|
||||
lemma matrix_apply_stdBasis (ν μ : Fin 1 ⊕ Fin d) :
|
||||
Λ ν μ = η ν ν * ⟪ ContrMod.stdBasis ν, Λ *ᵥ ContrMod.stdBasis μ⟫ₘ := by
|
||||
rw [on_basis_mulVec, ← mul_assoc]
|
||||
simp [η_apply_mul_η_apply_diag ν]
|
||||
|
||||
/-!
|
||||
|
||||
## Self-adjoint
|
||||
|
||||
-/
|
||||
|
||||
lemma same_eq_det_toSelfAdjoint (x : ContrMod 3) :
|
||||
⟪x, x⟫ₘ = det (ContrMod.toSelfAdjoint x).1 := by
|
||||
rw [ContrMod.toSelfAdjoint_apply_coe]
|
||||
simp only [Fin.isValue, as_sum_toSpace,
|
||||
PiLp.inner_apply, Function.comp_apply, RCLike.inner_apply, conj_trivial, Fin.sum_univ_three,
|
||||
ofReal_sub, ofReal_mul, ofReal_add]
|
||||
simp only [Fin.isValue, PauliMatrix.σ0, smul_of, smul_cons, real_smul, mul_one, smul_zero,
|
||||
smul_empty, PauliMatrix.σ1, of_sub_of, sub_cons, head_cons, sub_zero, tail_cons, zero_sub,
|
||||
sub_self, zero_empty, PauliMatrix.σ2, smul_neg, sub_neg_eq_add, PauliMatrix.σ3, det_fin_two_of]
|
||||
ring_nf
|
||||
simp only [Fin.isValue, ContrMod.toFin1dℝ_eq_val, I_sq, mul_neg, mul_one, ContrMod.toSpace,
|
||||
Function.comp_apply]
|
||||
ring
|
||||
|
||||
end contrContrContractField
|
||||
|
||||
end Lorentz
|
||||
end
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ import HepLean.Meta.Informal
|
|||
import HepLean.SpaceTime.LorentzGroup.Basic
|
||||
import Mathlib.RepresentationTheory.Rep
|
||||
import Mathlib.Logic.Equiv.TransferInstance
|
||||
import HepLean.SpaceTime.PauliMatrices.SelfAdjoint
|
||||
/-!
|
||||
|
||||
## Modules associated with Real Lorentz vectors
|
||||
|
|
@ -74,6 +75,7 @@ def toFin1dℝEquiv : ContrMod d ≃ₗ[ℝ] (Fin 1 ⊕ Fin d → ℝ) :=
|
|||
through the linear equivalence `toFin1dℝEquiv`. -/
|
||||
abbrev toFin1dℝ (ψ : ContrMod d) := toFin1dℝEquiv ψ
|
||||
|
||||
lemma toFin1dℝ_eq_val (ψ : ContrMod d) : ψ.toFin1dℝ = ψ.val := by rfl
|
||||
/-!
|
||||
|
||||
## The standard basis.
|
||||
|
|
@ -109,6 +111,13 @@ lemma stdBasis_inl_apply_inr (i : Fin d) : (stdBasis (Sum.inl 0)).val (Sum.inr i
|
|||
refine stdBasis_toFin1dℝEquiv_apply_ne ?_
|
||||
simp
|
||||
|
||||
lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : (stdBasis μ).val ν = if μ = ν then 1 else 0 := by
|
||||
simp [stdBasis, Pi.basisFun_apply, Pi.single_apply]
|
||||
change Pi.single μ 1 ν = _
|
||||
simp [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)
|
||||
|
||||
/-- Decomposition of a contrvariant Lorentz vector into the standard basis. -/
|
||||
lemma stdBasis_decomp (v : ContrMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis i := by
|
||||
apply toFin1dℝEquiv.injective
|
||||
|
|
@ -192,6 +201,76 @@ lemma rep_apply_toFin1dℝ (g : LorentzGroup d) (ψ : ContrMod d) :
|
|||
(rep g ψ).toFin1dℝ = g.1 *ᵥ ψ.toFin1dℝ := by
|
||||
rfl
|
||||
|
||||
/-!
|
||||
|
||||
## To Self-Adjoint Matrix
|
||||
-/
|
||||
|
||||
/-- The linear equivalence between the vector-space `ContrMod 3` and self-adjoint
|
||||
`2×2`-complex matrices. -/
|
||||
def toSelfAdjoint : ContrMod 3 ≃ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) :=
|
||||
toFin1dℝEquiv ≪≫ₗ (Finsupp.linearEquivFunOnFinite ℝ ℝ (Fin 1 ⊕ Fin 3)).symm ≪≫ₗ
|
||||
PauliMatrix.σSAL.repr.symm
|
||||
|
||||
lemma toSelfAdjoint_apply (x : ContrMod 3) : toSelfAdjoint x =
|
||||
x.toFin1dℝ (Sum.inl 0) • ⟨PauliMatrix.σ0, PauliMatrix.σ0_selfAdjoint⟩
|
||||
- x.toFin1dℝ (Sum.inr 0) • ⟨PauliMatrix.σ1, PauliMatrix.σ1_selfAdjoint⟩
|
||||
- x.toFin1dℝ (Sum.inr 1) • ⟨PauliMatrix.σ2, PauliMatrix.σ2_selfAdjoint⟩
|
||||
- x.toFin1dℝ (Sum.inr 2) • ⟨PauliMatrix.σ3, PauliMatrix.σ3_selfAdjoint⟩ := by
|
||||
simp only [toSelfAdjoint, PauliMatrix.σSAL, LinearEquiv.trans_apply, Basis.repr_symm_apply,
|
||||
Basis.coe_mk, Fin.isValue]
|
||||
rw [Finsupp.linearCombination_apply_of_mem_supported ℝ (s := Finset.univ)]
|
||||
· change (∑ i : Fin 1 ⊕ Fin 3, x.toFin1dℝ i • PauliMatrix.σSAL' i) = _
|
||||
simp only [PauliMatrix.σSAL', Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
|
||||
Fin.isValue, Finset.sum_singleton, Fin.sum_univ_three]
|
||||
apply Subtype.ext
|
||||
simp only [Fin.isValue, AddSubgroup.coe_add, selfAdjoint.val_smul, smul_neg,
|
||||
AddSubgroupClass.coe_sub]
|
||||
simp only [neg_add, add_assoc, sub_eq_add_neg]
|
||||
· simp_all only [Finset.coe_univ, Finsupp.supported_univ, Submodule.mem_top]
|
||||
|
||||
lemma toSelfAdjoint_apply_coe (x : ContrMod 3) : (toSelfAdjoint x).1 =
|
||||
x.toFin1dℝ (Sum.inl 0) • PauliMatrix.σ0
|
||||
- x.toFin1dℝ (Sum.inr 0) • PauliMatrix.σ1
|
||||
- x.toFin1dℝ (Sum.inr 1) • PauliMatrix.σ2
|
||||
- x.toFin1dℝ (Sum.inr 2) • PauliMatrix.σ3 := by
|
||||
rw [toSelfAdjoint_apply]
|
||||
rfl
|
||||
|
||||
|
||||
lemma toSelfAdjoint_stdBasis (i : Fin 1 ⊕ Fin 3) :
|
||||
toSelfAdjoint (stdBasis i) = PauliMatrix.σSAL i := by
|
||||
rw [toSelfAdjoint_apply]
|
||||
match i with
|
||||
| Sum.inl 0 =>
|
||||
simp only [stdBasis, Fin.isValue, Basis.coe_ofEquivFun, LinearEquiv.apply_symm_apply,
|
||||
Pi.single_eq_same, one_smul, ne_eq, reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne,
|
||||
zero_smul, sub_zero, PauliMatrix.σSAL, Basis.coe_mk, PauliMatrix.σSAL']
|
||||
| Sum.inr 0 =>
|
||||
simp only [stdBasis, Fin.isValue, Basis.coe_ofEquivFun, LinearEquiv.apply_symm_apply, ne_eq,
|
||||
reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul, Pi.single_eq_same, one_smul,
|
||||
zero_sub, Sum.inr.injEq, one_ne_zero, sub_zero, Fin.reduceEq, PauliMatrix.σSAL, Basis.coe_mk,
|
||||
PauliMatrix.σSAL']
|
||||
rfl
|
||||
| Sum.inr 1 =>
|
||||
simp only [stdBasis, Fin.isValue, Basis.coe_ofEquivFun, LinearEquiv.apply_symm_apply, ne_eq,
|
||||
reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul, Sum.inr.injEq, zero_ne_one,
|
||||
sub_self, Pi.single_eq_same, one_smul, zero_sub, Fin.reduceEq, sub_zero, PauliMatrix.σSAL,
|
||||
Basis.coe_mk, PauliMatrix.σSAL']
|
||||
rfl
|
||||
| Sum.inr 2 =>
|
||||
simp only [stdBasis, Fin.isValue, Basis.coe_ofEquivFun, LinearEquiv.apply_symm_apply, ne_eq,
|
||||
reduceCtorEq, not_false_eq_true, Pi.single_eq_of_ne, zero_smul, Sum.inr.injEq, Fin.reduceEq,
|
||||
sub_self, Pi.single_eq_same, one_smul, zero_sub, PauliMatrix.σSAL, Basis.coe_mk,
|
||||
PauliMatrix.σSAL']
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma toSelfAdjoint_symm_basis (i : Fin 1 ⊕ Fin 3) :
|
||||
toSelfAdjoint.symm (PauliMatrix.σSAL i) = (stdBasis i) := by
|
||||
refine (LinearEquiv.symm_apply_eq toSelfAdjoint).mpr ?_
|
||||
rw [toSelfAdjoint_stdBasis]
|
||||
|
||||
end ContrMod
|
||||
|
||||
/-- The module for covariant (up-index) complex Lorentz vectors. -/
|
||||
|
|
@ -266,6 +345,14 @@ lemma stdBasis_toFin1dℝEquiv_apply_ne {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν
|
|||
rw [@LinearEquiv.apply_symm_apply]
|
||||
exact Pi.single_eq_of_ne' h 1
|
||||
|
||||
lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : (stdBasis μ).val ν = if μ = ν then 1 else 0 := by
|
||||
simp [stdBasis, Pi.basisFun_apply, Pi.single_apply]
|
||||
change Pi.single μ 1 ν = _
|
||||
simp [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)
|
||||
|
||||
|
||||
/-- Decomposition of a covariant Lorentz vector into the standard basis. -/
|
||||
lemma stdBasis_decomp (v : CoMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis i := by
|
||||
apply toFin1dℝEquiv.injective
|
||||
|
|
|
|||
|
|
@ -29,9 +29,12 @@ namespace NormOne
|
|||
lemma mem_iff {v : Contr d} : v ∈ NormOne d ↔ ⟪v, v⟫ₘ = (1 : ℝ) := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma contr_self (v : NormOne d) : ⟪v.1, v.1⟫ₘ = (1 : ℝ) := v.2
|
||||
|
||||
lemma mem_mulAction (g : LorentzGroup d) (v : Contr d) :
|
||||
v ∈ NormOne d ↔ (Contr d).ρ g v ∈ NormOne d := by
|
||||
rw [mem_iff, mem_iff, contrContrContract.action_tmul]
|
||||
rw [mem_iff, mem_iff, contrContrContractField.action_tmul]
|
||||
|
||||
instance : TopologicalSpace (NormOne d) := instTopologicalSpaceSubtype
|
||||
|
||||
|
|
@ -49,7 +52,7 @@ def neg : NormOne d := ⟨- v, by
|
|||
@[simps!]
|
||||
def _root_.LorentzGroup.toNormOne (Λ : LorentzGroup d) : NormOne d :=
|
||||
⟨(Contr d).ρ Λ (ContrMod.stdBasis (Sum.inl 0)), by
|
||||
rw [mem_iff, contrContrContract.action_tmul, contrContrContract.stdBasis_inl]⟩
|
||||
rw [mem_iff, contrContrContractField.action_tmul, contrContrContractField.stdBasis_inl]⟩
|
||||
|
||||
lemma _root_.LorentzGroup.toNormOne_inl (Λ : LorentzGroup d) :
|
||||
(LorentzGroup.toNormOne Λ).val.val (Sum.inl 0) = Λ.1 (Sum.inl 0) (Sum.inl 0) := by
|
||||
|
|
@ -64,7 +67,7 @@ lemma _root_.LorentzGroup.toNormOne_inr (Λ : LorentzGroup d) (i : Fin d) :
|
|||
lemma _root_.LorentzGroup.inl_inl_mul (Λ Λ' : LorentzGroup d) : (Λ * Λ').1 (Sum.inl 0) (Sum.inl 0) =
|
||||
⟪(LorentzGroup.toNormOne (LorentzGroup.transpose Λ)).1,
|
||||
(Contr d).ρ LorentzGroup.parity (LorentzGroup.toNormOne Λ').1⟫ₘ := by
|
||||
rw [contrContrContract.right_parity]
|
||||
rw [contrContrContractField.right_parity]
|
||||
simp only [Fin.isValue, lorentzGroupIsGroup_mul_coe, Matrix.mul_apply, Fintype.sum_sum_type,
|
||||
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton,
|
||||
LorentzGroup.transpose, PiLp.inner_apply, Function.comp_apply,
|
||||
|
|
@ -78,7 +81,7 @@ lemma _root_.LorentzGroup.inl_inl_mul (Λ Λ' : LorentzGroup d) : (Λ * Λ').1 (
|
|||
rfl
|
||||
|
||||
lemma inl_sq : v.val.val (Sum.inl 0) ^ 2 = 1 + ‖ContrMod.toSpace v.val‖ ^ 2 := by
|
||||
rw [contrContrContract.inl_sq_eq, v.2]
|
||||
rw [contrContrContractField.inl_sq_eq, v.2]
|
||||
congr
|
||||
rw [← real_inner_self_eq_norm_sq]
|
||||
simp only [PiLp.inner_apply, RCLike.inner_apply, conj_trivial]
|
||||
|
|
@ -87,7 +90,7 @@ lemma inl_sq : v.val.val (Sum.inl 0) ^ 2 = 1 + ‖ContrMod.toSpace v.val‖ ^ 2
|
|||
exact pow_two ((v.val).val (Sum.inr x))
|
||||
|
||||
lemma one_le_abs_inl : 1 ≤ |v.val.val (Sum.inl 0)| := by
|
||||
have h1 := contrContrContract.le_inl_sq v.val
|
||||
have h1 := contrContrContractField.le_inl_sq v.val
|
||||
rw [v.2] at h1
|
||||
exact (one_le_sq_iff_one_le_abs _).mp h1
|
||||
|
||||
|
|
@ -175,34 +178,44 @@ lemma inl_nonneg : 0 ≤ f.val.val.val (Sum.inl 0):= le_of_lt f.2
|
|||
lemma abs_inl : |f.val.val.val (Sum.inl 0)| = f.val.val.val (Sum.inl 0) :=
|
||||
abs_of_nonneg (inl_nonneg f)
|
||||
|
||||
lemma inl_eq_sqrt : f.val.val.val (Sum.inl 0) = √(1 + ‖f.1.1.toSpace‖ ^ 2) := by
|
||||
symm
|
||||
rw [Real.sqrt_eq_cases]
|
||||
apply Or.inl
|
||||
rw [← inl_sq, sq]
|
||||
exact ⟨rfl, inl_nonneg f⟩
|
||||
|
||||
open InnerProductSpace
|
||||
lemma metric_nonneg : 0 ≤ toField d ⟪f.1.1, f'.1.1⟫ₘ := by
|
||||
lemma metric_nonneg : 0 ≤ ⟪f.1.1, f'.1.1⟫ₘ := by
|
||||
apply le_trans (inl_abs_sub_space_norm f f'.1)
|
||||
rw [abs_inl f, abs_inl f']
|
||||
exact contrContrContract.ge_sub_norm f.1.1 f'.1.1
|
||||
exact contrContrContractField.ge_sub_norm f.1.1 f'.1.1
|
||||
|
||||
lemma one_add_metric_non_zero : 1 + ⟪f.1.1, f'.1.1⟫ₘ ≠ 0 := by
|
||||
linarith [metric_nonneg f f']
|
||||
|
||||
variable {v w : NormOne d}
|
||||
|
||||
lemma metric_reflect_mem_mem (h : v ∈ FuturePointing d) (hw : w ∈ FuturePointing d) :
|
||||
0 ≤ toField d ⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ :=
|
||||
0 ≤ ⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ :=
|
||||
metric_nonneg ⟨v, h⟩ ⟨⟨(Contr d).ρ LorentzGroup.parity w.1,
|
||||
(NormOne.mem_mulAction _ _).mp w.2⟩, (mem_iff_parity_mem w).mp hw⟩
|
||||
|
||||
lemma metric_reflect_not_mem_not_mem (h : v ∉ FuturePointing d) (hw : w ∉ FuturePointing d) :
|
||||
0 ≤ toField d ⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ := by
|
||||
0 ≤ ⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ := by
|
||||
have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h) ((not_mem_iff_neg w).mp hw)
|
||||
apply le_of_le_of_eq h1 ?_
|
||||
simp [neg, neg_tmul, tmul_neg]
|
||||
|
||||
lemma metric_reflect_mem_not_mem (h : v ∈ FuturePointing d) (hw : w ∉ FuturePointing d) :
|
||||
toField d ⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ ≤ 0 := by
|
||||
⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ ≤ 0 := by
|
||||
rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, le_neg]
|
||||
have h1 := metric_reflect_mem_mem h ((not_mem_iff_neg w).mp hw)
|
||||
apply le_of_le_of_eq h1 ?_
|
||||
simp [neg, neg_tmul, tmul_neg]
|
||||
|
||||
lemma metric_reflect_not_mem_mem (h : v ∉ FuturePointing d) (hw : w ∈ FuturePointing d) :
|
||||
toField d ⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ ≤ 0 := by
|
||||
⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ ≤ 0 := by
|
||||
rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, le_neg]
|
||||
have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h) hw
|
||||
apply le_of_le_of_eq h1 ?_
|
||||
|
|
@ -212,6 +225,106 @@ end FuturePointing
|
|||
|
||||
end NormOne
|
||||
|
||||
namespace NormOne
|
||||
namespace FuturePointing
|
||||
/-!
|
||||
## Topology
|
||||
-/
|
||||
|
||||
|
||||
/-- The `FuturePointing d` which has all space components zero. -/
|
||||
@[simps!]
|
||||
noncomputable def timeVecNormOneFuture : FuturePointing d := ⟨⟨ContrMod.stdBasis (Sum.inl 0), by
|
||||
rw [NormOne.mem_iff, contrContrContractField.on_basis]
|
||||
rfl⟩, by
|
||||
rw [mem_iff]
|
||||
simp⟩
|
||||
|
||||
/-- A continuous path from `timeVecNormOneFuture` to any other. -/
|
||||
noncomputable def pathFromTime (u : FuturePointing d) : Path timeVecNormOneFuture u where
|
||||
toFun t := ⟨
|
||||
⟨{val := fun i => match i with
|
||||
| Sum.inl 0 => √(1 + t ^ 2 * ‖u.1.1.toSpace‖ ^ 2)
|
||||
| Sum.inr i => t * u.1.1.toSpace i},
|
||||
by
|
||||
rw [NormOne.mem_iff, contrContrContractField.as_sum_toSpace]
|
||||
simp only [ContrMod.toSpace, Function.comp_apply, PiLp.inner_apply, RCLike.inner_apply, map_mul,
|
||||
conj_trivial]
|
||||
rw [Real.mul_self_sqrt, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply]
|
||||
· simp only [Function.comp_apply, RCLike.inner_apply, conj_trivial]
|
||||
refine Eq.symm (eq_sub_of_add_eq (congrArg (HAdd.hAdd _) ?_))
|
||||
rw [Finset.mul_sum]
|
||||
apply Finset.sum_congr rfl
|
||||
intro i _
|
||||
ring_nf
|
||||
· exact Right.add_nonneg (zero_le_one' ℝ) $ mul_nonneg (sq_nonneg _) (sq_nonneg _)⟩,
|
||||
by
|
||||
simp only [ContrMod.toSpace, Function.comp_apply, mem_iff_inl_nonneg, Real.sqrt_pos]
|
||||
exact Real.sqrt_nonneg _⟩
|
||||
continuous_toFun := by
|
||||
refine Continuous.subtype_mk ?_ _
|
||||
refine Continuous.subtype_mk ?_ _
|
||||
refine continuous_contr _ ?_
|
||||
apply (continuous_pi_iff).mpr
|
||||
intro i
|
||||
match i with
|
||||
| Sum.inl 0 =>
|
||||
continuity
|
||||
| Sum.inr i =>
|
||||
continuity
|
||||
source' := by
|
||||
ext
|
||||
apply ContrMod.ext
|
||||
funext i
|
||||
match i with
|
||||
| Sum.inl 0 =>
|
||||
simp only [Set.Icc.coe_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow,
|
||||
zero_mul, add_zero, Real.sqrt_one, timeVecNormOneFuture, Fin.isValue,
|
||||
ContrMod.stdBasis_apply_same]
|
||||
| Sum.inr i =>
|
||||
simp only [Set.Icc.coe_zero, zero_mul, timeVecNormOneFuture, Fin.isValue,
|
||||
ContrMod.stdBasis_inl_apply_inr]
|
||||
target' := by
|
||||
ext
|
||||
apply ContrMod.ext
|
||||
funext i
|
||||
match i with
|
||||
| Sum.inl 0 =>
|
||||
simp [Set.Icc.coe_one, one_pow, one_mul, Fin.isValue]
|
||||
exact (inl_eq_sqrt u).symm
|
||||
| Sum.inr i =>
|
||||
simp only [Set.Icc.coe_one, one_pow, one_mul, Fin.isValue]
|
||||
rfl
|
||||
|
||||
lemma isPathConnected : IsPathConnected (@Set.univ (FuturePointing d)) := by
|
||||
use timeVecNormOneFuture
|
||||
apply And.intro trivial ?_
|
||||
intro y a
|
||||
use pathFromTime y
|
||||
exact fun _ => a
|
||||
|
||||
lemma metric_continuous (u : Contr d) :
|
||||
Continuous (fun (a : FuturePointing d) => ⟪u, a.1.1⟫ₘ) := by
|
||||
simp only [contrContrContractField.as_sum_toSpace]
|
||||
refine Continuous.add ?_ ?_
|
||||
· refine Continuous.comp' (continuous_mul_left _) $ Continuous.comp'
|
||||
(continuous_apply (Sum.inl 0))
|
||||
(Continuous.comp' ?_ ?_)
|
||||
· exact continuous_iff_le_induced.mpr fun U a => a
|
||||
· exact Continuous.comp' continuous_subtype_val continuous_subtype_val
|
||||
· refine Continuous.comp' continuous_neg $ Continuous.inner
|
||||
(Continuous.comp' (?_) continuous_const)
|
||||
(Continuous.comp' (?_) (Continuous.comp'
|
||||
continuous_subtype_val continuous_subtype_val))
|
||||
· apply contr_continuous
|
||||
exact Pi.continuous_precomp Sum.inr
|
||||
· apply contr_continuous
|
||||
exact Pi.continuous_precomp Sum.inr
|
||||
|
||||
end FuturePointing
|
||||
|
||||
end NormOne
|
||||
|
||||
end
|
||||
|
||||
end Contr
|
||||
|
|
|
|||
|
|
@ -3,7 +3,8 @@ 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.LorentzVector.Basic
|
||||
import Mathlib.Data.Complex.Exponential
|
||||
import Mathlib.Analysis.InnerProductSpace.PiL2
|
||||
import Mathlib.Algebra.Lie.Classical
|
||||
/-!
|
||||
|
||||
|
|
|
|||
|
|
@ -1,241 +0,0 @@
|
|||
/-
|
||||
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
|
||||
/-!
|
||||
|
||||
# The Minkowski Metric
|
||||
|
||||
This file introduces the Minkowski metric on spacetime in the mainly-minus signature.
|
||||
|
||||
We define the Minkowski metric as a bilinear map on the vector space
|
||||
of Lorentz vectors in d dimensions.
|
||||
|
||||
-/
|
||||
|
||||
open Matrix
|
||||
open InnerProductSpace
|
||||
|
||||
/-!
|
||||
|
||||
# The definition of the Minkowski Metric
|
||||
|
||||
-/
|
||||
|
||||
/-- Given a Lorentz vector `v` we define the the linear map `w ↦ v * η * w`. -/
|
||||
@[simps!]
|
||||
def minkowskiLinearForm {d : ℕ} (v : LorentzVector d) : LorentzVector d →ₗ[ℝ] ℝ where
|
||||
toFun w := v ⬝ᵥ (minkowskiMatrix *ᵥ w)
|
||||
map_add' y z := by
|
||||
noncomm_ring
|
||||
rw [mulVec_add, dotProduct_add]
|
||||
map_smul' c y := by
|
||||
simp only [RingHom.id_apply, smul_eq_mul]
|
||||
rw [mulVec_smul, dotProduct_smul]
|
||||
rfl
|
||||
|
||||
/-- The Minkowski metric as a bilinear map. -/
|
||||
def minkowskiMetric {d : ℕ} : LorentzVector d →ₗ[ℝ] LorentzVector d →ₗ[ℝ] ℝ where
|
||||
toFun v := minkowskiLinearForm v
|
||||
map_add' y z := by
|
||||
ext1 x
|
||||
simp only [minkowskiLinearForm_apply, LinearMap.add_apply]
|
||||
apply add_dotProduct
|
||||
map_smul' c y := by
|
||||
ext1 x
|
||||
simp only [minkowskiLinearForm_apply, RingHom.id_apply, LinearMap.smul_apply, smul_eq_mul]
|
||||
rw [smul_dotProduct]
|
||||
rfl
|
||||
|
||||
namespace minkowskiMetric
|
||||
|
||||
open minkowskiMatrix
|
||||
|
||||
open LorentzVector
|
||||
|
||||
variable {d : ℕ}
|
||||
variable (v w : LorentzVector d)
|
||||
|
||||
/-- Notation for `minkowskiMetric`. -/
|
||||
scoped[minkowskiMetric] notation:102 "⟪" v "," w "⟫ₘ" => minkowskiMetric v w
|
||||
/-!
|
||||
|
||||
# Equalitites involving the Minkowski metric
|
||||
|
||||
-/
|
||||
|
||||
/-- The Minkowski metric expressed as a sum. -/
|
||||
lemma as_sum :
|
||||
⟪v, w⟫ₘ = v.time * w.time - ∑ i, v.space i * w.space i := by
|
||||
simp only [minkowskiMetric, LinearMap.coe_mk, AddHom.coe_mk, minkowskiLinearForm_apply,
|
||||
dotProduct, LieAlgebra.Orthogonal.indefiniteDiagonal, mulVec_diagonal, Fintype.sum_sum_type,
|
||||
Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Sum.elim_inl, one_mul,
|
||||
Finset.sum_singleton, Sum.elim_inr, neg_mul, mul_neg, Finset.sum_neg_distrib, time, space,
|
||||
Function.comp_apply, minkowskiMatrix]
|
||||
rfl
|
||||
|
||||
/-- The Minkowski metric expressed as a sum for a single vector. -/
|
||||
lemma as_sum_self : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 := by
|
||||
rw [← real_inner_self_eq_norm_sq, PiLp.inner_apply, as_sum]
|
||||
noncomm_ring
|
||||
|
||||
lemma eq_time_minus_inner_prod : ⟪v, w⟫ₘ = v.time * w.time - ⟪v.space, w.space⟫_ℝ := by
|
||||
rw [as_sum, @PiLp.inner_apply]
|
||||
rfl
|
||||
|
||||
lemma self_eq_time_minus_norm : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 := by
|
||||
rw [← real_inner_self_eq_norm_sq, PiLp.inner_apply, as_sum]
|
||||
noncomm_ring
|
||||
|
||||
/-- The Minkowski metric is symmetric in its arguments.. -/
|
||||
lemma symm : ⟪v, w⟫ₘ = ⟪w, v⟫ₘ := by
|
||||
simp only [as_sum]
|
||||
ac_rfl
|
||||
|
||||
lemma time_sq_eq_metric_add_space : v.time ^ 2 = ⟪v, v⟫ₘ + ‖v.space‖ ^ 2 := by
|
||||
rw [self_eq_time_minus_norm]
|
||||
exact Eq.symm (sub_add_cancel (v.time ^ 2) (‖v.space‖ ^ 2))
|
||||
|
||||
/-!
|
||||
|
||||
# Minkowski metric and space reflections
|
||||
|
||||
-/
|
||||
|
||||
lemma right_spaceReflection : ⟪v, w.spaceReflection⟫ₘ = v.time * w.time + ⟪v.space, w.space⟫_ℝ := by
|
||||
rw [eq_time_minus_inner_prod, spaceReflection_space, spaceReflection_time]
|
||||
simp only [time, Fin.isValue, space, inner_neg_right, PiLp.inner_apply, Function.comp_apply,
|
||||
RCLike.inner_apply, conj_trivial, sub_neg_eq_add]
|
||||
|
||||
lemma self_spaceReflection_eq_zero_iff : ⟪v, v.spaceReflection⟫ₘ = 0 ↔ v = 0 := by
|
||||
refine Iff.intro (fun h => ?_) (fun h => ?_)
|
||||
· rw [right_spaceReflection] at h
|
||||
have h2 : 0 ≤ ⟪v.space, v.space⟫_ℝ := real_inner_self_nonneg
|
||||
have h3 : v.time * v.time = 0 := by linarith [mul_self_nonneg v.time]
|
||||
have h4 : ⟪v.space, v.space⟫_ℝ = 0 := by linarith
|
||||
simp only [time, Fin.isValue, mul_eq_zero, or_self] at h3
|
||||
rw [@inner_self_eq_zero] at h4
|
||||
funext i
|
||||
rcases i with i | i
|
||||
· fin_cases i
|
||||
exact h3
|
||||
· simpa using congrFun h4 i
|
||||
· rw [h]
|
||||
exact LinearMap.map_zero₂ minkowskiMetric (spaceReflection 0)
|
||||
|
||||
/-!
|
||||
|
||||
# Non degeneracy of the Minkowski metric
|
||||
|
||||
-/
|
||||
|
||||
/-- The metric tensor is non-degenerate. -/
|
||||
lemma nondegenerate : (∀ w, ⟪w, v⟫ₘ = 0) ↔ v = 0 := by
|
||||
refine Iff.intro (fun h => ?_) (fun h => ?_)
|
||||
· exact (self_spaceReflection_eq_zero_iff _).mp ((symm _ _).trans $ h v.spaceReflection)
|
||||
· simp [h]
|
||||
|
||||
/-!
|
||||
|
||||
# Inequalities involving the Minkowski metric
|
||||
|
||||
-/
|
||||
|
||||
lemma leq_time_sq : ⟪v, v⟫ₘ ≤ v.time ^ 2 := by
|
||||
rw [time_sq_eq_metric_add_space]
|
||||
exact (le_add_iff_nonneg_right _).mpr $ sq_nonneg ‖v.space‖
|
||||
|
||||
lemma ge_abs_inner_product : v.time * w.time - ‖⟪v.space, w.space⟫_ℝ‖ ≤ ⟪v, w⟫ₘ := by
|
||||
rw [eq_time_minus_inner_prod, sub_le_sub_iff_left]
|
||||
exact Real.le_norm_self ⟪v.space, w.space⟫_ℝ
|
||||
|
||||
lemma ge_sub_norm : v.time * w.time - ‖v.space‖ * ‖w.space‖ ≤ ⟪v, w⟫ₘ := by
|
||||
apply le_trans _ (ge_abs_inner_product v w)
|
||||
rw [sub_le_sub_iff_left]
|
||||
exact norm_inner_le_norm v.space w.space
|
||||
|
||||
/-!
|
||||
|
||||
# The Minkowski metric and matrices
|
||||
|
||||
-/
|
||||
section matrices
|
||||
|
||||
variable (Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
|
||||
|
||||
@[simp]
|
||||
lemma dual_mulVec_right : ⟪x, (dual Λ) *ᵥ y⟫ₘ = ⟪Λ *ᵥ x, y⟫ₘ := by
|
||||
simp only [minkowskiMetric, LinearMap.coe_mk, AddHom.coe_mk, dual, minkowskiLinearForm_apply,
|
||||
mulVec_mulVec, ← mul_assoc, minkowskiMatrix.sq, one_mul, (vecMul_transpose Λ x).symm, ←
|
||||
dotProduct_mulVec]
|
||||
|
||||
@[simp]
|
||||
lemma dual_mulVec_left : ⟪(dual Λ) *ᵥ x, y⟫ₘ = ⟪x, Λ *ᵥ y⟫ₘ := by
|
||||
rw [symm, dual_mulVec_right, symm]
|
||||
|
||||
lemma matrix_apply_eq_iff_sub : ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ ↔ ⟪v, (Λ - Λ') *ᵥ w⟫ₘ = 0 := by
|
||||
rw [← sub_eq_zero, ← LinearMap.map_sub, sub_mulVec]
|
||||
|
||||
lemma matrix_eq_iff_eq_forall' : (∀ v, Λ *ᵥ v = Λ' *ᵥ v) ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by
|
||||
refine Iff.intro (fun h ↦ fun w v ↦ ?_) (fun h ↦ fun v ↦ ?_)
|
||||
· rw [h w]
|
||||
· simp only [matrix_apply_eq_iff_sub] at h
|
||||
refine sub_eq_zero.1 ?_
|
||||
have h1 := h v
|
||||
rw [nondegenerate] at h1
|
||||
simp only [sub_mulVec] at h1
|
||||
exact h1
|
||||
|
||||
lemma matrix_eq_iff_eq_forall : Λ = Λ' ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by
|
||||
rw [← matrix_eq_iff_eq_forall']
|
||||
refine Iff.intro (fun h => ?_) (fun h => ?_)
|
||||
· exact fun _ => congrFun (congrArg mulVec h) _
|
||||
· rw [← (LinearMap.toMatrix stdBasis stdBasis).toEquiv.symm.apply_eq_iff_eq]
|
||||
ext x
|
||||
simp only [LinearEquiv.coe_toEquiv_symm, LinearMap.toMatrix_symm, EquivLike.coe_coe,
|
||||
toLin_apply, h, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
|
||||
Finset.sum_singleton]
|
||||
|
||||
lemma matrix_eq_id_iff : Λ = 1 ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, w⟫ₘ := by
|
||||
rw [matrix_eq_iff_eq_forall]
|
||||
simp
|
||||
|
||||
/-!
|
||||
|
||||
# The Minkowski metric and the standard basis
|
||||
|
||||
-/
|
||||
|
||||
@[simp]
|
||||
lemma basis_left (μ : Fin 1 ⊕ Fin d) : ⟪e μ, v⟫ₘ = η μ μ * v μ := by
|
||||
rw [as_sum]
|
||||
rcases μ with μ | μ
|
||||
· fin_cases μ
|
||||
simp [stdBasis_apply, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
|
||||
· simp [stdBasis_apply, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
|
||||
|
||||
lemma on_timeVec : ⟪timeVec, @timeVec d⟫ₘ = 1 := by
|
||||
simp only [timeVec, Fin.isValue, basis_left, minkowskiMatrix,
|
||||
LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_apply_eq, Sum.elim_inl, stdBasis_apply,
|
||||
↓reduceIte, mul_one]
|
||||
|
||||
lemma on_basis_mulVec (μ ν : Fin 1 ⊕ Fin d) : ⟪e μ, Λ *ᵥ e ν⟫ₘ = η μ μ * Λ μ ν := by
|
||||
simp [basis_left, mulVec, dotProduct, stdBasis_apply]
|
||||
|
||||
lemma on_basis (μ ν : Fin 1 ⊕ Fin d) : ⟪e μ, e ν⟫ₘ = η μ ν := by
|
||||
rw [basis_left, stdBasis_apply]
|
||||
by_cases h : μ = ν
|
||||
· simp [h]
|
||||
· simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_apply_eq,
|
||||
mul_ite, mul_one, mul_zero, ne_eq, h, not_false_eq_true, diagonal_apply_ne, ite_eq_right_iff]
|
||||
exact fun a => False.elim (h (id (Eq.symm a)))
|
||||
|
||||
lemma matrix_apply_stdBasis (ν μ : Fin 1 ⊕ Fin d) :
|
||||
Λ ν μ = η ν ν * ⟪e ν, Λ *ᵥ e μ⟫ₘ := by
|
||||
rw [on_basis_mulVec, ← mul_assoc]
|
||||
simp [η_apply_mul_η_apply_diag ν]
|
||||
|
||||
end matrices
|
||||
end minkowskiMetric
|
||||
|
|
@ -131,14 +131,14 @@ def asConsTensor : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ leftHanded ⊗
|
|||
map_sum, map_tmul]
|
||||
symm
|
||||
calc _ = ∑ x, ((complexContr.ρ M) (complexContrBasis x) ⊗ₜ[ℂ]
|
||||
leftRightToMatrix.symm (SL2C.repSelfAdjointMatrix M (σSA x))) := by
|
||||
leftRightToMatrix.symm (SL2C.toLinearMapSelfAdjointMatrix M (σSA x))) := by
|
||||
refine Finset.sum_congr rfl (fun x _ => ?_)
|
||||
rw [← leftRightToMatrix_ρ_symm_selfAdjoint]
|
||||
rfl
|
||||
_ = ∑ x, ((∑ i, (SL2C.toLorentzGroup M).1 i x • (complexContrBasis i)) ⊗ₜ[ℂ]
|
||||
∑ j, leftRightToMatrix.symm ((SL2C.toLorentzGroup M⁻¹).1 x j • (σSA j))) := by
|
||||
refine Finset.sum_congr rfl (fun x _ => ?_)
|
||||
rw [SL2CRep_ρ_basis, SL2C.repSelfAdjointMatrix_σSA]
|
||||
rw [SL2CRep_ρ_basis, SL2C.toLinearMapSelfAdjointMatrix_σSA]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, SL2C.toLorentzGroup_apply_coe,
|
||||
Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
|
||||
Finset.sum_singleton, map_inv, lorentzGroupIsGroup_inv, AddSubgroup.coe_add,
|
||||
|
|
|
|||
|
|
@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.SpaceTime.LorentzGroup.Basic
|
||||
import HepLean.SpaceTime.LorentzVector.Real.Basic
|
||||
import Mathlib.RepresentationTheory.Basic
|
||||
import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
|
||||
import HepLean.SpaceTime.LorentzGroup.Restricted
|
||||
import HepLean.SpaceTime.PauliMatrices.SelfAdjoint
|
||||
import HepLean.Meta.Informal
|
||||
/-!
|
||||
# The group SL(2, ℂ) and it's relation to the Lorentz group
|
||||
|
|
@ -71,107 +72,90 @@ def toLinearMapSelfAdjointMatrix (M : SL(2, ℂ)) :
|
|||
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
|
||||
lemma toLinearMapSelfAdjointMatrix_det (M : SL(2, ℂ)) (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
|
||||
det ((toLinearMapSelfAdjointMatrix M) A).1 = det A.1 := by
|
||||
simp only [LinearMap.coe_mk, AddHom.coe_mk, toLinearMapSelfAdjointMatrix, det_mul,
|
||||
selfAdjoint.mem_iff, det_conjTranspose, det_mul, det_one, RingHom.id_apply]
|
||||
simp only [SpecialLinearGroup.det_coe, one_mul, star_one, mul_one]
|
||||
|
||||
def toMatrix : SL(2, ℂ) →* Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ where
|
||||
toFun M := LinearMap.toMatrix PauliMatrix.σSAL PauliMatrix.σSAL (toLinearMapSelfAdjointMatrix M)
|
||||
map_one' := by
|
||||
noncomm_ring [toLinearMapSelfAdjointMatrix, SpecialLinearGroup.coe_one, one_mul,
|
||||
conjTranspose_one, mul_one, Subtype.coe_eta]
|
||||
simp only [toLinearMapSelfAdjointMatrix, SpecialLinearGroup.coe_one, one_mul, conjTranspose_one,
|
||||
mul_one, Subtype.coe_eta]
|
||||
erw [LinearMap.toMatrix_one]
|
||||
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]
|
||||
simp only
|
||||
rw [← LinearMap.toMatrix_mul]
|
||||
apply congrArg
|
||||
ext1 x
|
||||
simp only [toLinearMapSelfAdjointMatrix, SpecialLinearGroup.coe_mul, conjTranspose_mul,
|
||||
LinearMap.coe_mk, AddHom.coe_mk, LinearMap.mul_apply, Subtype.mk.injEq]
|
||||
noncomm_ring
|
||||
|
||||
/-- 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
|
||||
open Lorentz in
|
||||
lemma toMatrix_apply_contrMod (M : SL(2, ℂ)) (v : ContrMod 3) :
|
||||
(toMatrix M) *ᵥ v = ContrMod.toSelfAdjoint.symm
|
||||
((toLinearMapSelfAdjointMatrix M) (ContrMod.toSelfAdjoint v)) := by
|
||||
simp [toMatrix, LinearMap.toMatrix_apply, ContrMod.mulVec]
|
||||
obtain ⟨a, ha⟩ := ContrMod.toSelfAdjoint.symm.surjective v
|
||||
subst ha
|
||||
rw [LinearEquiv.apply_symm_apply]
|
||||
simp [ContrMod.toSelfAdjoint]
|
||||
change ContrMod.toFin1dℝEquiv.symm ((
|
||||
((LinearMap.toMatrix PauliMatrix.σSAL PauliMatrix.σSAL) (toLinearMapSelfAdjointMatrix M)))
|
||||
*ᵥ (((Finsupp.linearEquivFunOnFinite ℝ ℝ (Fin 1 ⊕ Fin 3)) (PauliMatrix.σSAL.repr a)))) = _
|
||||
apply congrArg
|
||||
erw [LinearMap.toMatrix_mulVec_repr]
|
||||
rfl
|
||||
|
||||
/-!
|
||||
|
||||
## 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
|
||||
lemma toMatrix_mem_lorentzGroup (M : SL(2, ℂ)) : toMatrix M ∈ LorentzGroup 3 := 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)
|
||||
intro x
|
||||
apply ofReal_injective
|
||||
rw [Lorentz.contrContrContractField.same_eq_det_toSelfAdjoint]
|
||||
rw [toMatrix_apply_contrMod]
|
||||
rw [LinearEquiv.apply_symm_apply]
|
||||
rw [toLinearMapSelfAdjointMatrix_det]
|
||||
rw [Lorentz.contrContrContractField.same_eq_det_toSelfAdjoint]
|
||||
|
||||
/-- 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 `𝓛`. -/
|
||||
/-- The group homomorphism from `SL(2, ℂ)` to the Lorentz group `𝓛`. -/
|
||||
@[simps!]
|
||||
def toLorentzGroup : SL(2, ℂ) →* LorentzGroup 3 where
|
||||
toFun := toLorentzGroupElem
|
||||
toFun M := ⟨toMatrix M, toMatrix_mem_lorentzGroup M⟩
|
||||
map_one' := by
|
||||
simp only [toLorentzGroupElem, _root_.map_one, LinearMap.toMatrix_one]
|
||||
simp only [_root_.map_one]
|
||||
rfl
|
||||
map_mul' M N := by
|
||||
apply Subtype.eq
|
||||
simp only [toLorentzGroupElem, _root_.map_mul, LinearMap.toMatrix_mul,
|
||||
lorentzGroupIsGroup_mul_coe]
|
||||
ext1
|
||||
simp only [_root_.map_mul, lorentzGroupIsGroup_mul_coe]
|
||||
|
||||
|
||||
lemma toLorentzGroup_eq_σSAL (M : SL(2, ℂ)) :
|
||||
toLorentzGroup M = LinearMap.toMatrix
|
||||
PauliMatrix.σSAL PauliMatrix.σSAL (repSelfAdjointMatrix M) := by
|
||||
PauliMatrix.σSAL PauliMatrix.σSAL (toLinearMapSelfAdjointMatrix 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) =
|
||||
lemma toLinearMapSelfAdjointMatrix_basis (i : Fin 1 ⊕ Fin 3) :
|
||||
toLinearMapSelfAdjointMatrix 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)))]
|
||||
((toLinearMapSelfAdjointMatrix M) (PauliMatrix.σSAL i)))]
|
||||
rfl
|
||||
|
||||
lemma repSelfAdjointMatrix_σSA (i : Fin 1 ⊕ Fin 3) :
|
||||
SL2C.repSelfAdjointMatrix M (PauliMatrix.σSA i) =
|
||||
lemma toLinearMapSelfAdjointMatrix_σSA (i : Fin 1 ⊕ Fin 3) :
|
||||
toLinearMapSelfAdjointMatrix 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 [toLinearMapSelfAdjointMatrix_basis]
|
||||
rw [Finset.smul_sum]
|
||||
apply congrArg
|
||||
funext j
|
||||
|
|
@ -180,18 +164,6 @@ lemma repSelfAdjointMatrix_σSA (i : Fin 1 ⊕ Fin 3) :
|
|||
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
|
||||
|
|
@ -205,13 +177,13 @@ 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
|
||||
informal_lemma toLorentzGroup_inl_inl_nonneg where
|
||||
math :≈ "The time coponent of the image of `SL(2, ℂ)` in the Lorentz group is non-negative."
|
||||
deps :≈ [``toLorentzGroup, ``LorentzGroup.timeComp]
|
||||
deps :≈ [``toLorentzGroup]
|
||||
|
||||
informal_lemma toRestrictedLorentzGroup where
|
||||
math :≈ "The homomorphism from `SL(2, ℂ)` to the restricted Lorentz group."
|
||||
deps :≈ [``toLorentzGroup, ``toLorentzGroup_det_one, ``toLorentzGroup_timeComp_nonneg,
|
||||
deps :≈ [``toLorentzGroup, ``toLorentzGroup_det_one, ``toLorentzGroup_inl_inl_nonneg,
|
||||
``LorentzGroup.Restricted]
|
||||
|
||||
/-! TODO: Define homomorphism from `SL(2, ℂ)` to the restricted Lorentz group. -/
|
||||
|
|
|
|||
|
|
@ -719,10 +719,10 @@ lemma altLeftAltRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2)
|
|||
(hv : IsSelfAdjoint v) (M : SL(2,ℂ)) :
|
||||
TensorProduct.map (altLeftHanded.ρ M) (altRightHanded.ρ M) (altLeftAltRightToMatrix.symm v) =
|
||||
altLeftAltRightToMatrix.symm
|
||||
(SL2C.repSelfAdjointMatrix (M.transpose⁻¹) ⟨v, hv⟩) := by
|
||||
(SL2C.toLinearMapSelfAdjointMatrix (M.transpose⁻¹) ⟨v, hv⟩) := by
|
||||
rw [altLeftAltRightToMatrix_ρ_symm]
|
||||
apply congrArg
|
||||
simp only [SL2C.repSelfAdjointMatrix, MonoidHom.coe_mk, OneHom.coe_mk,
|
||||
simp only [ MonoidHom.coe_mk, OneHom.coe_mk,
|
||||
SL2C.toLinearMapSelfAdjointMatrix_apply_coe, SpecialLinearGroup.coe_inv,
|
||||
SpecialLinearGroup.coe_transpose]
|
||||
congr
|
||||
|
|
@ -738,7 +738,7 @@ lemma leftRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2) ℂ)
|
|||
(hv : IsSelfAdjoint v) (M : SL(2,ℂ)) :
|
||||
TensorProduct.map (leftHanded.ρ M) (rightHanded.ρ M) (leftRightToMatrix.symm v) =
|
||||
leftRightToMatrix.symm
|
||||
(SL2C.repSelfAdjointMatrix M ⟨v, hv⟩) := by
|
||||
(SL2C.toLinearMapSelfAdjointMatrix M ⟨v, hv⟩) := by
|
||||
rw [leftRightToMatrix_ρ_symm]
|
||||
rfl
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue