DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: Move Real Lorentz vect

Browse source
This commit is contained in:
jstoobysmith 2024-11-09 17:37:12 +00:00
parent 58ea861113
commit e3ad445866
9 changed files with 10 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/Lorentz/Algebra/Basic.lean
View file

@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
-/
import HepLean.SpaceTime.MinkowskiMatrix
import Mathlib.Algebra.Lie.Classical
import HepLean.SpaceTime.LorentzVector.Real.Basic
import HepLean.Lorentz.RealVector.Basic
/-!
# The Lorentz Algebra

2
HepLean/Lorentz/Group/Boosts.lean
View file

@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
-/
import HepLean.Lorentz.Group.Proper
import Mathlib.Topology.Constructions
import HepLean.SpaceTime.LorentzVector.Real.NormOne
import HepLean.Lorentz.RealVector.NormOne
/-!
# Boosts

2
HepLean/Lorentz/Group/Orthochronous.lean
View file

@ -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.LorentzVector.Real.NormOne
import HepLean.Lorentz.RealVector.NormOne
import HepLean.Lorentz.Group.Proper
/-!
# The Orthochronous Lorentz Group

150
HepLean/Lorentz/RealVector/Basic.lean Normal file
View file

@ -0,0 +1,150 @@
/-
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.Lorentz.Group.Basic
import HepLean.Meta.Informal
import Mathlib.RepresentationTheory.Rep
import HepLean.Lorentz.RealVector.Modules
/-!
# Real Lorentz vectors
We define real Lorentz vectors in as representations of the Lorentz group.
-/
noncomputable section
open Matrix
open MatrixGroups
open Complex
open TensorProduct
namespace Lorentz
open minkowskiMatrix
/-- The representation of `LorentzGroup d` on real vectors corresponding to contravariant
Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
def Contr (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of ContrMod.rep
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 `ψⁱ`. -/
def Co (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of CoMod.rep
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
-/
/-- The morphism of representations from `Contr d` to `Co d` defined by multiplication
with the metric. -/
def Contr.toCo (d : ℕ) : Contr d ⟶ Co d where
hom := {
toFun := fun ψ => CoMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ),
map_add' := by
intro ψ ψ'
simp only [map_add, mulVec_add]
map_smul' := by
intro r ψ
simp only [_root_.map_smul, mulVec_smul, RingHom.id_apply]}
comm g := by
ext ψ : 2
simp only [ModuleCat.coe_comp, Function.comp_apply]
conv_lhs =>
change CoMod.toFin1dℝEquiv.symm (η *ᵥ (g.1 *ᵥ ψ.toFin1dℝ))
rw [mulVec_mulVec, LorentzGroup.minkowskiMatrix_comm, ← mulVec_mulVec]
rfl
/-- The morphism of representations from `Co d` to `Contr d` defined by multiplication
with the metric. -/
def Co.toContr (d : ℕ) : Co d ⟶ Contr d where
hom := {
toFun := fun ψ => ContrMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ),
map_add' := by
intro ψ ψ'
simp only [map_add, mulVec_add]
map_smul' := by
intro r ψ
simp only [_root_.map_smul, mulVec_smul, RingHom.id_apply]}
comm g := by
ext ψ : 2
simp only [ModuleCat.coe_comp, Function.comp_apply]
conv_lhs =>
change ContrMod.toFin1dℝEquiv.symm (η *ᵥ ((LorentzGroup.transpose g⁻¹).1 *ᵥ ψ.toFin1dℝ))
rw [mulVec_mulVec, ← LorentzGroup.comm_minkowskiMatrix, ← mulVec_mulVec]
rfl
/-- The isomorphism between `Contr d` and `Co d` induced by multiplication with the
Minkowski metric. -/
def contrIsoCo (d : ℕ) : Contr d ≅ Co d where
hom := Contr.toCo d
inv := Co.toContr d
hom_inv_id := by
ext ψ
simp only [Action.comp_hom, ModuleCat.coe_comp, Function.comp_apply, Action.id_hom,
ModuleCat.id_apply]
conv_lhs => change ContrMod.toFin1dℝEquiv.symm (η *ᵥ
CoMod.toFin1dℝEquiv (CoMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ)))
rw [LinearEquiv.apply_symm_apply, mulVec_mulVec, minkowskiMatrix.sq]
simp
inv_hom_id := by
ext ψ
simp only [Action.comp_hom, ModuleCat.coe_comp, Function.comp_apply, Action.id_hom,
ModuleCat.id_apply]
conv_lhs => change CoMod.toFin1dℝEquiv.symm (η *ᵥ
ContrMod.toFin1dℝEquiv (ContrMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ)))
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

454
HepLean/Lorentz/RealVector/Contraction.lean Normal file
View file

