refactor: Lorentz action on tensors
This commit is contained in:
jstoobysmith
parent
d385f72087
commit
757afbc60f
3 changed files with 298 additions and 119 deletions
|
|
@ -62,6 +62,10 @@ namespace RealLorentzTensor
|
|||
open Matrix
|
||||
universe u1
|
||||
variable {d : ℕ} {X Y Z : Type}
|
||||
variable (c : X → Colors)
|
||||
|
||||
|
||||
|
||||
|
||||
/-!
|
||||
|
||||
|
|
@ -144,6 +148,11 @@ lemma color_eq_dual_symm {μ ν : Colors} (h : μ = τ ν) : ν = τ μ :=
|
|||
|
||||
-/
|
||||
|
||||
instance [Fintype X] [DecidableEq X] : Fintype (IndexValue d c) := Pi.fintype
|
||||
|
||||
instance [Fintype X] [DecidableEq X] : DecidableEq (IndexValue d c) :=
|
||||
Fintype.decidablePiFintype
|
||||
|
||||
/-- 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
|
||||
|
|
@ -196,10 +205,19 @@ lemma ext' {T₁ T₂ : RealLorentzTensor d X} (h : T₁.color = T₂.color)
|
|||
|
||||
/-- An equivalence between `X → Fin 1 ⊕ Fin d` and `Y → Fin 1 ⊕ Fin d` given an isomorphism
|
||||
between `X` and `Y`. -/
|
||||
@[simps!]
|
||||
def congrSetIndexValue (d : ℕ) (f : X ≃ Y) (i : X → Colors) :
|
||||
IndexValue d i ≃ IndexValue d (i ∘ f.symm) :=
|
||||
Equiv.piCongrLeft' _ f
|
||||
|
||||
@[simp]
|
||||
lemma castColorsIndex_comp_congrSetIndexValue (c : X → Colors) (j : IndexValue d c) (f : X ≃ Y)
|
||||
(h1 : (c <| f.symm <| f <| x) = c x) : (castColorsIndex h1 <| congrSetIndexValue d f c j <| f x)
|
||||
= j x := by
|
||||
rw [congrSetIndexValue_apply]
|
||||
refine cast_eq_iff_heq.mpr ?_
|
||||
rw [Equiv.symm_apply_apply]
|
||||
|
||||
/-- 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
|
||||
|
|
@ -301,60 +319,103 @@ To define contraction and multiplication of Lorentz tensors we need to mark indi
|
|||
|
||||
/-- A `RealLorentzTensor` with `n` marked indices. -/
|
||||
def Marked (d : ℕ) (X : Type) (n : ℕ) : Type :=
|
||||
RealLorentzTensor d (X ⊕ Σ _ : Fin n, PUnit)
|
||||
RealLorentzTensor d (X ⊕ Fin n)
|
||||
|
||||
namespace Marked
|
||||
|
||||
variable {n m : ℕ}
|
||||
|
||||
|
||||
/-- The marked point. -/
|
||||
def markedPoint (X : Type) (i : Fin n) : (X ⊕ Σ _ : Fin n, PUnit) :=
|
||||
Sum.inr ⟨i, PUnit.unit⟩
|
||||
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, PUnit) → Colors :=
|
||||
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
|
||||
|
||||
/-- The index values restricted to marked indices. -/
|
||||
def MarkedIndexValue (T : Marked d X n) : Type :=
|
||||
IndexValue d T.markedColor
|
||||
|
||||
instance [Fintype X] [DecidableEq X] (T : Marked d X n) : Fintype T.MarkedIndexValue :=
|
||||
Pi.fintype
|
||||
|
||||
lemma sumElimIndexColor_of_marked (T : Marked d X n) :
|
||||
sumElimIndexColor T.unmarkedColor T.markedColor = T.color := by
|
||||
ext1 x
|
||||
cases' x <;> rfl
|
||||
|
||||
def toUnmarkedIndexValue {T : Marked d X n} (i : IndexValue d T.color) : UnmarkedIndexValue T :=
|
||||
inlIndexValue <| castIndexValue T.sumElimIndexColor_of_marked.symm <| i
|
||||
|
||||
def toMarkedIndexValue {T : Marked d X n} (i : IndexValue d T.color) : MarkedIndexValue T :=
|
||||
inrIndexValue <| castIndexValue T.sumElimIndexColor_of_marked.symm <| i
|
||||
|
||||
def splitIndexValue {T : Marked d X n} :
|
||||
IndexValue d T.color ≃ UnmarkedIndexValue T × MarkedIndexValue T where
|
||||
toFun i := ⟨toUnmarkedIndexValue i, toMarkedIndexValue i⟩
|
||||
invFun p := castIndexValue T.sumElimIndexColor_of_marked $
|
||||
sumElimIndexValue p.1 p.2
|
||||
left_inv i := by
|
||||
simp_all only [IndexValue]
|
||||
ext1 x
|
||||
cases x with
|
||||
| inl _ => rfl
|
||||
| inr _ => rfl
|
||||
right_inv p := by
|
||||
simp_all only [IndexValue]
|
||||
obtain ⟨fst, snd⟩ := p
|
||||
simp_all only [Prod.mk.injEq]
|
||||
apply And.intro rfl rfl
|
||||
|
||||
@[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) (x : ColorsIndex d (T.color (markedPoint X 0))) :
|
||||
T.MarkedIndexValue := fun i => match i with
|
||||
| ⟨0, PUnit.unit⟩ => x
|
||||
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, PUnit.unit⟩ => x
|
||||
| ⟨1, PUnit.unit⟩ => y
|
||||
| 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, PUnit) ≃
|
||||
(X ⊕ PUnit) ⊕ Σ _ : Fin n, PUnit :=
|
||||
trans (Equiv.sumCongr (Equiv.refl _) $ (Equiv.sigmaPUnit (Fin n.succ)).trans
|
||||
(((Fin.castOrderIso (Nat.succ_eq_one_add n)).toEquiv.trans finSumFinEquiv.symm).trans
|
||||
(Equiv.sumCongr finOneEquiv (Equiv.sigmaPUnit (Fin n)).symm)))
|
||||
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 ⊕ PUnit) n :=
|
||||
def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ Fin 1) n :=
|
||||
congrSet (unmarkFirstSet X n)
|
||||
|
||||
end Marked
|
||||
|
|
@ -371,18 +432,16 @@ 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⟩)) :
|
||||
(h : T.markedColor 0 = τ (S.markedColor 0)) :
|
||||
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))
|
||||
T.coord (splitIndexValue.symm (inlIndexValue i, oneMarkedIndexValue x)) *
|
||||
S.coord (splitIndexValue.symm (inrIndexValue i, 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⟩)) :
|
||||
(h : T.markedColor 0 = τ (S.markedColor 0)) :
|
||||
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 ∘
|
||||
|
|
@ -408,13 +467,11 @@ lemma sumComm_mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
|
|||
-/
|
||||
|
||||
/-- 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⟩)) :
|
||||
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 (castIndexValue T.sumElimIndexColor_of_marked $
|
||||
sumElimIndexValue i $ T.twoMarkedIndexValue x $ congrColorsDual h x)
|
||||
∑ x, T.coord (splitIndexValue.symm (i, T.twoMarkedIndexValue x $ congrColorsDual h x))
|
||||
|
||||
/-! TODO: Following the ethos of modular operads, prove properties of contraction. -/
|
||||
|
||||
|
|
|
|||
|
|
@ -38,7 +38,7 @@ def ofReal (d : ℕ) (r : ℝ) : RealLorentzTensor d Empty where
|
|||
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⟩
|
||||
coord := fun i => v <| i <| Sum.inr <| 0
|
||||
|
||||
/-- A marked 1-tensor with a single down index constructed from a vector.
|
||||
|
||||
|
|
@ -46,7 +46,7 @@ def ofVecUp {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
|
|||
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⟩
|
||||
coord := fun i => v <| i <| Sum.inr <| 0
|
||||
|
||||
/-- A tensor with two up indices constructed from a matrix.
|
||||
|
||||
|
|
@ -54,7 +54,7 @@ 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⟩))
|
||||
coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1))
|
||||
|
||||
/-- A tensor with two down indices constructed from a matrix.
|
||||
|
||||
|
|
@ -62,7 +62,7 @@ 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⟩))
|
||||
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.
|
||||
|
||||
|
|
@ -71,9 +71,9 @@ Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
|
|||
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⟩))
|
||||
| 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.
|
||||
|
||||
|
|
@ -81,9 +81,9 @@ 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⟩))
|
||||
| Sum.inr 0 => Colors.down
|
||||
| Sum.inr 1 => Colors.up
|
||||
coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1))
|
||||
|
||||
/-!
|
||||
|
||||
|
|
@ -94,85 +94,85 @@ def ofMatDownUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
|||
/-- 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, PUnit.unit⟩)
|
||||
toFun i := i (Sum.inr 0)
|
||||
invFun x := fun i => match i with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => x
|
||||
| Sum.inr 0 => x
|
||||
left_inv i := by
|
||||
funext y
|
||||
match y with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => rfl
|
||||
| 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, PUnit.unit⟩)
|
||||
toFun i := i (Sum.inr 0)
|
||||
invFun x := fun i => match i with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => x
|
||||
| Sum.inr 0 => x
|
||||
left_inv i := by
|
||||
funext y
|
||||
match y with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => rfl
|
||||
| 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, PUnit.unit⟩), i (Sum.inr ⟨1, PUnit.unit⟩))
|
||||
toFun i := (i (Sum.inr 0), i (Sum.inr 1))
|
||||
invFun x := fun i => match i with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => x.1
|
||||
| Sum.inr ⟨1, PUnit.unit⟩ => x.2
|
||||
| Sum.inr 0 => x.1
|
||||
| Sum.inr 1 => x.2
|
||||
left_inv i := by
|
||||
funext y
|
||||
match y with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => rfl
|
||||
| Sum.inr ⟨1, PUnit.unit⟩ => rfl
|
||||
| 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, PUnit.unit⟩), i (Sum.inr ⟨1, PUnit.unit⟩))
|
||||
toFun i := (i (Sum.inr 0), i (Sum.inr 1))
|
||||
invFun x := fun i => match i with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => x.1
|
||||
| Sum.inr ⟨1, PUnit.unit⟩ => x.2
|
||||
| Sum.inr 0 => x.1
|
||||
| Sum.inr 1 => x.2
|
||||
left_inv i := by
|
||||
funext y
|
||||
match y with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => rfl
|
||||
| Sum.inr ⟨1, PUnit.unit⟩ => rfl
|
||||
| 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, PUnit.unit⟩), i (Sum.inr ⟨1, PUnit.unit⟩))
|
||||
toFun i := (i (Sum.inr 0), i (Sum.inr 1))
|
||||
invFun x := fun i => match i with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => x.1
|
||||
| Sum.inr ⟨1, PUnit.unit⟩ => x.2
|
||||
| Sum.inr 0 => x.1
|
||||
| Sum.inr 1 => x.2
|
||||
left_inv i := by
|
||||
funext y
|
||||
match y with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => rfl
|
||||
| Sum.inr ⟨1, PUnit.unit⟩ => rfl
|
||||
| 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, PUnit.unit⟩), i (Sum.inr ⟨1, PUnit.unit⟩))
|
||||
toFun i := (i (Sum.inr 0), i (Sum.inr 1))
|
||||
invFun x := fun i => match i with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => x.1
|
||||
| Sum.inr ⟨1, PUnit.unit⟩ => x.2
|
||||
| Sum.inr 0 => x.1
|
||||
| Sum.inr 1 => x.2
|
||||
left_inv i := by
|
||||
funext y
|
||||
match y with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => rfl
|
||||
| Sum.inr ⟨1, PUnit.unit⟩ => rfl
|
||||
| Sum.inr 0 => rfl
|
||||
| Sum.inr 1 => rfl
|
||||
right_inv x := rfl
|
||||
|
||||
/-!
|
||||
|
|
@ -235,7 +235,7 @@ lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d
|
|||
|
||||
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)
|
||||
congrSet ((Equiv.sumEmpty (Empty ⊕ Fin 1) Empty))
|
||||
(mul (unmarkFirst $ ofMatUpDown M) (ofVecUp v) rfl) = ofVecUp (M *ᵥ v) := by
|
||||
refine ext' ?_ ?_
|
||||
· funext i
|
||||
|
|
@ -247,7 +247,7 @@ lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d)
|
|||
|
||||
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)
|
||||
congrSet (Equiv.sumEmpty (Empty ⊕ Fin 1) Empty)
|
||||
(mul (unmarkFirst $ ofMatDownUp M) (ofVecDown v) rfl) = ofVecDown (M *ᵥ v) := by
|
||||
refine ext' ?_ ?_
|
||||
· funext i
|
||||
|
|
@ -326,7 +326,6 @@ lemma lorentzAction_ofMatUpUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)
|
|||
refine Finset.sum_congr rfl (fun x _ => ?_)
|
||||
rw [Finset.sum_mul]
|
||||
refine Finset.sum_congr rfl (fun y _ => ?_)
|
||||
erw [← Equiv.prod_comp (Equiv.sigmaPUnit (Fin 2)).symm]
|
||||
rw [Fin.prod_univ_two]
|
||||
simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
|
||||
rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
|
||||
|
|
@ -346,7 +345,6 @@ lemma lorentzAction_ofMatDownDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d
|
|||
refine Finset.sum_congr rfl (fun x _ => ?_)
|
||||
rw [Finset.sum_mul]
|
||||
refine Finset.sum_congr rfl (fun y _ => ?_)
|
||||
erw [← Equiv.prod_comp (Equiv.sigmaPUnit (Fin 2)).symm]
|
||||
rw [Fin.prod_univ_two]
|
||||
simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
|
||||
rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
|
||||
|
|
@ -366,7 +364,6 @@ lemma lorentzAction_ofMatUpDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)
|
|||
refine Finset.sum_congr rfl (fun x _ => ?_)
|
||||
rw [Finset.sum_mul]
|
||||
refine Finset.sum_congr rfl (fun y _ => ?_)
|
||||
erw [← Equiv.prod_comp (Equiv.sigmaPUnit (Fin 2)).symm]
|
||||
rw [Fin.prod_univ_two]
|
||||
simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
|
||||
rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
|
||||
|
|
@ -387,7 +384,6 @@ lemma lorentzAction_ofMatDownUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)
|
|||
refine Finset.sum_congr rfl (fun x _ => ?_)
|
||||
rw [Finset.sum_mul]
|
||||
refine Finset.sum_congr rfl (fun y _ => ?_)
|
||||
erw [← Equiv.prod_comp (Equiv.sigmaPUnit (Fin 2)).symm]
|
||||
rw [Fin.prod_univ_two]
|
||||
simp only [colorMatrix, Fin.isValue, MonoidHom.coe_mk, OneHom.coe_mk]
|
||||
rw [mul_assoc, mul_comm _ (M _ _), ← mul_assoc]
|
||||
|
|
|
|||
|
|
@ -17,12 +17,13 @@ The Lorentz action is currently only defined for finite and decidable types `X`.
|
|||
|
||||
namespace RealLorentzTensor
|
||||
|
||||
variable {d : ℕ} {X : Type} [Fintype X] [DecidableEq X] (T : RealLorentzTensor d X) (c : X → Colors)
|
||||
variable {d : ℕ} {X Y : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
|
||||
variable (T : RealLorentzTensor d X) (c : X → Colors)
|
||||
variable (Λ Λ' : LorentzGroup d)
|
||||
open LorentzGroup
|
||||
open BigOperators
|
||||
|
||||
instance : Fintype (IndexValue d c) := Pi.fintype
|
||||
|
||||
variable {μ : Colors}
|
||||
|
||||
/-- Monoid homomorphism from the Lorentz group to matrices indexed by `ColorsIndex d μ` for a
|
||||
|
|
@ -56,88 +57,159 @@ def colorMatrix (μ : Colors) : LorentzGroup d →* Matrix (ColorsIndex d μ) (C
|
|||
Matrix.transpose_mul, Matrix.transpose_apply]
|
||||
rfl
|
||||
|
||||
/-- A real number occuring in the action of the Lorentz group on Lorentz tensors. -/
|
||||
@[simp]
|
||||
def prodColorMatrixOnIndexValue (i j : IndexValue d c) : ℝ :=
|
||||
∏ x, colorMatrix (c x) Λ (i x) (j x)
|
||||
|
||||
/-- `prodColorMatrixOnIndexValue` evaluated at `1` on the diagonal returns `1`. -/
|
||||
lemma one_prodColorMatrixOnIndexValue_on_diag (i : IndexValue d c) :
|
||||
prodColorMatrixOnIndexValue c 1 i i = 1 := by
|
||||
simp only [prodColorMatrixOnIndexValue]
|
||||
rw [Finset.prod_eq_one]
|
||||
intro x _
|
||||
simp only [colorMatrix, MonoidHom.map_one, Matrix.one_apply]
|
||||
lemma colorMatrix_cast {μ ν : Colors} (h : μ = ν) (Λ : LorentzGroup d) :
|
||||
colorMatrix μ Λ =
|
||||
Matrix.reindex (castColorsIndex h).symm (castColorsIndex h).symm (colorMatrix ν Λ) := by
|
||||
subst h
|
||||
rfl
|
||||
|
||||
/-- `prodColorMatrixOnIndexValue` evaluated at `1` off the diagonal returns `0`. -/
|
||||
lemma one_prodColorMatrixOnIndexValue_off_diag {i j : IndexValue d c} (hij : j ≠ i) :
|
||||
prodColorMatrixOnIndexValue c 1 i j = 0 := by
|
||||
simp only [prodColorMatrixOnIndexValue]
|
||||
obtain ⟨x, hijx⟩ := Function.ne_iff.mp hij
|
||||
rw [@Finset.prod_eq_zero _ _ _ _ _ x]
|
||||
exact Finset.mem_univ x
|
||||
simp only [map_one]
|
||||
exact Matrix.one_apply_ne' hijx
|
||||
/-- A real number occuring in the action of the Lorentz group on Lorentz tensors. -/
|
||||
@[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]
|
||||
apply Finset.sum_congr
|
||||
simp only [IndexValue, Fintype.piFinset_univ]
|
||||
intro x _
|
||||
rfl
|
||||
rw [h1]
|
||||
simp only [map_mul]
|
||||
exact Finset.prod_congr rfl (fun x _ => rfl)
|
||||
refine Finset.sum_congr rfl (fun k _ => ?_)
|
||||
rw [Finset.prod_mul_distrib]
|
||||
|
||||
lemma mul_prodColorMatrixOnIndexValue (i j : IndexValue d c) :
|
||||
prodColorMatrixOnIndexValue c (Λ * Λ') i j =
|
||||
∑ (k : IndexValue d c),
|
||||
∏ x, (colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x)) := by
|
||||
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]
|
||||
apply Finset.sum_congr
|
||||
simp only [IndexValue, Fintype.piFinset_univ]
|
||||
intro x _
|
||||
rfl
|
||||
rw [h1]
|
||||
simp only [prodColorMatrixOnIndexValue, map_mul]
|
||||
exact Finset.prod_congr rfl (fun x _ => rfl)
|
||||
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]
|
||||
refine Finset.sum_congr rfl (fun k _ => ?_)
|
||||
rw [Finset.prod_mul_distrib]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma toTensorRepMat_on_sum {cX : X → Colors} {cY : Y → Colors}
|
||||
(i j : IndexValue d (sumElimIndexColor cX cY)) :
|
||||
toTensorRepMat Λ i j = toTensorRepMat Λ (inlIndexValue i) (inlIndexValue j) *
|
||||
toTensorRepMat Λ (inrIndexValue i) (inrIndexValue j) := by
|
||||
simp only [toTensorRepMat_apply]
|
||||
rw [Fintype.prod_sum_type]
|
||||
rfl
|
||||
|
||||
open Marked
|
||||
|
||||
lemma toTensorRepMap_on_splitIndexValue (T : Marked d X n)
|
||||
(i : T.UnmarkedIndexValue) (k : T.MarkedIndexValue) (j : IndexValue d T.color) :
|
||||
toTensorRepMat Λ (splitIndexValue.symm (i, k)) j =
|
||||
toTensorRepMat Λ i (toUnmarkedIndexValue j) *
|
||||
toTensorRepMat Λ k (toMarkedIndexValue j) := by
|
||||
simp only [toTensorRepMat_apply]
|
||||
rw [Fintype.prod_sum_type]
|
||||
rfl
|
||||
|
||||
/-!
|
||||
|
||||
## 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, prodColorMatrixOnIndexValue T.color Λ i j * T.coord j}
|
||||
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]
|
||||
rw [one_prodColorMatrixOnIndexValue_on_diag]
|
||||
simp only [one_mul, IndexValue]
|
||||
simp only [Matrix.one_apply_eq, one_mul, IndexValue]
|
||||
rfl
|
||||
exact Finset.mem_univ i
|
||||
intro j _ hij
|
||||
rw [one_prodColorMatrixOnIndexValue_off_diag]
|
||||
simp only [zero_mul]
|
||||
exact hij
|
||||
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, prodColorMatrixOnIndexValue T.color (Λ * Λ') i j
|
||||
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 [mul_prodColorMatrixOnIndexValue, Finset.sum_mul]
|
||||
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 [prodColorMatrixOnIndexValue, IndexValue]
|
||||
simp only [toTensorRepMat, IndexValue]
|
||||
rw [← mul_assoc]
|
||||
congr
|
||||
rw [Finset.prod_mul_distrib]
|
||||
rfl
|
||||
|
||||
/-!
|
||||
|
||||
## The Lorentz action on marked tensors.
|
||||
|
||||
-/
|
||||
|
||||
@[simps!]
|
||||
instance : MulAction (LorentzGroup d) (Marked d X n) := lorentzAction
|
||||
instance : MulAction (LorentzGroup d) (Marked d X n) := lorentzAction
|
||||
|
||||
lemma lorentzAction_on_splitIndexValue' (T : Marked d X n)
|
||||
(i : T.UnmarkedIndexValue) (k : T.MarkedIndexValue) :
|
||||
(Λ • T).coord (splitIndexValue.symm (i, k)) =
|
||||
∑ (x : T.UnmarkedIndexValue), ∑ (y : T.MarkedIndexValue),
|
||||
(toTensorRepMat Λ i x * toTensorRepMat Λ k y) * T.coord (splitIndexValue.symm (x, y)) := by
|
||||
erw [lorentzAction_smul_coord]
|
||||
erw [← Equiv.sum_comp splitIndexValue.symm]
|
||||
rw [Fintype.sum_prod_type]
|
||||
refine Finset.sum_congr rfl (fun x _ => ?_)
|
||||
refine Finset.sum_congr rfl (fun y _ => ?_)
|
||||
erw [toTensorRepMap_on_splitIndexValue]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma lorentzAction_on_splitIndexValue (T : Marked d X n)
|
||||
(i : T.UnmarkedIndexValue) (k : T.MarkedIndexValue) :
|
||||
(Λ • T).coord (splitIndexValue.symm (i, k)) =
|
||||
∑ (x : T.UnmarkedIndexValue), toTensorRepMat Λ i x *
|
||||
∑ (y : T.MarkedIndexValue), toTensorRepMat Λ k y *
|
||||
T.coord (splitIndexValue.symm (x, y)) := by
|
||||
rw [lorentzAction_on_splitIndexValue']
|
||||
refine Finset.sum_congr rfl (fun x _ => ?_)
|
||||
rw [Finset.mul_sum]
|
||||
refine Finset.sum_congr rfl (fun y _ => ?_)
|
||||
rw [NonUnitalRing.mul_assoc]
|
||||
|
||||
|
||||
/-!
|
||||
|
||||
## 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) :
|
||||
|
|
@ -146,8 +218,62 @@ lemma lorentzAction_on_isEmpty [IsEmpty X] (Λ : LorentzGroup d) (T : RealLorent
|
|||
funext i
|
||||
erw [lorentzAction_smul_coord]
|
||||
simp only [Finset.univ_unique, Finset.univ_eq_empty, Finset.prod_empty, one_mul,
|
||||
Finset.sum_singleton]
|
||||
simp only [IndexValue, Unique.eq_default]
|
||||
Finset.sum_singleton, toTensorRepMat_apply]
|
||||
erw [toTensorRepMat_apply]
|
||||
simp only [IndexValue, toTensorRepMat, Unique.eq_default]
|
||||
rw [@mul_left_eq_self₀]
|
||||
exact Or.inl rfl
|
||||
|
||||
/-- The Lorentz action commutes with `congrSet`. -/
|
||||
lemma lorentzAction_comm_congrSet (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzTensor d X) :
|
||||
congrSet f (Λ • T) = Λ • (congrSet f T) := by
|
||||
refine ext' rfl ?_
|
||||
funext i
|
||||
erw [lorentzAction_smul_coord, lorentzAction_smul_coord]
|
||||
erw [← Equiv.sum_comp (congrSetIndexValue d f T.color)]
|
||||
refine Finset.sum_congr rfl (fun j _ => ?_)
|
||||
simp [toTensorRepMat]
|
||||
erw [← Equiv.prod_comp f]
|
||||
apply Or.inl
|
||||
congr
|
||||
funext x
|
||||
have h1 : (T.color (f.symm (f x))) = T.color x := by
|
||||
simp only [Equiv.symm_apply_apply]
|
||||
rw [colorMatrix_cast h1]
|
||||
simp only [Matrix.reindex_apply, Equiv.symm_symm, Matrix.submatrix_apply]
|
||||
erw [castColorsIndex_comp_congrSetIndexValue]
|
||||
apply congrFun
|
||||
apply congrArg
|
||||
symm
|
||||
refine cast_eq_iff_heq.mpr ?_
|
||||
simp only [congrSetIndexValue, Equiv.piCongrLeft'_symm_apply, heq_eqRec_iff_heq, heq_eq_eq]
|
||||
rfl
|
||||
|
||||
open Marked
|
||||
|
||||
lemma lorentzAction_comm_mul (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
|
||||
trans ∑ j, toTensorRepMat Λ (inlIndexValue i) (inlIndexValue j) *
|
||||
toTensorRepMat Λ (inrIndexValue i) (inrIndexValue j)
|
||||
* (mul T S h).coord j
|
||||
swap
|
||||
refine Finset.sum_congr rfl (fun j _ => ?_)
|
||||
erw [toTensorRepMat_on_sum]
|
||||
rfl
|
||||
change ∑ x, (∑ j, toTensorRepMat Λ (splitIndexValue.symm
|
||||
(inlIndexValue i, T.oneMarkedIndexValue x)) j * T.coord j) *
|
||||
(∑ k, toTensorRepMat Λ _ k * S.coord k) = _
|
||||
trans ∑ x, (∑ j,
|
||||
toTensorRepMat Λ (inlIndexValue i) (toUnmarkedIndexValue j)
|
||||
* toTensorRepMat Λ (T.oneMarkedIndexValue x) (toMarkedIndexValue j)
|
||||
* T.coord j) *
|
||||
|
||||
sorry
|
||||
|
||||
|
||||
|
||||
/-! TODO: Show that the Lorentz action commutes with multiplication. -/
|
||||
/-! TODO: Show that the Lorentz action commutes with contraction. -/
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue