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

refactor: Partial major refactor wip

Browse source
This commit is contained in:
jstoobysmith 2024-07-23 08:54:53 -04:00
parent 782f4929d1
commit f90fa1ac1a
6 changed files with 636 additions and 188 deletions
Download patch file Download diff file Expand all files Collapse all files

284
HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
View file

@ -9,6 +9,9 @@ import Mathlib.Data.Fintype.BigOperators
import Mathlib.Logic.Equiv.Fin
import Mathlib.Tactic.FinCases
import Mathlib.Logic.Equiv.Fintype
import Mathlib.Algebra.Module.Pi
import Mathlib.Algebra.Module.Equiv
import Mathlib.Algebra.Module.LinearMap.Basic
/-!
# Real Lorentz Tensors
@ -53,12 +56,24 @@ instance (d : ℕ) (μ : RealLorentzTensor.Colors) : DecidableEq (RealLorentzTen
def RealLorentzTensor.IndexValue {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) :
Type 0 := (x : X) → RealLorentzTensor.ColorsIndex d (c x)
def RealLorentzTensor.ColorFiber {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) : Type :=
RealLorentzTensor.IndexValue d c → ℝ
instance {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) :
AddCommMonoid (RealLorentzTensor.ColorFiber d c) := Pi.addCommMonoid
instance {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) :
Module ℝ (RealLorentzTensor.ColorFiber d c) := Pi.module _ _ _
instance {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) :
AddCommGroup (RealLorentzTensor.ColorFiber d c) := Pi.addCommGroup
/-- 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 → ℝ
coord : RealLorentzTensor.ColorFiber d color
namespace RealLorentzTensor
open Matrix
@ -85,6 +100,9 @@ lemma τ_involutive : Function.Involutive τ := by
lemma color_eq_dual_symm {μ ν : Colors} (h : μ = τ ν) : ν = τ μ :=
(Function.Involutive.eq_iff τ_involutive).mp h.symm
lemma color_comp_τ_symm {c1 c2 : X → Colors} (h : c1 = τ ∘ c2) : c2 = τ ∘ c1 :=
funext (fun x => color_eq_dual_symm (congrFun h x))
/-- 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
@ -93,6 +111,11 @@ def colorsIndexCast {d : ℕ} {μ₁ μ₂ : RealLorentzTensor.Colors} (h : μ
ColorsIndex d μ₁ ≃ ColorsIndex d μ₂ :=
Equiv.cast (congrArg (ColorsIndex d) h)
@[simp]
lemma colorsIndexCast_symm {d : ℕ} {μ₁ μ₂ : RealLorentzTensor.Colors} (h : μ₁ = μ₂) :
(@colorsIndexCast d _ _ h).symm = colorsIndexCast h.symm := by
rfl
/-- An equivalence of `ColorsIndex` between that of a color and that of its dual. -/
def colorsIndexDualCastSelf {d : ℕ} {μ : RealLorentzTensor.Colors}:
ColorsIndex d μ ≃ ColorsIndex d (τ μ) where
@ -112,6 +135,7 @@ def colorsIndexDualCast {μ ν : Colors} (h : μ = τ ν) :
ColorsIndex d μ ≃ ColorsIndex d ν :=
(colorsIndexCast h).trans colorsIndexDualCastSelf.symm
@[simp]
lemma colorsIndexDualCast_symm {μ ν : Colors} (h : μ = τ ν) :
(colorsIndexDualCast h).symm =
@colorsIndexDualCast d _ _ ((Function.Involutive.eq_iff τ_involutive).mp h.symm) := by
@ -119,6 +143,31 @@ lemma colorsIndexDualCast_symm {μ ν : Colors} (h : μ = τ ν) :
| Colors.up, Colors.down => rfl
| Colors.down, Colors.up => rfl
@[simp]
lemma colorsIndexDualCast_trans {μ ν ξ : Colors} (h : μ = τ ν) (h' : ν = τ ξ) :
(@colorsIndexDualCast d _ _ h).trans (colorsIndexDualCast h') =
colorsIndexCast (by rw [h, h', τ_involutive]) := by
match μ, ν, ξ with
| Colors.up, Colors.down, Colors.up => rfl
| Colors.down, Colors.up, Colors.down => rfl
@[simp]
lemma colorsIndexDualCast_trans_colorsIndexCast {μ ν ξ : Colors} (h : μ = τ ν) (h' : ν = ξ) :
(@colorsIndexDualCast d _ _ h).trans (colorsIndexCast h') =
colorsIndexDualCast (by rw [h, h']) := by
match μ, ν, ξ with
| Colors.down, Colors.up, Colors.up => rfl
| Colors.up, Colors.down, Colors.down => rfl
@[simp]
lemma colorsIndexCast_trans_colorsIndexDualCast {μ ν ξ : Colors} (h : μ = ν) (h' : ν = τ ξ) :
(colorsIndexCast h).trans (@colorsIndexDualCast d _ _ h') =
colorsIndexDualCast (by rw [h, h']) := by
match μ, ν, ξ with
| Colors.up, Colors.up, Colors.down => rfl
| Colors.down, Colors.down, Colors.up => rfl
/-!
## Index values
@ -137,12 +186,12 @@ instance [Fintype X] : DecidableEq (IndexValue d c) :=
-/
/-- 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
@[simp]
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
@ -159,9 +208,10 @@ lemma indexValueIso_trans (d : ℕ) (f : X ≃ Y) (g : Y ≃ Z) {i : X → Color
exact Equiv.coe_inj.mp rfl
simpa only [Equiv.symm_symm] using congrArg (fun e => e.symm) h1
@[simp]
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
indexValueIso d f.symm ((Equiv.eq_comp_symm f j i).mpr h.symm) := by
ext i : 1
rw [← Equiv.symm_apply_eq]
funext y
@ -172,7 +222,7 @@ lemma indexValueIso_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
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
(indexValueIso d f.symm ((Equiv.eq_comp_symm f j i).mpr h.symm)).symm := by
rw [indexValueIso_symm]
rfl
@ -188,10 +238,161 @@ lemma indexValueIso_refl (d : ℕ) (i : X → Colors) :
-/
/-- The isomorphism between the index values of a color map and its dual. -/
def indexValueDualIso (d : ℕ) {i : X → Colors} {j : Y → Colors} (e : X ≃ Y)
(h : i = τ ∘ j ∘ e) : IndexValue d i ≃ IndexValue d j :=
(Equiv.piCongrRight (fun μ => colorsIndexDualCast (congrFun h μ))).trans $
Equiv.piCongrLeft (fun y => ColorsIndex d (j y)) e
lemma indexValueDualIso_symm_apply' (d : ℕ) {i : X → Colors} {j : Y → Colors} (e : X ≃ Y)
(h : i = τ ∘ j ∘ e) (y : IndexValue d j) (x : X) :
(indexValueDualIso d e h).symm y x = (colorsIndexDualCast (congrFun h x)).symm (y (e x)) := by
rfl
lemma indexValueDualIso_cond_symm {i : X → Colors} {j : Y → Colors} {e : X ≃ Y}
(h : i = τ ∘ j ∘ e) : j = τ ∘ i ∘ e.symm := by
subst h
simp only [Function.comp.assoc, Equiv.self_comp_symm, CompTriple.comp_eq]
rw [← Function.comp.assoc]
funext a
simp only [τ_involutive, Function.Involutive.comp_self, Function.comp_apply, id_eq]
@[simp]
lemma indexValueDualIso_symm {d : ℕ} {i : X → Colors} {j : Y → Colors} (e : X ≃ Y)
(h : i = τ ∘ j ∘ e) : (indexValueDualIso d e h).symm =
indexValueDualIso d e.symm (indexValueDualIso_cond_symm h) := by
ext i : 1
rw [← Equiv.symm_apply_eq]
funext a
rw [indexValueDualIso_symm_apply', indexValueDualIso_symm_apply']
erw [← Equiv.trans_apply, colorsIndexDualCast_symm, colorsIndexDualCast_symm,
colorsIndexDualCast_trans]
simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_apply]
apply cast_eq_iff_heq.mpr
rw [Equiv.apply_symm_apply]
lemma indexValueDualIso_eq_symm {d : ℕ} {i : X → Colors} {j : Y → Colors} (e : X ≃ Y)
(h : i = τ ∘ j ∘ e) :
indexValueDualIso d e h = (indexValueDualIso d e.symm (indexValueDualIso_cond_symm h)).symm := by
rw [indexValueDualIso_symm]
simp
lemma indexValueDualIso_cond_trans {i : X → Colors} {j : Y → Colors} {k : Z → Colors}
{e : X ≃ Y} {f : Y ≃ Z} (h : i = τ ∘ j ∘ e) (h' : j = τ ∘ k ∘ f) :
i = k ∘ (e.trans f) := by
rw [h, h']
funext a
simp only [Function.comp_apply, Equiv.coe_trans]
rw [τ_involutive]
@[simp]
lemma indexValueDualIso_trans {d : ℕ} {i : X → Colors} {j : Y → Colors} {k : Z → Colors}
(e : X ≃ Y) (f : Y ≃ Z) (h : i = τ ∘ j ∘ e) (h' : j = τ ∘ k ∘ f) :
(indexValueDualIso d e h).trans (indexValueDualIso d f h') =
indexValueIso d (e.trans f) (indexValueDualIso_cond_trans h h') := by
ext i
rw [Equiv.trans_apply]
rw [← Equiv.eq_symm_apply, ← Equiv.eq_symm_apply, indexValueIso_eq_symm]
funext a
rw [indexValueDualIso_symm_apply', indexValueDualIso_symm_apply',
indexValueIso_symm_apply']
erw [← Equiv.trans_apply]
rw [colorsIndexDualCast_symm, colorsIndexDualCast_symm, colorsIndexDualCast_trans]
simp only [Function.comp_apply, colorsIndexCast, Equiv.symm_trans_apply, Equiv.cast_symm,
Equiv.cast_apply, cast_cast]
symm
apply cast_eq_iff_heq.mpr
rw [Equiv.symm_apply_apply, Equiv.symm_apply_apply]
lemma indexValueDualIso_cond_trans_indexValueIso {i : X → Colors} {j : Y → Colors} {k : Z → Colors}
{e : X ≃ Y} {f : Y ≃ Z} (h : i = τ ∘ j ∘ e) (h' : j = k ∘ f) :
i = τ ∘ k ∘ (e.trans f) := by
rw [h, h']
funext a
simp only [Function.comp_apply, Equiv.coe_trans]
@[simp]
lemma indexValueDualIso_trans_indexValueIso {d : ℕ} {i : X → Colors} {j : Y → Colors} {k : Z → Colors}
(e : X ≃ Y) (f : Y ≃ Z) (h : i = τ ∘ j ∘ e) (h' : j = k ∘ f) :
(indexValueDualIso d e h).trans (indexValueIso d f h') =
indexValueDualIso d (e.trans f) (indexValueDualIso_cond_trans_indexValueIso h h') := by
ext i
rw [Equiv.trans_apply, ← Equiv.eq_symm_apply]
funext a
rw [ indexValueDualIso_eq_symm, indexValueDualIso_symm_apply',
indexValueIso_symm_apply',indexValueDualIso_eq_symm, indexValueDualIso_symm_apply']
rw [Equiv.symm_apply_eq]
erw [← Equiv.trans_apply, ← Equiv.trans_apply]
simp only [Function.comp_apply, Equiv.symm_trans_apply, colorsIndexDualCast_symm,
colorsIndexCast_symm, colorsIndexCast_trans_colorsIndexDualCast, colorsIndexDualCast_trans]
simp only [colorsIndexCast, Equiv.cast_apply]
symm
apply cast_eq_iff_heq.mpr
rw [Equiv.symm_apply_apply]
lemma indexValueIso_trans_indexValueDualIso_cond {i : X → Colors} {j : Y → Colors} {k : Z → Colors}
{e : X ≃ Y} {f : Y ≃ Z} (h : i = j ∘ e) (h' : j = τ ∘ k ∘ f) :
i = τ ∘ k ∘ (e.trans f) := by
rw [h, h']
funext a
simp only [Function.comp_apply, Equiv.coe_trans]
@[simp]
lemma indexValueIso_trans_indexValueDualIso {d : ℕ} {i : X → Colors} {j : Y → Colors} {k : Z → Colors}
(e : X ≃ Y) (f : Y ≃ Z) (h : i = j ∘ e) (h' : j = τ ∘ k ∘ f) :
(indexValueIso d e h).trans (indexValueDualIso d f h') =
indexValueDualIso d (e.trans f) (indexValueIso_trans_indexValueDualIso_cond h h') := by
ext i
rw [Equiv.trans_apply, ← Equiv.eq_symm_apply, ← Equiv.eq_symm_apply]
funext a
rw [indexValueIso_symm_apply', indexValueDualIso_symm_apply',
indexValueDualIso_eq_symm, indexValueDualIso_symm_apply']
erw [← Equiv.trans_apply, ← Equiv.trans_apply]
simp only [Function.comp_apply, Equiv.symm_trans_apply, colorsIndexDualCast_symm,
colorsIndexCast_symm, colorsIndexDualCast_trans_colorsIndexCast, colorsIndexDualCast_trans]
simp only [colorsIndexCast, Equiv.cast_apply]
symm
apply cast_eq_iff_heq.mpr
rw [Equiv.symm_apply_apply, Equiv.symm_apply_apply]
/-!
## Mapping isomorphisms on fibers
-/
@[simps!]
def indexValueDualIso (d : ℕ) {i j : X → Colors} (h : i = τ ∘ j) :
IndexValue d i ≃ IndexValue d j :=
(Equiv.piCongrRight (fun μ => colorsIndexDualCast (congrFun h μ)))
def mapIsoFiber (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors} (h : i = j ∘ f) :
ColorFiber d i ≃ₗ[ℝ] ColorFiber d j where
toFun F := F ∘ (indexValueIso d f h).symm
invFun F := F ∘ indexValueIso d f h
map_add' F G := by rfl
map_smul' a F := by rfl
left_inv F := by
funext x
simp only [Function.comp_apply]
exact congrArg _ $ Equiv.symm_apply_apply (indexValueIso d f h) x
right_inv F := by
funext x
simp only [Function.comp_apply]
exact congrArg _ $ Equiv.apply_symm_apply (indexValueIso d f h) x
@[simp]
lemma mapIsoFiber_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) :
(mapIsoFiber d f h).trans (mapIsoFiber d g h') =
mapIsoFiber d (f.trans g) (by rw [h, h', Function.comp.assoc]; rfl) := by
refine LinearEquiv.toEquiv_inj.mp (Equiv.ext (fun x => (funext (fun a => ?_))))
simp only [LinearEquiv.coe_toEquiv, LinearEquiv.trans_apply, mapIsoFiber_apply,
indexValueIso_symm, ← Equiv.trans_apply, indexValueIso_trans]
rfl
lemma mapIsoFiber_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
(mapIsoFiber d f h).symm = mapIsoFiber d f.symm ((Equiv.eq_comp_symm f j i).mpr h.symm) := by
refine LinearEquiv.toEquiv_inj.mp (Equiv.ext (fun x => (funext (fun a => ?_))))
simp only [LinearEquiv.coe_toEquiv, mapIsoFiber_symm_apply, mapIsoFiber_apply, indexValueIso_symm,
Equiv.symm_symm]
/-!
@ -200,62 +401,40 @@ def indexValueDualIso (d : ℕ) {i j : X → Colors} (h : i = τ ∘ j) :
-/
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
(h' : T₁.coord = mapIsoFiber d (Equiv.refl X) h.symm T₂.coord) : 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.
## 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}
toFun T := ⟨T.color ∘ f.symm, mapIsoFiber d f (by funext x; simp) T.coord⟩
invFun T := ⟨T.color ∘ f, (mapIsoFiber d f (by funext x; simp)).symm T.coord⟩
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
· simp only [Function.comp_apply, ← LinearEquiv.trans_apply, mapIsoFiber_symm,
mapIsoFiber_trans]
congr
exact Equiv.symm_apply_apply f x
exact Equiv.self_trans_symm f
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
· simp only [Function.comp_apply, ← LinearEquiv.trans_apply, mapIsoFiber_symm,
mapIsoFiber_trans]
congr
exact Equiv.apply_symm_apply f x
exact Equiv.symm_trans_self f
@[simp]
lemma mapIso_trans (f : X ≃ Y) (g : Y ≃ Z) :
@ -263,16 +442,17 @@ lemma mapIso_trans (f : X ≃ Y) (g : Y ≃ Z) :
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]
simp
erw [← LinearEquiv.trans_apply, ← LinearEquiv.trans_apply, mapIsoFiber_trans, mapIsoFiber_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_symm (f : X ≃ Y) : (mapIso d f).symm = mapIso d f.symm := by
refine Equiv.coe_inj.mp ?_
funext T
refine ext rfl ?_
erw [← LinearEquiv.trans_apply]
rw [mapIso_symm_apply_coord, mapIsoFiber_trans, mapIsoFiber_symm]
rfl
lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl
@ -302,6 +482,16 @@ 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)
def indexValueFinOne {c : Fin 1 → Colors} :
ColorsIndex d (c 0) ≃ IndexValue d c 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
/-!
## Marked Lorentz tensors

8
HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
View file

@ -238,7 +238,7 @@ lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1
/-- Multiplying `ofVecUp` with `ofVecDown` gives the dot product. -/
@[simp]
lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
mul (ofVecUp v₁) (ofVecDown v₂) rfl = (toReal d instIsEmptySum).symm (v₁ ⬝ᵥ v₂) := by
multMarked (ofVecUp v₁) (ofVecDown v₂) rfl = (toReal d instIsEmptySum).symm (v₁ ⬝ᵥ v₂) := by
refine ext ?_ rfl
· funext i
exact IsEmpty.elim instIsEmptySum i
@ -246,7 +246,7 @@ lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d
/-- Multiplying `ofVecDown` with `ofVecUp` gives the dot product. -/
@[simp]
lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
mul (ofVecDown v₁) (ofVecUp v₂) rfl = (toReal d instIsEmptySum).symm (v₁ ⬝ᵥ v₂) := by
multMarked (ofVecDown v₁) (ofVecUp v₂) rfl = (toReal d instIsEmptySum).symm (v₁ ⬝ᵥ v₂) := by
refine ext ?_ rfl
· funext i
exact IsEmpty.elim instIsEmptySum i
@ -254,7 +254,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 → ℝ) :
mapIso d ((Equiv.sumEmpty (Empty ⊕ Fin 1) Empty))
(mul (unmarkFirst $ ofMatUpDown M) (ofVecUp v) rfl) = ofVecUp (M *ᵥ v) := by
(multMarked (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]
@ -264,7 +264,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 → ℝ) :
mapIso d (Equiv.sumEmpty (Empty ⊕ Fin 1) Empty)
(mul (unmarkFirst $ ofMatDownUp M) (ofVecDown v) rfl) = ofVecDown (M *ᵥ v) := by
(multMarked (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]

155
HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
View file

@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
-/
import HepLean.SpaceTime.LorentzTensor.Real.Basic
import HepLean.SpaceTime.LorentzGroup.Basic
import Mathlib.RepresentationTheory.Basic
/-!
# Lorentz group action on Real Lorentz Tensors
@ -31,44 +32,49 @@ def colorMatrix (μ : Colors) : LorentzGroup d →* Matrix (ColorsIndex d μ) (C
| .up => fun i j => Λ.1 i j
| .down => fun i j => (LorentzGroup.transpose Λ⁻¹).1 i j
map_one' := by
ext i j
match μ with
| .up =>
simp only [lorentzGroupIsGroup_one_coe]
ext i j
simp only [OfNat.ofNat, One.one, ColorsIndex]
simp only [lorentzGroupIsGroup_one_coe, 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
ext i j
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
colorMatrix ν Λ =
Matrix.reindex (colorsIndexCast h) (colorsIndexCast h) (colorMatrix μ Λ) := by
subst h
rfl
lemma colorMatrix_dual_cast {μ : Colors} (Λ : LorentzGroup d) :
colorMatrix (τ μ) Λ = Matrix.reindex (colorsIndexDualCastSelf) (colorsIndexDualCastSelf)
lemma colorMatrix_dual_cast {μ ν : Colors} (Λ : LorentzGroup d) (h : μ = τ ν) :
colorMatrix ν Λ = Matrix.reindex (colorsIndexDualCast h) (colorsIndexDualCast h)
(colorMatrix μ (LorentzGroup.transpose Λ⁻¹)) := by
match μ with
| .up => rfl
subst h
match ν with
| .up =>
ext i j
simp only [colorMatrix, MonoidHom.coe_mk, OneHom.coe_mk, τ, transpose, lorentzGroupIsGroup_inv,
Matrix.transpose_apply, minkowskiMetric.dual_transpose, minkowskiMetric.dual_dual,
Matrix.reindex_apply, colorsIndexDualCast_symm, Matrix.submatrix_apply]
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]
rfl
lemma colorMatrix_transpose {μ : Colors} (Λ : LorentzGroup d) :
colorMatrix μ (LorentzGroup.transpose Λ) = (colorMatrix μ Λ).transpose := by
match μ with
@ -144,6 +150,52 @@ lemma toTensorRepMat_of_indexValueSumEquiv' {cX : X → Colors} {cY : Y → Colo
-/
lemma toTensorRepMat_oneMarkedIndexValue_inv {f1 f2 : X → Colors} (hc : f1 = τ ∘ f2)
(i : IndexValue d f1) (k : IndexValue d f2) :
toTensorRepMat Λ ((indexValueDualIso d (Equiv.refl _) hc) i) k =
toTensorRepMat Λ⁻¹ (indexValueDualIso d (Equiv.refl _) (color_comp_τ_symm hc) k) i := by
rw [toTensorRepMat_apply, toTensorRepMat_apply]
apply Finset.prod_congr rfl (fun x _ => ?_)
rw [colorMatrix_cast (congrFun hc x)]
erw [colorMatrix_dual_cast]
rw [Matrix.reindex_apply, Matrix.reindex_apply]
simp
rw [colorMatrix_transpose]
simp
apply congrArg
simp
have colorsIndexDualCast_colorsIndexCast (μ1 μ2 : Colors) (h : μ1 = τ μ2) (x : ColorsIndex d μ2) :
colorsIndexDualCastSelf.symm ((colorsIndexCast h)
((colorsIndexDualCast (color_eq_dual_symm h)) x))= x := by
match μ1, μ2 with
| .up, .up => rfl
| .down, .down => rfl
| .up, .down => rfl
| .down, .up => rfl
rw [colorsIndexDualCast_colorsIndexCast]
lemma toTensorRepMat_indexValueDualIso {f1 f2 : X → Colors} (hc : f1 = τ ∘ f2)
(j : IndexValue d f1) (k : IndexValue d f2) :
(∑ i : IndexValue d f1, toTensorRepMat Λ ((indexValueDualIso d (Equiv.refl _) hc) i) k * toTensorRepMat Λ i j) =
toTensorRepMat 1 (indexValueDualIso d (Equiv.refl _) (color_comp_τ_symm hc) k) j := by
trans ∑ i, toTensorRepMat Λ⁻¹ (indexValueDualIso d (Equiv.refl _) (color_comp_τ_symm hc) k) i
* toTensorRepMat Λ i j
apply Finset.sum_congr rfl (fun i _ => ?_)
rw [toTensorRepMat_oneMarkedIndexValue_inv]
rw [← Matrix.mul_apply, ← toTensorRepMat.map_mul, inv_mul_self Λ]
lemma toTensorRepMat_one_coord_sum' {f1 : X → Colors}
(T : ColorFiber d f1) (k : IndexValue d f1) :
∑ j, (toTensorRepMat 1 k j) * T j = T k := 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 only [IndexValue, map_one, mul_eq_zero]
exact Or.inl (Matrix.one_apply_ne' hjk)
lemma toTensorRepMat_of_splitIndexValue' (T : Marked d X n)
(i j : T.UnmarkedIndexValue) (k l : T.MarkedIndexValue) :
toTensorRepMat Λ i j * toTensorRepMat Λ k l =
@ -202,40 +254,61 @@ lemma toTensorRepMat_one_coord_sum (T : Marked d X n) (i : T.UnmarkedIndexValue)
## Definition of the Lorentz group action on Real Lorentz Tensors.
-/
@[simps!]
def lorentzActionFiber {c : X → Colors} :
Representation ℝ (LorentzGroup d) (ColorFiber d c) where
toFun Λ := {
toFun := fun T i => ∑ j, toTensorRepMat Λ i j * T j,
map_add' := fun T S => by
funext i
trans ∑ j, (toTensorRepMat Λ i j * T j + toTensorRepMat Λ i j * S j)
· refine Finset.sum_congr rfl (fun j _ => ?_)
erw [mul_add]
· rw [Finset.sum_add_distrib]
rfl
map_smul' := fun a T => by
funext i
simp only [ RingHom.id_apply]
trans ∑ j, a * (toTensorRepMat Λ i j * T j)
· refine Finset.sum_congr rfl (fun j _ => ?_)
rw [← mul_assoc, mul_comm a _, mul_assoc]
rfl
· rw [← Finset.mul_sum]
rfl}
map_one' := by
ext T
simp only [map_one, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.one_apply]
funext i
rw [Finset.sum_eq_single_of_mem i]
simp only [Matrix.one_apply_eq, one_mul]
exact Finset.mem_univ i
exact fun j _ hij => mul_eq_zero.mpr (Or.inl (Matrix.one_apply_ne' hij))
map_mul' Λ Λ' := by
ext T
simp only
funext i
trans ∑ j, ∑ k : IndexValue d c, (∏ x, colorMatrix (c x) Λ (i x) (k x) *
colorMatrix (c x) Λ' (k x) (j x)) * T j
· refine Finset.sum_congr rfl (fun j _ => ?_)
rw [toTensorRepMat_mul', Finset.sum_mul]
· rw [Finset.sum_comm]
refine Finset.sum_congr rfl (fun j _ => ?_)
simp only [LinearMap.coe_mk, AddHom.coe_mk, Finset.mul_sum, toTensorRepMat, IndexValue]
refine Finset.sum_congr rfl (fun k _ => ?_)
rw [← mul_assoc, Finset.prod_mul_distrib]
rfl
/-- 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}
smul Λ T := ⟨T.color, lorentzActionFiber Λ T.coord⟩
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]
simp only [HSMul.hSMul, map_one, LinearMap.one_apply]
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]
simp [HSMul.hSMul]
rfl
lemma lorentzAction_smul_coord' {d : ℕ} {X : Type} [Fintype X] [DecidableEq X] (Λ : ↑(𝓛 d))
@ -254,9 +327,9 @@ lemma lorentzAction_on_isEmpty [IsEmpty X] (Λ : LorentzGroup d) (T : RealLorent
Λ • 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]
erw [lorentzAction_smul_coord, mapIsoFiber_apply]
simp only [lorentzActionFiber_apply_apply, Finset.univ_eq_empty, Finset.prod_empty, one_mul,
indexValueIso_refl, Equiv.refl_symm]
simp only [IndexValue, Unique.eq_default, Finset.univ_unique, Finset.sum_const,
Finset.card_singleton, one_smul]
@ -265,7 +338,7 @@ lemma lorentzAction_mapIso (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzT
mapIso d f (Λ • T) = Λ • (mapIso d f T) := by
refine ext rfl ?_
funext i
rw [mapIso_apply_coord]
rw [mapIso_apply_coord, mapIsoFiber_apply, mapIsoFiber_apply]
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)

233
HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
View file

@ -24,11 +24,61 @@ variable {d : ℕ} {X Y : Type} [Fintype X] [DecidableEq X] [Fintype Y] [Decidab
open Marked
section mulMarkedFiber
variable {cX : X → Colors} {cY : Y → Colors} {fX : Fin 1 → Colors} {fY : Fin 1 → Colors}
/-- The index value appearing in the multiplication of Marked tensors on the left. -/
def mulMarkedFiberFstArg (i : IndexValue d (Sum.elim cX cY)) (x : ColorsIndex d (fX 0)) :
IndexValue d (Sum.elim cX fX) :=
indexValueSumEquiv.symm ((indexValueSumEquiv i).1, indexValueFinOne x)
/-- The index value appearing in the multiplication of Marked tensors on the right. -/
def mulMarkedFiberSndArg (i : IndexValue d (Sum.elim cX cY)) (x : ColorsIndex d (fX 0))
(h : fX 0 = τ (fY 0)) : IndexValue d (Sum.elim cY fY) :=
indexValueSumEquiv.symm ((indexValueSumEquiv i).2, indexValueFinOne $ colorsIndexDualCast h x)
def mulMarkedFiber (h : fX 0 = τ (fY 0)) : ColorFiber d (Sum.elim cX fX) →ₗ[ℝ]
ColorFiber d (Sum.elim cY fY) →ₗ[ℝ] ColorFiber d (Sum.elim cX cY) where
toFun T := {
toFun := fun S i => ∑ x, T (mulMarkedFiberFstArg i x) * S (mulMarkedFiberSndArg i x h),
map_add' := fun F S => by
funext i
trans ∑ x , (T (mulMarkedFiberFstArg i x) * F (mulMarkedFiberSndArg i x h) +
T (mulMarkedFiberFstArg i x) * S (mulMarkedFiberSndArg i x h))
exact Finset.sum_congr rfl (fun x _ => mul_add _ _ _ )
exact Finset.sum_add_distrib,
map_smul' := fun r S => by
funext i
trans ∑ x , r * (T (mulMarkedFiberFstArg i x) * S (mulMarkedFiberSndArg i x h))
refine Finset.sum_congr rfl (fun x _ => ?_)
ring_nf
rw [mul_assoc]
rfl
rw [← Finset.mul_sum]
rfl}
map_add' := fun T S => by
ext F
funext i
trans ∑ x , (T (mulMarkedFiberFstArg i x) * F (mulMarkedFiberSndArg i x h) +
S (mulMarkedFiberFstArg i x) * F (mulMarkedFiberSndArg i x h))
exact Finset.sum_congr rfl (fun x _ => add_mul _ _ _)
exact Finset.sum_add_distrib
map_smul' := fun r T => by
ext S
funext i
trans ∑ x , r * (T (mulMarkedFiberFstArg i x) * S (mulMarkedFiberSndArg i x h))
refine Finset.sum_congr rfl (fun x _ => mul_assoc _ _ _)
rw [← Finset.mul_sum]
rfl
end mulMarkedFiber
/-- 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)
def mulMarked {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
@ -38,25 +88,25 @@ def mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
oneMarkedIndexValue $ colorsIndexDualCast h x))
/-- The index value appearing in the multiplication of Marked tensors on the left. -/
def mulFstArg {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
def mulMarkedFstArg {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
(i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
(x : ColorsIndex d (T.color (markedPoint X 0))) : IndexValue d T.color :=
splitIndexValue.symm ((indexValueSumEquiv i).1, oneMarkedIndexValue x)
lemma mulFstArg_inr {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
lemma mulMarkedFstArg_inr {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
(i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
(x : ColorsIndex d (T.color (markedPoint X 0))) :
mulFstArg i x (Sum.inr 0) = x := by
mulMarkedFstArg i x (Sum.inr 0) = x := by
rfl
lemma mulFstArg_inl {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
lemma mulMarkedFstArg_inl {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
(i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
(x : ColorsIndex d (T.color (markedPoint X 0))) (c : X):
mulFstArg i x (Sum.inl c) = i (Sum.inl c) := by
mulMarkedFstArg i x (Sum.inl c) = i (Sum.inl c) := by
rfl
/-- The index value appearing in the multiplication of Marked tensors on the right. -/
def mulSndArg {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
def mulMarkedSndArg {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
(i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
(x : ColorsIndex d (T.color (markedPoint X 0))) (h : T.markedColor 0 = τ (S.markedColor 0)) :
IndexValue d S.color :=
@ -68,9 +118,9 @@ def mulSndArg {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
-/
/-! TODO: Where appropriate write these expresions in terms of `indexValueDualIso`. -/
lemma mul_colorsIndex_right {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
lemma mulMarked_colorsIndex_right {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
(h : T.markedColor 0 = τ (S.markedColor 0)) :
(mul T S h).coord = fun i => ∑ x,
(mulMarked T S h).coord = fun i => ∑ x,
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1,
oneMarkedIndexValue $ colorsIndexDualCast (color_eq_dual_symm h) x)) *
S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, oneMarkedIndexValue x)) := by
@ -81,9 +131,9 @@ lemma mul_colorsIndex_right {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
rw [← colorsIndexDualCast_symm]
exact (Equiv.apply_eq_iff_eq_symm_apply (colorsIndexDualCast h)).mp rfl
lemma mul_indexValue_left {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
lemma mulMarked_indexValue_left {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
(h : T.markedColor 0 = τ (S.markedColor 0)) :
(mul T S h).coord = fun i => ∑ j,
(mulMarked T S h).coord = fun i => ∑ j,
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j)) *
S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2,
(oneMarkedIndexValue $ (colorsIndexDualCast h) $ oneMarkedIndexValue.symm j))) := by
@ -91,14 +141,14 @@ lemma mul_indexValue_left {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
rw [← Equiv.sum_comp (oneMarkedIndexValue)]
rfl
lemma mul_indexValue_right {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
lemma mulMarked_indexValue_right {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
(h : T.markedColor 0 = τ (S.markedColor 0)) :
(mul T S h).coord = fun i => ∑ j,
(mulMarked T S h).coord = fun i => ∑ j,
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1,
oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm j)) *
S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, j)) := by
funext i
rw [mul_colorsIndex_right]
rw [mulMarked_colorsIndex_right]
rw [← Equiv.sum_comp (oneMarkedIndexValue)]
apply Finset.sum_congr rfl (fun x _ => ?_)
congr
@ -111,24 +161,24 @@ lemma mul_indexValue_right {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
-/
/-- 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)
lemma mulMarked_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
mapIso d (Equiv.sumComm X Y) (mulMarked T S h) = mulMarked S T (color_eq_dual_symm h) := by
refine ext ?_ ?_
· funext a
cases a with
| inl _ => rfl
| inr _ => rfl
· funext i
rw [mul_colorsIndex_right]
rw [mulMarked_colorsIndex_right]
refine Fintype.sum_congr _ _ (fun x => ?_)
rw [mul_comm]
rfl
/-- Multiplication commutes with `mapIso`. -/
lemma mul_mapIso {X Y Z : Type} (T : Marked d X 1) (S : Marked d Y 1) (f : X ≃ W)
lemma mulMarked_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 f g) (mulMarked T S h) = mulMarked (mapIso d (Equiv.sumCongr f (Equiv.refl _)) T)
(mapIso d (Equiv.sumCongr g (Equiv.refl _)) S) h := by
refine ext ?_ ?_
· funext a
@ -136,7 +186,7 @@ lemma mul_mapIso {X Y Z : Type} (T : Marked d X 1) (S : Marked d Y 1) (f : X ≃
| inl _ => rfl
| inr _ => rfl
· funext i
rw [mapIso_apply_coord, mul_coord, mul_coord]
rw [mapIso_apply_coord, mapIsoFiber_apply, mapIsoFiber_apply, mulMarked_coord, mulMarked_coord]
refine Fintype.sum_congr _ _ (fun x => ?_)
rw [mapIso_apply_coord, mapIso_apply_coord]
refine Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl
@ -152,9 +202,9 @@ lemma mul_mapIso {X Y Z : Type} (T : Marked d X 1) (S : Marked d Y 1) (f : X ≃
-/
/-- The marked Lorentz Action leaves multiplication invariant. -/
lemma mul_markedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
lemma mulMarked_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
mulMarked (Λ •ₘ T) (Λ •ₘ S) h = mulMarked T S h := by
refine ext rfl ?_
funext i
change ∑ x, (∑ j, toTensorRepMat Λ (oneMarkedIndexValue x) j *
@ -186,8 +236,7 @@ lemma mul_markedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
erw [toTensorRepMap_sum_dual]
rfl
rw [Finset.sum_comm]
trans ∑ k,
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1,
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 _ => ?_)
@ -198,9 +247,9 @@ lemma mul_markedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
rfl
/-- The unmarked Lorentz Action commutes with multiplication. -/
lemma mul_unmarkedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
lemma mulMarked_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
mulMarked (Λ •ᵤₘ T) (Λ •ᵤₘ S) h = Λ • mulMarked T S h := by
refine ext rfl ?_
funext i
change ∑ x, (∑ j, toTensorRepMat Λ (indexValueSumEquiv i).1 j *
@ -236,7 +285,7 @@ lemma mul_unmarkedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
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]
simp only [IndexValue, Finset.mem_univ, Prod.mk.eta, Equiv.symm_apply_apply, mulMarked_color]
trans ∑ p, toTensorRepMat Λ i p *
∑ x, (T.coord (splitIndexValue.symm ((indexValueSumEquiv p).1, oneMarkedIndexValue x)))
* S.coord (splitIndexValue.symm ((indexValueSumEquiv p).2,
@ -246,11 +295,11 @@ lemma mul_unmarkedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
rfl
/-- The Lorentz action commutes with multiplication. -/
lemma mul_lorentzAction (T : Marked d X 1) (S : Marked d Y 1)
lemma mulMarked_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
mulMarked (Λ • T) (Λ • S) h = Λ • mulMarked T S h := by
simp only [← marked_unmarked_action_eq_action]
rw [mul_markedLorentzAction, mul_unmarkedLorentzAction]
rw [mulMarked_markedLorentzAction, mulMarked_unmarkedLorentzAction]
/-!
@ -264,28 +313,28 @@ variable {n m : ℕ} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
/-- The multiplication of two real Lorentz Tensors along specified indices. -/
@[simps!]
def mulS (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (x : X) (y : Y)
def mult (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (x : X) (y : Y)
(h : T.color x = τ (S.color y)) : RealLorentzTensor d ({x' // x' ≠ x} ⊕ {y' // y' ≠ y}) :=
mul (markSingle x T) (markSingle y S) h
mulMarked (markSingle x T) (markSingle y S) h
/-- The first index value appearing in the multiplication of two Lorentz tensors. -/
def mulSFstArg {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
def multFstArg {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
(i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
(a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))) :
IndexValue d T.color := (markSingleIndexValue T x).symm (mulFstArg i a)
IndexValue d T.color := (markSingleIndexValue T x).symm (mulMarkedFstArg i a)
lemma mulSFstArg_ext {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
lemma multFstArg_ext {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
{i j : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)}
{a b : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))}
(hij : i = j) (hab : a = b) : mulSFstArg i a = mulSFstArg j b := by
(hij : i = j) (hab : a = b) : multFstArg i a = multFstArg j b := by
subst hij; subst hab
rfl
lemma mulSFstArg_on_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
lemma multFstArg_on_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
(i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
(a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))) :
mulSFstArg i a x = a := by
rw [mulSFstArg, markSingleIndexValue]
multFstArg i a x = a := by
rw [multFstArg, markSingleIndexValue]
simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
Sum.map_inr, id_eq]
erw [markEmbeddingIndexValue_apply_symm_on_mem]
@ -300,11 +349,11 @@ lemma mulSFstArg_on_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y}
rw [embedSingleton_toEquivRange_symm]
rfl
lemma mulSFstArg_on_not_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
lemma multFstArg_on_not_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
(i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
(a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
(c : X) (hc : c ≠ x) : mulSFstArg i a c = i (Sum.inl ⟨c, hc⟩) := by
rw [mulSFstArg, markSingleIndexValue]
(c : X) (hc : c ≠ x) : multFstArg i a c = i (Sum.inl ⟨c, hc⟩) := by
rw [multFstArg, markSingleIndexValue]
simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
Sum.map_inr, id_eq]
erw [markEmbeddingIndexValue_apply_symm_on_not_mem]
@ -313,17 +362,17 @@ lemma mulSFstArg_on_not_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d
rfl
/-- The second index value appearing in the multiplication of two Lorentz tensors. -/
def mulSSndArg {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
def multSndArg {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
(i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
(a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
(h : T.color x = τ (S.color y)) : IndexValue d S.color :=
(markSingleIndexValue S y).symm (mulSndArg i a h)
(markSingleIndexValue S y).symm (mulMarkedSndArg i a h)
lemma mulSSndArg_on_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
lemma multSndArg_on_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
(i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
(a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
(h : T.color x = τ (S.color y)) : mulSSndArg i a h y = colorsIndexDualCast h a := by
rw [mulSSndArg, markSingleIndexValue]
(h : T.color x = τ (S.color y)) : multSndArg i a h y = colorsIndexDualCast h a := by
rw [multSndArg, markSingleIndexValue]
simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
Sum.map_inr, id_eq]
erw [markEmbeddingIndexValue_apply_symm_on_mem]
@ -338,12 +387,12 @@ lemma mulSSndArg_on_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y}
rw [embedSingleton_toEquivRange_symm]
rfl
lemma mulSSndArg_on_not_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
lemma multSndArg_on_not_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
(i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
(a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
(h : T.color x = τ (S.color y)) (c : Y) (hc : c ≠ y) :
mulSSndArg i a h c = i (Sum.inr ⟨c, hc⟩) := by
rw [mulSSndArg, markSingleIndexValue]
multSndArg i a h c = i (Sum.inr ⟨c, hc⟩) := by
rw [multSndArg, markSingleIndexValue]
simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
Sum.map_inr, id_eq]
erw [markEmbeddingIndexValue_apply_symm_on_not_mem]
@ -351,48 +400,48 @@ lemma mulSSndArg_on_not_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d
simpa using hc
rfl
lemma mulSSndArg_ext {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
lemma multSndArg_ext {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
{i j : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)}
{a b : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))}
(h : T.color x = τ (S.color y)) (hij : i = j) (hab : a = b) :
mulSSndArg i a h = mulSSndArg j b h := by
multSndArg i a h = multSndArg j b h := by
subst hij
subst hab
rfl
lemma mulS_coord_arg (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (x : X) (y : Y)
lemma mult_coord_arg (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (x : X) (y : Y)
(h : T.color x = τ (S.color y))
(i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)) :
(mulS T S x y h).coord i = ∑ a, T.coord (mulSFstArg i a) * S.coord (mulSSndArg i a h) := by
(mult T S x y h).coord i = ∑ a, T.coord (multFstArg i a) * S.coord (multSndArg i a h) := by
rfl
lemma mulS_mapIso (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
lemma mult_mapIso (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
(eX : X ≃ X') (eY : Y ≃ Y') (x : X) (y : Y) (x' : X') (y' : Y') (hx : eX x = x')
(hy : eY y = y') (h : T.color x = τ (S.color y)) :
mulS (mapIso d eX T) (mapIso d eY S) x' y' (by subst hx hy; simpa using h) =
mult (mapIso d eX T) (mapIso d eY S) x' y' (by subst hx hy; simpa using h) =
mapIso d (Equiv.sumCongr (equivSingleCompl eX hx) (equivSingleCompl eY hy))
(mulS T S x y h) := by
rw [mulS, mulS, mul_mapIso]
(mult T S x y h) := by
rw [mult, mult, mulMarked_mapIso]
congr 1 <;> rw [markSingle_mapIso]
lemma mulS_lorentzAction (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
lemma mult_lorentzAction (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
(x : X) (y : Y) (h : T.color x = τ (S.color y)) (Λ : LorentzGroup d) :
mulS (Λ • T) (Λ • S) x y h = Λ • mulS T S x y h := by
rw [mulS, mulS, ← mul_lorentzAction]
mult (Λ • T) (Λ • S) x y h = Λ • mult T S x y h := by
rw [mult, mult, ← mulMarked_lorentzAction]
congr 1
all_goals
rw [markSingle, markEmbedding, Equiv.trans_apply]
erw [lorentzAction_mapIso, lorentzAction_mapIso]
rfl
lemma mulS_symm (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
lemma mult_symm (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
(x : X) (y : Y) (h : T.color x = τ (S.color y)) :
mapIso d (Equiv.sumComm _ _) (mulS T S x y h) = mulS S T y x (color_eq_dual_symm h) := by
rw [mulS, mulS, mul_symm]
mapIso d (Equiv.sumComm _ _) (mult T S x y h) = mult S T y x (color_eq_dual_symm h) := by
rw [mult, mult, mulMarked_symm]
/-- An equivalence of types associated with multiplying two consecutive indices,
with the second index appearing on the left. -/
def mulSSplitLeft {y y' : Y} (hy : y ≠ y') (z : Z) :
def multSplitLeft {y y' : Y} (hy : y ≠ y') (z : Z) :
{yz // yz ≠ (Sum.inl ⟨y, hy⟩ : {y'' // y'' ≠ y'} ⊕ {z' // z' ≠ z})} ≃
{y'' // y'' ≠ y' ∧ y'' ≠ y} ⊕ {z' // z' ≠ z} :=
Equiv.subtypeSum.trans <|
@ -404,7 +453,7 @@ def mulSSplitLeft {y y' : Y} (hy : y ≠ y') (z : Z) :
/-- An equivalence of types associated with multiplying two consecutive indices with the
second index appearing on the right. -/
def mulSSplitRight {y y' : Y} (hy : y ≠ y') (z : Z) :
def multSplitRight {y y' : Y} (hy : y ≠ y') (z : Z) :
{yz // yz ≠ (Sum.inr ⟨y', hy.symm⟩ : {z' // z' ≠ z} ⊕ {y'' // y'' ≠ y})} ≃
{z' // z' ≠ z} ⊕ {y'' // y'' ≠ y' ∧ y'' ≠ y} :=
Equiv.subtypeSum.trans <|
@ -415,18 +464,18 @@ def mulSSplitRight {y y' : Y} (hy : y ≠ y') (z : Z) :
(Equiv.subtypeEquivRight (fun y'' => And.comm)))
/-- An equivalence of types associated with the associativity property of multiplication. -/
def mulSAssocIso (x : X) {y y' : Y} (hy : y ≠ y') (z : Z) :
def multAssocIso (x : X) {y y' : Y} (hy : y ≠ y') (z : Z) :
{x' // x' ≠ x} ⊕ {yz // yz ≠ (Sum.inl ⟨y, hy⟩ : {y'' // y'' ≠ y'} ⊕ {z' // z' ≠ z})}
≃ {xy // xy ≠ (Sum.inr ⟨y', hy.symm⟩ : {x' // x' ≠ x} ⊕ {y'' // y'' ≠ y})} ⊕ {z' // z' ≠ z} :=
(Equiv.sumCongr (Equiv.refl _) (mulSSplitLeft hy z)).trans <|
(Equiv.sumCongr (Equiv.refl _) (multSplitLeft hy z)).trans <|
(Equiv.sumAssoc _ _ _).symm.trans <|
(Equiv.sumCongr (mulSSplitRight hy x).symm (Equiv.refl _))
(Equiv.sumCongr (multSplitRight hy x).symm (Equiv.refl _))
lemma mulS_assoc_color {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y}
lemma mult_assoc_color {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y}
{U : RealLorentzTensor d Z} {x : X} {y y' : Y} (hy : y ≠ y') {z : Z}
(h : T.color x = τ (S.color y))
(h' : S.color y' = τ (U.color z)) : (mulS (mulS T S x y h) U (Sum.inr ⟨y', hy.symm⟩) z h').color
= (mapIso d (mulSAssocIso x hy z) (mulS T (mulS S U y' z h') x (Sum.inl ⟨y, hy⟩) h)).color := by
(h' : S.color y' = τ (U.color z)) : (mult (mult T S x y h) U (Sum.inr ⟨y', hy.symm⟩) z h').color
= (mapIso d (multAssocIso x hy z) (mult T (mult S U y' z h') x (Sum.inl ⟨y, hy⟩) h)).color := by
funext a
match a with
| .inl ⟨.inl _, _⟩ => rfl
@ -434,28 +483,28 @@ lemma mulS_assoc_color {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y}
| .inr _ => rfl
/-- An equivalence of index values associated with the associativity property of multiplication. -/
def mulSAssocIndexValue {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y}
def multAssocIndexValue {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y}
{U : RealLorentzTensor d Z} {x : X} {y y' : Y} (hy : y ≠ y') {z : Z}
(h : T.color x = τ (S.color y)) (h' : S.color y' = τ (U.color z)) :
IndexValue d ((T.mulS S x y h).mulS U (Sum.inr ⟨y', hy.symm⟩) z h').color ≃
IndexValue d (T.mulS (S.mulS U y' z h') x (Sum.inl ⟨y, hy⟩) h).color :=
indexValueIso d (mulSAssocIso x hy z).symm (mulS_assoc_color hy h h')
IndexValue d ((T.mult S x y h).mult U (Sum.inr ⟨y', hy.symm⟩) z h').color ≃
IndexValue d (T.mult (S.mult U y' z h') x (Sum.inl ⟨y, hy⟩) h).color :=
indexValueIso d (multAssocIso x hy z).symm (mult_assoc_color hy h h')
/-- Multiplication of indices is associative, up to a `mapIso` equivalence. -/
lemma mulS_assoc (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (U : RealLorentzTensor d Z)
lemma mult_assoc (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (U : RealLorentzTensor d Z)
(x : X) (y y' : Y) (hy : y ≠ y') (z : Z) (h : T.color x = τ (S.color y))
(h' : S.color y' = τ (U.color z)) : mulS (mulS T S x y h) U (Sum.inr ⟨y', hy.symm⟩) z h' =
mapIso d (mulSAssocIso x hy z) (mulS T (mulS S U y' z h') x (Sum.inl ⟨y, hy⟩) h) := by
apply ext (mulS_assoc_color _ _ _) ?_
(h' : S.color y' = τ (U.color z)) : mult (mult T S x y h) U (Sum.inr ⟨y', hy.symm⟩) z h' =
mapIso d (multAssocIso x hy z) (mult T (mult S U y' z h') x (Sum.inl ⟨y, hy⟩) h) := by
apply ext (mult_assoc_color _ _ _) ?_
funext i
trans ∑ a, (∑ b, T.coord (mulSFstArg (mulSFstArg i a) b) *
S.coord (mulSSndArg (mulSFstArg i a) b h)) * U.coord (mulSSndArg i a h')
trans ∑ a, (∑ b, T.coord (multFstArg (multFstArg i a) b) *
S.coord (multSndArg (multFstArg i a) b h)) * U.coord (multSndArg i a h')
rfl
trans ∑ a, T.coord (mulSFstArg (mulSAssocIndexValue hy h h' i) a) *
(∑ b, S.coord (mulSFstArg (mulSSndArg (mulSAssocIndexValue hy h h' i) a h) b) *
U.coord (mulSSndArg (mulSSndArg (mulSAssocIndexValue hy h h' i) a h) b h'))
trans ∑ a, T.coord (multFstArg (multAssocIndexValue hy h h' i) a) *
(∑ b, S.coord (multFstArg (multSndArg (multAssocIndexValue hy h h' i) a h) b) *
U.coord (multSndArg (multSndArg (multAssocIndexValue hy h h' i) a h) b h'))
swap
rw [mapIso_apply_coord, mulS_coord_arg, indexValueIso_symm]
rw [mapIso_apply_coord, mapIsoFiber_apply, mapIsoFiber_apply, mult_coord_arg, indexValueIso_symm]
rfl
rw [Finset.sum_congr rfl (fun x _ => Finset.sum_mul _ _ _)]
rw [Finset.sum_congr rfl (fun x _ => Finset.mul_sum _ _ _)]
@ -467,15 +516,15 @@ lemma mulS_assoc (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (U : Re
funext c
by_cases hcy : c = y
· subst hcy
rw [mulSSndArg_on_mem, mulSFstArg_on_not_mem, mulSSndArg_on_mem]
rw [multSndArg_on_mem, multFstArg_on_not_mem, multSndArg_on_mem]
rfl
· by_cases hcy' : c = y'
· subst hcy'
rw [mulSFstArg_on_mem, mulSSndArg_on_not_mem, mulSFstArg_on_mem]
· rw [mulSFstArg_on_not_mem, mulSSndArg_on_not_mem, mulSSndArg_on_not_mem,
mulSFstArg_on_not_mem]
rw [mulSAssocIndexValue, indexValueIso_eq_symm, indexValueIso_symm_apply']
simp only [ne_eq, Function.comp_apply, Equiv.symm_symm_apply, mulS_color, Sum.elim_inr,
rw [multFstArg_on_mem, multSndArg_on_not_mem, multFstArg_on_mem]
· rw [multFstArg_on_not_mem, multSndArg_on_not_mem, multSndArg_on_not_mem,
multFstArg_on_not_mem]
rw [multAssocIndexValue, indexValueIso_eq_symm, indexValueIso_symm_apply']
simp only [ne_eq, Function.comp_apply, Equiv.symm_symm_apply, mult_color, Sum.elim_inr,
colorsIndexCast, Equiv.cast_refl, Equiv.refl_symm]
erw [Equiv.refl_apply]
rfl

8
HepLean/SpaceTime/LorentzTensor/Real/MultiplicationUnit.lean
View file

@ -119,7 +119,7 @@ lemma mulUnit_coord_off_diag (μ : Colors) (i: (mulUnit d μ).UnmarkedIndexValue
exact hb (id (Eq.symm h1))
lemma mulUnit_right (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ) :
mul T (mulUnit d μ) (h.trans (mulUnit_dual_markedColor μ).symm) = T := by
multMarked T (mulUnit d μ) (h.trans (mulUnit_dual_markedColor μ).symm) = T := by
refine ext ?_ ?_
· funext a
match a with
@ -128,7 +128,7 @@ lemma mulUnit_right (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ)
simp only [Fin.isValue, mul_color, Sum.elim_inr, mulUnit_unmarkedColor]
exact h.symm
funext i
rw [mul_indexValue_right]
rw [mulMarked_indexValue_right]
change ∑ j,
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, _)) *
(mulUnit d μ).coord (splitIndexValue.symm ((indexValueSumEquiv i).2, j)) = _
@ -160,9 +160,9 @@ lemma mulUnit_right (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ)
exact mulUnit_coord_off_diag μ (indexValueSumEquiv i).2 b hab
lemma mulUnit_left (μ : Colors) (T : Marked d X 1) (h : T.markedColor 0 = μ) :
mul (mulUnit d μ) T ((mulUnit_markedColor μ).trans (congrArg τ h.symm)) =
multMarked (mulUnit d μ) T ((mulUnit_markedColor μ).trans (congrArg τ h.symm)) =
mapIso d (Equiv.sumComm X (Fin 1)) T := by
rw [← mul_symm, mulUnit_right]
rw [← mult_symmd_symm, mulUnit_right]
exact h
lemma mulUnit_lorentzAction (μ : Colors) (Λ : LorentzGroup d) :

136
HepLean/SpaceTime/LorentzTensor/Real/TensorProducts.lean Normal file
View file

@ -0,0 +1,136 @@
/-
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.LorentzAction
import Mathlib.LinearAlgebra.TensorProduct.Basic
import Mathlib.LinearAlgebra.TensorProduct.Basis
/-!
# Tensor products of real Lorentz Tensors
-/
noncomputable section
namespace RealLorentzTensor
open TensorProduct
open Set LinearMap Submodule
variable {d : ℕ} {X Y : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
(cX : X → Colors) (cY : Y → Colors)
def basisColorFiber : Basis (IndexValue d cX) ℝ (ColorFiber d cX) := Pi.basisFun _ _
def colorFiberElim {cX : X → Colors} {cY : Y → Colors} : ColorFiber d (Sum.elim cX cY) ≃ₗ[ℝ] ColorFiber d cX ⊗[ℝ] ColorFiber d cY :=
(basisColorFiber (Sum.elim cX cY)).equiv
(Basis.tensorProduct (basisColorFiber cX) (basisColorFiber cY)) indexValueSumEquiv
def splitOnEmbeddingSet (f : Y ↪ X) :
X ≃ {x // x ∈ (Finset.image f Finset.univ)ᶜ} ⊕ Y :=
(Equiv.Set.sumCompl (Set.range ⇑f)).symm.trans <|
(Equiv.sumComm _ _).trans <|
Equiv.sumCongr ((Equiv.subtypeEquivRight (by simp))) <|
(Function.Embedding.toEquivRange f).symm
def embedLeftColor (f : Y ↪ X) : {x // x ∈ (Finset.image f Finset.univ)ᶜ} → Colors :=
(cX ∘ (splitOnEmbeddingSet f).symm) ∘ Sum.inl
def embedRightColor (f : Y ↪ X) : Y → Colors :=
(cX ∘ (splitOnEmbeddingSet f).symm) ∘ Sum.inr
def embedTensorProd (f : Y ↪ X) : ColorFiber d cX ≃ₗ[ℝ] ColorFiber d (embedLeftColor cX f) ⊗[ℝ]
ColorFiber d (embedRightColor cX f) :=
(@mapIsoFiber _ _ d (splitOnEmbeddingSet f) cX (Sum.elim (embedLeftColor cX f)
(embedRightColor cX f)) (by
simpa [embedLeftColor, embedRightColor] using (Equiv.comp_symm_eq _ _ _).mp rfl)).trans
colorFiberElim
/-- The contraction of all indices of two tensors with dual index-colors.
This is a bilinear map to ℝ. -/
@[simps!]
def contrAll {f1 f2 : X → Colors} (hc : f1 = τ ∘ f2) :
ColorFiber d f1 →ₗ[ℝ] ColorFiber d f2 →ₗ[ℝ] ℝ where
toFun T := {
toFun := fun S => ∑ i, T i * S (indexValueDualIso d hc i),
map_add' := fun S F => by
trans ∑ i, (T i * S (indexValueDualIso d hc i) + T i * F (indexValueDualIso d hc i))
exact Finset.sum_congr rfl (fun i _ => mul_add _ _ _ )
exact Finset.sum_add_distrib,
map_smul' := fun r S => by
trans ∑ i , r * (T i * S (indexValueDualIso d hc i))
refine Finset.sum_congr rfl (fun x _ => ?_)
ring_nf
rw [mul_assoc]
rfl
rw [← Finset.mul_sum]
rfl}
map_add' := fun T S => by
ext F
trans ∑ i , (T i * F (indexValueDualIso d hc i) + S i * F (indexValueDualIso d hc i))
exact Finset.sum_congr rfl (fun x _ => add_mul _ _ _)
exact Finset.sum_add_distrib
map_smul' := fun r T => by
ext S
trans ∑ i , r * (T i * S (indexValueDualIso d hc i))
refine Finset.sum_congr rfl (fun x _ => mul_assoc _ _ _)
rw [← Finset.mul_sum]
rfl
lemma contrAll_mapIsoFiber {f1 f2 : X → Colors} (hc : f1 = τ ∘ f2)
(e : X ≃ Y) {g1 g2 : Y → Colors} (h1 : f1 = g1 ∘ e) (h2 : f2 = g2 ∘ e) (T : ColorFiber d f1)
(S : ColorFiber d f2) : contrAll hc T S = contrAll (by
rw [h1, h2, ← Function.comp.assoc, ← Equiv.comp_symm_eq] at hc
simpa [Function.comp.assoc] using hc) (mapIsoFiber d e h1 T) (mapIsoFiber d e h2 S) := by
rw [contrAll_apply_apply, contrAll_apply_apply]
rw [← Equiv.sum_comp (indexValueIso d e h1)]
refine Finset.sum_congr rfl (fun i _ => ?_)
rw [mapIsoFiber_apply, Equiv.symm_apply_apply]
rw [mapIsoFiber_apply]
congr 2
rw [← indexValueDualIso_symm]
lemma contrAll_symm {f1 f2 : X → Colors} (hc : f1 = τ ∘ f2) (T : ColorFiber d f1)
(S : ColorFiber d f2) : contrAll hc T S = contrAll (color_comp_τ_symm hc) S T := by
rw [contrAll_apply_apply, contrAll_apply_apply, ← Equiv.sum_comp (indexValueDualIso d hc)]
refine Finset.sum_congr rfl (fun i _ => ?_)
rw [mul_comm]
congr
rw [← indexValueDualIso_symm]
exact (Equiv.apply_eq_iff_eq_symm_apply (indexValueDualIso d hc)).mp rfl
lemma contrAll_lorentzAction {f1 f2 : X → Colors} (hc : f1 = τ ∘ f2) (T : ColorFiber d f1)
(S : ColorFiber d f2) (Λ : LorentzGroup d) :
contrAll hc (lorentzActionFiber Λ T) (lorentzActionFiber Λ S) = contrAll hc T S := by
change ∑ i, (∑ j, toTensorRepMat Λ i j * T j) *
(∑ k, toTensorRepMat Λ (indexValueDualIso d hc i) k * S k) = _
trans ∑ i, ∑ j, ∑ k, (toTensorRepMat Λ (indexValueDualIso d hc i) k * toTensorRepMat Λ i j)
* T j * S 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, ∑ i, (toTensorRepMat Λ (indexValueDualIso d hc i) k
* toTensorRepMat Λ i j) * T j * S k
· apply Finset.sum_congr rfl (fun j _ => ?_)
rw [Finset.sum_comm]
trans ∑ j, ∑ k, (toTensorRepMat 1 (indexValueDualIso d (color_comp_τ_symm hc) k) j) * T j * S k
· apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_))
rw [← Finset.sum_mul, ← Finset.sum_mul]
erw [toTensorRepMat_indexValueDualIso]
rw [Finset.sum_comm]
trans ∑ k, T (indexValueDualIso d (color_comp_τ_symm hc) k) * S k
· apply Finset.sum_congr rfl (fun k _ => ?_)
rw [← Finset.sum_mul, ← toTensorRepMat_one_coord_sum' T]
rw [← Equiv.sum_comp (indexValueDualIso d hc), ← indexValueDualIso_symm d hc]
simp only [Equiv.symm_apply_apply, contrAll_apply_apply]
end RealLorentzTensor
end