@ -0,0 +1,454 @@
/-
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.RealVector.Basic
/-!
# Contraction of Real Lorentz vectors
-/
noncomputable section
open Matrix
open MatrixGroups
open Complex
open TensorProduct
open CategoryTheory.MonoidalCategory
open minkowskiMatrix
namespace Lorentz
variable {d : ℕ}
/-- The bi-linear map corresponding to contraction of a contravariant Lorentz vector with a
covariant Lorentz vector. -/
def contrModCoModBi (d : ℕ) : ContrMod d →ₗ[ℝ] CoMod d →ₗ[ℝ] ℝ where
toFun ψ := {
toFun := fun φ => ψ.toFin1dℝ ⬝ᵥ φ.toFin1dℝ,
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 coModContrModBi (d : ℕ) : CoMod d →ₗ[ℝ] ContrMod d →ₗ[ℝ] ℝ where
toFun φ := {
toFun := fun ψ => φ.toFin1dℝ ⬝ᵥ ψ.toFin1dℝ,
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 Contr d ⊗ Co d 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 contrCoContract : Contr d ⊗ Co d ⟶ 𝟙_ (Rep ℝ (LorentzGroup d)) where
hom := TensorProduct.lift (contrModCoModBi d)
comm M := TensorProduct.ext' fun ψ φ => by
change (M.1 *ᵥ ψ.toFin1dℝ) ⬝ᵥ ((LorentzGroup.transpose M⁻¹).1 *ᵥ φ.toFin1dℝ) = _
rw [dotProduct_mulVec, LorentzGroup.transpose_val,
vecMul_transpose, mulVec_mulVec, LorentzGroup.coe_inv, inv_mul_of_invertible M.1]
simp only [one_mulVec, CategoryTheory.Equivalence.symm_inverse,
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
Action.tensorUnit_ρ', CategoryTheory.Category.comp_id, lift.tmul]
rfl
/-- Notation for `contrCoContract` acting on a tmul. -/
scoped[Lorentz] notation "⟪" ψ "," φ "⟫ₘ" => contrCoContract.hom (ψ ⊗ₜ φ)
lemma contrCoContract_hom_tmul (ψ : Contr d) (φ : Co d) : ⟪ψ, φ⟫ₘ = ψ.toFin1dℝ ⬝ᵥ φ.toFin1dℝ := by
rfl
/-- The linear map from Co d ⊗ Contr d 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 coContrContract : Co d ⊗ Contr d ⟶ 𝟙_ (Rep ℝ (LorentzGroup d)) where
hom := TensorProduct.lift (coModContrModBi d)
comm M := TensorProduct.ext' fun ψ φ => by
change ((LorentzGroup.transpose M⁻¹).1 *ᵥ ψ.toFin1dℝ) ⬝ᵥ (M.1 *ᵥ φ.toFin1dℝ) = _
rw [dotProduct_mulVec, LorentzGroup.transpose_val, mulVec_transpose, vecMul_vecMul,
LorentzGroup.coe_inv, inv_mul_of_invertible M.1]
simp only [vecMul_one, CategoryTheory.Equivalence.symm_inverse,
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
Action.tensorUnit_ρ', CategoryTheory.Category.comp_id, lift.tmul]
rfl
/-- Notation for `coContrContract` acting on a tmul. -/
scoped[Lorentz] notation "⟪" φ "," ψ "⟫ₘ" => coContrContract.hom (φ ⊗ₜ ψ)
lemma coContrContract_hom_tmul (φ : Co d) (ψ : Contr d) : ⟪φ, ψ⟫ₘ = φ.toFin1dℝ ⬝ᵥ ψ.toFin1dℝ := by
rfl
/-!
## Symmetry relations
-/
lemma contrCoContract_tmul_symm (φ : Contr d) (ψ : Co d) : ⟪φ, ψ⟫ₘ = ⟪ψ, φ⟫ₘ := by
rw [contrCoContract_hom_tmul, coContrContract_hom_tmul, dotProduct_comm]
lemma coContrContract_tmul_symm (φ : Co d) (ψ : Contr d) : ⟪φ, ψ⟫ₘ = ⟪ψ, φ⟫ₘ := by
rw [contrCoContract_tmul_symm]
/-!
## Contracting contr vectors with contr vectors etc.
-/
open CategoryTheory.MonoidalCategory
open CategoryTheory
/-- The linear map from Contr d ⊗ Contr d to ℝ induced by the homomorphism
`Contr.toCo` and the contraction `contrCoContract`. -/
def contrContrContract : Contr d ⊗ Contr d ⟶ 𝟙_ (Rep ℝ (LorentzGroup d)) :=
(Contr d ◁ Contr.toCo d) ≫ contrCoContract
/-- 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,
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]
erw [contrCoContract_hom_tmul]
rfl
/-- The linear map from Co d ⊗ Co d to ℝ induced by the homomorphism
`Co.toContr` and the contraction `coContrContract`. -/
def coCoContract : Co d ⊗ Co d ⟶ 𝟙_ (Rep ℝ (LorentzGroup d)) :=
(Co d ◁ Co.toContr d) ≫ coContrContract
/-- Notation for `coCoContract` acting on a tmul. -/
scoped[Lorentz] notation "⟪" ψ "," φ "⟫ₘ" => coCoContract.hom (ψ ⊗ₜ φ)
lemma coCoContract_hom_tmul (φ : Co d) (ψ : Co d) :
⟪φ, ψ⟫ₘ = φ.toFin1dℝ ⬝ᵥ η *ᵥ ψ.toFin1dℝ:= by
simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
contrContrContract, 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]
erw [coContrContract_hom_tmul]
rfl
/-!
## Lemmas related to contraction.
We derive the lemmas in main for `contrContrContractField`.
-/
namespace contrContrContractField
variable (x y : Contr d)
@[simp]
lemma action_tmul (g : LorentzGroup d) : ⟪(Contr d).ρ g x, (Contr d).ρ g y⟫ₘ = ⟪x, y⟫ₘ := by
conv =>
lhs
change (CategoryTheory.CategoryStruct.comp
((CategoryTheory.MonoidalCategory.tensorObj (Contr d) (Contr d)).ρ g)
contrContrContract.hom) (x ⊗ₜ[ℝ] y)
arg 1
apply contrContrContract.comm g
rfl
lemma as_sum : ⟪x, y⟫ₘ = x.val (Sum.inl 0) * y.val (Sum.inl 0) -
∑ i, x.val (Sum.inr i) * y.val (Sum.inr i) := by
rw [contrContrContract_hom_tmul]
simp only [dotProduct, minkowskiMatrix, 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]
rfl
open InnerProductSpace
lemma as_sum_toSpace : ⟪x, y⟫ₘ = x.val (Sum.inl 0) * y.val (Sum.inl 0) -
⟪x.toSpace, y.toSpace⟫_ℝ := by
rw [as_sum]
rfl
@[simp]
lemma stdBasis_inl {d : ℕ} :
⟪@ContrMod.stdBasis d (Sum.inl 0), ContrMod.stdBasis (Sum.inl 0)⟫ₘ = (1 : ℝ) := by
rw [as_sum]
trans (1 : ℝ) - (0 : ℝ)
congr
· rw [ContrMod.stdBasis_apply_same]
simp
· rw [Fintype.sum_eq_zero]
intro a
simp
· ring
lemma symm : ⟪x, y⟫ₘ = ⟪y, x⟫ₘ := by
rw [as_sum, as_sum]
congr 1
rw [mul_comm]
congr
funext i
rw [mul_comm]
lemma dual_mulVec_right : ⟪x, dual Λ *ᵥ y⟫ₘ = ⟪Λ *ᵥ x, y⟫ₘ := by
rw [contrContrContract_hom_tmul, contrContrContract_hom_tmul]
simp only [Action.instMonoidalCategory_tensorUnit_V, ContrMod.mulVec_toFin1dℝ, mulVec_mulVec]
simp only [dual, ← mul_assoc, minkowskiMatrix.sq, one_mul]
rw [← mulVec_mulVec, dotProduct_mulVec, vecMul_transpose]
lemma dual_mulVec_left : ⟪dual Λ *ᵥ x, y⟫ₘ = ⟪x, Λ *ᵥ y⟫ₘ := by
rw [symm, dual_mulVec_right, symm]
lemma right_parity : ⟪x, (Contr d).ρ LorentzGroup.parity y⟫ₘ = ∑ i, x.val i * y.val i := by
rw [as_sum]
simp only [Action.instMonoidalCategory_tensorUnit_V, Fin.isValue, Fintype.sum_sum_type,
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
trans x.val (Sum.inl 0) * (((Contr d).ρ LorentzGroup.parity) y).val (Sum.inl 0) +
∑ i : Fin d, - (x.val (Sum.inr i) * (((Contr d).ρ LorentzGroup.parity) y).val (Sum.inr i))
· simp only [Fin.isValue, Finset.sum_neg_distrib]
rfl
congr 1
· change x.val (Sum.inl 0) * (η *ᵥ y.toFin1dℝ) (Sum.inl 0) = _
simp only [Fin.isValue, mulVec_inl_0, mul_eq_mul_left_iff]
exact mul_eq_mul_left_iff.mp rfl
· congr
funext i
change - (x.val (Sum.inr i) * ((η *ᵥ y.toFin1dℝ) (Sum.inr i))) = _
simp only [mulVec_inr_i, mul_neg, neg_neg, mul_eq_mul_left_iff]
exact mul_eq_mul_left_iff.mp rfl
lemma self_parity_eq_zero_iff : ⟪y, (Contr d).ρ LorentzGroup.parity y⟫ₘ = 0 ↔ y = 0 := by
refine Iff.intro (fun h => ?_) (fun h => ?_)
· rw [right_parity] at h
have hn := Fintype.sum_eq_zero_iff_of_nonneg (f := fun i => y.val i * y.val i) (fun i => by
simpa using mul_self_nonneg (y.val i))
rw [h] at hn
simp at hn
apply ContrMod.ext
funext i
simpa using congrFun hn i
· rw [h]
simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj, map_zero, tmul_zero]
/-- The metric tensor is non-degenerate. -/
lemma nondegenerate : (∀ (x : Contr d), ⟪x, y⟫ₘ = 0) ↔ y = 0 := by
refine Iff.intro (fun h => ?_) (fun h => ?_)
· exact (self_parity_eq_zero_iff _).mp ((symm _ _).trans $ h _)
· simp [h]
lemma matrix_apply_eq_iff_sub : ⟪x, Λ *ᵥ y⟫ₘ = ⟪x, Λ' *ᵥ y⟫ₘ ↔ ⟪x, (Λ - Λ') *ᵥ y⟫ₘ = 0 := by
rw [← sub_eq_zero, ← LinearMap.map_sub, ← tmul_sub, ← ContrMod.sub_mulVec Λ Λ' y]
lemma matrix_eq_iff_eq_forall' : (∀ (v : Contr d), (Λ *ᵥ v) = Λ' *ᵥ v) ↔
∀ (w v : Contr d), ⟪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 [ContrMod.sub_mulVec] at h1
exact h1
lemma matrix_eq_iff_eq_forall : Λ = Λ' ↔ ∀ (w v : Contr d), ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by
rw [← matrix_eq_iff_eq_forall']
refine Iff.intro (fun h => ?_) (fun h => ?_)
· subst h
exact fun v => rfl
· rw [← (LinearMap.toMatrix ContrMod.stdBasis ContrMod.stdBasis).toEquiv.symm.apply_eq_iff_eq]
ext1 v
exact h v
lemma matrix_eq_id_iff : Λ = 1 ↔ ∀ (w v : Contr d), ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, w⟫ₘ := by
rw [matrix_eq_iff_eq_forall]
simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj, ContrMod.one_mulVec]
lemma _root_.LorentzGroup.mem_iff_invariant : Λ ∈ LorentzGroup d ↔
∀ (w v : Contr d), ⟪Λ *ᵥ v, Λ *ᵥ w⟫ₘ = ⟪v, w⟫ₘ := by
refine Iff.intro (fun h => ?_) (fun h => ?_)
· intro x y
rw [← dual_mulVec_right, ContrMod.mulVec_mulVec]
have h1 := LorentzGroup.mem_iff_dual_mul_self.mp h
rw [h1]
simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj, ContrMod.one_mulVec]
· conv at h =>
intro x y
rw [← dual_mulVec_right, ContrMod.mulVec_mulVec]
rw [← matrix_eq_id_iff] at h
exact LorentzGroup.mem_iff_dual_mul_self.mpr h
lemma _root_.LorentzGroup.mem_iff_norm : Λ ∈ LorentzGroup d ↔
∀ (w : Contr d), ⟪Λ *ᵥ w, Λ *ᵥ w⟫ₘ = ⟪w, w⟫ₘ := by
rw [LorentzGroup.mem_iff_invariant]
refine Iff.intro (fun h x => h x x) (fun h x y => ?_)
have hp := h (x + y)
have hn := h (x - y)
rw [ContrMod.mulVec_add, tmul_add, add_tmul, add_tmul, tmul_add, add_tmul, add_tmul] at hp
rw [ContrMod.mulVec_sub, tmul_sub, sub_tmul, sub_tmul, tmul_sub, sub_tmul, sub_tmul] at hn
simp only [map_add, LinearMap.add_apply, map_sub, LinearMap.sub_apply] at hp hn
rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x] at hp hn
let e : 𝟙_ (Rep ℝ ↑(LorentzGroup d)) ≃ₗ[ℝ] ℝ :=
LinearEquiv.refl ℝ (CoeSort.coe (𝟙_ (Rep ℝ ↑(LorentzGroup d))))
apply e.injective
have hp' := e.injective.eq_iff.mpr hp
have hn' := e.injective.eq_iff.mpr hn
simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj, map_add, map_sub] at hp' hn'
linear_combination (norm := ring_nf) (1 / 4) * hp' + (-1/ 4) * hn'
rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x]
simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj, add_sub_cancel, neg_add_cancel, e]
/-!
## Some equalities and inequalities
-/
lemma inl_sq_eq (v : Contr d) : v.val (Sum.inl 0) ^ 2 =
(⟪v, v⟫ₘ) + ∑ i, v.val (Sum.inr i) ^ 2:= by
rw [as_sum]
apply sub_eq_iff_eq_add.mp
congr
· exact pow_two (v.val (Sum.inl 0))
· funext i
exact pow_two (v.val (Sum.inr i))
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
exact fun i => pow_two_nonneg (v.val (Sum.inr i))
lemma ge_abs_inner_product (v w : Contr d) : v.val (Sum.inl 0) * w.val (Sum.inl 0) -
‖⟪v.toSpace, w.toSpace⟫_ℝ‖ ≤ ⟪v, w⟫ₘ := by
rw [as_sum_toSpace, sub_le_sub_iff_left]
exact Real.le_norm_self ⟪v.toSpace, w.toSpace⟫_ℝ
lemma ge_sub_norm (v w : Contr d) : v.val (Sum.inl 0) * w.val (Sum.inl 0) -
‖v.toSpace‖ * ‖w.toSpace‖ ≤ ⟪v, w⟫ₘ := by
apply le_trans _ (ge_abs_inner_product v w)
rw [sub_le_sub_iff_left]
exact norm_inner_le_norm v.toSpace w.toSpace
/-!
# 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

