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

refactor: Lorentz Tensors

Browse source
This commit is contained in:
jstoobysmith 2024-07-23 14:34:37 -04:00
parent f90fa1ac1a
commit 23e041295f
3 changed files with 290 additions and 148 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -12,6 +12,8 @@ import Mathlib.Logic.Equiv.Fintype
import Mathlib.Algebra.Module.Pi
import Mathlib.Algebra.Module.Equiv
import Mathlib.Algebra.Module.LinearMap.Basic
import Mathlib.LinearAlgebra.TensorProduct.Basic
import Mathlib.LinearAlgebra.TensorProduct.Basis
/-!
# Real Lorentz Tensors
@ -231,6 +233,8 @@ lemma indexValueIso_refl (d : ℕ) (i : X → Colors) :
indexValueIso d (Equiv.refl X) (rfl : i = i) = Equiv.refl _ := by
rfl
/-!
## Dual isomorphism for index values
@ -810,6 +814,47 @@ end markingElements
end Marked
noncomputable section basis
open TensorProduct
open Set LinearMap Submodule
variable {d : ℕ} {X Y Y' X' : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
[Fintype Y'] [DecidableEq Y'] [Fintype X'] [DecidableEq X']
(cX : X → Colors) (cY : Y → Colors)
def basisColorFiber : Basis (IndexValue d cX) ℝ (ColorFiber d cX) := Pi.basisFun _ _
@[simp]
def basisProd :
Basis (IndexValue d cX × IndexValue d cY) ℝ (ColorFiber d cX ⊗[ℝ] ColorFiber d cY) :=
(Basis.tensorProduct (basisColorFiber cX) (basisColorFiber cY))
lemma mapIsoFiber_basis {cX : X → Colors} {cY : Y → Colors} (e : X ≃ Y) (h : cX = cY ∘ e)
(i : IndexValue d cX) : (mapIsoFiber d e h) (basisColorFiber cX i)
= basisColorFiber cY (indexValueIso d e h i) := by
funext a
rw [mapIsoFiber_apply]
by_cases ha : a = ((indexValueIso d e h) i)
· subst ha
nth_rewrite 2 [indexValueIso_eq_symm]
rw [Equiv.apply_symm_apply]
simp only [basisColorFiber]
erw [Pi.basisFun_apply, Pi.basisFun_apply]
simp only [stdBasis_same]
· simp only [basisColorFiber]
erw [Pi.basisFun_apply, Pi.basisFun_apply]
simp
rw [if_neg, if_neg]
exact fun a_1 => ha (_root_.id (Eq.symm a_1))
rw [← Equiv.symm_apply_eq, indexValueIso_symm]
exact fun a_1 => ha (_root_.id (Eq.symm a_1))
end basis
/-!
## Contraction of indices

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

@ -51,6 +51,10 @@ def colorMatrix (μ : Colors) : LorentzGroup d →* Matrix (ColorsIndex d μ) (C
Matrix.transpose_mul, Matrix.transpose_apply]
rfl
lemma colorMatrix_ext {μ : Colors} {a b c d : ColorsIndex d μ} (hab : a = b) (hcd : c = d) :
(colorMatrix μ) Λ a c = (colorMatrix μ) Λ b d := by
rw [hab, hcd]
lemma colorMatrix_cast {μ ν : Colors} (h : μ = ν) (Λ : LorentzGroup d) :
colorMatrix ν Λ =
Matrix.reindex (colorsIndexCast h) (colorsIndexCast h) (colorMatrix μ Λ) := by
@ -150,42 +154,35 @@ 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]
lemma toTensorRepMat_indexValueDualIso_left {f1 : X → Colors} {f2 : Y → Colors}
(e : X ≃ Y) (hc : f1 = τ ∘ f2 ∘ e) (i : IndexValue d f1) (j : IndexValue d f2) :
toTensorRepMat Λ (indexValueDualIso d e hc i) j =
toTensorRepMat Λ⁻¹ (indexValueDualIso d e.symm (indexValueDualIso_cond_symm hc) j) i := by
rw [toTensorRepMat_apply, toTensorRepMat_apply, ← Equiv.prod_comp e]
apply Finset.prod_congr rfl (fun x _ => ?_)
rw [colorMatrix_cast (congrFun hc x)]
erw [colorMatrix_dual_cast]
rw [Matrix.reindex_apply, Matrix.reindex_apply]
erw [colorMatrix_dual_cast Λ (congrFun hc x)]
rw [Matrix.reindex_apply, colorMatrix_transpose]
simp only [Function.comp_apply, colorsIndexDualCast_symm,
Matrix.submatrix_apply, Matrix.transpose_apply]
rw [indexValueDualIso_eq_symm, indexValueDualIso_symm_apply',
indexValueDualIso_eq_symm, indexValueDualIso_symm_apply']
rw [← Equiv.trans_apply, colorsIndexDualCast_symm, colorsIndexDualCast_trans]
apply colorMatrix_ext
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]
simp [colorsIndexCast]
apply cast_eq_iff_heq.mpr
rw [Equiv.symm_apply_apply]
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
lemma toTensorRepMat_indexValueDualIso_sum {f1 : X → Colors} {f2 : Y → Colors}
(e : X ≃ Y) (hc : f1 = τ ∘ f2 ∘ e) (j : IndexValue d f1) (k : IndexValue d f2) :
(∑ i : IndexValue d f1, toTensorRepMat Λ ((indexValueDualIso d e hc) i) k * toTensorRepMat Λ i j) =
toTensorRepMat 1 (indexValueDualIso d e.symm (indexValueDualIso_cond_symm hc) k) j := by
trans ∑ i, toTensorRepMat Λ⁻¹ (indexValueDualIso d e.symm (indexValueDualIso_cond_symm hc) k) i
* toTensorRepMat Λ i j
apply Finset.sum_congr rfl (fun i _ => ?_)
rw [toTensorRepMat_oneMarkedIndexValue_inv]
rw [toTensorRepMat_indexValueDualIso_left]
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
@ -203,41 +200,6 @@ lemma toTensorRepMat_of_splitIndexValue' (T : Marked d X n)
(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 *
@ -298,6 +260,35 @@ def lorentzActionFiber {c : X → Colors} :
rw [← mul_assoc, Finset.prod_mul_distrib]
rfl
/-- The Lorentz action commutes with `mapIso`. -/
lemma lorentzActionFiber_mapIsoFiber (e : X ≃ Y) {f1 : X → Colors}
{f2 : Y → Colors} (h : f1 = f2 ∘ e) (Λ : LorentzGroup d)
(T : ColorFiber d f1) : mapIsoFiber d e h (lorentzActionFiber Λ T) =
lorentzActionFiber Λ (mapIsoFiber d e h T) := by
funext i
rw [mapIsoFiber_apply, lorentzActionFiber_apply_apply, lorentzActionFiber_apply_apply]
rw [← Equiv.sum_comp (indexValueIso d e h)]
refine Finset.sum_congr rfl (fun j _ => Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl)
· rw [← Equiv.prod_comp e]
apply Finset.prod_congr rfl (fun x _ => ?_)
erw [colorMatrix_cast (congrFun h x)]
rw [Matrix.reindex_apply]
simp
apply colorMatrix_ext
rw [indexValueIso_eq_symm, indexValueIso_symm_apply']
erw [← Equiv.eq_symm_apply]
simp only [Function.comp_apply, Equiv.symm_symm_apply, colorsIndexCast, Equiv.cast_symm,
Equiv.cast_apply, cast_cast, cast_eq]
rw [indexValueIso_eq_symm, indexValueIso_symm_apply']
simp [colorsIndexCast]
symm
refine cast_eq_iff_heq.mpr ?_
rw [Equiv.symm_apply_apply]
· rw [mapIsoFiber_apply]
apply congrArg
rw [← Equiv.trans_apply]
simp
/-- Action of the Lorentz group on `X`-indexed Real Lorentz Tensors. -/
@[simps!]
instance lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) where
@ -335,36 +326,40 @@ lemma lorentzAction_on_isEmpty [IsEmpty X] (Λ : LorentzGroup d) (T : RealLorent
/-- 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, 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)
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
mapIso d f (Λ • T) = Λ • (mapIso d f T) :=
ext rfl (lorentzActionFiber_mapIsoFiber f _ Λ T.coord)
section
variable {d : ℕ} {X Y Y' X' : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
[Fintype Y'] [DecidableEq Y'] [Fintype X'] [DecidableEq X']
(cX : X → Colors) (cY : Y → Colors)
lemma lorentzActionFiber_basis (Λ : LorentzGroup d) (i : IndexValue d cX) :
lorentzActionFiber Λ (basisColorFiber cX i) =
∑ j, toTensorRepMat Λ j i • basisColorFiber cX j := by
funext k
simp only [lorentzActionFiber, MonoidHom.coe_mk, OneHom.coe_mk,
LinearMap.coe_mk, AddHom.coe_mk]
rw [Finset.sum_apply]
rw [Finset.sum_eq_single_of_mem i, Finset.sum_eq_single_of_mem k]
change _ = toTensorRepMat Λ k i * (Pi.basisFun ℝ (IndexValue d cX)) k k
rw [basisColorFiber]
erw [Pi.basisFun_apply, Pi.basisFun_apply]
simp
exact Finset.mem_univ k
intro b _ hbk
change toTensorRepMat Λ b i • (basisColorFiber cX) b k = 0
erw [basisColorFiber, Pi.basisFun_apply]
simp [hbk]
exact Finset.mem_univ i
intro b hb hbk
erw [basisColorFiber, Pi.basisFun_apply]
simp [hbk]
intro a
subst a
simp_all only [Finset.mem_univ, ne_eq, not_true_eq_false]
end
/-!
## The Lorentz action on marked tensors.

212
HepLean/SpaceTime/LorentzTensor/Real/TensorProducts.lean
View file

@ -17,48 +17,146 @@ namespace RealLorentzTensor
open TensorProduct
open Set LinearMap Submodule
variable {d : ℕ} {X Y : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
variable {d : ℕ} {X Y Y' X' : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
[Fintype Y'] [DecidableEq Y'] [Fintype X'] [DecidableEq X']
(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) :
## The tensorator and properties thereof
-/
/-- An equivalence between `ColorFiber d (Sum.elim cX cY)` and
`ColorFiber d cX ⊗[ℝ] ColorFiber d cY`. This is related to the `tensorator` of
the monoidal functor defined by `ColorFiber`, hence the terminology. -/
def tensorator {cX : X → Colors} {cY : Y → Colors} :
ColorFiber d (Sum.elim cX cY) ≃ₗ[ℝ] ColorFiber d cX ⊗[ℝ] ColorFiber d cY :=
(basisColorFiber (Sum.elim cX cY)).equiv (basisProd cX cY) indexValueSumEquiv
lemma tensorator_symm_apply {cX : X → Colors} {cY : Y → Colors}
(X : ColorFiber d cX ⊗[ℝ] ColorFiber d cY) (i : IndexValue d (Sum.elim cX cY)) :
(tensorator.symm X) i = (basisProd cX cY).repr X (indexValueSumEquiv i) := by
rfl
/-! TODO : Move -/
lemma tensorator_mapIso_cond {cX : X → Colors} {cY : Y → Colors} {cX' : X' → Colors}
{cY' : Y' → Colors} {eX : X ≃ X'} {eY : Y ≃ Y'} (hX : cX = cX' ∘ eX) (hY : cY = cY' ∘ eY) :
Sum.elim cX cY = Sum.elim cX' cY' ∘ ⇑(eX.sumCongr eY) := by
subst hX hY
ext1 x
simp_all only [Function.comp_apply, Equiv.sumCongr_apply]
cases x with
| inl val => simp_all only [Sum.elim_inl, Function.comp_apply, Sum.map_inl]
| inr val_1 => simp_all only [Sum.elim_inr, Function.comp_apply, Sum.map_inr]
/-- The naturality condition for the `tensorator`. -/
lemma tensorator_mapIso {cX : X → Colors} {cY : Y → Colors} {cX' : X' → Colors}
{cY' : Y' → Colors} (eX : X ≃ X') (eY : Y ≃ Y') (hX : cX = cX' ∘ eX) (hY : cY = cY' ∘ eY) :
(mapIsoFiber d (Equiv.sumCongr eX eY) (tensorator_mapIso_cond hX hY)).trans tensorator =
tensorator.trans (TensorProduct.congr (mapIsoFiber d eX hX) (mapIsoFiber d eY hY)) := by
apply (basisColorFiber (Sum.elim cX cY)).ext'
intro i
simp
nth_rewrite 2 [tensorator]
simp
rw [Basis.tensorProduct_apply, TensorProduct.congr_tmul, mapIsoFiber_basis]
rw [tensorator]
simp
rw [Basis.tensorProduct_apply, mapIsoFiber_basis, mapIsoFiber_basis]
congr
sorry
sorry
lemma tensorator_lorentzAction (Λ : LorentzGroup d) :
(tensorator).toLinearMap ∘ₗ lorentzActionFiber Λ
= (TensorProduct.map (lorentzActionFiber Λ) (lorentzActionFiber Λ) ) ∘ₗ
((@tensorator d X Y _ _ _ _ cX cY).toLinearMap) := by
apply (basisColorFiber (Sum.elim cX cY)).ext
intro i
nth_rewrite 2 [tensorator]
simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, Basis.equiv_apply]
rw [basisProd, Basis.tensorProduct_apply, TensorProduct.map_tmul, lorentzActionFiber_basis,
lorentzActionFiber_basis, lorentzActionFiber_basis, map_sum, tmul_sum]
simp only [sum_tmul]
rw [← Equiv.sum_comp (indexValueSumEquiv).symm, Fintype.sum_prod_type, Finset.sum_comm]
refine Finset.sum_congr rfl (fun j _ => (Finset.sum_congr rfl (fun k _ => ?_)))
rw [tmul_smul, smul_tmul, tmul_smul, smul_smul, map_smul]
congr 1
· rw [toTensorRepMat_of_indexValueSumEquiv, Equiv.apply_symm_apply, mul_comm]
· simp [tensorator]
lemma tensorator_lorentzAction_apply (Λ : LorentzGroup d) (T : ColorFiber d (Sum.elim cX cY)) :
tensorator (lorentzActionFiber Λ T) =
TensorProduct.map (lorentzActionFiber Λ) (lorentzActionFiber Λ) (tensorator T) := by
erw [← LinearMap.comp_apply, tensorator_lorentzAction]
rfl
/-!
## Decomposing tensors based on embeddings
-/
def decompEmbedSet (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 decompEmbedColorLeft (f : Y ↪ X) : {x // x ∈ (Finset.image f Finset.univ)ᶜ} → Colors :=
(cX ∘ (decompEmbedSet f).symm) ∘ Sum.inl
def decompEmbedColorRight (f : Y ↪ X) : Y → Colors :=
(cX ∘ (decompEmbedSet f).symm) ∘ Sum.inr
/-- Decomposes a tensor into a tensor product based on an embedding. -/
def decompEmbed (f : Y ↪ X) :
ColorFiber d cX ≃ₗ[ℝ] ColorFiber d (decompEmbedColorLeft cX f) ⊗[ℝ] ColorFiber d (cX ∘ f) :=
(@mapIsoFiber _ _ d (decompEmbedSet f) cX (Sum.elim (decompEmbedColorLeft cX f)
(decompEmbedColorRight cX f)) (by
simpa [decompEmbedColorLeft, decompEmbedColorRight] using (Equiv.comp_symm_eq _ _ _).mp rfl)).trans
tensorator
lemma decompEmbed_lorentzAction_apply {f : Y ↪ X} (Λ : LorentzGroup d) (T : ColorFiber d cX) :
decompEmbed cX f (lorentzActionFiber Λ T) =
TensorProduct.map (lorentzActionFiber Λ) (lorentzActionFiber Λ) (decompEmbed cX f T) := by
rw [decompEmbed]
simp
rw [lorentzActionFiber_mapIsoFiber]
exact tensorator_lorentzAction_apply (decompEmbedColorLeft cX f) (decompEmbedColorRight cX f) Λ
((mapIsoFiber d (decompEmbedSet f) (decompEmbed.proof_2 cX f)) T)
def decompEmbedProd (f : X' ↪ X) (g : Y' ↪ Y) :
ColorFiber d cX ⊗[ℝ] ColorFiber d cY ≃ₗ[ℝ]
ColorFiber d (Sum.elim (decompEmbedColorLeft cX f) (decompEmbedColorLeft cY g))
⊗[ℝ] (ColorFiber d (cX ∘ f) ⊗[ℝ] ColorFiber d (cY ∘ g)) :=
(TensorProduct.congr (decompEmbed cX f) (decompEmbed cY g)).trans <|
(TensorProduct.assoc ℝ _ _ _).trans <|
(TensorProduct.congr (LinearEquiv.refl ℝ _)
((TensorProduct.assoc ℝ _ _ _).symm.trans <|
(TensorProduct.congr (TensorProduct.comm _ _ _) (LinearEquiv.refl ℝ _)).trans <|
(TensorProduct.assoc ℝ _ _ _))).trans <|
(TensorProduct.assoc ℝ _ _ _).symm.trans <|
(TensorProduct.congr tensorator.symm (LinearEquiv.refl ℝ _))
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) :
def contrAll {f1 : X → Colors} {f2 : Y → Colors} (e : X ≃ Y) (hc : f1 = τ ∘ f2 ∘ e) :
ColorFiber d f1 →ₗ[ℝ] ColorFiber d f2 →ₗ[ℝ] ℝ where
toFun T := {
toFun := fun S => ∑ i, T i * S (indexValueDualIso d hc i),
toFun := fun S => ∑ i, T i * S (indexValueDualIso d e hc i),
map_add' := fun S F => by
trans ∑ i, (T i * S (indexValueDualIso d hc i) + T i * F (indexValueDualIso d hc i))
trans ∑ i, (T i * S (indexValueDualIso d e hc i) + T i * F (indexValueDualIso d e 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))
trans ∑ i , r * (T i * S (indexValueDualIso d e hc i))
refine Finset.sum_congr rfl (fun x _ => ?_)
ring_nf
rw [mul_assoc]
@ -67,48 +165,52 @@ def contrAll {f1 f2 : X → Colors} (hc : f1 = τ ∘ f2) :
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))
trans ∑ i , (T i * F (indexValueDualIso d e hc i) + S i * F (indexValueDualIso d e 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))
trans ∑ i , r * (T i * S (indexValueDualIso d e 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
lemma contrAll_symm {f1 : X → Colors} {f2 : Y → Colors} (e : X ≃ Y)
(h : f1 = τ ∘ f2 ∘ e) (T : ColorFiber d f1) (S : ColorFiber d f2) :
contrAll e h T S = contrAll e.symm (indexValueDualIso_cond_symm h) S T := by
rw [contrAll_apply_apply, contrAll_apply_apply, ← Equiv.sum_comp (indexValueDualIso d e h)]
refine Finset.sum_congr rfl (fun i _ => ?_)
rw [mul_comm, ← Equiv.trans_apply]
simp
lemma contrAll_mapIsoFiber_right {f1 : X → Colors} {f2 : Y → Colors}
{g2 : Y' → Colors} (e : X ≃ Y) (eY : Y ≃ Y')
(h : f1 = τ ∘ f2 ∘ e) (hY : f2 = g2 ∘ eY) (T : ColorFiber d f1) (S : ColorFiber d f2) :
contrAll e h T S = contrAll (e.trans eY) (indexValueDualIso_cond_trans_indexValueIso h hY)
T (mapIsoFiber d eY hY 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]
refine Finset.sum_congr rfl (fun i _ => Mathlib.Tactic.Ring.mul_congr rfl ?_ rfl)
rw [mapIsoFiber_apply, ← Equiv.trans_apply]
simp only [indexValueDualIso_trans_indexValueIso]
congr
rw [← indexValueDualIso_symm]
exact (Equiv.apply_eq_iff_eq_symm_apply (indexValueDualIso d hc)).mp rfl
ext1 x
simp only [Equiv.trans_apply, Equiv.symm_apply_apply]
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
lemma contrAll_mapIsoFiber_left {f1 : X → Colors} {f2 : Y → Colors}
{g1 : X' → Colors} (e : X ≃ Y) (eX : X ≃ X')
(h : f1 = τ ∘ f2 ∘ e) (hX : f1 = g1 ∘ eX) (T : ColorFiber d f1) (S : ColorFiber d f2) :
contrAll e h T S = contrAll (eX.symm.trans e)
(indexValueIso_trans_indexValueDualIso_cond ((Equiv.eq_comp_symm eX g1 f1).mpr hX.symm) h)
(mapIsoFiber d eX hX T) S := by
rw [contrAll_symm, contrAll_mapIsoFiber_right _ eX _ hX, contrAll_symm]
rfl
lemma contrAll_lorentzAction {f1 : X → Colors} {f2 : Y → Colors} (e : X ≃ Y)
(hc : f1 = τ ∘ f2 ∘ e) (T : ColorFiber d f1) (S : ColorFiber d f2) (Λ : LorentzGroup d) :
contrAll e hc (lorentzActionFiber Λ T) (lorentzActionFiber Λ S) = contrAll e 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)
(∑ k, toTensorRepMat Λ (indexValueDualIso d e hc i) k * S k) = _
trans ∑ i, ∑ j, ∑ k, (toTensorRepMat Λ (indexValueDualIso d e hc i) k * toTensorRepMat Λ i j)
* T j * S k
· apply Finset.sum_congr rfl (fun x _ => ?_)
rw [Finset.sum_mul_sum]
@ -116,19 +218,19 @@ lemma contrAll_lorentzAction {f1 f2 : X → Colors} (hc : f1 = τ ∘ f2) (T : C
apply Finset.sum_congr rfl (fun k _ => ?_)
ring
rw [Finset.sum_comm]
trans ∑ j, ∑ k, ∑ i, (toTensorRepMat Λ (indexValueDualIso d hc i) k
trans ∑ j, ∑ k, ∑ i, (toTensorRepMat Λ (indexValueDualIso d e 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
trans ∑ j, ∑ k, (toTensorRepMat 1 (indexValueDualIso d e.symm (indexValueDualIso_cond_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]
erw [toTensorRepMat_indexValueDualIso_sum]
rw [Finset.sum_comm]
trans ∑ k, T (indexValueDualIso d (color_comp_τ_symm hc) k) * S k
trans ∑ k, T (indexValueDualIso d e.symm (indexValueDualIso_cond_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]
rw [← Equiv.sum_comp (indexValueDualIso d e hc), ← indexValueDualIso_symm e hc]
simp only [Equiv.symm_apply_apply, contrAll_apply_apply]