Merge pull request #90 from HEPLean/Tensors
feat: Lorentz action on Lorentz tensors
This commit is contained in:
Joseph Tooby-Smith
GitHub
commit
3784cc0413
9 changed files with 1438 additions and 601 deletions
|
|
@ -70,7 +70,10 @@ import HepLean.SpaceTime.LorentzGroup.Orthochronous
|
|||
import HepLean.SpaceTime.LorentzGroup.Proper
|
||||
import HepLean.SpaceTime.LorentzGroup.Restricted
|
||||
import HepLean.SpaceTime.LorentzGroup.Rotations
|
||||
import HepLean.SpaceTime.LorentzTensor.Basic
|
||||
import HepLean.SpaceTime.LorentzTensor.Real.Basic
|
||||
import HepLean.SpaceTime.LorentzTensor.Real.Constructors
|
||||
import HepLean.SpaceTime.LorentzTensor.Real.LorentzAction
|
||||
import HepLean.SpaceTime.LorentzTensor.Real.Multiplication
|
||||
import HepLean.SpaceTime.LorentzVector.AsSelfAdjointMatrix
|
||||
import HepLean.SpaceTime.LorentzVector.Basic
|
||||
import HepLean.SpaceTime.LorentzVector.NormOne
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ open SMνCharges
|
|||
open SMνACCs
|
||||
open BigOperators
|
||||
|
||||
/-- A proposition which is true if for a given `n` a plane of charges of dimension `n` exists
|
||||
/-- A proposition which is true if for a given `n`, a plane of charges of dimension `n` exists
|
||||
in which each point is a solution. -/
|
||||
def ExistsPlane (n : ℕ) : Prop := ∃ (B : Fin n → (PlusU1 3).Charges),
|
||||
LinearIndependent ℚ B ∧ ∀ (f : Fin n → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i)
|
||||
|
|
|
|||
|
|
@ -96,7 +96,7 @@ lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
|
|||
rw [sin_sq, sin_sq]
|
||||
ring
|
||||
|
||||
/-- A CKM Matrix from four reals `θ₁₂`, `θ₁₃`, `θ₂₃`, and `δ₁₃`. This is the standard
|
||||
/-- A CKM Matrix from four reals `θ₁₂`, `θ₁₃`, `θ₂₃`, and `δ₁₃`. This is the standard
|
||||
parameterization of CKM matrices. -/
|
||||
def standParam (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix :=
|
||||
⟨standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, by
|
||||
|
|
|
|||
|
|
@ -1,598 +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.Logic.Function.CompTypeclasses
|
||||
import Mathlib.Data.Real.Basic
|
||||
import Mathlib.Analysis.Normed.Field.Basic
|
||||
import Mathlib.LinearAlgebra.Matrix.Trace
|
||||
/-!
|
||||
|
||||
# Lorentz Tensors
|
||||
|
||||
In this file we define real Lorentz tensors.
|
||||
|
||||
We implicitly follow the definition of a modular operad.
|
||||
This will relation should be made explicit in the future.
|
||||
|
||||
## References
|
||||
|
||||
-- For modular operads see: [Raynor][raynor2021graphical]
|
||||
|
||||
-/
|
||||
/-! TODO: Do complex tensors, with Van der Waerden notation for fermions. -/
|
||||
/-! TODO: Generalize to maps into Lorentz tensors. -/
|
||||
/-!
|
||||
|
||||
## Real Lorentz tensors
|
||||
|
||||
-/
|
||||
|
||||
/-- The possible `colors` of an index for a RealLorentzTensor.
|
||||
There are two possiblities, `up` and `down`. -/
|
||||
inductive RealLorentzTensor.Colors where
|
||||
| up : RealLorentzTensor.Colors
|
||||
| down : RealLorentzTensor.Colors
|
||||
|
||||
/-- The association of colors with indices. For up and down this is `Fin 1 ⊕ Fin d`. -/
|
||||
def RealLorentzTensor.ColorsIndex (d : ℕ) (μ : RealLorentzTensor.Colors) : Type :=
|
||||
match μ with
|
||||
| RealLorentzTensor.Colors.up => Fin 1 ⊕ Fin d
|
||||
| RealLorentzTensor.Colors.down => Fin 1 ⊕ Fin d
|
||||
|
||||
instance (d : ℕ) (μ : RealLorentzTensor.Colors) : Fintype (RealLorentzTensor.ColorsIndex d μ) :=
|
||||
match μ with
|
||||
| RealLorentzTensor.Colors.up => instFintypeSum (Fin 1) (Fin d)
|
||||
| RealLorentzTensor.Colors.down => instFintypeSum (Fin 1) (Fin d)
|
||||
|
||||
/-- An `IndexValue` is a set of actual values an index can take. e.g. for a
|
||||
3-tensor (0, 1, 2). -/
|
||||
@[simp]
|
||||
def RealLorentzTensor.IndexValue {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) :
|
||||
Type 0 := (x : X) → RealLorentzTensor.ColorsIndex d (c x)
|
||||
|
||||
/-- A Lorentz Tensor defined by its coordinate map. -/
|
||||
structure RealLorentzTensor (d : ℕ) (X : Type) where
|
||||
/-- The color associated to each index of the tensor. -/
|
||||
color : X → RealLorentzTensor.Colors
|
||||
/-- The coordinate map for the tensor. -/
|
||||
coord : RealLorentzTensor.IndexValue d color → ℝ
|
||||
|
||||
namespace RealLorentzTensor
|
||||
open Matrix
|
||||
universe u1
|
||||
variable {d : ℕ} {X Y Z : Type}
|
||||
|
||||
/-!
|
||||
|
||||
## Some equivalences of types
|
||||
|
||||
These come in use casting Lorentz tensors.
|
||||
There is likely a better way to deal with these castings.
|
||||
|
||||
-/
|
||||
|
||||
/-- An equivalence from `Empty ⊕ PUnit.{1}` to `Empty ⊕ Σ _ : Fin 1, PUnit`. -/
|
||||
def equivPUnitToSigma :
|
||||
(Empty ⊕ PUnit.{1}) ≃ (Empty ⊕ Σ _ : Fin 1, PUnit) where
|
||||
toFun x := match x with
|
||||
| Sum.inr x => Sum.inr ⟨0, x⟩
|
||||
invFun x := match x with
|
||||
| Sum.inr ⟨0, x⟩ => Sum.inr x
|
||||
left_inv x := match x with
|
||||
| Sum.inr _ => rfl
|
||||
right_inv x := match x with
|
||||
| Sum.inr ⟨0, _⟩ => rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Colors
|
||||
|
||||
-/
|
||||
|
||||
/-- The involution acting on colors. -/
|
||||
def τ : Colors → Colors
|
||||
| Colors.up => Colors.down
|
||||
| Colors.down => Colors.up
|
||||
|
||||
/-- The map τ is an involution. -/
|
||||
@[simp]
|
||||
lemma τ_involutive : Function.Involutive τ := by
|
||||
intro x
|
||||
cases x <;> rfl
|
||||
|
||||
/-- The color associated with an element of `x ∈ X` for a tensor `T`. -/
|
||||
def ch {X : Type} (x : X) (T : RealLorentzTensor d X) : Colors := T.color x
|
||||
|
||||
/-- An equivalence of `ColorsIndex` between that of a color and that of its dual. -/
|
||||
def dualColorsIndex {d : ℕ} {μ : RealLorentzTensor.Colors}:
|
||||
ColorsIndex d μ ≃ ColorsIndex d (τ μ) where
|
||||
toFun x :=
|
||||
match μ with
|
||||
| RealLorentzTensor.Colors.up => x
|
||||
| RealLorentzTensor.Colors.down => x
|
||||
invFun x :=
|
||||
match μ with
|
||||
| RealLorentzTensor.Colors.up => x
|
||||
| RealLorentzTensor.Colors.down => x
|
||||
left_inv x := by cases μ <;> rfl
|
||||
right_inv x := by cases μ <;> rfl
|
||||
|
||||
/-- An equivalence of `ColorsIndex` types given an equality of a colors. -/
|
||||
def castColorsIndex {d : ℕ} {μ₁ μ₂ : RealLorentzTensor.Colors} (h : μ₁ = μ₂) :
|
||||
ColorsIndex d μ₁ ≃ ColorsIndex d μ₂ :=
|
||||
Equiv.cast (by rw [h])
|
||||
|
||||
/-- An equivalence of `ColorsIndex` types given an equality of a color and the dual of a color. -/
|
||||
def congrColorsDual {μ ν : Colors} (h : μ = τ ν) :
|
||||
ColorsIndex d μ ≃ ColorsIndex d ν :=
|
||||
(castColorsIndex h).trans dualColorsIndex.symm
|
||||
|
||||
lemma congrColorsDual_symm {μ ν : Colors} (h : μ = τ ν) :
|
||||
(congrColorsDual h).symm =
|
||||
@congrColorsDual d _ _ ((Function.Involutive.eq_iff τ_involutive).mp h.symm) := by
|
||||
match μ, ν with
|
||||
| Colors.up, Colors.down => rfl
|
||||
| Colors.down, Colors.up => rfl
|
||||
|
||||
lemma color_eq_dual_symm {μ ν : Colors} (h : μ = τ ν) : ν = τ μ :=
|
||||
(Function.Involutive.eq_iff τ_involutive).mp h.symm
|
||||
|
||||
/-!
|
||||
|
||||
## Index values
|
||||
|
||||
-/
|
||||
|
||||
/-- An equivalence of Index values from an equality of color maps. -/
|
||||
def castIndexValue {X : Type} {T S : X → Colors} (h : T = S) :
|
||||
IndexValue d T ≃ IndexValue d S where
|
||||
toFun i := (fun μ => castColorsIndex (congrFun h μ) (i μ))
|
||||
invFun i := (fun μ => (castColorsIndex (congrFun h μ)).symm (i μ))
|
||||
left_inv i := by
|
||||
simp
|
||||
right_inv i := by
|
||||
simp
|
||||
|
||||
lemma indexValue_eq {T₁ T₂ : X → RealLorentzTensor.Colors} (d : ℕ) (h : T₁ = T₂) :
|
||||
IndexValue d T₁ = IndexValue d T₂ :=
|
||||
pi_congr fun a => congrArg (ColorsIndex d) (congrFun h a)
|
||||
|
||||
/-!
|
||||
|
||||
## Extensionality
|
||||
|
||||
-/
|
||||
|
||||
lemma ext {T₁ T₂ : RealLorentzTensor d X} (h : T₁.color = T₂.color)
|
||||
(h' : T₁.coord = T₂.coord ∘ Equiv.cast (indexValue_eq d h)) : T₁ = T₂ := by
|
||||
cases T₁
|
||||
cases T₂
|
||||
simp_all only [IndexValue, mk.injEq]
|
||||
apply And.intro h
|
||||
simp only at h
|
||||
subst h
|
||||
simp only [Equiv.cast_refl, Equiv.coe_refl, CompTriple.comp_eq] at h'
|
||||
subst h'
|
||||
rfl
|
||||
|
||||
lemma ext' {T₁ T₂ : RealLorentzTensor d X} (h : T₁.color = T₂.color)
|
||||
(h' : T₁.coord = fun i => T₂.coord (castIndexValue h i)) :
|
||||
T₁ = T₂ := by
|
||||
cases T₁
|
||||
cases T₂
|
||||
simp_all only [IndexValue, mk.injEq]
|
||||
apply And.intro h
|
||||
simp only at h
|
||||
subst h
|
||||
simp only [Equiv.cast_refl, Equiv.coe_refl, CompTriple.comp_eq] at h'
|
||||
rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Congruence
|
||||
|
||||
-/
|
||||
|
||||
/-- An equivalence between `X → Fin 1 ⊕ Fin d` and `Y → Fin 1 ⊕ Fin d` given an isomorphism
|
||||
between `X` and `Y`. -/
|
||||
def congrSetIndexValue (d : ℕ) (f : X ≃ Y) (i : X → Colors) :
|
||||
IndexValue d i ≃ IndexValue d (i ∘ f.symm) :=
|
||||
Equiv.piCongrLeft' _ f
|
||||
|
||||
/-- Given an equivalence of indexing sets, a map on Lorentz tensors. -/
|
||||
@[simps!]
|
||||
def congrSetMap (f : X ≃ Y) (T : RealLorentzTensor d X) : RealLorentzTensor d Y where
|
||||
color := T.color ∘ f.symm
|
||||
coord := T.coord ∘ (congrSetIndexValue d f T.color).symm
|
||||
|
||||
lemma congrSetMap_trans (f : X ≃ Y) (g : Y ≃ Z) (T : RealLorentzTensor d X) :
|
||||
congrSetMap g (congrSetMap f T) = congrSetMap (f.trans g) T := by
|
||||
apply ext (by rfl)
|
||||
have h1 : congrSetIndexValue d (f.trans g) T.color = (congrSetIndexValue d f T.color).trans
|
||||
(congrSetIndexValue d g $ Equiv.piCongrLeft' (fun _ => Colors) f T.color) := by
|
||||
exact Equiv.coe_inj.mp rfl
|
||||
simp only [congrSetMap, Equiv.piCongrLeft'_apply, IndexValue, Equiv.symm_trans_apply, h1,
|
||||
Equiv.cast_refl, Equiv.coe_refl, CompTriple.comp_eq]
|
||||
rfl
|
||||
|
||||
/-- An equivalence of Tensors given an equivalence of underlying sets. -/
|
||||
@[simps!]
|
||||
def congrSet (f : X ≃ Y) : RealLorentzTensor d X ≃ RealLorentzTensor d Y where
|
||||
toFun := congrSetMap f
|
||||
invFun := congrSetMap f.symm
|
||||
left_inv T := by
|
||||
rw [congrSetMap_trans, Equiv.self_trans_symm]
|
||||
rfl
|
||||
right_inv T := by
|
||||
rw [congrSetMap_trans, Equiv.symm_trans_self]
|
||||
rfl
|
||||
|
||||
lemma congrSet_trans (f : X ≃ Y) (g : Y ≃ Z) :
|
||||
(@congrSet d _ _ f).trans (congrSet g) = congrSet (f.trans g) := by
|
||||
refine Equiv.coe_inj.mp ?_
|
||||
funext T
|
||||
exact congrSetMap_trans f g T
|
||||
|
||||
lemma congrSet_refl : @congrSet d _ _ (Equiv.refl X) = Equiv.refl _ := rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Sums
|
||||
|
||||
-/
|
||||
|
||||
/-- The sum of two color maps. -/
|
||||
def sumElimIndexColor (Tc : X → Colors) (Sc : Y → Colors) :
|
||||
(X ⊕ Y) → Colors :=
|
||||
Sum.elim Tc Sc
|
||||
|
||||
/-- The symmetry property on `sumElimIndexColor`. -/
|
||||
lemma sumElimIndexColor_symm (Tc : X → Colors) (Sc : Y → Colors) : sumElimIndexColor Tc Sc =
|
||||
Equiv.piCongrLeft' _ (Equiv.sumComm X Y).symm (sumElimIndexColor Sc Tc) := by
|
||||
ext1 x
|
||||
simp_all only [Equiv.piCongrLeft'_apply, Equiv.sumComm_symm, Equiv.sumComm_apply]
|
||||
cases x <;> rfl
|
||||
|
||||
/-- The sum of two index values for different color maps. -/
|
||||
@[simp]
|
||||
def sumElimIndexValue {X Y : Type} {TX : X → Colors} {TY : Y → Colors}
|
||||
(i : IndexValue d TX) (j : IndexValue d TY) :
|
||||
IndexValue d (sumElimIndexColor TX TY) :=
|
||||
fun c => match c with
|
||||
| Sum.inl x => i x
|
||||
| Sum.inr x => j x
|
||||
|
||||
/-- The projection of an index value on a sum of color maps to its left component. -/
|
||||
def inlIndexValue {Tc : X → Colors} {Sc : Y → Colors} (i : IndexValue d (sumElimIndexColor Tc Sc)) :
|
||||
IndexValue d Tc := fun x => i (Sum.inl x)
|
||||
|
||||
/-- The projection of an index value on a sum of color maps to its right component. -/
|
||||
def inrIndexValue {Tc : X → Colors} {Sc : Y → Colors}
|
||||
(i : IndexValue d (sumElimIndexColor Tc Sc)) :
|
||||
IndexValue d Sc := fun y => i (Sum.inr y)
|
||||
|
||||
/-- An equivalence between index values formed by commuting sums. -/
|
||||
def sumCommIndexValue {X Y : Type} (Tc : X → Colors) (Sc : Y → Colors) :
|
||||
IndexValue d (sumElimIndexColor Tc Sc) ≃ IndexValue d (sumElimIndexColor Sc Tc) :=
|
||||
(congrSetIndexValue d (Equiv.sumComm X Y) (sumElimIndexColor Tc Sc)).trans
|
||||
(castIndexValue (sumElimIndexColor_symm Sc Tc).symm)
|
||||
|
||||
lemma sumCommIndexValue_inlIndexValue {X Y : Type} {Tc : X → Colors} {Sc : Y → Colors}
|
||||
(i : IndexValue d <| sumElimIndexColor Tc Sc) :
|
||||
inlIndexValue (sumCommIndexValue Tc Sc i) = inrIndexValue i := rfl
|
||||
|
||||
lemma sumCommIndexValue_inrIndexValue {X Y : Type} {Tc : X → Colors} {Sc : Y → Colors}
|
||||
(i : IndexValue d <| sumElimIndexColor Tc Sc) :
|
||||
inrIndexValue (sumCommIndexValue Tc Sc i) = inlIndexValue i := rfl
|
||||
|
||||
/-- Equivalence between sets of `RealLorentzTensor` formed by commuting sums. -/
|
||||
@[simps!]
|
||||
def sumComm : RealLorentzTensor d (X ⊕ Y) ≃ RealLorentzTensor d (Y ⊕ X) :=
|
||||
congrSet (Equiv.sumComm X Y)
|
||||
|
||||
/-!
|
||||
|
||||
## Marked Lorentz tensors
|
||||
|
||||
To define contraction and multiplication of Lorentz tensors we need to mark indices.
|
||||
|
||||
-/
|
||||
|
||||
/-- A `RealLorentzTensor` with `n` marked indices. -/
|
||||
def Marked (d : ℕ) (X : Type) (n : ℕ) : Type :=
|
||||
RealLorentzTensor d (X ⊕ Σ _ : Fin n, PUnit)
|
||||
|
||||
namespace Marked
|
||||
|
||||
variable {n m : ℕ}
|
||||
|
||||
/-- The marked point. -/
|
||||
def markedPoint (X : Type) (i : Fin n) : (X ⊕ Σ _ : Fin n, PUnit) :=
|
||||
Sum.inr ⟨i, PUnit.unit⟩
|
||||
|
||||
/-- The colors of unmarked indices. -/
|
||||
def unmarkedColor (T : Marked d X n) : X → Colors :=
|
||||
T.color ∘ Sum.inl
|
||||
|
||||
/-- The colors of marked indices. -/
|
||||
def markedColor (T : Marked d X n) : (Σ _ : Fin n, PUnit) → Colors :=
|
||||
T.color ∘ Sum.inr
|
||||
|
||||
/-- The index values restricted to unmarked indices. -/
|
||||
def UnmarkedIndexValue (T : Marked d X n) : Type :=
|
||||
IndexValue d T.unmarkedColor
|
||||
|
||||
/-- The index values restricted to marked indices. -/
|
||||
def MarkedIndexValue (T : Marked d X n) : Type :=
|
||||
IndexValue d T.markedColor
|
||||
|
||||
lemma sumElimIndexColor_of_marked (T : Marked d X n) :
|
||||
sumElimIndexColor T.unmarkedColor T.markedColor = T.color := by
|
||||
ext1 x
|
||||
cases' x <;> rfl
|
||||
|
||||
/-- Contruction of marked index values for the case of 1 marked index. -/
|
||||
def oneMarkedIndexValue (T : Marked d X 1) (x : ColorsIndex d (T.color (markedPoint X 0))) :
|
||||
T.MarkedIndexValue := fun i => match i with
|
||||
| ⟨0, PUnit.unit⟩ => x
|
||||
|
||||
/-- Contruction of marked index values for the case of 2 marked index. -/
|
||||
def twoMarkedIndexValue (T : Marked d X 2) (x : ColorsIndex d (T.color (markedPoint X 0)))
|
||||
(y : ColorsIndex d <| T.color <| markedPoint X 1) :
|
||||
T.MarkedIndexValue := fun i =>
|
||||
match i with
|
||||
| ⟨0, PUnit.unit⟩ => x
|
||||
| ⟨1, PUnit.unit⟩ => y
|
||||
|
||||
/-- An equivalence of types used to turn the first marked index into an unmarked index. -/
|
||||
def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Σ _ : Fin n.succ, PUnit) ≃
|
||||
((X ⊕ PUnit) ⊕ Σ _ : Fin n, PUnit) where
|
||||
toFun x := match x with
|
||||
| Sum.inl x => Sum.inl (Sum.inl x)
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => Sum.inl (Sum.inr PUnit.unit)
|
||||
| Sum.inr ⟨⟨Nat.succ i, h⟩, PUnit.unit⟩ => Sum.inr ⟨⟨i, Nat.succ_lt_succ_iff.mp h⟩, PUnit.unit⟩
|
||||
invFun x := match x with
|
||||
| Sum.inl (Sum.inl x) => Sum.inl x
|
||||
| Sum.inl (Sum.inr PUnit.unit) => Sum.inr ⟨0, PUnit.unit⟩
|
||||
| Sum.inr ⟨⟨i, h⟩, PUnit.unit⟩ => Sum.inr ⟨⟨Nat.succ i, Nat.succ_lt_succ h⟩, PUnit.unit⟩
|
||||
left_inv x := by match x with
|
||||
| Sum.inl x => rfl
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => rfl
|
||||
| Sum.inr ⟨⟨Nat.succ i, h⟩, PUnit.unit⟩ => rfl
|
||||
right_inv x := by match x with
|
||||
| Sum.inl (Sum.inl x) => rfl
|
||||
| Sum.inl (Sum.inr PUnit.unit) => rfl
|
||||
| Sum.inr ⟨⟨i, h⟩, PUnit.unit⟩ => rfl
|
||||
|
||||
/-- Unmark the first marked index of a marked thensor. -/
|
||||
def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ PUnit) n :=
|
||||
congrSet (unmarkFirstSet X n)
|
||||
|
||||
end Marked
|
||||
|
||||
/-!
|
||||
|
||||
## Multiplication
|
||||
|
||||
-/
|
||||
open Marked
|
||||
|
||||
/-- The contraction of the marked indices of two tensors each with one marked index, which
|
||||
is dual to the others. The contraction is done via
|
||||
`φ^μ ψ_μ = φ^0 ψ_0 + φ^1 ψ_1 + ...`. -/
|
||||
@[simps!]
|
||||
def mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
|
||||
(h : T.markedColor ⟨0, PUnit.unit⟩ = τ (S.markedColor ⟨0, PUnit.unit⟩)) :
|
||||
RealLorentzTensor d (X ⊕ Y) where
|
||||
color := sumElimIndexColor T.unmarkedColor S.unmarkedColor
|
||||
coord := fun i => ∑ x,
|
||||
T.coord (castIndexValue T.sumElimIndexColor_of_marked $
|
||||
sumElimIndexValue (inlIndexValue i) (T.oneMarkedIndexValue x)) *
|
||||
S.coord (castIndexValue S.sumElimIndexColor_of_marked $
|
||||
sumElimIndexValue (inrIndexValue i) (S.oneMarkedIndexValue $ congrColorsDual h x))
|
||||
|
||||
/-- Multiplication is well behaved with regard to swapping tensors. -/
|
||||
lemma sumComm_mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
|
||||
(h : T.markedColor ⟨0, PUnit.unit⟩ = τ (S.markedColor ⟨0, PUnit.unit⟩)) :
|
||||
sumComm (mul T S h) = mul S T (color_eq_dual_symm h) := by
|
||||
refine ext' (sumElimIndexColor_symm S.unmarkedColor T.unmarkedColor).symm ?_
|
||||
change (mul T S h).coord ∘
|
||||
(congrSetIndexValue d (Equiv.sumComm X Y) (mul T S h).color).symm = _
|
||||
rw [Equiv.comp_symm_eq]
|
||||
funext i
|
||||
simp only [mul_coord, IndexValue, mul_color, Function.comp_apply, sumComm_apply_color]
|
||||
erw [sumCommIndexValue_inlIndexValue, sumCommIndexValue_inrIndexValue,
|
||||
← Equiv.sum_comp (congrColorsDual h)]
|
||||
refine Fintype.sum_congr _ _ (fun a => ?_)
|
||||
rw [mul_comm]
|
||||
repeat apply congrArg
|
||||
rw [← congrColorsDual_symm h]
|
||||
exact (Equiv.apply_eq_iff_eq_symm_apply <| congrColorsDual h).mp rfl
|
||||
|
||||
/-! TODO: Following the ethos of modular operads, prove properties of multiplication. -/
|
||||
|
||||
/-! TODO: Use `mul` to generalize to any pair of marked index. -/
|
||||
/-!
|
||||
|
||||
## Contraction of indices
|
||||
|
||||
-/
|
||||
|
||||
/-- The contraction of the marked indices in a tensor with two marked indices. -/
|
||||
def contr {X : Type} (T : Marked d X 2)
|
||||
(h : T.markedColor ⟨0, PUnit.unit⟩ = τ (T.markedColor ⟨1, PUnit.unit⟩)) :
|
||||
RealLorentzTensor d X where
|
||||
color := T.unmarkedColor
|
||||
coord := fun i =>
|
||||
∑ x, T.coord (castIndexValue T.sumElimIndexColor_of_marked $
|
||||
sumElimIndexValue i $ T.twoMarkedIndexValue x $ congrColorsDual h x)
|
||||
|
||||
/-! TODO: Following the ethos of modular operads, prove properties of contraction. -/
|
||||
|
||||
/-! TODO: Use `contr` to generalize to any pair of marked index. -/
|
||||
|
||||
/-!
|
||||
|
||||
# Tensors from reals, vectors and matrices
|
||||
|
||||
Note that that these definitions are not equivariant with respect to an
|
||||
action of the Lorentz group. They are provided for constructive purposes.
|
||||
|
||||
-/
|
||||
|
||||
/-- A 0-tensor from a real number. -/
|
||||
def ofReal (d : ℕ) (r : ℝ) : RealLorentzTensor d Empty where
|
||||
color := fun _ => Colors.up
|
||||
coord := fun _ => r
|
||||
|
||||
/-- A marked 1-tensor with a single up index constructed from a vector.
|
||||
|
||||
Note: This is not the same as rising indices on `ofVecDown`. -/
|
||||
def ofVecUp {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
Marked d Empty 1 where
|
||||
color := fun _ => Colors.up
|
||||
coord := fun i => v <| i <| Sum.inr <| ⟨0, PUnit.unit⟩
|
||||
|
||||
/-- A marked 1-tensor with a single down index constructed from a vector.
|
||||
|
||||
Note: This is not the same as lowering indices on `ofVecUp`. -/
|
||||
def ofVecDown {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
Marked d Empty 1 where
|
||||
color := fun _ => Colors.down
|
||||
coord := fun i => v <| i <| Sum.inr <| ⟨0, PUnit.unit⟩
|
||||
|
||||
/-- A tensor with two up indices constructed from a matrix.
|
||||
|
||||
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
|
||||
def ofMatUpUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Marked d Empty 2 where
|
||||
color := fun _ => Colors.up
|
||||
coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
|
||||
|
||||
/-- A tensor with two down indices constructed from a matrix.
|
||||
|
||||
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
|
||||
def ofMatDownDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Marked d Empty 2 where
|
||||
color := fun _ => Colors.down
|
||||
coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
|
||||
|
||||
/-- A marked 2-tensor with the first index up and the second index down.
|
||||
|
||||
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
|
||||
@[simps!]
|
||||
def ofMatUpDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Marked d Empty 2 where
|
||||
color := fun i => match i with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => Colors.up
|
||||
| Sum.inr ⟨1, PUnit.unit⟩ => Colors.down
|
||||
coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
|
||||
|
||||
/-- A marked 2-tensor with the first index down and the second index up.
|
||||
|
||||
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
|
||||
def ofMatDownUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Marked d Empty 2 where
|
||||
color := fun i => match i with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => Colors.down
|
||||
| Sum.inr ⟨1, PUnit.unit⟩ => Colors.up
|
||||
coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
|
||||
|
||||
/-- Contracting the indices of `ofMatUpDown` returns the trace of the matrix. -/
|
||||
lemma contr_ofMatUpDown_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
contr (ofMatUpDown M) (by rfl) = ofReal d M.trace := by
|
||||
refine ext' ?_ ?_
|
||||
· funext i
|
||||
exact Empty.elim i
|
||||
· funext i
|
||||
simp only [Fin.isValue, contr, IndexValue, Equiv.cast_apply, trace, diag_apply, ofReal,
|
||||
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
|
||||
apply Finset.sum_congr rfl
|
||||
intro x _
|
||||
rfl
|
||||
|
||||
/-- Contracting the indices of `ofMatDownUp` returns the trace of the matrix. -/
|
||||
lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
contr (ofMatDownUp M) (by rfl) = ofReal d M.trace := by
|
||||
refine ext' ?_ ?_
|
||||
· funext i
|
||||
exact Empty.elim i
|
||||
· funext i
|
||||
rfl
|
||||
|
||||
/-- Multiplying `ofVecUp` with `ofVecDown` gives the dot product. -/
|
||||
@[simp]
|
||||
lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
|
||||
congrSet (@Equiv.equivEmpty (Empty ⊕ Empty) instIsEmptySum)
|
||||
(mul (ofVecUp v₁) (ofVecDown v₂) (by rfl)) = ofReal d (v₁ ⬝ᵥ v₂) := by
|
||||
refine ext' ?_ ?_
|
||||
· funext i
|
||||
exact Empty.elim i
|
||||
· funext i
|
||||
rfl
|
||||
|
||||
/-- Multiplying `ofVecDown` with `ofVecUp` gives the dot product. -/
|
||||
@[simp]
|
||||
lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
|
||||
congrSet (Equiv.equivEmpty (Empty ⊕ Empty))
|
||||
(mul (ofVecDown v₁) (ofVecUp v₂) rfl) = ofReal d (v₁ ⬝ᵥ v₂) := by
|
||||
refine ext' ?_ ?_
|
||||
· funext i
|
||||
exact Empty.elim i
|
||||
· funext i
|
||||
rfl
|
||||
|
||||
lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
|
||||
(v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
congrSet ((Equiv.sumEmpty (Empty ⊕ PUnit.{1}) Empty).trans equivPUnitToSigma)
|
||||
(mul (unmarkFirst $ ofMatUpDown M) (ofVecUp v) rfl) = ofVecUp (M *ᵥ v) := by
|
||||
refine ext' ?_ ?_
|
||||
· funext i
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, congrSet_apply_color, mul_color, Equiv.symm_symm]
|
||||
fin_cases i
|
||||
rfl
|
||||
· funext i
|
||||
rfl
|
||||
|
||||
lemma mul_ofMatDownUp_ofVecDown_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
|
||||
(v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
congrSet ((Equiv.sumEmpty (Empty ⊕ PUnit.{1}) Empty).trans equivPUnitToSigma)
|
||||
(mul (unmarkFirst $ ofMatDownUp M) (ofVecDown v) rfl) = ofVecDown (M *ᵥ v) := by
|
||||
refine ext' ?_ ?_
|
||||
· funext i
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, congrSet_apply_color, mul_color, Equiv.symm_symm]
|
||||
fin_cases i
|
||||
rfl
|
||||
· funext i
|
||||
rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Rising and lowering indices
|
||||
|
||||
Rising or lowering an index corresponds to changing the color of that index.
|
||||
|
||||
-/
|
||||
|
||||
/-! TODO: Define the rising and lowering of indices using contraction with the metric. -/
|
||||
|
||||
/-!
|
||||
|
||||
## Action of the Lorentz group
|
||||
|
||||
-/
|
||||
|
||||
/-! TODO: Define the action of the Lorentz group on the sets of Tensors. -/
|
||||
|
||||
/-!
|
||||
|
||||
## Graphical species and Lorentz tensors
|
||||
|
||||
-/
|
||||
|
||||
/-! TODO: From Lorentz tensors graphical species. -/
|
||||
/-! TODO: Show that the action of the Lorentz group defines an action on the graphical species. -/
|
||||
|
||||
end RealLorentzTensor
|
||||
427
HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
Normal file
427
HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
Normal file
|
|
@ -0,0 +1,427 @@
|
|||
/-
|
||||
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.Logic.Function.CompTypeclasses
|
||||
import Mathlib.Data.Real.Basic
|
||||
import Mathlib.Data.Fintype.BigOperators
|
||||
import Mathlib.Logic.Equiv.Fin
|
||||
import Mathlib.Tactic.FinCases
|
||||
/-!
|
||||
|
||||
# Real Lorentz Tensors
|
||||
|
||||
In this file we define real Lorentz tensors.
|
||||
|
||||
We implicitly follow the definition of a modular operad.
|
||||
This will relation should be made explicit in the future.
|
||||
|
||||
## References
|
||||
|
||||
-- For modular operads see: [Raynor][raynor2021graphical]
|
||||
|
||||
-/
|
||||
/-! TODO: Do complex tensors, with Van der Waerden notation for fermions. -/
|
||||
/-! TODO: Generalize to maps into Lorentz tensors. -/
|
||||
|
||||
/-- The possible `colors` of an index for a RealLorentzTensor.
|
||||
There are two possiblities, `up` and `down`. -/
|
||||
inductive RealLorentzTensor.Colors where
|
||||
| up : RealLorentzTensor.Colors
|
||||
| down : RealLorentzTensor.Colors
|
||||
|
||||
/-- The association of colors with indices. For up and down this is `Fin 1 ⊕ Fin d`. -/
|
||||
def RealLorentzTensor.ColorsIndex (d : ℕ) (μ : RealLorentzTensor.Colors) : Type :=
|
||||
match μ with
|
||||
| RealLorentzTensor.Colors.up => Fin 1 ⊕ Fin d
|
||||
| RealLorentzTensor.Colors.down => Fin 1 ⊕ Fin d
|
||||
|
||||
instance (d : ℕ) (μ : RealLorentzTensor.Colors) : Fintype (RealLorentzTensor.ColorsIndex d μ) :=
|
||||
match μ with
|
||||
| RealLorentzTensor.Colors.up => instFintypeSum (Fin 1) (Fin d)
|
||||
| RealLorentzTensor.Colors.down => instFintypeSum (Fin 1) (Fin d)
|
||||
|
||||
instance (d : ℕ) (μ : RealLorentzTensor.Colors) : DecidableEq (RealLorentzTensor.ColorsIndex d μ) :=
|
||||
match μ with
|
||||
| RealLorentzTensor.Colors.up => instDecidableEqSum
|
||||
| RealLorentzTensor.Colors.down => instDecidableEqSum
|
||||
|
||||
/-- An `IndexValue` is a set of actual values an index can take. e.g. for a
|
||||
3-tensor (0, 1, 2). -/
|
||||
def RealLorentzTensor.IndexValue {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) :
|
||||
Type 0 := (x : X) → RealLorentzTensor.ColorsIndex d (c x)
|
||||
|
||||
/-- A Lorentz Tensor defined by its coordinate map. -/
|
||||
structure RealLorentzTensor (d : ℕ) (X : Type) where
|
||||
/-- The color associated to each index of the tensor. -/
|
||||
color : X → RealLorentzTensor.Colors
|
||||
/-- The coordinate map for the tensor. -/
|
||||
coord : RealLorentzTensor.IndexValue d color → ℝ
|
||||
|
||||
namespace RealLorentzTensor
|
||||
open Matrix
|
||||
universe u1
|
||||
variable {d : ℕ} {X Y Z : Type} (c : X → Colors)
|
||||
|
||||
/-!
|
||||
|
||||
## Colors
|
||||
|
||||
-/
|
||||
|
||||
/-- The involution acting on colors. -/
|
||||
def τ : Colors → Colors
|
||||
| Colors.up => Colors.down
|
||||
| Colors.down => Colors.up
|
||||
|
||||
/-- The map τ is an involution. -/
|
||||
@[simp]
|
||||
lemma τ_involutive : Function.Involutive τ := by
|
||||
intro x
|
||||
cases x <;> rfl
|
||||
|
||||
lemma color_eq_dual_symm {μ ν : Colors} (h : μ = τ ν) : ν = τ μ :=
|
||||
(Function.Involutive.eq_iff τ_involutive).mp h.symm
|
||||
|
||||
/-- The color associated with an element of `x ∈ X` for a tensor `T`. -/
|
||||
def ch {X : Type} (x : X) (T : RealLorentzTensor d X) : Colors := T.color x
|
||||
|
||||
/-- An equivalence of `ColorsIndex` types given an equality of a colors. -/
|
||||
def colorsIndexCast {d : ℕ} {μ₁ μ₂ : RealLorentzTensor.Colors} (h : μ₁ = μ₂) :
|
||||
ColorsIndex d μ₁ ≃ ColorsIndex d μ₂ :=
|
||||
Equiv.cast (congrArg (ColorsIndex d) h)
|
||||
|
||||
/-- An equivalence of `ColorsIndex` between that of a color and that of its dual. -/
|
||||
def colorsIndexDualCastSelf {d : ℕ} {μ : RealLorentzTensor.Colors}:
|
||||
ColorsIndex d μ ≃ ColorsIndex d (τ μ) where
|
||||
toFun x :=
|
||||
match μ with
|
||||
| RealLorentzTensor.Colors.up => x
|
||||
| RealLorentzTensor.Colors.down => x
|
||||
invFun x :=
|
||||
match μ with
|
||||
| RealLorentzTensor.Colors.up => x
|
||||
| RealLorentzTensor.Colors.down => x
|
||||
left_inv x := by cases μ <;> rfl
|
||||
right_inv x := by cases μ <;> rfl
|
||||
|
||||
/-- An equivalence of `ColorsIndex` types given an equality of a color and the dual of a color. -/
|
||||
def colorsIndexDualCast {μ ν : Colors} (h : μ = τ ν) :
|
||||
ColorsIndex d μ ≃ ColorsIndex d ν :=
|
||||
(colorsIndexCast h).trans colorsIndexDualCastSelf.symm
|
||||
|
||||
lemma colorsIndexDualCast_symm {μ ν : Colors} (h : μ = τ ν) :
|
||||
(colorsIndexDualCast h).symm =
|
||||
@colorsIndexDualCast d _ _ ((Function.Involutive.eq_iff τ_involutive).mp h.symm) := by
|
||||
match μ, ν with
|
||||
| Colors.up, Colors.down => rfl
|
||||
| Colors.down, Colors.up => rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Index values
|
||||
|
||||
-/
|
||||
|
||||
instance [Fintype X] [DecidableEq X] : Fintype (IndexValue d c) := Pi.fintype
|
||||
|
||||
instance [Fintype X] : DecidableEq (IndexValue d c) :=
|
||||
Fintype.decidablePiFintype
|
||||
|
||||
/-!
|
||||
|
||||
## Induced isomorphisms between IndexValue sets
|
||||
|
||||
-/
|
||||
|
||||
/-- An isomorphism of the type of index values given an isomorphism of sets. -/
|
||||
@[simps!]
|
||||
def indexValueIso (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors} (h : i = j ∘ f) :
|
||||
IndexValue d i ≃ IndexValue d j :=
|
||||
(Equiv.piCongrRight (fun μ => colorsIndexCast (congrFun h μ))).trans $
|
||||
Equiv.piCongrLeft (fun y => RealLorentzTensor.ColorsIndex d (j y)) f
|
||||
|
||||
lemma indexValueIso_symm_apply' (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors}
|
||||
(h : i = j ∘ f) (y : IndexValue d j) (x : X) :
|
||||
(indexValueIso d f h).symm y x = (colorsIndexCast (congrFun h x)).symm (y (f x)) := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma indexValueIso_trans (d : ℕ) (f : X ≃ Y) (g : Y ≃ Z) {i : X → Colors}
|
||||
{j : Y → Colors} {k : Z → Colors} (h : i = j ∘ f) (h' : j = k ∘ g) :
|
||||
(indexValueIso d f h).trans (indexValueIso d g h') =
|
||||
indexValueIso d (f.trans g) (by rw [h, h', Function.comp.assoc]; rfl) := by
|
||||
have h1 : ((indexValueIso d f h).trans (indexValueIso d g h')).symm =
|
||||
(indexValueIso d (f.trans g) (by rw [h, h', Function.comp.assoc]; rfl)).symm := by
|
||||
subst h' h
|
||||
exact Equiv.coe_inj.mp rfl
|
||||
simpa only [Equiv.symm_symm] using congrArg (fun e => e.symm) h1
|
||||
|
||||
lemma indexValueIso_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
|
||||
(indexValueIso d f h).symm =
|
||||
indexValueIso d f.symm ((Equiv.eq_comp_symm f j i).mpr (id (Eq.symm h))) := by
|
||||
ext i : 1
|
||||
rw [← Equiv.symm_apply_eq]
|
||||
funext y
|
||||
rw [indexValueIso_symm_apply', indexValueIso_symm_apply']
|
||||
simp [colorsIndexCast]
|
||||
apply cast_eq_iff_heq.mpr
|
||||
rw [Equiv.apply_symm_apply]
|
||||
|
||||
lemma indexValueIso_eq_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
|
||||
indexValueIso d f h =
|
||||
(indexValueIso d f.symm ((Equiv.eq_comp_symm f j i).mpr (id (Eq.symm h)))).symm := by
|
||||
rw [indexValueIso_symm]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma indexValueIso_refl (d : ℕ) (i : X → Colors) :
|
||||
indexValueIso d (Equiv.refl X) (rfl : i = i) = Equiv.refl _ := by
|
||||
rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Extensionality
|
||||
|
||||
-/
|
||||
|
||||
lemma ext {T₁ T₂ : RealLorentzTensor d X} (h : T₁.color = T₂.color)
|
||||
(h' : T₁.coord = fun i => T₂.coord (indexValueIso d (Equiv.refl X) h i)) :
|
||||
T₁ = T₂ := by
|
||||
cases T₁
|
||||
cases T₂
|
||||
simp_all only [IndexValue, mk.injEq]
|
||||
apply And.intro h
|
||||
simp only at h
|
||||
subst h
|
||||
simp only [Equiv.cast_refl, Equiv.coe_refl, CompTriple.comp_eq] at h'
|
||||
rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Mapping isomorphisms.
|
||||
|
||||
-/
|
||||
|
||||
/-- An equivalence of Tensors given an equivalence of underlying sets. -/
|
||||
@[simps!]
|
||||
def mapIso (d : ℕ) (f : X ≃ Y) : RealLorentzTensor d X ≃ RealLorentzTensor d Y where
|
||||
toFun T := {
|
||||
color := T.color ∘ f.symm,
|
||||
coord := T.coord ∘ (indexValueIso d f (by simp : T.color = T.color ∘ f.symm ∘ f)).symm}
|
||||
invFun T := {
|
||||
color := T.color ∘ f,
|
||||
coord := T.coord ∘ (indexValueIso d f.symm (by simp : T.color = T.color ∘ f ∘ f.symm)).symm}
|
||||
left_inv T := by
|
||||
refine ext ?_ ?_
|
||||
· simp [Function.comp.assoc]
|
||||
· funext i
|
||||
simp only [IndexValue, Function.comp_apply, Function.comp_id]
|
||||
apply congrArg
|
||||
funext x
|
||||
erw [indexValueIso_symm_apply', indexValueIso_symm_apply', indexValueIso_eq_symm,
|
||||
indexValueIso_symm_apply']
|
||||
rw [← Equiv.apply_eq_iff_eq_symm_apply]
|
||||
simp only [Equiv.refl_symm, Equiv.coe_refl, Function.comp_apply, id_eq, colorsIndexCast,
|
||||
Equiv.cast_symm, Equiv.cast_apply, cast_cast, Equiv.refl_apply]
|
||||
apply cast_eq_iff_heq.mpr
|
||||
congr
|
||||
exact Equiv.symm_apply_apply f x
|
||||
right_inv T := by
|
||||
refine ext ?_ ?_
|
||||
· simp [Function.comp.assoc]
|
||||
· funext i
|
||||
simp only [IndexValue, Function.comp_apply, Function.comp_id]
|
||||
apply congrArg
|
||||
funext x
|
||||
erw [indexValueIso_symm_apply', indexValueIso_symm_apply', indexValueIso_eq_symm,
|
||||
indexValueIso_symm_apply']
|
||||
rw [← Equiv.apply_eq_iff_eq_symm_apply]
|
||||
simp only [Equiv.refl_symm, Equiv.coe_refl, Function.comp_apply, id_eq, colorsIndexCast,
|
||||
Equiv.cast_symm, Equiv.cast_apply, cast_cast, Equiv.refl_apply]
|
||||
apply cast_eq_iff_heq.mpr
|
||||
congr
|
||||
exact Equiv.apply_symm_apply f x
|
||||
|
||||
@[simp]
|
||||
lemma mapIso_trans (f : X ≃ Y) (g : Y ≃ Z) :
|
||||
(mapIso d f).trans (mapIso d g) = mapIso d (f.trans g) := by
|
||||
refine Equiv.coe_inj.mp ?_
|
||||
funext T
|
||||
refine ext rfl ?_
|
||||
simp only [Equiv.trans_apply, IndexValue, mapIso_apply_color, Equiv.symm_trans_apply,
|
||||
indexValueIso_refl, Equiv.refl_apply, mapIso_apply_coord]
|
||||
funext i
|
||||
rw [mapIso_apply_coord, mapIso_apply_coord]
|
||||
apply congrArg
|
||||
rw [← indexValueIso_trans]
|
||||
rfl
|
||||
exact (Equiv.comp_symm_eq f (T.color ∘ ⇑f.symm) T.color).mp rfl
|
||||
|
||||
lemma mapIso_symm (f : X ≃ Y) : (mapIso d f).symm = mapIso d f.symm := rfl
|
||||
|
||||
lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Sums
|
||||
|
||||
-/
|
||||
/-- An equivalence splitting elements of `IndexValue d (Sum.elim TX TY)` into two components. -/
|
||||
def indexValueSumEquiv {X Y : Type} {TX : X → Colors} {TY : Y → Colors} :
|
||||
IndexValue d (Sum.elim TX TY) ≃ IndexValue d TX × IndexValue d TY where
|
||||
toFun i := (fun x => i (Sum.inl x), fun x => i (Sum.inr x))
|
||||
invFun p := fun c => match c with
|
||||
| Sum.inl x => (p.1 x)
|
||||
| Sum.inr x => (p.2 x)
|
||||
left_inv i := by
|
||||
simp only [IndexValue]
|
||||
ext1 x
|
||||
cases x with
|
||||
| inl val => rfl
|
||||
| inr val_1 => rfl
|
||||
right_inv p := rfl
|
||||
|
||||
/-- An equivalence between index values formed by commuting sums. -/
|
||||
def indexValueSumComm {X Y : Type} (Tc : X → Colors) (Sc : Y → Colors) :
|
||||
IndexValue d (Sum.elim Tc Sc) ≃ IndexValue d (Sum.elim Sc Tc) :=
|
||||
indexValueIso d (Equiv.sumComm X Y) (by aesop)
|
||||
|
||||
/-!
|
||||
|
||||
## Marked Lorentz tensors
|
||||
|
||||
To define contraction and multiplication of Lorentz tensors we need to mark indices.
|
||||
|
||||
-/
|
||||
|
||||
/-- A `RealLorentzTensor` with `n` marked indices. -/
|
||||
def Marked (d : ℕ) (X : Type) (n : ℕ) : Type :=
|
||||
RealLorentzTensor d (X ⊕ Fin n)
|
||||
|
||||
namespace Marked
|
||||
|
||||
variable {n m : ℕ}
|
||||
|
||||
/-- The marked point. -/
|
||||
def markedPoint (X : Type) (i : Fin n) : (X ⊕ Fin n) :=
|
||||
Sum.inr i
|
||||
|
||||
/-- The colors of unmarked indices. -/
|
||||
def unmarkedColor (T : Marked d X n) : X → Colors :=
|
||||
T.color ∘ Sum.inl
|
||||
|
||||
/-- The colors of marked indices. -/
|
||||
def markedColor (T : Marked d X n) : Fin n → Colors :=
|
||||
T.color ∘ Sum.inr
|
||||
|
||||
/-- The index values restricted to unmarked indices. -/
|
||||
def UnmarkedIndexValue (T : Marked d X n) : Type :=
|
||||
IndexValue d T.unmarkedColor
|
||||
|
||||
instance [Fintype X] [DecidableEq X] (T : Marked d X n) : Fintype T.UnmarkedIndexValue :=
|
||||
Pi.fintype
|
||||
|
||||
instance [Fintype X] (T : Marked d X n) : DecidableEq T.UnmarkedIndexValue :=
|
||||
Fintype.decidablePiFintype
|
||||
|
||||
/-- The index values restricted to marked indices. -/
|
||||
def MarkedIndexValue (T : Marked d X n) : Type :=
|
||||
IndexValue d T.markedColor
|
||||
|
||||
instance (T : Marked d X n) : Fintype T.MarkedIndexValue :=
|
||||
Pi.fintype
|
||||
|
||||
instance (T : Marked d X n) : DecidableEq T.MarkedIndexValue :=
|
||||
Fintype.decidablePiFintype
|
||||
|
||||
lemma color_eq_elim (T : Marked d X n) :
|
||||
T.color = Sum.elim T.unmarkedColor T.markedColor := by
|
||||
ext1 x
|
||||
cases' x <;> rfl
|
||||
|
||||
/-- An equivalence splitting elements of `IndexValue d T.color` into their two components. -/
|
||||
def splitIndexValue {T : Marked d X n} :
|
||||
IndexValue d T.color ≃ T.UnmarkedIndexValue × T.MarkedIndexValue :=
|
||||
(indexValueIso d (Equiv.refl _) T.color_eq_elim).trans
|
||||
indexValueSumEquiv
|
||||
|
||||
@[simp]
|
||||
lemma splitIndexValue_sum {T : Marked d X n} [Fintype X] [DecidableEq X]
|
||||
(P : T.UnmarkedIndexValue × T.MarkedIndexValue → ℝ) :
|
||||
∑ i, P (splitIndexValue i) = ∑ j, ∑ k, P (j, k) := by
|
||||
rw [Equiv.sum_comp splitIndexValue, Fintype.sum_prod_type]
|
||||
|
||||
/-- Contruction of marked index values for the case of 1 marked index. -/
|
||||
def oneMarkedIndexValue {T : Marked d X 1} :
|
||||
ColorsIndex d (T.color (markedPoint X 0)) ≃ T.MarkedIndexValue where
|
||||
toFun x := fun i => match i with
|
||||
| 0 => x
|
||||
invFun i := i 0
|
||||
left_inv x := rfl
|
||||
right_inv i := by
|
||||
funext x
|
||||
fin_cases x
|
||||
rfl
|
||||
|
||||
/-- Contruction of marked index values for the case of 2 marked index. -/
|
||||
def twoMarkedIndexValue (T : Marked d X 2) (x : ColorsIndex d (T.color (markedPoint X 0)))
|
||||
(y : ColorsIndex d <| T.color <| markedPoint X 1) :
|
||||
T.MarkedIndexValue := fun i =>
|
||||
match i with
|
||||
| 0 => x
|
||||
| 1 => y
|
||||
|
||||
/-- An equivalence of types used to turn the first marked index into an unmarked index. -/
|
||||
def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Fin n.succ) ≃
|
||||
(X ⊕ Fin 1) ⊕ Fin n :=
|
||||
trans (Equiv.sumCongr (Equiv.refl _) $
|
||||
(((Fin.castOrderIso (Nat.succ_eq_one_add n)).toEquiv.trans finSumFinEquiv.symm)))
|
||||
(Equiv.sumAssoc _ _ _).symm
|
||||
|
||||
/-- Unmark the first marked index of a marked thensor. -/
|
||||
def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ Fin 1) n :=
|
||||
mapIso d (unmarkFirstSet X n)
|
||||
|
||||
end Marked
|
||||
|
||||
/-!
|
||||
|
||||
## Contraction of indices
|
||||
|
||||
-/
|
||||
|
||||
open Marked
|
||||
|
||||
/-- The contraction of the marked indices in a tensor with two marked indices. -/
|
||||
def contr {X : Type} (T : Marked d X 2) (h : T.markedColor 0 = τ (T.markedColor 1)) :
|
||||
RealLorentzTensor d X where
|
||||
color := T.unmarkedColor
|
||||
coord := fun i =>
|
||||
∑ x, T.coord (splitIndexValue.symm (i, T.twoMarkedIndexValue x $ colorsIndexDualCast h x))
|
||||
|
||||
/-! TODO: Following the ethos of modular operads, prove properties of contraction. -/
|
||||
|
||||
/-! TODO: Use `contr` to generalize to any pair of marked index. -/
|
||||
|
||||
/-!
|
||||
|
||||
## Rising and lowering indices
|
||||
|
||||
Rising or lowering an index corresponds to changing the color of that index.
|
||||
|
||||
-/
|
||||
|
||||
/-! TODO: Define the rising and lowering of indices using contraction with the metric. -/
|
||||
|
||||
/-!
|
||||
|
||||
## Graphical species and Lorentz tensors
|
||||
|
||||
-/
|
||||
|
||||
/-! TODO: From Lorentz tensors graphical species. -/
|
||||
/-! TODO: Show that the action of the Lorentz group defines an action on the graphical species. -/
|
||||
|
||||
end RealLorentzTensor
|
||||
371
HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
Normal file
371
HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
Normal file
|
|
@ -0,0 +1,371 @@
|
|||
/-
|
||||
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.LorentzTensor.Real.Basic
|
||||
import HepLean.SpaceTime.LorentzTensor.Real.LorentzAction
|
||||
import HepLean.SpaceTime.LorentzTensor.Real.Multiplication
|
||||
/-!
|
||||
|
||||
# Constructors for real Lorentz tensors
|
||||
|
||||
In this file we will constructors of real Lorentz tensors from real numbers,
|
||||
vectors and matrices.
|
||||
|
||||
We will derive properties of these constructors.
|
||||
|
||||
-/
|
||||
|
||||
namespace RealLorentzTensor
|
||||
|
||||
/-!
|
||||
|
||||
# Tensors from reals, vectors and matrices
|
||||
|
||||
Note that that these definitions are not equivariant with respect to an
|
||||
action of the Lorentz group. They are provided for constructive purposes.
|
||||
|
||||
-/
|
||||
|
||||
/-- A 0-tensor from a real number. -/
|
||||
def ofReal (d : ℕ) (r : ℝ) : RealLorentzTensor d Empty where
|
||||
color := fun _ => Colors.up
|
||||
coord := fun _ => r
|
||||
|
||||
/-- A marked 1-tensor with a single up index constructed from a vector.
|
||||
|
||||
Note: This is not the same as rising indices on `ofVecDown`. -/
|
||||
def ofVecUp {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
Marked d Empty 1 where
|
||||
color := fun _ => Colors.up
|
||||
coord := fun i => v <| i <| Sum.inr <| 0
|
||||
|
||||
/-- A marked 1-tensor with a single down index constructed from a vector.
|
||||
|
||||
Note: This is not the same as lowering indices on `ofVecUp`. -/
|
||||
def ofVecDown {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
Marked d Empty 1 where
|
||||
color := fun _ => Colors.down
|
||||
coord := fun i => v <| i <| Sum.inr <| 0
|
||||
|
||||
/-- A tensor with two up indices constructed from a matrix.
|
||||
|
||||
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
|
||||
def ofMatUpUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Marked d Empty 2 where
|
||||
color := fun _ => Colors.up
|
||||
coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1))
|
||||
|
||||
/-- A tensor with two down indices constructed from a matrix.
|
||||
|
||||
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
|
||||
def ofMatDownDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Marked d Empty 2 where
|
||||
color := fun _ => Colors.down
|
||||
coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1))
|
||||
|
||||
/-- A marked 2-tensor with the first index up and the second index down.
|
||||
|
||||
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
|
||||
@[simps!]
|
||||
def ofMatUpDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Marked d Empty 2 where
|
||||
color := fun i => match i with
|
||||
| Sum.inr 0 => Colors.up
|
||||
| Sum.inr 1 => Colors.down
|
||||
coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1))
|
||||
|
||||
/-- A marked 2-tensor with the first index down and the second index up.
|
||||
|
||||
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
|
||||
def ofMatDownUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Marked d Empty 2 where
|
||||
color := fun i => match i with
|
||||
| Sum.inr 0 => Colors.down
|
||||
| Sum.inr 1 => Colors.up
|
||||
coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1))
|
||||
|
||||
/-!
|
||||
|
||||
## Equivalence of `IndexValue` for constructors
|
||||
|
||||
-/
|
||||
|
||||
/-- Index values for `ofVecUp v` are equivalent to elements of `Fin 1 ⊕ Fin d`. -/
|
||||
def ofVecUpIndexValue (v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
IndexValue d (ofVecUp v).color ≃ (Fin 1 ⊕ Fin d) where
|
||||
toFun i := i (Sum.inr 0)
|
||||
invFun x := fun i => match i with
|
||||
| Sum.inr 0 => x
|
||||
left_inv i := by
|
||||
funext y
|
||||
match y with
|
||||
| Sum.inr 0 => rfl
|
||||
right_inv x := rfl
|
||||
|
||||
/-- Index values for `ofVecDown v` are equivalent to elements of `Fin 1 ⊕ Fin d`. -/
|
||||
def ofVecDownIndexValue (v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
IndexValue d (ofVecDown v).color ≃ (Fin 1 ⊕ Fin d) where
|
||||
toFun i := i (Sum.inr 0)
|
||||
invFun x := fun i => match i with
|
||||
| Sum.inr 0 => x
|
||||
left_inv i := by
|
||||
funext y
|
||||
match y with
|
||||
| Sum.inr 0 => rfl
|
||||
right_inv x := rfl
|
||||
|
||||
/-- Index values for `ofMatUpUp v` are equivalent to elements of
|
||||
`(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
|
||||
def ofMatUpUpIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
IndexValue d (ofMatUpUp M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
|
||||
toFun i := (i (Sum.inr 0), i (Sum.inr 1))
|
||||
invFun x := fun i => match i with
|
||||
| Sum.inr 0 => x.1
|
||||
| Sum.inr 1 => x.2
|
||||
left_inv i := by
|
||||
funext y
|
||||
match y with
|
||||
| Sum.inr 0 => rfl
|
||||
| Sum.inr 1 => rfl
|
||||
right_inv x := rfl
|
||||
|
||||
/-- Index values for `ofMatDownDown v` are equivalent to elements of
|
||||
`(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
|
||||
def ofMatDownDownIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
IndexValue d (ofMatDownDown M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
|
||||
toFun i := (i (Sum.inr 0), i (Sum.inr 1))
|
||||
invFun x := fun i => match i with
|
||||
| Sum.inr 0 => x.1
|
||||
| Sum.inr 1 => x.2
|
||||
left_inv i := by
|
||||
funext y
|
||||
match y with
|
||||
| Sum.inr 0 => rfl
|
||||
| Sum.inr 1 => rfl
|
||||
right_inv x := rfl
|
||||
|
||||
/-- Index values for `ofMatUpDown v` are equivalent to elements of
|
||||
`(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
|
||||
def ofMatUpDownIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
IndexValue d (ofMatUpDown M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
|
||||
toFun i := (i (Sum.inr 0), i (Sum.inr 1))
|
||||
invFun x := fun i => match i with
|
||||
| Sum.inr 0 => x.1
|
||||
| Sum.inr 1 => x.2
|
||||
left_inv i := by
|
||||
funext y
|
||||
match y with
|
||||
| Sum.inr 0 => rfl
|
||||
| Sum.inr 1 => rfl
|
||||
right_inv x := rfl
|
||||
|
||||
/-- Index values for `ofMatDownUp v` are equivalent to elements of
|
||||
`(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
|
||||
def ofMatDownUpIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
IndexValue d (ofMatDownUp M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
|
||||
toFun i := (i (Sum.inr 0), i (Sum.inr 1))
|
||||
invFun x := fun i => match i with
|
||||
| Sum.inr 0 => x.1
|
||||
| Sum.inr 1 => x.2
|
||||
left_inv i := by
|
||||
funext y
|
||||
match y with
|
||||
| Sum.inr 0 => rfl
|
||||
| Sum.inr 1 => rfl
|
||||
right_inv x := rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Contraction of indices of tensors from matrices
|
||||
|
||||
-/
|
||||
open Matrix
|
||||
open Marked
|
||||
|
||||
/-- Contracting the indices of `ofMatUpDown` returns the trace of the matrix. -/
|
||||
lemma contr_ofMatUpDown_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
contr (ofMatUpDown M) (by rfl) = ofReal d M.trace := by
|
||||
refine ext ?_ rfl
|
||||
· funext i
|
||||
exact Empty.elim i
|
||||
|
||||
/-- Contracting the indices of `ofMatDownUp` returns the trace of the matrix. -/
|
||||
lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
contr (ofMatDownUp M) (by rfl) = ofReal d M.trace := by
|
||||
refine ext ?_ rfl
|
||||
· funext i
|
||||
exact Empty.elim i
|
||||
|
||||
/-!
|
||||
|
||||
## Multiplication of tensors from vectors and matrices
|
||||
|
||||
-/
|
||||
|
||||
/-- Multiplying `ofVecUp` with `ofVecDown` gives the dot product. -/
|
||||
@[simp]
|
||||
lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
|
||||
mapIso d (@Equiv.equivEmpty (Empty ⊕ Empty) instIsEmptySum)
|
||||
(mul (ofVecUp v₁) (ofVecDown v₂) (by rfl)) = ofReal d (v₁ ⬝ᵥ v₂) := by
|
||||
refine ext ?_ rfl
|
||||
· funext i
|
||||
exact Empty.elim i
|
||||
|
||||
/-- Multiplying `ofVecDown` with `ofVecUp` gives the dot product. -/
|
||||
@[simp]
|
||||
lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
|
||||
mapIso d (Equiv.equivEmpty (Empty ⊕ Empty))
|
||||
(mul (ofVecDown v₁) (ofVecUp v₂) rfl) = ofReal d (v₁ ⬝ᵥ v₂) := by
|
||||
refine ext ?_ rfl
|
||||
· funext i
|
||||
exact Empty.elim i
|
||||
|
||||
lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
|
||||
(v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
mapIso d ((Equiv.sumEmpty (Empty ⊕ Fin 1) Empty))
|
||||
(mul (unmarkFirst $ ofMatUpDown M) (ofVecUp v) rfl) = ofVecUp (M *ᵥ v) := by
|
||||
refine ext ?_ rfl
|
||||
· funext i
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, mapIso_apply_color, mul_color, Equiv.symm_symm]
|
||||
fin_cases i
|
||||
rfl
|
||||
|
||||
lemma mul_ofMatDownUp_ofVecDown_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
|
||||
(v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
mapIso d (Equiv.sumEmpty (Empty ⊕ Fin 1) Empty)
|
||||
(mul (unmarkFirst $ ofMatDownUp M) (ofVecDown v) rfl) = ofVecDown (M *ᵥ v) := by
|
||||
refine ext ?_ rfl
|
||||
· funext i
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, mapIso_apply_color, mul_color, Equiv.symm_symm]
|
||||
fin_cases i
|
||||
rfl
|
||||
|
||||
/-!
|
||||
|
||||
## The Lorentz action on constructors
|
||||
|
||||
-/
|
||||
section lorentzAction
|
||||
variable {d : ℕ} {X : Type} [Fintype X] [DecidableEq X] (T : RealLorentzTensor d X) (c : X → Colors)
|
||||
variable (Λ Λ' : LorentzGroup d)
|
||||
|
||||
open Matrix
|
||||
|
||||
/-- The action of the Lorentz group on `ofReal v` is trivial. -/
|
||||
@[simp]
|
||||
lemma lorentzAction_ofReal (r : ℝ) : Λ • ofReal d r = ofReal d r :=
|
||||
lorentzAction_on_isEmpty Λ (ofReal d r)
|
||||
|
||||
/-- The action of the Lorentz group on `ofVecUp v` is by vector multiplication. -/
|
||||
@[simp]
|
||||
lemma lorentzAction_ofVecUp (v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
Λ • ofVecUp v = ofVecUp (Λ *ᵥ v) := by
|
||||
refine ext rfl ?_
|
||||
funext i
|
||||
erw [lorentzAction_smul_coord]
|
||||
simp only [ofVecUp, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
|
||||
Finset.prod_empty, one_mul]
|
||||
rw [mulVec]
|
||||
simp only [Fin.isValue, dotProduct, Finset.univ_unique, Fin.default_eq_zero,
|
||||
Finset.sum_singleton]
|
||||
erw [Finset.sum_equiv (ofVecUpIndexValue v)]
|
||||
intro i
|
||||
simp_all only [Finset.mem_univ, Fin.isValue, Equiv.coe_fn_mk]
|
||||
intro j _
|
||||
simp_all only [Finset.mem_univ, Fin.isValue, Finset.prod_singleton, indexValueIso_refl]
|
||||
rfl
|
||||
|
||||
/-- The action of the Lorentz group on `ofVecDown v` is
|
||||
by vector multiplication of the transpose-inverse. -/
|
||||
@[simp]
|
||||
lemma lorentzAction_ofVecDown (v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
Λ • ofVecDown v = ofVecDown ((LorentzGroup.transpose Λ⁻¹) *ᵥ v) := by
|
||||
refine ext rfl ?_
|
||||
funext i
|
||||
erw [lorentzAction_smul_coord]
|
||||
simp only [ofVecDown, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
|
||||
Finset.prod_empty, one_mul, lorentzGroupIsGroup_inv]
|
||||
rw [mulVec]
|
||||
simp only [Fin.isValue, dotProduct, Finset.univ_unique, Fin.default_eq_zero,
|
||||
Finset.sum_singleton]
|
||||
erw [Finset.sum_equiv (ofVecUpIndexValue v)]
|
||||
intro i
|
||||
simp_all only [Finset.mem_univ, Fin.isValue, Equiv.coe_fn_mk]
|
||||
intro j _
|
||||
simp_all only [Finset.mem_univ, Fin.isValue, Finset.prod_singleton, indexValueIso_refl]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma lorentzAction_ofMatUpUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Λ • ofMatUpUp M = ofMatUpUp (Λ.1 * M * (LorentzGroup.transpose Λ).1) := by
|
||||
refine ext rfl ?_
|
||||
funext i
|
||||
erw [lorentzAction_smul_coord]
|
||||
erw [← Equiv.sum_comp (ofMatUpUpIndexValue M).symm]
|
||||
simp only [ofMatUpUp, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
|
||||
Finset.prod_empty, one_mul, mul_apply]
|
||||
erw [Finset.sum_product]
|
||||
rw [Finset.sum_comm]
|
||||
refine Finset.sum_congr rfl (fun x _ => ?_)
|
||||
rw [Finset.sum_mul]
|
||||
refine Finset.sum_congr rfl (fun y _ => ?_)
|
||||
simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue]
|
||||
exact mul_right_comm _ _ _
|
||||
|
||||
@[simp]
|
||||
lemma lorentzAction_ofMatDownDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Λ • ofMatDownDown M = ofMatDownDown ((LorentzGroup.transpose Λ⁻¹).1 * M * (Λ⁻¹).1) := by
|
||||
refine ext rfl ?_
|
||||
funext i
|
||||
erw [lorentzAction_smul_coord]
|
||||
erw [← Equiv.sum_comp (ofMatDownDownIndexValue M).symm]
|
||||
simp only [ofMatDownDown, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
|
||||
Finset.prod_empty, one_mul, mul_apply]
|
||||
erw [Finset.sum_product]
|
||||
rw [Finset.sum_comm]
|
||||
refine Finset.sum_congr rfl (fun x _ => ?_)
|
||||
rw [Finset.sum_mul]
|
||||
refine Finset.sum_congr rfl (fun y _ => ?_)
|
||||
simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue]
|
||||
exact mul_right_comm _ _ _
|
||||
|
||||
@[simp]
|
||||
lemma lorentzAction_ofMatUpDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Λ • ofMatUpDown M = ofMatUpDown (Λ.1 * M * (Λ⁻¹).1) := by
|
||||
refine ext rfl ?_
|
||||
funext i
|
||||
erw [lorentzAction_smul_coord]
|
||||
erw [← Equiv.sum_comp (ofMatUpDownIndexValue M).symm]
|
||||
simp only [ofMatUpDown, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
|
||||
Finset.prod_empty, one_mul, mul_apply]
|
||||
erw [Finset.sum_product]
|
||||
rw [Finset.sum_comm]
|
||||
refine Finset.sum_congr rfl (fun x _ => ?_)
|
||||
rw [Finset.sum_mul]
|
||||
refine Finset.sum_congr rfl (fun y _ => ?_)
|
||||
simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue]
|
||||
exact mul_right_comm _ _ _
|
||||
|
||||
@[simp]
|
||||
lemma lorentzAction_ofMatDownUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Λ • ofMatDownUp M =
|
||||
ofMatDownUp ((LorentzGroup.transpose Λ⁻¹).1 * M * (LorentzGroup.transpose Λ).1) := by
|
||||
refine ext rfl ?_
|
||||
funext i
|
||||
erw [lorentzAction_smul_coord]
|
||||
erw [← Equiv.sum_comp (ofMatDownUpIndexValue M).symm]
|
||||
simp only [ofMatDownUp, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
|
||||
Finset.prod_empty, one_mul, mul_apply]
|
||||
erw [Finset.sum_product]
|
||||
rw [Finset.sum_comm]
|
||||
refine Finset.sum_congr rfl (fun x _ => ?_)
|
||||
rw [Finset.sum_mul]
|
||||
refine Finset.sum_congr rfl (fun y _ => ?_)
|
||||
simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue]
|
||||
exact mul_right_comm _ _ _
|
||||
|
||||
end lorentzAction
|
||||
|
||||
end RealLorentzTensor
|
||||
444
HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
Normal file
444
HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
Normal file
|
|
@ -0,0 +1,444 @@
|
|||
/-
|
||||
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.LorentzTensor.Real.Basic
|
||||
import HepLean.SpaceTime.LorentzGroup.Basic
|
||||
/-!
|
||||
|
||||
# Lorentz group action on Real Lorentz Tensors
|
||||
|
||||
We define the action of the Lorentz group on Real Lorentz Tensors.
|
||||
|
||||
The Lorentz action is currently only defined for finite and decidable types `X`.
|
||||
|
||||
-/
|
||||
|
||||
namespace RealLorentzTensor
|
||||
|
||||
variable {d : ℕ} {X Y : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
|
||||
(T : RealLorentzTensor d X) (c : X → Colors) (Λ Λ' : LorentzGroup d) {μ : Colors}
|
||||
|
||||
open LorentzGroup BigOperators Marked
|
||||
|
||||
/-- Monoid homomorphism from the Lorentz group to matrices indexed by `ColorsIndex d μ` for a
|
||||
color `μ`.
|
||||
|
||||
This can be thought of as the representation of the Lorentz group for that color index. -/
|
||||
def colorMatrix (μ : Colors) : LorentzGroup d →* Matrix (ColorsIndex d μ) (ColorsIndex d μ) ℝ where
|
||||
toFun Λ := match μ with
|
||||
| .up => fun i j => Λ.1 i j
|
||||
| .down => fun i j => (LorentzGroup.transpose Λ⁻¹).1 i j
|
||||
map_one' := by
|
||||
match μ with
|
||||
| .up =>
|
||||
simp only [lorentzGroupIsGroup_one_coe]
|
||||
ext i j
|
||||
simp only [OfNat.ofNat, One.one, ColorsIndex]
|
||||
congr
|
||||
| .down =>
|
||||
simp only [transpose, inv_one, lorentzGroupIsGroup_one_coe, Matrix.transpose_one]
|
||||
ext i j
|
||||
simp only [OfNat.ofNat, One.one, ColorsIndex]
|
||||
congr
|
||||
map_mul' Λ Λ' := by
|
||||
match μ with
|
||||
| .up =>
|
||||
ext i j
|
||||
simp only [lorentzGroupIsGroup_mul_coe]
|
||||
| .down =>
|
||||
ext i j
|
||||
simp only [transpose, mul_inv_rev, lorentzGroupIsGroup_inv, lorentzGroupIsGroup_mul_coe,
|
||||
Matrix.transpose_mul, Matrix.transpose_apply]
|
||||
rfl
|
||||
|
||||
lemma colorMatrix_cast {μ ν : Colors} (h : μ = ν) (Λ : LorentzGroup d) :
|
||||
colorMatrix μ Λ =
|
||||
Matrix.reindex (colorsIndexCast h).symm (colorsIndexCast h).symm (colorMatrix ν Λ) := by
|
||||
subst h
|
||||
rfl
|
||||
|
||||
lemma colorMatrix_dual_cast {μ : Colors} (Λ : LorentzGroup d) :
|
||||
colorMatrix (τ μ) Λ = Matrix.reindex (colorsIndexDualCastSelf) (colorsIndexDualCastSelf)
|
||||
(colorMatrix μ (LorentzGroup.transpose Λ⁻¹)) := by
|
||||
match μ with
|
||||
| .up => rfl
|
||||
| .down =>
|
||||
ext i j
|
||||
simp only [τ, colorMatrix, MonoidHom.coe_mk, OneHom.coe_mk, colorsIndexDualCastSelf, transpose,
|
||||
lorentzGroupIsGroup_inv, Matrix.transpose_apply, minkowskiMetric.dual_transpose,
|
||||
minkowskiMetric.dual_dual, Matrix.reindex_apply, Equiv.coe_fn_symm_mk, Matrix.submatrix_apply]
|
||||
lemma colorMatrix_transpose {μ : Colors} (Λ : LorentzGroup d) :
|
||||
colorMatrix μ (LorentzGroup.transpose Λ) = (colorMatrix μ Λ).transpose := by
|
||||
match μ with
|
||||
| .up => rfl
|
||||
| .down =>
|
||||
ext i j
|
||||
simp only [colorMatrix, transpose, lorentzGroupIsGroup_inv, Matrix.transpose_apply,
|
||||
MonoidHom.coe_mk, OneHom.coe_mk, minkowskiMetric.dual_transpose]
|
||||
|
||||
/-!
|
||||
|
||||
## Lorentz group to tensor representation matrices.
|
||||
|
||||
-/
|
||||
|
||||
/-- The matrix representation of the Lorentz group given a color of index. -/
|
||||
@[simps!]
|
||||
def toTensorRepMat {c : X → Colors} :
|
||||
LorentzGroup d →* Matrix (IndexValue d c) (IndexValue d c) ℝ where
|
||||
toFun Λ := fun i j => ∏ x, colorMatrix (c x) Λ (i x) (j x)
|
||||
map_one' := by
|
||||
ext i j
|
||||
by_cases hij : i = j
|
||||
· subst hij
|
||||
simp only [map_one, Matrix.one_apply_eq, Finset.prod_const_one]
|
||||
· obtain ⟨x, hijx⟩ := Function.ne_iff.mp hij
|
||||
simp only [map_one]
|
||||
rw [@Finset.prod_eq_zero _ _ _ _ _ x]
|
||||
exact Eq.symm (Matrix.one_apply_ne' fun a => hij (id (Eq.symm a)))
|
||||
exact Finset.mem_univ x
|
||||
exact Matrix.one_apply_ne' (id (Ne.symm hijx))
|
||||
map_mul' Λ Λ' := by
|
||||
ext i j
|
||||
rw [Matrix.mul_apply]
|
||||
trans ∑ (k : IndexValue d c), ∏ x,
|
||||
(colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x))
|
||||
have h1 : ∑ (k : IndexValue d c), ∏ x,
|
||||
(colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x)) =
|
||||
∏ x, ∑ y, (colorMatrix (c x) Λ (i x) y) * (colorMatrix (c x) Λ' y (j x)) := by
|
||||
rw [Finset.prod_sum]
|
||||
simp only [Finset.prod_attach_univ, Finset.sum_univ_pi]
|
||||
rfl
|
||||
rw [h1]
|
||||
simp only [map_mul]
|
||||
rfl
|
||||
refine Finset.sum_congr rfl (fun k _ => ?_)
|
||||
rw [Finset.prod_mul_distrib]
|
||||
|
||||
lemma toTensorRepMat_mul' (i j : IndexValue d c) :
|
||||
toTensorRepMat (Λ * Λ') i j = ∑ (k : IndexValue d c),
|
||||
∏ x, colorMatrix (c x) Λ (i x) (k x) * colorMatrix (c x) Λ' (k x) (j x) := by
|
||||
simp [Matrix.mul_apply, IndexValue]
|
||||
refine Finset.sum_congr rfl (fun k _ => ?_)
|
||||
rw [Finset.prod_mul_distrib]
|
||||
rfl
|
||||
|
||||
lemma toTensorRepMat_of_indexValueSumEquiv {cX : X → Colors} {cY : Y → Colors}
|
||||
(i j : IndexValue d (Sum.elim cX cY)) :
|
||||
toTensorRepMat Λ i j = toTensorRepMat Λ (indexValueSumEquiv i).1 (indexValueSumEquiv j).1 *
|
||||
toTensorRepMat Λ (indexValueSumEquiv i).2 (indexValueSumEquiv j).2 :=
|
||||
Fintype.prod_sum_type fun x => (colorMatrix (Sum.elim cX cY x)) Λ (i x) (j x)
|
||||
|
||||
lemma toTensorRepMat_of_indexValueSumEquiv' {cX : X → Colors} {cY : Y → Colors}
|
||||
(i j : IndexValue d cX) (k l : IndexValue d cY) :
|
||||
toTensorRepMat Λ i j * toTensorRepMat Λ k l =
|
||||
toTensorRepMat Λ (indexValueSumEquiv.symm (i, k)) (indexValueSumEquiv.symm (j, l)) :=
|
||||
(Fintype.prod_sum_type fun x => (colorMatrix (Sum.elim cX cY x)) Λ
|
||||
(indexValueSumEquiv.symm (i, k) x) (indexValueSumEquiv.symm (j, l) x)).symm
|
||||
|
||||
/-!
|
||||
|
||||
## Tensor representation matrices and marked tensors.
|
||||
|
||||
-/
|
||||
|
||||
lemma toTensorRepMat_of_splitIndexValue' (T : Marked d X n)
|
||||
(i j : T.UnmarkedIndexValue) (k l : T.MarkedIndexValue) :
|
||||
toTensorRepMat Λ i j * toTensorRepMat Λ k l =
|
||||
toTensorRepMat Λ (splitIndexValue.symm (i, k)) (splitIndexValue.symm (j, l)) :=
|
||||
(Fintype.prod_sum_type fun x =>
|
||||
(colorMatrix (T.color x)) Λ (splitIndexValue.symm (i, k) x) (splitIndexValue.symm (j, l) x)).symm
|
||||
|
||||
lemma toTensorRepMat_oneMarkedIndexValue_dual (T : Marked d X 1) (S : Marked d Y 1)
|
||||
(h : T.markedColor 0 = τ (S.markedColor 0)) (x : ColorsIndex d (T.markedColor 0))
|
||||
(k : S.MarkedIndexValue) :
|
||||
toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k =
|
||||
toTensorRepMat Λ⁻¹ (oneMarkedIndexValue
|
||||
$ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k)
|
||||
(oneMarkedIndexValue x) := by
|
||||
rw [toTensorRepMat_apply, toTensorRepMat_apply]
|
||||
erw [Finset.prod_singleton, Finset.prod_singleton]
|
||||
simp only [Fin.zero_eta, Fin.isValue, lorentzGroupIsGroup_inv]
|
||||
rw [colorMatrix_cast h, colorMatrix_dual_cast]
|
||||
rw [Matrix.reindex_apply, Matrix.reindex_apply]
|
||||
simp only [Fin.isValue, lorentzGroupIsGroup_inv, minkowskiMetric.dual_dual, Subtype.coe_eta,
|
||||
Equiv.symm_symm, Matrix.submatrix_apply]
|
||||
rw [colorMatrix_transpose]
|
||||
simp only [Fin.isValue, Matrix.transpose_apply]
|
||||
apply congrArg
|
||||
simp only [Fin.isValue, oneMarkedIndexValue, colorsIndexDualCast, Equiv.coe_fn_symm_mk,
|
||||
Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.coe_fn_mk, Equiv.apply_symm_apply,
|
||||
Equiv.symm_apply_apply]
|
||||
|
||||
lemma toTensorRepMap_sum_dual (T : Marked d X 1) (S : Marked d Y 1)
|
||||
(h : T.markedColor 0 = τ (S.markedColor 0)) (j : T.MarkedIndexValue) (k : S.MarkedIndexValue) :
|
||||
∑ x, toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k
|
||||
* toTensorRepMat Λ (oneMarkedIndexValue x) j =
|
||||
toTensorRepMat 1
|
||||
(oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k) j := by
|
||||
trans ∑ x, toTensorRepMat Λ⁻¹ (oneMarkedIndexValue$ (colorsIndexDualCast h).symm $
|
||||
oneMarkedIndexValue.symm k) (oneMarkedIndexValue x) * toTensorRepMat Λ (oneMarkedIndexValue x) j
|
||||
apply Finset.sum_congr rfl (fun x _ => ?_)
|
||||
rw [toTensorRepMat_oneMarkedIndexValue_dual]
|
||||
rw [← Equiv.sum_comp oneMarkedIndexValue.symm]
|
||||
change ∑ i, toTensorRepMat Λ⁻¹ (oneMarkedIndexValue $ (colorsIndexDualCast h).symm $
|
||||
oneMarkedIndexValue.symm k) i * toTensorRepMat Λ i j = _
|
||||
rw [← Matrix.mul_apply, ← toTensorRepMat.map_mul, inv_mul_self Λ]
|
||||
|
||||
lemma toTensorRepMat_one_coord_sum (T : Marked d X n) (i : T.UnmarkedIndexValue)
|
||||
(k : T.MarkedIndexValue) : T.coord (splitIndexValue.symm (i, k)) = ∑ j, toTensorRepMat 1 k j *
|
||||
T.coord (splitIndexValue.symm (i, j)) := by
|
||||
erw [Finset.sum_eq_single_of_mem k]
|
||||
simp only [IndexValue, map_one, Matrix.one_apply_eq, one_mul]
|
||||
exact Finset.mem_univ k
|
||||
intro j _ hjk
|
||||
simp [hjk, IndexValue]
|
||||
exact Or.inl (Matrix.one_apply_ne' hjk)
|
||||
|
||||
/-!
|
||||
|
||||
## Definition of the Lorentz group action on Real Lorentz Tensors.
|
||||
|
||||
-/
|
||||
|
||||
/-- Action of the Lorentz group on `X`-indexed Real Lorentz Tensors. -/
|
||||
@[simps!]
|
||||
instance lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) where
|
||||
smul Λ T := {color := T.color,
|
||||
coord := fun i => ∑ j, toTensorRepMat Λ i j * T.coord j}
|
||||
one_smul T := by
|
||||
refine ext rfl ?_
|
||||
funext i
|
||||
simp only [HSMul.hSMul, map_one]
|
||||
erw [Finset.sum_eq_single_of_mem i]
|
||||
simp only [Matrix.one_apply_eq, one_mul, IndexValue]
|
||||
rfl
|
||||
exact Finset.mem_univ i
|
||||
exact fun j _ hij => mul_eq_zero.mpr (Or.inl (Matrix.one_apply_ne' hij))
|
||||
mul_smul Λ Λ' T := by
|
||||
refine ext rfl ?_
|
||||
simp only [HSMul.hSMul]
|
||||
funext i
|
||||
have h1 : ∑ j : IndexValue d T.color, toTensorRepMat (Λ * Λ') i j
|
||||
* T.coord j = ∑ j : IndexValue d T.color, ∑ (k : IndexValue d T.color),
|
||||
(∏ x, ((colorMatrix (T.color x) Λ (i x) (k x)) *
|
||||
(colorMatrix (T.color x) Λ' (k x) (j x)))) * T.coord j := by
|
||||
refine Finset.sum_congr rfl (fun j _ => ?_)
|
||||
rw [toTensorRepMat_mul', Finset.sum_mul]
|
||||
rw [h1]
|
||||
rw [Finset.sum_comm]
|
||||
refine Finset.sum_congr rfl (fun j _ => ?_)
|
||||
rw [Finset.mul_sum]
|
||||
refine Finset.sum_congr rfl (fun k _ => ?_)
|
||||
simp only [toTensorRepMat, IndexValue]
|
||||
rw [← mul_assoc]
|
||||
congr
|
||||
rw [Finset.prod_mul_distrib]
|
||||
rfl
|
||||
|
||||
lemma lorentzAction_smul_coord' {d : ℕ} {X : Type} [Fintype X] [DecidableEq X] (Λ : ↑(𝓛 d))
|
||||
(T : RealLorentzTensor d X) (i : IndexValue d T.color) :
|
||||
(Λ • T).coord i = ∑ j : IndexValue d T.color, toTensorRepMat Λ i j * T.coord j := by
|
||||
rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Properties of the Lorentz action.
|
||||
|
||||
-/
|
||||
|
||||
/-- The action on an empty Lorentz tensor is trivial. -/
|
||||
lemma lorentzAction_on_isEmpty [IsEmpty X] (Λ : LorentzGroup d) (T : RealLorentzTensor d X) :
|
||||
Λ • T = T := by
|
||||
refine ext rfl ?_
|
||||
funext i
|
||||
erw [lorentzAction_smul_coord]
|
||||
simp only [Finset.univ_unique, Finset.univ_eq_empty, Finset.prod_empty, one_mul,
|
||||
Finset.sum_singleton, toTensorRepMat_apply]
|
||||
simp only [IndexValue, Unique.eq_default, Finset.univ_unique, Finset.sum_const,
|
||||
Finset.card_singleton, one_smul]
|
||||
|
||||
/-- The Lorentz action commutes with `mapIso`. -/
|
||||
lemma lorentzAction_mapIso (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzTensor d X) :
|
||||
mapIso d f (Λ • T) = Λ • (mapIso d f T) := by
|
||||
refine ext rfl ?_
|
||||
funext i
|
||||
rw [mapIso_apply_coord]
|
||||
rw [lorentzAction_smul_coord', lorentzAction_smul_coord']
|
||||
let is : IndexValue d T.color ≃ IndexValue d ((mapIso d f) T).color :=
|
||||
indexValueIso d f ((Equiv.comp_symm_eq f ((mapIso d f) T).color T.color).mp rfl)
|
||||
rw [← Equiv.sum_comp is]
|
||||
refine Finset.sum_congr rfl (fun j _ => ?_)
|
||||
rw [mapIso_apply_coord]
|
||||
refine Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl
|
||||
· simp only [IndexValue, toTensorRepMat, MonoidHom.coe_mk, OneHom.coe_mk, mapIso_apply_color,
|
||||
indexValueIso_refl]
|
||||
rw [← Equiv.prod_comp f]
|
||||
apply Finset.prod_congr rfl (fun x _ => ?_)
|
||||
have h1 : (T.color (f.symm (f x))) = T.color x := by
|
||||
simp only [Equiv.symm_apply_apply]
|
||||
rw [colorMatrix_cast h1]
|
||||
apply congrArg
|
||||
simp only [is]
|
||||
erw [indexValueIso_eq_symm, indexValueIso_symm_apply']
|
||||
simp only [colorsIndexCast, Function.comp_apply, mapIso_apply_color, Equiv.cast_refl,
|
||||
Equiv.refl_symm, Equiv.refl_apply, Equiv.cast_apply]
|
||||
symm
|
||||
refine cast_eq_iff_heq.mpr ?_
|
||||
congr
|
||||
exact Equiv.symm_apply_apply f x
|
||||
· apply congrArg
|
||||
exact (Equiv.apply_eq_iff_eq_symm_apply (indexValueIso d f (mapIso.proof_1 d f T))).mp rfl
|
||||
|
||||
/-!
|
||||
|
||||
## The Lorentz action on marked tensors.
|
||||
|
||||
-/
|
||||
|
||||
@[simps!]
|
||||
instance : MulAction (LorentzGroup d) (Marked d X n) := lorentzAction
|
||||
|
||||
/-- Action of the Lorentz group on just marked indices. -/
|
||||
@[simps!]
|
||||
def markedLorentzAction : MulAction (LorentzGroup d) (Marked d X n) where
|
||||
smul Λ T := {
|
||||
color := T.color,
|
||||
coord := fun i => ∑ j, toTensorRepMat Λ (splitIndexValue i).2 j *
|
||||
T.coord (splitIndexValue.symm ((splitIndexValue i).1, j))}
|
||||
one_smul T := by
|
||||
refine ext rfl ?_
|
||||
funext i
|
||||
simp only [HSMul.hSMul, map_one]
|
||||
erw [Finset.sum_eq_single_of_mem (splitIndexValue i).2]
|
||||
erw [Matrix.one_apply_eq (splitIndexValue i).2]
|
||||
simp only [IndexValue, one_mul, indexValueIso_refl, Equiv.refl_apply]
|
||||
apply congrArg
|
||||
exact Equiv.symm_apply_apply splitIndexValue i
|
||||
exact Finset.mem_univ (splitIndexValue i).2
|
||||
exact fun j _ hij => mul_eq_zero.mpr (Or.inl (Matrix.one_apply_ne' hij))
|
||||
mul_smul Λ Λ' T := by
|
||||
refine ext rfl ?_
|
||||
simp only [HSMul.hSMul]
|
||||
funext i
|
||||
have h1 : ∑ (j : T.MarkedIndexValue), toTensorRepMat (Λ * Λ') (splitIndexValue i).2 j
|
||||
* T.coord (splitIndexValue.symm ((splitIndexValue i).1, j)) =
|
||||
∑ (j : T.MarkedIndexValue), ∑ (k : T.MarkedIndexValue),
|
||||
(∏ x, ((colorMatrix (T.markedColor x) Λ ((splitIndexValue i).2 x) (k x)) *
|
||||
(colorMatrix (T.markedColor x) Λ' (k x) (j x)))) *
|
||||
T.coord (splitIndexValue.symm ((splitIndexValue i).1, j)) := by
|
||||
refine Finset.sum_congr rfl (fun j _ => ?_)
|
||||
rw [toTensorRepMat_mul', Finset.sum_mul]
|
||||
rfl
|
||||
erw [h1]
|
||||
rw [Finset.sum_comm]
|
||||
refine Finset.sum_congr rfl (fun j _ => ?_)
|
||||
rw [Finset.mul_sum]
|
||||
refine Finset.sum_congr rfl (fun k _ => ?_)
|
||||
simp only [toTensorRepMat, IndexValue]
|
||||
rw [← mul_assoc]
|
||||
congr
|
||||
rw [Finset.prod_mul_distrib]
|
||||
rfl
|
||||
|
||||
/-- Action of the Lorentz group on just unmarked indices. -/
|
||||
@[simps!]
|
||||
def unmarkedLorentzAction : MulAction (LorentzGroup d) (Marked d X n) where
|
||||
smul Λ T := {
|
||||
color := T.color,
|
||||
coord := fun i => ∑ j, toTensorRepMat Λ (splitIndexValue i).1 j *
|
||||
T.coord (splitIndexValue.symm (j, (splitIndexValue i).2))}
|
||||
one_smul T := by
|
||||
refine ext rfl ?_
|
||||
funext i
|
||||
simp only [HSMul.hSMul, map_one]
|
||||
erw [Finset.sum_eq_single_of_mem (splitIndexValue i).1]
|
||||
erw [Matrix.one_apply_eq (splitIndexValue i).1]
|
||||
simp only [IndexValue, one_mul, indexValueIso_refl, Equiv.refl_apply]
|
||||
apply congrArg
|
||||
exact Equiv.symm_apply_apply splitIndexValue i
|
||||
exact Finset.mem_univ (splitIndexValue i).1
|
||||
exact fun j _ hij => mul_eq_zero.mpr (Or.inl (Matrix.one_apply_ne' hij))
|
||||
mul_smul Λ Λ' T := by
|
||||
refine ext rfl ?_
|
||||
simp only [HSMul.hSMul]
|
||||
funext i
|
||||
have h1 : ∑ (j : T.UnmarkedIndexValue), toTensorRepMat (Λ * Λ') (splitIndexValue i).1 j
|
||||
* T.coord (splitIndexValue.symm (j, (splitIndexValue i).2)) =
|
||||
∑ (j : T.UnmarkedIndexValue), ∑ (k : T.UnmarkedIndexValue),
|
||||
(∏ x, ((colorMatrix (T.unmarkedColor x) Λ ((splitIndexValue i).1 x) (k x)) *
|
||||
(colorMatrix (T.unmarkedColor x) Λ' (k x) (j x)))) *
|
||||
T.coord (splitIndexValue.symm (j, (splitIndexValue i).2)) := by
|
||||
refine Finset.sum_congr rfl (fun j _ => ?_)
|
||||
rw [toTensorRepMat_mul', Finset.sum_mul]
|
||||
rfl
|
||||
erw [h1]
|
||||
rw [Finset.sum_comm]
|
||||
refine Finset.sum_congr rfl (fun j _ => ?_)
|
||||
rw [Finset.mul_sum]
|
||||
refine Finset.sum_congr rfl (fun k _ => ?_)
|
||||
simp only [toTensorRepMat, IndexValue]
|
||||
rw [← mul_assoc]
|
||||
congr
|
||||
rw [Finset.prod_mul_distrib]
|
||||
rfl
|
||||
|
||||
/-- Notation for `markedLorentzAction.smul`. -/
|
||||
scoped[RealLorentzTensor] infixr:73 " •ₘ " => markedLorentzAction.smul
|
||||
|
||||
/-- Notation for `unmarkedLorentzAction.smul`. -/
|
||||
scoped[RealLorentzTensor] infixr:73 " •ᵤₘ " => unmarkedLorentzAction.smul
|
||||
|
||||
/-- Acting on unmarked and then marked indices is equivalent to acting on all indices. -/
|
||||
lemma marked_unmarked_action_eq_action (T : Marked d X n) : Λ •ₘ (Λ •ᵤₘ T) = Λ • T := by
|
||||
refine ext rfl ?_
|
||||
funext i
|
||||
change ∑ j, toTensorRepMat Λ (splitIndexValue i).2 j *
|
||||
(∑ k, toTensorRepMat Λ (splitIndexValue i).1 k * T.coord (splitIndexValue.symm (k, j))) = _
|
||||
trans ∑ j, ∑ k, (toTensorRepMat Λ (splitIndexValue i).2 j *
|
||||
toTensorRepMat Λ (splitIndexValue i).1 k) * T.coord (splitIndexValue.symm (k, j))
|
||||
apply Finset.sum_congr rfl (fun j _ => ?_)
|
||||
rw [Finset.mul_sum]
|
||||
apply Finset.sum_congr rfl (fun k _ => ?_)
|
||||
exact Eq.symm (mul_assoc _ _ _)
|
||||
trans ∑ j, ∑ k, (toTensorRepMat Λ i (splitIndexValue.symm (k, j))
|
||||
* T.coord (splitIndexValue.symm (k, j)))
|
||||
apply Finset.sum_congr rfl (fun j _ => (Finset.sum_congr rfl (fun k _ => ?_)))
|
||||
rw [mul_comm (toTensorRepMat _ _ _), toTensorRepMat_of_splitIndexValue']
|
||||
simp only [IndexValue, Finset.mem_univ, Prod.mk.eta, Equiv.symm_apply_apply]
|
||||
trans ∑ p, (toTensorRepMat Λ i p * T.coord p)
|
||||
rw [← Equiv.sum_comp splitIndexValue.symm, Fintype.sum_prod_type, Finset.sum_comm]
|
||||
rfl
|
||||
rfl
|
||||
|
||||
/-- Acting on marked and then unmarked indices is equivalent to acting on all indices. -/
|
||||
lemma unmarked_marked_action_eq_action (T : Marked d X n) : Λ •ᵤₘ (Λ •ₘ T) = Λ • T := by
|
||||
refine ext rfl ?_
|
||||
funext i
|
||||
change ∑ j, toTensorRepMat Λ (splitIndexValue i).1 j *
|
||||
(∑ k, toTensorRepMat Λ (splitIndexValue i).2 k * T.coord (splitIndexValue.symm (j, k))) = _
|
||||
trans ∑ j, ∑ k, (toTensorRepMat Λ (splitIndexValue i).1 j *
|
||||
toTensorRepMat Λ (splitIndexValue i).2 k) * T.coord (splitIndexValue.symm (j, k))
|
||||
apply Finset.sum_congr rfl (fun j _ => ?_)
|
||||
rw [Finset.mul_sum]
|
||||
apply Finset.sum_congr rfl (fun k _ => ?_)
|
||||
exact Eq.symm (mul_assoc _ _ _)
|
||||
trans ∑ j, ∑ k, (toTensorRepMat Λ i (splitIndexValue.symm (j, k))
|
||||
* T.coord (splitIndexValue.symm (j, k)))
|
||||
apply Finset.sum_congr rfl (fun j _ => (Finset.sum_congr rfl (fun k _ => ?_)))
|
||||
rw [toTensorRepMat_of_splitIndexValue']
|
||||
simp only [IndexValue, Finset.mem_univ, Prod.mk.eta, Equiv.symm_apply_apply]
|
||||
trans ∑ p, (toTensorRepMat Λ i p * T.coord p)
|
||||
rw [← Equiv.sum_comp splitIndexValue.symm, Fintype.sum_prod_type]
|
||||
rfl
|
||||
rfl
|
||||
|
||||
/-- The marked and unmarked actions commute. -/
|
||||
lemma marked_unmarked_action_comm (T : Marked d X n) : Λ •ᵤₘ (Λ •ₘ T) = Λ •ₘ (Λ •ᵤₘ T) := by
|
||||
rw [unmarked_marked_action_eq_action, marked_unmarked_action_eq_action]
|
||||
|
||||
/-! TODO: Show that the Lorentz action commutes with contraction. -/
|
||||
/-! TODO: Show that the Lorentz action commutes with rising and lowering indices. -/
|
||||
end RealLorentzTensor
|
||||
189
HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
Normal file
189
HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
Normal file
|
|
@ -0,0 +1,189 @@
|
|||
/-
|
||||
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.LorentzTensor.Real.Basic
|
||||
import HepLean.SpaceTime.LorentzTensor.Real.LorentzAction
|
||||
/-!
|
||||
|
||||
# Multiplication of Real Lorentz Tensors along an index
|
||||
|
||||
We define the multiplication of two singularly marked Lorentz tensors along the
|
||||
marked index. This is equivalent to contracting two Lorentz tensors.
|
||||
|
||||
We prove various results about this multiplication.
|
||||
|
||||
-/
|
||||
/-! TODO: Add unit to the multiplication. -/
|
||||
/-! TODO: Generalize to contracting any marked index of a marked tensor. -/
|
||||
/-! TODO: Set up a good notation for the multiplication. -/
|
||||
|
||||
namespace RealLorentzTensor
|
||||
|
||||
variable {d : ℕ} {X Y : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
|
||||
(T : RealLorentzTensor d X) (c : X → Colors) (Λ Λ' : LorentzGroup d) {μ : Colors}
|
||||
|
||||
open Marked
|
||||
|
||||
/-- The contraction of the marked indices of two tensors each with one marked index, which
|
||||
is dual to the others. The contraction is done via
|
||||
`φ^μ ψ_μ = φ^0 ψ_0 + φ^1 ψ_1 + ...`. -/
|
||||
@[simps!]
|
||||
def mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
|
||||
(h : T.markedColor 0 = τ (S.markedColor 0)) :
|
||||
RealLorentzTensor d (X ⊕ Y) where
|
||||
color := Sum.elim T.unmarkedColor S.unmarkedColor
|
||||
coord := fun i => ∑ x,
|
||||
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, oneMarkedIndexValue x)) *
|
||||
S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2,
|
||||
oneMarkedIndexValue $ colorsIndexDualCast h x))
|
||||
|
||||
/-- Multiplication is well behaved with regard to swapping tensors. -/
|
||||
lemma mul_symm {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
|
||||
(h : T.markedColor 0 = τ (S.markedColor 0)) :
|
||||
mapIso d (Equiv.sumComm X Y) (mul T S h) = mul S T (color_eq_dual_symm h) := by
|
||||
refine ext ?_ ?_
|
||||
· funext a
|
||||
cases a with
|
||||
| inl _ => rfl
|
||||
| inr _ => rfl
|
||||
· funext i
|
||||
rw [mapIso_apply_coord, mul_coord, mul_coord]
|
||||
erw [← Equiv.sum_comp (colorsIndexDualCast h).symm]
|
||||
refine Fintype.sum_congr _ _ (fun x => ?_)
|
||||
rw [mul_comm]
|
||||
congr
|
||||
· exact Equiv.apply_symm_apply (colorsIndexDualCast h) x
|
||||
· exact colorsIndexDualCast_symm h
|
||||
|
||||
lemma mul_mapIso {X Y Z : Type} (T : Marked d X 1) (S : Marked d Y 1) (f : X ≃ W)
|
||||
(g : Y ≃ Z) (h : T.markedColor 0 = τ (S.markedColor 0)) :
|
||||
mapIso d (Equiv.sumCongr f g) (mul T S h) = mul (mapIso d (Equiv.sumCongr f (Equiv.refl _)) T)
|
||||
(mapIso d (Equiv.sumCongr g (Equiv.refl _)) S) h := by
|
||||
refine ext ?_ ?_
|
||||
· funext a
|
||||
cases a with
|
||||
| inl _ => rfl
|
||||
| inr _ => rfl
|
||||
· funext i
|
||||
rw [mapIso_apply_coord, mul_coord, mul_coord]
|
||||
refine Fintype.sum_congr _ _ (fun x => ?_)
|
||||
rw [mapIso_apply_coord, mapIso_apply_coord]
|
||||
refine Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl
|
||||
· apply congrArg
|
||||
simp only [IndexValue]
|
||||
exact (Equiv.symm_apply_eq splitIndexValue).mpr rfl
|
||||
· apply congrArg
|
||||
exact (Equiv.symm_apply_eq splitIndexValue).mpr rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Lorentz action and multiplication.
|
||||
|
||||
-/
|
||||
|
||||
/-- The marked Lorentz Action leaves multiplication invariant. -/
|
||||
lemma mul_markedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
|
||||
(h : T.markedColor 0 = τ (S.markedColor 1)) :
|
||||
mul (Λ •ₘ T) (Λ •ₘ S) h = mul T S h := by
|
||||
refine ext rfl ?_
|
||||
funext i
|
||||
change ∑ x, (∑ j, toTensorRepMat Λ (oneMarkedIndexValue x) j *
|
||||
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j))) *
|
||||
(∑ k, toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k *
|
||||
S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))) = _
|
||||
trans ∑ x, ∑ j, ∑ k, (toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k
|
||||
* toTensorRepMat Λ (oneMarkedIndexValue x) j) *
|
||||
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j))
|
||||
* S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))
|
||||
apply Finset.sum_congr rfl (fun x _ => ?_)
|
||||
rw [Finset.sum_mul_sum ]
|
||||
apply Finset.sum_congr rfl (fun j _ => ?_)
|
||||
apply Finset.sum_congr rfl (fun k _ => ?_)
|
||||
ring
|
||||
rw [Finset.sum_comm]
|
||||
trans ∑ j, ∑ k, ∑ x, (toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k
|
||||
* toTensorRepMat Λ (oneMarkedIndexValue x) j) *
|
||||
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j))
|
||||
* S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))
|
||||
apply Finset.sum_congr rfl (fun j _ => ?_)
|
||||
rw [Finset.sum_comm]
|
||||
trans ∑ j, ∑ k, (toTensorRepMat 1
|
||||
(oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k) j) *
|
||||
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j))
|
||||
* S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))
|
||||
apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_))
|
||||
rw [← Finset.sum_mul, ← Finset.sum_mul]
|
||||
erw [toTensorRepMap_sum_dual]
|
||||
rfl
|
||||
rw [Finset.sum_comm]
|
||||
trans ∑ k,
|
||||
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1,
|
||||
(oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k)))*
|
||||
S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))
|
||||
apply Finset.sum_congr rfl (fun k _ => ?_)
|
||||
rw [← Finset.sum_mul, ← toTensorRepMat_one_coord_sum T]
|
||||
rw [← Equiv.sum_comp (oneMarkedIndexValue)]
|
||||
erw [← Equiv.sum_comp (colorsIndexDualCast h)]
|
||||
simp
|
||||
rfl
|
||||
|
||||
/-- The unmarked Lorentz Action commutes with multiplication. -/
|
||||
lemma mul_unmarkedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
|
||||
(h : T.markedColor 0 = τ (S.markedColor 1)) :
|
||||
mul (Λ •ᵤₘ T) (Λ •ᵤₘ S) h = Λ • mul T S h := by
|
||||
refine ext rfl ?_
|
||||
funext i
|
||||
change ∑ x, (∑ j, toTensorRepMat Λ (indexValueSumEquiv i).1 j *
|
||||
T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))*
|
||||
∑ k, toTensorRepMat Λ (indexValueSumEquiv i).2 k *
|
||||
S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x)) = _
|
||||
trans ∑ x, ∑ j, ∑ k, (toTensorRepMat Λ (indexValueSumEquiv i).1 j *
|
||||
T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))*
|
||||
toTensorRepMat Λ (indexValueSumEquiv i).2 k *
|
||||
S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
|
||||
apply Finset.sum_congr rfl (fun x _ => ?_)
|
||||
rw [Finset.sum_mul_sum ]
|
||||
apply Finset.sum_congr rfl (fun j _ => ?_)
|
||||
apply Finset.sum_congr rfl (fun k _ => ?_)
|
||||
ring
|
||||
rw [Finset.sum_comm]
|
||||
trans ∑ j, ∑ k, ∑ x, (toTensorRepMat Λ (indexValueSumEquiv i).1 j *
|
||||
T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))*
|
||||
toTensorRepMat Λ (indexValueSumEquiv i).2 k *
|
||||
S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
|
||||
apply Finset.sum_congr rfl (fun j _ => ?_)
|
||||
rw [Finset.sum_comm]
|
||||
trans ∑ j, ∑ k,
|
||||
((toTensorRepMat Λ (indexValueSumEquiv i).1 j) * toTensorRepMat Λ (indexValueSumEquiv i).2 k)
|
||||
* ∑ x, (T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))
|
||||
* S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
|
||||
apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_))
|
||||
rw [Finset.mul_sum]
|
||||
apply Finset.sum_congr rfl (fun x _ => ?_)
|
||||
ring
|
||||
trans ∑ j, ∑ k, toTensorRepMat Λ i (indexValueSumEquiv.symm (j, k)) *
|
||||
∑ x, (T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))
|
||||
* S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
|
||||
apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_))
|
||||
rw [toTensorRepMat_of_indexValueSumEquiv']
|
||||
congr
|
||||
simp only [IndexValue, Finset.mem_univ, Prod.mk.eta, Equiv.symm_apply_apply, mul_color]
|
||||
trans ∑ p, toTensorRepMat Λ i p *
|
||||
∑ x, (T.coord (splitIndexValue.symm ((indexValueSumEquiv p).1, oneMarkedIndexValue x)))
|
||||
* S.coord (splitIndexValue.symm ((indexValueSumEquiv p).2,
|
||||
oneMarkedIndexValue $ colorsIndexDualCast h x))
|
||||
erw [← Equiv.sum_comp indexValueSumEquiv.symm]
|
||||
rw [Fintype.sum_prod_type]
|
||||
rfl
|
||||
rfl
|
||||
|
||||
/-- The Lorentz action commutes with multiplication. -/
|
||||
lemma mul_lorentzAction (T : Marked d X 1) (S : Marked d Y 1)
|
||||
(h : T.markedColor 0 = τ (S.markedColor 1)) :
|
||||
mul (Λ • T) (Λ • S) h = Λ • mul T S h := by
|
||||
simp only [← marked_unmarked_action_eq_action]
|
||||
rw [mul_markedLorentzAction, mul_unmarkedLorentzAction]
|
||||
|
||||
end RealLorentzTensor
|
||||
1
scripts/nolints.json
Normal file
1
scripts/nolints.json
Normal file
|
|
@ -0,0 +1 @@
|
|||
[]
|
||||
Loading…
Add table
Add a link
Reference in a new issue