403
HepLean/Lorentz/RealVector/Modules.lean Normal file
View file

@ -0,0 +1,403 @@
/-
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.Lorentz.Group.Basic
import Mathlib.RepresentationTheory.Rep
import Mathlib.Logic.Equiv.TransferInstance
import HepLean.SpaceTime.PauliMatrices.SelfAdjoint
/-!
## Modules associated with Real Lorentz vectors
We define the modules underlying real Lorentz vectors.
These definitions are preludes to the definitions of
`Lorentz.contr` and `Lorentz.co`.
-/
namespace Lorentz
noncomputable section
open Matrix
open MatrixGroups
open Complex
/-- The module for contravariant (up-index) real Lorentz vectors. -/
structure ContrMod (d : ℕ) where
/-- The underlying value as a vector `Fin 1 ⊕ Fin d → ℝ`. -/
val : Fin 1 ⊕ Fin d → ℝ
namespace ContrMod
variable {d : ℕ}
@[ext]
lemma ext {ψ ψ' : ContrMod d} (h : ψ.val = ψ'.val) : ψ = ψ' := by
cases ψ
cases ψ'
subst h
rfl
/-- The equivalence between `ContrℝModule` and `Fin 1 ⊕ Fin d → ℂ`. -/
def toFin1dℝFun : ContrMod d ≃ (Fin 1 ⊕ Fin d → ℝ) 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 d → ℝ`. -/
instance : AddCommMonoid (ContrMod d) := Equiv.addCommMonoid toFin1dℝFun
/-- The instance of `AddCommGroup` on `ContrℝModule` defined via its equivalence
with `Fin 1 ⊕ Fin d → ℝ`. -/
instance : AddCommGroup (ContrMod d) := Equiv.addCommGroup toFin1dℝFun
/-- The instance of `Module` on `ContrℝModule` defined via its equivalence
with `Fin 1 ⊕ Fin d → ℝ`. -/
instance : Module ℝ (ContrMod d) := Equiv.module ℝ toFin1dℝFun
@[simp]
lemma val_add (ψ ψ' : ContrMod d) : (ψ + ψ').val = ψ.val + ψ'.val := rfl
@[simp]
lemma val_smul (r : ℝ) (ψ : ContrMod d) : (r • ψ).val = r • ψ.val := rfl
/-- The linear equivalence between `ContrℝModule` and `(Fin 1 ⊕ Fin d → ℝ)`. -/
def toFin1dℝEquiv : ContrMod d ≃ₗ[ℝ] (Fin 1 ⊕ Fin d → ℝ) :=
Equiv.linearEquiv ℝ toFin1dℝFun
/-- The underlying element of `Fin 1 ⊕ Fin d → ℝ` of a element in `ContrℝModule` defined
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.
-/
/-- The standard basis of `ContrℝModule` indexed by `Fin 1 ⊕ Fin d`. -/
@[simps!]
def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (ContrMod d) := Basis.ofEquivFun toFin1dℝEquiv
@[simp]
lemma stdBasis_toFin1dℝEquiv_apply_same (μ : Fin 1 ⊕ Fin d) :
toFin1dℝEquiv (stdBasis μ) μ = 1 := by
simp only [stdBasis, Basis.ofEquivFun, Basis.coe_ofRepr, LinearEquiv.trans_symm,
LinearEquiv.symm_symm, LinearEquiv.trans_apply, Finsupp.linearEquivFunOnFinite_single]
rw [@LinearEquiv.apply_symm_apply]
exact Pi.single_eq_same μ 1
@[simp]
lemma stdBasis_apply_same (μ : Fin 1 ⊕ Fin d) : (stdBasis μ).val μ = 1 :=
stdBasis_toFin1dℝEquiv_apply_same μ
lemma stdBasis_toFin1dℝEquiv_apply_ne {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) :
toFin1dℝEquiv (stdBasis μ) ν = 0 := by
simp only [stdBasis, Basis.ofEquivFun, Basis.coe_ofRepr, LinearEquiv.trans_symm,
LinearEquiv.symm_symm, LinearEquiv.trans_apply, Finsupp.linearEquivFunOnFinite_single]
rw [@LinearEquiv.apply_symm_apply]
exact Pi.single_eq_of_ne' h 1
@[simp]
lemma stdBasis_inl_apply_inr (i : Fin d) : (stdBasis (Sum.inl 0)).val (Sum.inr i) = 0 := by
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
simp only [map_sum, _root_.map_smul]
funext μ
rw [Fintype.sum_apply μ fun c => toFin1dℝEquiv v c • toFin1dℝEquiv (stdBasis c)]
change _ = ∑ x : Fin 1 ⊕ Fin d, toFin1dℝEquiv v x • (toFin1dℝEquiv (stdBasis x) μ)
rw [Finset.sum_eq_single_of_mem μ (Finset.mem_univ μ)]
· simp only [stdBasis_toFin1dℝEquiv_apply_same, smul_eq_mul, mul_one]
· intro b _ hbμ
rw [stdBasis_toFin1dℝEquiv_apply_ne hbμ]
simp only [smul_eq_mul, mul_zero]
/-!
## mulVec
-/
abbrev mulVec (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) :
ContrMod d := Matrix.toLinAlgEquiv stdBasis M v
scoped[Lorentz] infixr:73 " *ᵥ " => ContrMod.mulVec
@[simp]
lemma mulVec_toFin1dℝ (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) :
(M *ᵥ v).toFin1dℝ = M *ᵥ v.toFin1dℝ := by
rfl
lemma mulVec_sub (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v w : ContrMod d) :
M *ᵥ (v - w) = M *ᵥ v - M *ᵥ w := by
simp only [mulVec, LinearMap.map_sub]
lemma sub_mulVec (M N : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) :
(M - N) *ᵥ v = M *ᵥ v - N *ᵥ v := by
simp only [mulVec, map_sub, LinearMap.sub_apply]
lemma mulVec_add (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v w : ContrMod d) :
M *ᵥ (v + w) = M *ᵥ v + M *ᵥ w := by
simp only [mulVec, LinearMap.map_add]
@[simp]
lemma one_mulVec (v : ContrMod d) : (1 : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) *ᵥ v = v := by
simp only [mulVec, _root_.map_one, LinearMap.one_apply]
lemma mulVec_mulVec (M N : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) :
M *ᵥ (N *ᵥ v) = (M * N) *ᵥ v := by
simp only [mulVec, _root_.map_mul, LinearMap.mul_apply]
/-!
## The norm
(Not the Minkowski norm, but the norm of a vector in `ContrℝModule d`.)
-/
def norm : NormedAddCommGroup (ContrMod d) where
norm v := ‖v.val‖₊
dist_self x := Pi.normedAddCommGroup.dist_self x.val
dist_triangle x y z := Pi.normedAddCommGroup.dist_triangle x.val y.val z.val
dist_comm x y := Pi.normedAddCommGroup.dist_comm x.val y.val
eq_of_dist_eq_zero {x y} := fun h => ext (MetricSpace.eq_of_dist_eq_zero h)
def toSpace (v : ContrMod d) : EuclideanSpace ℝ (Fin d) := v.val ∘ Sum.inr
/-!
## The representation.
-/
/-- The representation of the Lorentz group acting on `ContrℝModule d`. -/
def rep : Representation ℝ (LorentzGroup d) (ContrMod d) where
toFun g := Matrix.toLinAlgEquiv stdBasis g
map_one' := (MulEquivClass.map_eq_one_iff (Matrix.toLinAlgEquiv stdBasis)).mpr rfl
map_mul' x y := by
simp only [lorentzGroupIsGroup_mul_coe, _root_.map_mul]
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. -/
structure CoMod (d : ℕ) where
/-- The underlying value as a vector `Fin 1 ⊕ Fin d → ℝ`. -/
val : Fin 1 ⊕ Fin d → ℝ
namespace CoMod
variable {d : ℕ}
@[ext]
lemma ext {ψ ψ' : CoMod d} (h : ψ.val = ψ'.val) : ψ = ψ' := by
cases ψ
cases ψ'
subst h
rfl
/-- The equivalence between `CoℝModule` and `Fin 1 ⊕ Fin d → ℝ`. -/
def toFin1dℝFun : CoMod d ≃ (Fin 1 ⊕ Fin d → ℝ) 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 d → ℝ`. -/
instance : AddCommMonoid (CoMod d) := Equiv.addCommMonoid toFin1dℝFun
/-- The instance of `AddCommGroup` on `CoℝModule` defined via its equivalence
with `Fin 1 ⊕ Fin d → ℝ`. -/
instance : AddCommGroup (CoMod d) := Equiv.addCommGroup toFin1dℝFun
/-- The instance of `Module` on `CoℝModule` defined via its equivalence
with `Fin 1 ⊕ Fin d → ℝ`. -/
instance : Module ℝ (CoMod d) := Equiv.module ℝ toFin1dℝFun
/-- The linear equivalence between `CoℝModule` and `(Fin 1 ⊕ Fin d → ℝ)`. -/
def toFin1dℝEquiv : CoMod d ≃ₗ[ℝ] (Fin 1 ⊕ Fin d → ℝ) :=
Equiv.linearEquiv ℝ toFin1dℝFun
/-- The underlying element of `Fin 1 ⊕ Fin d → ℝ` of a element in `CoℝModule` defined
through the linear equivalence `toFin1dℝEquiv`. -/
abbrev toFin1dℝ (ψ : CoMod d) := toFin1dℝEquiv ψ
/-!
## The standard basis.
-/
/-- The standard basis of `CoℝModule` indexed by `Fin 1 ⊕ Fin d`. -/
@[simps!]
def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (CoMod d) := Basis.ofEquivFun toFin1dℝEquiv
@[simp]
lemma stdBasis_toFin1dℝEquiv_apply_same (μ : Fin 1 ⊕ Fin d) :
toFin1dℝEquiv (stdBasis μ) μ = 1 := by
simp only [stdBasis, Basis.ofEquivFun, Basis.coe_ofRepr, LinearEquiv.trans_symm,
LinearEquiv.symm_symm, LinearEquiv.trans_apply, Finsupp.linearEquivFunOnFinite_single]
rw [@LinearEquiv.apply_symm_apply]
exact Pi.single_eq_same μ 1
@[simp]
lemma stdBasis_apply_same (μ : Fin 1 ⊕ Fin d) : (stdBasis μ).val μ = 1 :=
stdBasis_toFin1dℝEquiv_apply_same μ
lemma stdBasis_toFin1dℝEquiv_apply_ne {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) :
toFin1dℝEquiv (stdBasis μ) ν = 0 := by
simp only [stdBasis, Basis.ofEquivFun, Basis.coe_ofRepr, LinearEquiv.trans_symm,
LinearEquiv.symm_symm, LinearEquiv.trans_apply, Finsupp.linearEquivFunOnFinite_single]
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
simp only [map_sum, _root_.map_smul]
funext μ
rw [Fintype.sum_apply μ fun c => toFin1dℝEquiv v c • toFin1dℝEquiv (stdBasis c)]
change _ = ∑ x : Fin 1 ⊕ Fin d, toFin1dℝEquiv v x • (toFin1dℝEquiv (stdBasis x) μ)
rw [Finset.sum_eq_single_of_mem μ (Finset.mem_univ μ)]
· simp only [stdBasis_toFin1dℝEquiv_apply_same, smul_eq_mul, mul_one]
· intro b _ hbμ
rw [stdBasis_toFin1dℝEquiv_apply_ne hbμ]
simp only [smul_eq_mul, mul_zero]
/-!
## mulVec
-/
abbrev mulVec (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : CoMod d) :
CoMod d := Matrix.toLinAlgEquiv stdBasis M v
scoped[Lorentz] infixr:73 " *ᵥ " => CoMod.mulVec
@[simp]
lemma mulVec_toFin1dℝ (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : CoMod d) :
(M *ᵥ v).toFin1dℝ = M *ᵥ v.toFin1dℝ := by
rfl
/-!
## The representation
-/
/-- The representation of the Lorentz group acting on `CoℝModule d`. -/
def rep : Representation ℝ (LorentzGroup d) (CoMod d) where
toFun g := Matrix.toLinAlgEquiv stdBasis (LorentzGroup.transpose g⁻¹)
map_one' := by
simp only [inv_one, LorentzGroup.transpose_one, lorentzGroupIsGroup_one_coe, _root_.map_one]
map_mul' x y := by
simp only [_root_.mul_inv_rev, lorentzGroupIsGroup_inv, LorentzGroup.transpose_mul,
lorentzGroupIsGroup_mul_coe, _root_.map_mul]
end CoMod
end
end Lorentz

331
HepLean/Lorentz/RealVector/NormOne.lean Normal file
View file

@ -0,0 +1,331 @@
/-
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.RealVector.Contraction
import Mathlib.GroupTheory.GroupAction.Blocks
/-!
# Lorentz vectors with norm one
-/
open TensorProduct
namespace Lorentz
namespace Contr
variable {d : ℕ}
/-- The set of Lorentz vectors with norm 1. -/
def NormOne (d : ℕ) : Set (Contr d) := fun v => ⟪v, v⟫ₘ = (1 : ℝ)
noncomputable section
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, contrContrContractField.action_tmul]
instance : TopologicalSpace (NormOne d) := instTopologicalSpaceSubtype
variable (v w : NormOne d)
/-- The negative of a `NormOne` as a `NormOne`. -/
def neg : NormOne d := ⟨- v, by
rw [mem_iff]
simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
CategoryTheory.Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj, tmul_neg, neg_tmul, neg_neg]
exact v.2⟩
/-- The first column of a Lorentz matrix as a `NormOneLorentzVector`. -/
@[simps!]
def _root_.LorentzGroup.toNormOne (Λ : LorentzGroup d) : NormOne d :=
⟨(Contr d).ρ Λ (ContrMod.stdBasis (Sum.inl 0)), by
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
simp only [Fin.isValue, LorentzGroup.toNormOne_coe_val, Finsupp.single, one_ne_zero, ↓reduceIte,
Finsupp.coe_mk, Matrix.mulVec_single, mul_one]
lemma _root_.LorentzGroup.toNormOne_inr (Λ : LorentzGroup d) (i : Fin d) :
(LorentzGroup.toNormOne Λ).val.val (Sum.inr i) = Λ.1 (Sum.inr i) (Sum.inl 0) := by
simp only [LorentzGroup.toNormOne_coe_val, Finsupp.single, one_ne_zero, ↓reduceIte, Fin.isValue,
Finsupp.coe_mk, Matrix.mulVec_single, mul_one]
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 [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,
RCLike.inner_apply, conj_trivial]
congr
· rw [LorentzGroup.toNormOne_inl]
rfl
· rw [LorentzGroup.toNormOne_inl]
· funext x
rw [LorentzGroup.toNormOne_inr, LorentzGroup.toNormOne_inr]
rfl
lemma inl_sq : v.val.val (Sum.inl 0) ^ 2 = 1 + ‖ContrMod.toSpace v.val‖ ^ 2 := by
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]
congr
funext x
exact pow_two ((v.val).val (Sum.inr x))
lemma one_le_abs_inl : 1 ≤ |v.val.val (Sum.inl 0)| := by
have h1 := contrContrContractField.le_inl_sq v.val
rw [v.2] at h1
exact (one_le_sq_iff_one_le_abs _).mp h1
lemma inl_le_neg_one_or_one_le_inl : v.val.val (Sum.inl 0) ≤ -1 ∨ 1 ≤ v.val.val (Sum.inl 0) :=
le_abs'.mp (one_le_abs_inl v)
lemma norm_space_le_abs_inl : ‖v.1.toSpace‖ < |v.val.val (Sum.inl 0)| := by
rw [(abs_norm _).symm, ← @sq_lt_sq, inl_sq]
change ‖ContrMod.toSpace v.val‖ ^ 2 < 1 + ‖ContrMod.toSpace v.val‖ ^ 2
exact lt_one_add (‖(v.1).toSpace‖ ^ 2)
lemma norm_space_leq_abs_inl : ‖v.1.toSpace‖ ≤ |v.val.val (Sum.inl 0)| :=
le_of_lt (norm_space_le_abs_inl v)
lemma inl_abs_sub_space_norm :
0 ≤ |v.val.val (Sum.inl 0)| * |w.val.val (Sum.inl 0)| - ‖v.1.toSpace‖ * ‖w.1.toSpace‖ := by
apply sub_nonneg.mpr
apply mul_le_mul (norm_space_leq_abs_inl v) (norm_space_leq_abs_inl w) ?_ ?_
· exact norm_nonneg _
· exact abs_nonneg _
/-!
# Future pointing norm one Lorentz vectors
-/
/-- The future pointing Lorentz vectors with Norm one. -/
def FuturePointing (d : ℕ) : Set (NormOne d) :=
fun x => 0 < x.val.val (Sum.inl 0)
namespace FuturePointing
lemma mem_iff : v ∈ FuturePointing d ↔ 0 < v.val.val (Sum.inl 0) := by
rfl
lemma mem_iff_inl_nonneg : v ∈ FuturePointing d ↔ 0 ≤ v.val.val (Sum.inl 0) := by
refine Iff.intro (fun h => le_of_lt h) (fun h => ?_)
rw [mem_iff]
rcases inl_le_neg_one_or_one_le_inl v with (h | h)
· linarith
· linarith
lemma mem_iff_inl_one_le_inl : v ∈ FuturePointing d ↔ 1 ≤ v.val.val (Sum.inl 0) := by
rw [mem_iff_inl_nonneg]
refine Iff.intro (fun h => ?_) (fun h => ?_)
· rcases inl_le_neg_one_or_one_le_inl v with (h | h)
· linarith
· linarith
· linarith
lemma mem_iff_parity_mem : v ∈ FuturePointing d ↔ ⟨(Contr d).ρ LorentzGroup.parity v.1,
(NormOne.mem_mulAction _ _).mp v.2⟩ ∈ FuturePointing d := by
rw [mem_iff, mem_iff]
change _ ↔ 0 < (minkowskiMatrix.mulVec v.val.val) (Sum.inl 0)
simp only [Fin.isValue, minkowskiMatrix.mulVec_inl_0]
lemma not_mem_iff_inl_le_zero : v ∉ FuturePointing d ↔ v.val.val (Sum.inl 0) ≤ 0 := by
rw [mem_iff]
simp
lemma not_mem_iff_inl_lt_zero : v ∉ FuturePointing d ↔ v.val.val (Sum.inl 0) < 0 := by
rw [mem_iff_inl_nonneg]
simp
lemma not_mem_iff_inl_le_neg_one : v ∉ FuturePointing d ↔ v.val.val (Sum.inl 0) ≤ -1 := by
rw [not_mem_iff_inl_le_zero]
refine Iff.intro (fun h => ?_) (fun h => ?_)
· rcases inl_le_neg_one_or_one_le_inl v with (h | h)
· linarith
· linarith
· linarith
lemma not_mem_iff_neg : v ∉ FuturePointing d ↔ neg v ∈ FuturePointing d := by
rw [not_mem_iff_inl_le_zero, mem_iff_inl_nonneg]
simp only [Fin.isValue, neg]
change (v).val.val (Sum.inl 0) ≤ 0 ↔ 0 ≤ - (v.val).val (Sum.inl 0)
simp
variable (f f' : FuturePointing d)
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 ≤ ⟪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 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 ≤ ⟪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 ≤ ⟪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) :
⟪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) :
⟪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 ?_
simp [neg, neg_tmul, tmul_neg]
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
end Lorentz