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

Merge pull request #97 from HEPLean/Tensors-V2

Browse source 
feat: Add general tensor definitions
This commit is contained in:
Joseph Tooby-Smith 2024-07-26 16:08:32 -04:00 • committed by GitHub
commit 689ce73a2b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
9 changed files with 845 additions and 2192 deletions
Download patch file Download diff file Expand all files Collapse all files

826
HepLean/SpaceTime/LorentzTensor/Basic.lean Normal file
View file

@ -0,0 +1,826 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import Mathlib.LinearAlgebra.PiTensorProduct
import Mathlib.RepresentationTheory.Basic
/-!
# Structure of Lorentz Tensors
In this file we set up the basic structures we will use to define Lorentz tensors.
## References
-- For modular operads see: [Raynor][raynor2021graphical]
-/
noncomputable section
open TensorProduct
variable {R : Type} [CommSemiring R]
/-- An initial structure specifying a tensor system (e.g. a system in which you can
define real Lorentz tensors). -/
structure PreTensorStructure (R : Type) [CommSemiring R] where
/-- The allowed colors of indices.
For example for a real Lorentz tensor these are `{up, down}`. -/
Color : Type
/-- To each color we associate a module. -/
ColorModule : Color → Type
/-- A map taking every color to its dual color. -/
τ : Color → Color
/-- The map `τ` is an involution. -/
τ_involutive : Function.Involutive τ
/-- Each `ColorModule` has the structure of an additive commutative monoid. -/
colorModule_addCommMonoid : ∀ μ, AddCommMonoid (ColorModule μ)
/-- Each `ColorModule` has the structure of a module over `R`. -/
colorModule_module : ∀ μ, Module R (ColorModule μ)
/-- The contraction of a vector with a vector with dual color. -/
contrDual : ∀ μ, ColorModule μ ⊗[R] ColorModule (τ μ) →ₗ[R] R
namespace PreTensorStructure
variable (𝓣 : PreTensorStructure R)
variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
[Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
{cX cX2 : X → 𝓣.Color} {cY : Y → 𝓣.Color} {cZ : Z → 𝓣.Color}
{cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν: 𝓣.Color}
instance : AddCommMonoid (𝓣.ColorModule μ) := 𝓣.colorModule_addCommMonoid μ
instance : Module R (𝓣.ColorModule μ) := 𝓣.colorModule_module μ
/-- The type of tensors given a map from an indexing set `X` to the type of colors,
specifying the color of that index. -/
def Tensor (c : X → 𝓣.Color) : Type := ⨂[R] x, 𝓣.ColorModule (c x)
instance : AddCommMonoid (𝓣.Tensor cX) :=
PiTensorProduct.instAddCommMonoid fun i => 𝓣.ColorModule (cX i)
instance : Module R (𝓣.Tensor cX) := PiTensorProduct.instModule
/-- Equivalence of `ColorModule` given an equality of colors. -/
def colorModuleCast (h : μ = ν) : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.ColorModule ν where
toFun x := Equiv.cast (congrArg 𝓣.ColorModule h) x
invFun x := (Equiv.cast (congrArg 𝓣.ColorModule h)).symm x
map_add' x y := by
subst h
rfl
map_smul' x y := by
subst h
rfl
left_inv x := Equiv.symm_apply_apply (Equiv.cast (congrArg 𝓣.ColorModule h)) x
right_inv x := Equiv.apply_symm_apply (Equiv.cast (congrArg 𝓣.ColorModule h)) x
lemma tensorProd_piTensorProd_ext {M : Type} [AddCommMonoid M] [Module R M]
{f g : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY →ₗ[R] M}
(h : ∀ p q, f (PiTensorProduct.tprod R p ⊗ₜ[R] PiTensorProduct.tprod R q)
= g (PiTensorProduct.tprod R p ⊗ₜ[R] PiTensorProduct.tprod R q)) : f = g := by
apply TensorProduct.ext'
refine fun x ↦
PiTensorProduct.induction_on' x ?_ (by
intro a b hx hy y
simp [map_add, add_tmul, hx, hy])
intro rx fx
refine fun y ↦
PiTensorProduct.induction_on' y ?_ (by
intro a b hx hy
simp at hx hy
simp [map_add, tmul_add, hx, hy])
intro ry fy
simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, tmul_smul, LinearMapClass.map_smul]
apply congrArg
simp only [smul_tmul, tmul_smul, LinearMapClass.map_smul]
exact congrArg (HSMul.hSMul rx) (h fx fy)
/-!
## Mapping isomorphisms
-/
/-- An linear equivalence of tensor spaces given a color-preserving equivalence of indexing sets. -/
def mapIso {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = d ∘ e) :
𝓣.Tensor c ≃ₗ[R] 𝓣.Tensor d :=
(PiTensorProduct.reindex R _ e) ≪≫ₗ
(PiTensorProduct.congr (fun y => 𝓣.colorModuleCast (by rw [h]; simp)))
lemma mapIso_trans_cond {e : X ≃ Y} {e' : Y ≃ Z} (h : cX = cY ∘ e) (h' : cY = cZ ∘ e') :
cX = cZ ∘ (e.trans e') := by
funext a
subst h h'
simp
@[simp]
lemma mapIso_trans (e : X ≃ Y) (e' : Y ≃ Z) (h : cX = cY ∘ e) (h' : cY = cZ ∘ e') :
(𝓣.mapIso e h ≪≫ₗ 𝓣.mapIso e' h') = 𝓣.mapIso (e.trans e') (𝓣.mapIso_trans_cond h h') := by
refine LinearEquiv.toLinearMap_inj.mp ?_
apply PiTensorProduct.ext
apply MultilinearMap.ext
intro x
simp only [mapIso, LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe,
LinearEquiv.trans_apply, PiTensorProduct.reindex_tprod, Equiv.symm_trans_apply]
change (PiTensorProduct.congr fun y => 𝓣.colorModuleCast _)
((PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (cY x)) e')
((PiTensorProduct.congr fun y => 𝓣.colorModuleCast _) _)) =
(PiTensorProduct.congr fun y => 𝓣.colorModuleCast _)
((PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (cX x)) (e.trans e')) _)
rw [PiTensorProduct.congr_tprod, PiTensorProduct.reindex_tprod,
PiTensorProduct.congr_tprod, PiTensorProduct.reindex_tprod, PiTensorProduct.congr]
simp [colorModuleCast]
@[simp]
lemma mapIso_mapIso (e : X ≃ Y) (e' : Y ≃ Z) (h : cX = cY ∘ e) (h' : cY = cZ ∘ e')
(T : 𝓣.Tensor cX) :
(𝓣.mapIso e' h') (𝓣.mapIso e h T) = 𝓣.mapIso (e.trans e') (𝓣.mapIso_trans_cond h h') T := by
rw [← LinearEquiv.trans_apply, mapIso_trans]
@[simp]
lemma mapIso_symm (e : X ≃ Y) (h : cX = cY ∘ e) :
(𝓣.mapIso e h).symm = 𝓣.mapIso e.symm ((Equiv.eq_comp_symm e cY cX).mpr h.symm) := by
refine LinearEquiv.toLinearMap_inj.mp ?_
apply PiTensorProduct.ext
apply MultilinearMap.ext
intro x
simp [mapIso, LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe,
LinearEquiv.symm_apply_apply, PiTensorProduct.reindex_tprod]
change (PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (cX x)) e).symm
((PiTensorProduct.congr fun y => 𝓣.colorModuleCast _).symm ((PiTensorProduct.tprod R) x)) =
(PiTensorProduct.congr fun y => 𝓣.colorModuleCast _)
((PiTensorProduct.reindex R (fun x => 𝓣.ColorModule (cY x)) e.symm)
((PiTensorProduct.tprod R) x))
rw [PiTensorProduct.reindex_tprod, PiTensorProduct.congr_tprod, PiTensorProduct.congr_symm_tprod,
LinearEquiv.symm_apply_eq, PiTensorProduct.reindex_tprod]
apply congrArg
funext i
simp only [colorModuleCast, Equiv.cast_symm, LinearEquiv.coe_symm_mk,
Equiv.symm_symm_apply, LinearEquiv.coe_mk]
rw [← Equiv.symm_apply_eq]
simp only [Equiv.cast_symm, Equiv.cast_apply, cast_cast]
apply cast_eq_iff_heq.mpr
rw [Equiv.apply_symm_apply]
@[simp]
lemma mapIso_refl : 𝓣.mapIso (Equiv.refl X) (rfl : cX = cX) = LinearEquiv.refl R _ := by
refine LinearEquiv.toLinearMap_inj.mp ?_
apply PiTensorProduct.ext
apply MultilinearMap.ext
intro x
simp only [mapIso, Equiv.refl_symm, Equiv.refl_apply, PiTensorProduct.reindex_refl,
LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
LinearEquiv.refl_apply, LinearEquiv.refl_toLinearMap, LinearMap.id, LinearMap.coe_mk,
AddHom.coe_mk, id_eq]
change (PiTensorProduct.congr fun y => 𝓣.colorModuleCast _) ((PiTensorProduct.tprod R) x) = _
rw [PiTensorProduct.congr_tprod]
rfl
@[simp]
lemma mapIso_tprod {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = d ∘ e)
(f : (i : X) → 𝓣.ColorModule (c i)) : (𝓣.mapIso e h) (PiTensorProduct.tprod R f) =
(PiTensorProduct.tprod R (fun i => 𝓣.colorModuleCast (by rw [h]; simp) (f (e.symm i)))) := by
simp [mapIso]
change (PiTensorProduct.congr fun y => 𝓣.colorModuleCast _)
((PiTensorProduct.reindex R _ e) ((PiTensorProduct.tprod R) f)) = _
rw [PiTensorProduct.reindex_tprod]
exact PiTensorProduct.congr_tprod (fun y => 𝓣.colorModuleCast _) fun i => f (e.symm i)
/-!
## Pure tensors
This section is needed since: `PiTensorProduct.tmulEquiv` is not defined for dependent types.
Hence we need to construct a version of it here.
-/
/-- The type of pure tensors, i.e. of the form `v1 ⊗ v2 ⊗ v3 ⊗ ...`. -/
abbrev PureTensor (c : X → 𝓣.Color) := (x : X) → 𝓣.ColorModule (c x)
/-- A pure tensor in `𝓣.PureTensor (Sum.elim cX cY)` constructed from a pure tensor
in `𝓣.PureTensor cX` and a pure tensor in `𝓣.PureTensor cY`. -/
def elimPureTensor (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY) : 𝓣.PureTensor (Sum.elim cX cY) :=
fun x =>
match x with
| Sum.inl x => p x
| Sum.inr x => q x
@[simp]
lemma elimPureTensor_update_right (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY)
(y : Y) (r : 𝓣.ColorModule (cY y)) : 𝓣.elimPureTensor p (Function.update q y r) =
Function.update (𝓣.elimPureTensor p q) (Sum.inr y) r := by
funext x
match x with
| Sum.inl x => rfl
| Sum.inr x =>
change Function.update q y r x = _
simp only [Function.update, Sum.inr.injEq, Sum.elim_inr]
split_ifs
rename_i h
subst h
simp_all only
rfl
@[simp]
lemma elimPureTensor_update_left (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY)
(x : X) (r : 𝓣.ColorModule (cX x)) : 𝓣.elimPureTensor (Function.update p x r) q =
Function.update (𝓣.elimPureTensor p q) (Sum.inl x) r := by
funext y
match y with
| Sum.inl y =>
change (Function.update p x r) y = _
simp only [Function.update, Sum.inl.injEq, Sum.elim_inl]
split_ifs
rename_i h
subst h
simp_all only
rfl
| Sum.inr y => rfl
/-- The projection of a pure tensor in `𝓣.PureTensor (Sum.elim cX cY)` onto a pure tensor in
`𝓣.PureTensor cX`. -/
def inlPureTensor (p : 𝓣.PureTensor (Sum.elim cX cY)) : 𝓣.PureTensor cX := fun x => p (Sum.inl x)
/-- The projection of a pure tensor in `𝓣.PureTensor (Sum.elim cX cY)` onto a pure tensor in
`𝓣.PureTensor cY`. -/
def inrPureTensor (p : 𝓣.PureTensor (Sum.elim cX cY)) : 𝓣.PureTensor cY := fun y => p (Sum.inr y)
@[simp]
lemma inlPureTensor_update_left [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Sum.elim cX cY)) (x : X)
(v1 : 𝓣.ColorModule (Sum.elim cX cY (Sum.inl x))) :
𝓣.inlPureTensor (Function.update f (Sum.inl x) v1) =
Function.update (𝓣.inlPureTensor f) x v1 := by
funext y
simp [inlPureTensor, Function.update, Sum.inl.injEq, Sum.elim_inl]
split
next h =>
subst h
simp_all only
rfl
@[simp]
lemma inrPureTensor_update_left [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Sum.elim cX cY)) (x : X)
(v1 : 𝓣.ColorModule (Sum.elim cX cY (Sum.inl x))) :
𝓣.inrPureTensor (Function.update f (Sum.inl x) v1) = (𝓣.inrPureTensor f) := by
funext x
simp [inrPureTensor, Function.update]
@[simp]
lemma inrPureTensor_update_right [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Sum.elim cX cY)) (y : Y)
(v1 : 𝓣.ColorModule (Sum.elim cX cY (Sum.inr y))) :
𝓣.inrPureTensor (Function.update f (Sum.inr y) v1) =
Function.update (𝓣.inrPureTensor f) y v1 := by
funext y
simp [inrPureTensor, Function.update, Sum.inl.injEq, Sum.elim_inl]
split
next h =>
subst h
simp_all only
rfl
@[simp]
lemma inlPureTensor_update_right [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Sum.elim cX cY)) (y : Y)
(v1 : 𝓣.ColorModule (Sum.elim cX cY (Sum.inr y))) :
𝓣.inlPureTensor (Function.update f (Sum.inr y) v1) = (𝓣.inlPureTensor f) := by
funext x
simp [inlPureTensor, Function.update]
/-- The multilinear map taking pure tensors a `𝓣.PureTensor cX` and a pure tensor in
`𝓣.PureTensor cY`, and constructing a tensor in `𝓣.Tensor (Sum.elim cX cY))`. -/
def elimPureTensorMulLin : MultilinearMap R (fun i => 𝓣.ColorModule (cX i))
(MultilinearMap R (fun x => 𝓣.ColorModule (cY x)) (𝓣.Tensor (Sum.elim cX cY))) where
toFun p := {
toFun := fun q => PiTensorProduct.tprod R (𝓣.elimPureTensor p q)
map_add' := fun m x v1 v2 => by
simp [Sum.elim_inl, Sum.elim_inr]
map_smul' := fun m x r v => by
simp [Sum.elim_inl, Sum.elim_inr]}
map_add' p x v1 v2 := by
apply MultilinearMap.ext
intro y
simp
map_smul' p x r v := by
apply MultilinearMap.ext
intro y
simp
/-!
## tensorator
-/
/-! TODO: Replace with dependent type version of `MultilinearMap.domCoprod` when in Mathlib. -/
/-- The multi-linear map taking a pure tensor in `𝓣.PureTensor (Sum.elim cX cY)` and constructing
a vector in `𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY`. -/
def domCoprod : MultilinearMap R (fun x => 𝓣.ColorModule (Sum.elim cX cY x))
(𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY) where
toFun f := (PiTensorProduct.tprod R (𝓣.inlPureTensor f)) ⊗ₜ
(PiTensorProduct.tprod R (𝓣.inrPureTensor f))
map_add' f xy v1 v2:= by
match xy with
| Sum.inl x => simp [← TensorProduct.add_tmul]
| Sum.inr y => simp [← TensorProduct.tmul_add]
map_smul' f xy r p := by
match xy with
| Sum.inl x => simp [TensorProduct.tmul_smul, TensorProduct.smul_tmul]
| Sum.inr y => simp [TensorProduct.tmul_smul, TensorProduct.smul_tmul]
/-- The linear map combining two tensors into a single tensor
via the tensor product i.e. `v1 v2 ↦ v1 ⊗ v2`. -/
def tensoratorSymm : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY →ₗ[R] 𝓣.Tensor (Sum.elim cX cY) := by
refine TensorProduct.lift {
toFun := fun a ↦
PiTensorProduct.lift <|
PiTensorProduct.lift (𝓣.elimPureTensorMulLin) a,
map_add' := fun a b ↦ by simp
map_smul' := fun r a ↦ by simp}
/-! TODO: Replace with dependent type version of `PiTensorProduct.tmulEquiv` when in Mathlib. -/
/-- Splitting a tensor in `𝓣.Tensor (Sum.elim cX cY)` into the tensor product of two tensors. -/
def tensorator : 𝓣.Tensor (Sum.elim cX cY) →ₗ[R] 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY :=
PiTensorProduct.lift 𝓣.domCoprod
/-- An equivalence formed by taking the tensor product of tensors. -/
def tensoratorEquiv (c : X → 𝓣.Color) (d : Y → 𝓣.Color) :
𝓣.Tensor c ⊗[R] 𝓣.Tensor d ≃ₗ[R] 𝓣.Tensor (Sum.elim c d) :=
LinearEquiv.ofLinear (𝓣.tensoratorSymm) (𝓣.tensorator)
(by
apply PiTensorProduct.ext
apply MultilinearMap.ext
intro p
simp [tensorator, tensoratorSymm, domCoprod]
change (PiTensorProduct.lift _) ((PiTensorProduct.tprod R) _) =
LinearMap.id ((PiTensorProduct.tprod R) p)
rw [PiTensorProduct.lift.tprod]
simp [elimPureTensorMulLin, elimPureTensor]
change (PiTensorProduct.tprod R) _ = _
apply congrArg
funext x
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl)
(by
apply tensorProd_piTensorProd_ext
intro p q
simp [tensorator, tensoratorSymm]
change (PiTensorProduct.lift 𝓣.domCoprod)
((PiTensorProduct.lift (𝓣.elimPureTensorMulLin p)) ((PiTensorProduct.tprod R) q)) =_
rw [PiTensorProduct.lift.tprod]
simp [elimPureTensorMulLin]
rfl)
@[simp]
lemma tensoratorEquiv_tmul_tprod (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY) :
(𝓣.tensoratorEquiv cX cY) ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q) =
(PiTensorProduct.tprod R) (𝓣.elimPureTensor p q) := by
simp only [tensoratorEquiv, tensoratorSymm, tensorator, domCoprod, LinearEquiv.ofLinear_apply,
lift.tmul, LinearMap.coe_mk, AddHom.coe_mk, PiTensorProduct.lift.tprod]
exact PiTensorProduct.lift.tprod q
lemma tensoratorEquiv_mapIso_cond {e : X ≃ Y} {e' : Z ≃ Y} {e'' : W ≃ X}
(h : cX = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') (h'' : bW = cX ∘ e'') :
Sum.elim bW cZ = Sum.elim cX cY ∘ ⇑(e''.sumCongr e') := by
subst h h' h''
funext x
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl
@[simp]
lemma tensoratorEquiv_mapIso (e : X ≃ Y) (e' : Z ≃ Y) (e'' : W ≃ X)
(h : cX = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') (h'' : bW = cX ∘ e'') :
(TensorProduct.congr (𝓣.mapIso e'' h'') (𝓣.mapIso e' h')) ≪≫ₗ (𝓣.tensoratorEquiv cX cY)
= (𝓣.tensoratorEquiv bW cZ)
≪≫ₗ (𝓣.mapIso (Equiv.sumCongr e'' e') (𝓣.tensoratorEquiv_mapIso_cond h h' h'')) := by
apply LinearEquiv.toLinearMap_inj.mp
apply tensorProd_piTensorProd_ext
intro p q
simp only [LinearEquiv.coe_coe, LinearEquiv.trans_apply, congr_tmul, mapIso_tprod,
tensoratorEquiv_tmul_tprod, Equiv.sumCongr_symm, Equiv.sumCongr_apply]
apply congrArg
funext x
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl
@[simp]
lemma tensoratorEquiv_mapIso_apply (e : X ≃ Y) (e' : Z ≃ Y) (e'' : W ≃ X)
(h : cX = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') (h'' : cW = cX ∘ e'')
(x : 𝓣.Tensor cW ⊗[R] 𝓣.Tensor cZ) :
(𝓣.tensoratorEquiv cX cY) ((TensorProduct.congr (𝓣.mapIso e'' h'') (𝓣.mapIso e' h')) x) =
(𝓣.mapIso (Equiv.sumCongr e'' e') (𝓣.tensoratorEquiv_mapIso_cond h h' h''))
((𝓣.tensoratorEquiv cW cZ) x) := by
trans ((TensorProduct.congr (𝓣.mapIso e'' h'') (𝓣.mapIso e' h')) ≪≫ₗ
(𝓣.tensoratorEquiv cX cY)) x
rfl
rw [tensoratorEquiv_mapIso]
rfl
exact e
exact h
lemma tensoratorEquiv_mapIso_tmul (e : X ≃ Y) (e' : Z ≃ Y) (e'' : W ≃ X)
(h : cX = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') (h'' : cW = cX ∘ e'')
(x : 𝓣.Tensor cW) (y : 𝓣.Tensor cZ) :
(𝓣.tensoratorEquiv cX cY) ((𝓣.mapIso e'' h'' x) ⊗ₜ[R] (𝓣.mapIso e' h' y)) =
(𝓣.mapIso (Equiv.sumCongr e'' e') (𝓣.tensoratorEquiv_mapIso_cond h h' h''))
((𝓣.tensoratorEquiv cW cZ) (x ⊗ₜ y)) := by
rw [← tensoratorEquiv_mapIso_apply]
rfl
exact e
exact h
/-!
## Splitting tensors into tensor products
-/
/-- The decomposition of a set into a direct sum based on the image of an injection. -/
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
/-- The restriction of a map from an indexing set to the space to the complement of the image
of an embedding. -/
def decompEmbedColorLeft (c : X → 𝓣.Color) (f : Y ↪ X) :
{x // x ∈ (Finset.image f Finset.univ)ᶜ} → 𝓣.Color :=
(c ∘ (decompEmbedSet f).symm) ∘ Sum.inl
/-- The restriction of a map from an indexing set to the space to the image
of an embedding. -/
def decompEmbedColorRight (c : X → 𝓣.Color) (f : Y ↪ X) : Y → 𝓣.Color :=
(c ∘ (decompEmbedSet f).symm) ∘ Sum.inr
lemma decompEmbed_cond (c : X → 𝓣.Color) (f : Y ↪ X) : c =
(Sum.elim (𝓣.decompEmbedColorLeft c f) (𝓣.decompEmbedColorRight c f)) ∘ decompEmbedSet f := by
simpa [decompEmbedColorLeft, decompEmbedColorRight] using (Equiv.comp_symm_eq _ _ _).mp rfl
/-- Decomposes a tensor into a tensor product of two tensors
one which has indices in the image of the given embedding, and the other has indices in
the complement of that image. -/
def decompEmbed (f : Y ↪ X) :
𝓣.Tensor cX ≃ₗ[R] 𝓣.Tensor (𝓣.decompEmbedColorLeft cX f) ⊗[R] 𝓣.Tensor (cX ∘ f) :=
(𝓣.mapIso (decompEmbedSet f) (𝓣.decompEmbed_cond cX f)) ≪≫ₗ
(𝓣.tensoratorEquiv (𝓣.decompEmbedColorLeft cX f) (𝓣.decompEmbedColorRight cX f)).symm
/-!
## Contraction
-/
/-- A linear map taking tensors mapped with the same index set to the product of paired tensors. -/
def pairProd : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cX2 →ₗ[R]
⨂[R] x, 𝓣.ColorModule (cX x) ⊗[R] 𝓣.ColorModule (cX2 x) :=
TensorProduct.lift (
PiTensorProduct.map₂ (fun x =>
TensorProduct.mk R (𝓣.ColorModule (cX x)) (𝓣.ColorModule (cX2 x))))
lemma mkPiAlgebra_equiv (e : X ≃ Y) :
(PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R X R)) =
(PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R Y R)) ∘ₗ
(PiTensorProduct.reindex R _ e).toLinearMap := by
apply PiTensorProduct.ext
apply MultilinearMap.ext
intro x
simp only [LinearMap.compMultilinearMap_apply, PiTensorProduct.lift.tprod,
MultilinearMap.mkPiAlgebra_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
PiTensorProduct.reindex_tprod, Equiv.prod_comp]
/-- Given a tensor in `𝓣.Tensor cX` and a tensor in `𝓣.Tensor (𝓣.τ ∘ cX)`, the element of
`R` formed by contracting all of their indices. -/
def contrAll' : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor (𝓣.τ ∘ cX) →ₗ[R] R :=
(PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R X R)) ∘ₗ
(PiTensorProduct.map (fun x => 𝓣.contrDual (cX x))) ∘ₗ
(𝓣.pairProd)
lemma contrAll'_mapIso_cond {e : X ≃ Y} (h : cX = cY ∘ e) :
𝓣.τ ∘ cY = (𝓣.τ ∘ cX) ∘ ⇑e.symm := by
subst h
exact (Equiv.eq_comp_symm e (𝓣.τ ∘ cY) (𝓣.τ ∘ cY ∘ ⇑e)).mpr rfl
@[simp]
lemma contrAll'_mapIso (e : X ≃ Y) (h : c = cY ∘ e) :
𝓣.contrAll' ∘ₗ
(TensorProduct.congr (𝓣.mapIso e h) (LinearEquiv.refl R _)).toLinearMap =
𝓣.contrAll' ∘ₗ (TensorProduct.congr (LinearEquiv.refl R _)
(𝓣.mapIso e.symm (𝓣.contrAll'_mapIso_cond h))).toLinearMap := by
apply TensorProduct.ext'
refine fun x ↦
PiTensorProduct.induction_on' x ?_ (by
intro a b hx hy y
simp [map_add, add_tmul, hx, hy])
intro rx fx
refine fun y ↦
PiTensorProduct.induction_on' y ?_ (by
intro a b hx hy
simp at hx hy
simp [map_add, tmul_add, hx, hy])
intro ry fy
simp [contrAll']
rw [mkPiAlgebra_equiv e]
apply congrArg
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply]
apply congrArg
rw [← LinearEquiv.symm_apply_eq]
rw [PiTensorProduct.reindex_symm]
rw [← PiTensorProduct.map_reindex]
subst h
simp only [Equiv.symm_symm_apply, Function.comp_apply]
apply congrArg
rw [pairProd, pairProd]
simp only [Function.comp_apply, lift.tmul, LinearMapClass.map_smul, LinearMap.smul_apply]
apply congrArg
change _ = ((PiTensorProduct.map₂ fun x => TensorProduct.mk R (𝓣.ColorModule (cY (e x)))
(𝓣.ColorModule (𝓣.τ (cY (e x)))))
((PiTensorProduct.tprod R) fx))
((𝓣.mapIso e.symm _) ((PiTensorProduct.tprod R) fy))
rw [mapIso_tprod]
simp only [Equiv.symm_symm_apply, Function.comp_apply]
rw [PiTensorProduct.map₂_tprod_tprod]
change PiTensorProduct.reindex R _ e.symm
((PiTensorProduct.map₂ _
((PiTensorProduct.tprod R) fun i => (𝓣.colorModuleCast _) (fx (e.symm i))))
((PiTensorProduct.tprod R) fy)) = _
rw [PiTensorProduct.map₂_tprod_tprod]
simp only [Equiv.symm_symm_apply, Function.comp_apply, mk_apply]
erw [PiTensorProduct.reindex_tprod]
apply congrArg
funext i
simp only [Equiv.symm_symm_apply]
congr
simp [colorModuleCast]
apply cast_eq_iff_heq.mpr
rw [Equiv.symm_apply_apply]
@[simp]
lemma contrAll'_mapIso_tmul (e : X ≃ Y) (h : c = cY ∘ e) (x : 𝓣.Tensor c)
(y : 𝓣.Tensor (𝓣.τ ∘ cY)) : 𝓣.contrAll' ((𝓣.mapIso e h) x ⊗ₜ[R] y) =
𝓣.contrAll' (x ⊗ₜ[R] (𝓣.mapIso e.symm (𝓣.contrAll'_mapIso_cond h) y)) := by
change (𝓣.contrAll' ∘ₗ
(TensorProduct.congr (𝓣.mapIso e h) (LinearEquiv.refl R _)).toLinearMap) (x ⊗ₜ[R] y) = _
rw [contrAll'_mapIso]
rfl
/-- The contraction of all the indices of two tensors with dual colors. -/
def contrAll {c : X → 𝓣.Color} {d : Y → 𝓣.Color}
(e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e) : 𝓣.Tensor c ⊗[R] 𝓣.Tensor d →ₗ[R] R :=
𝓣.contrAll' ∘ₗ (TensorProduct.congr (LinearEquiv.refl _ _)
(𝓣.mapIso e.symm (by subst h; funext a; simp; rw [𝓣.τ_involutive]))).toLinearMap
lemma contrAll_symm_cond {e : X ≃ Y} (h : c = 𝓣.τ ∘ cY ∘ e) :
cY = 𝓣.τ ∘ c ∘ ⇑e.symm := by
subst h
ext1 x
simp only [Function.comp_apply, Equiv.apply_symm_apply]
rw [𝓣.τ_involutive]
lemma contrAll_mapIso_right_cond {e : X ≃ Y} {e' : Z ≃ Y}
(h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') : c = 𝓣.τ ∘ cZ ∘ ⇑(e.trans e'.symm) := by
subst h h'
ext1 x
simp only [Function.comp_apply, Equiv.coe_trans, Equiv.apply_symm_apply]
@[simp]
lemma contrAll_mapIso_right_tmul (e : X ≃ Y) (e' : Z ≃ Y)
(h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') (x : 𝓣.Tensor c) (z : 𝓣.Tensor cZ) :
𝓣.contrAll e h (x ⊗ₜ[R] 𝓣.mapIso e' h' z) =
𝓣.contrAll (e.trans e'.symm) (𝓣.contrAll_mapIso_right_cond h h') (x ⊗ₜ[R] z) := by
rw [contrAll, contrAll]
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, congr_tmul,
LinearEquiv.refl_apply, mapIso_mapIso]
congr
@[simp]
lemma contrAll_comp_mapIso_right (e : X ≃ Y) (e' : Z ≃ Y)
(h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = cY ∘ e') : 𝓣.contrAll e h ∘ₗ
(TensorProduct.congr (LinearEquiv.refl R (𝓣.Tensor c)) (𝓣.mapIso e' h')).toLinearMap
= 𝓣.contrAll (e.trans e'.symm) (𝓣.contrAll_mapIso_right_cond h h') := by
apply TensorProduct.ext'
intro x y
exact 𝓣.contrAll_mapIso_right_tmul e e' h h' x y
lemma contrAll_mapIso_left_cond {e : X ≃ Y} {e' : Z ≃ X}
(h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = c ∘ e') : cZ = 𝓣.τ ∘ cY ∘ ⇑(e'.trans e) := by
subst h h'
ext1 x
simp only [Function.comp_apply, Equiv.coe_trans, Equiv.apply_symm_apply]
@[simp]
lemma contrAll_mapIso_left_tmul {e : X ≃ Y} {e' : Z ≃ X}
(h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = c ∘ e') (x : 𝓣.Tensor cZ) (y : 𝓣.Tensor cY) :
𝓣.contrAll e h (𝓣.mapIso e' h' x ⊗ₜ[R] y) =
𝓣.contrAll (e'.trans e) (𝓣.contrAll_mapIso_left_cond h h') (x ⊗ₜ[R] y) := by
rw [contrAll, contrAll]
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, congr_tmul,
LinearEquiv.refl_apply, contrAll'_mapIso_tmul, mapIso_mapIso]
congr
@[simp]
lemma contrAll_mapIso_left {e : X ≃ Y} {e' : Z ≃ X}
(h : c = 𝓣.τ ∘ cY ∘ e) (h' : cZ = c ∘ e') :
𝓣.contrAll e h ∘ₗ
(TensorProduct.congr (𝓣.mapIso e' h') (LinearEquiv.refl R (𝓣.Tensor cY))).toLinearMap
= 𝓣.contrAll (e'.trans e) (𝓣.contrAll_mapIso_left_cond h h') := by
apply TensorProduct.ext'
intro x y
exact 𝓣.contrAll_mapIso_left_tmul h h' x y
end PreTensorStructure
/-! TODO: Add unit here. -/
/-- A `PreTensorStructure` with the additional constraint that `contrDua` is symmetric. -/
structure TensorStructure (R : Type) [CommSemiring R] extends PreTensorStructure R where
/-- The symmetry condition on `contrDua`. -/
contrDual_symm : ∀ μ,
(contrDual μ) ∘ₗ (TensorProduct.comm R (ColorModule (τ μ)) (ColorModule μ)).toLinearMap =
(contrDual (τ μ)) ∘ₗ (TensorProduct.congr (LinearEquiv.refl _ _)
(toPreTensorStructure.colorModuleCast (by rw[toPreTensorStructure.τ_involutive]))).toLinearMap
namespace TensorStructure
open PreTensorStructure
variable (𝓣 : TensorStructure R)
variable {d : ℕ} {X Y Y' Z : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
[Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z]
{c c₂ : X → 𝓣.Color} {d : Y → 𝓣.Color} {b : Z → 𝓣.Color} {d' : Y' → 𝓣.Color} {μ ν: 𝓣.Color}
end TensorStructure
/-- A `TensorStructure` with a group action. -/
structure GroupTensorStructure (R : Type) [CommSemiring R]
(G : Type) [Group G] extends TensorStructure R where
/-- For each color `μ` a representation of `G` on `ColorModule μ`. -/
repColorModule : (μ : Color) → Representation R G (ColorModule μ)
/-- The contraction of a vector with its dual is invariant under the group action. -/
contrDual_inv : ∀ μ g, contrDual μ ∘ₗ
TensorProduct.map (repColorModule μ g) (repColorModule (τ μ) g) = contrDual μ
namespace GroupTensorStructure
open TensorStructure
open PreTensorStructure
variable {G : Type} [Group G]
variable (𝓣 : GroupTensorStructure R G)
variable {d : ℕ} {X Y Y' Z : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
[Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z]
{cX cX2 : X → 𝓣.Color} {cY : Y → 𝓣.Color} {cZ : Z → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν: 𝓣.Color}
/-- The representation of the group `G` on the vector space of tensors. -/
def rep : Representation R G (𝓣.Tensor cX) where
toFun g := PiTensorProduct.map (fun x => 𝓣.repColorModule (cX x) g)
map_one' := by
simp_all only [_root_.map_one, PiTensorProduct.map_one]
map_mul' g g' := by
simp_all only [_root_.map_mul]
exact PiTensorProduct.map_mul _ _
local infixl:78 " • " => 𝓣.rep
lemma repColorModule_colorModuleCast_apply (h : μ = ν) (g : G) (x : 𝓣.ColorModule μ) :
(𝓣.repColorModule ν g) (𝓣.colorModuleCast h x) =
(𝓣.colorModuleCast h) (𝓣.repColorModule μ g x) := by
subst h
simp [colorModuleCast]
@[simp]
lemma repColorModule_colorModuleCast (h : μ = ν) (g : G) :
(𝓣.repColorModule ν g) ∘ₗ (𝓣.colorModuleCast h).toLinearMap =
(𝓣.colorModuleCast h).toLinearMap ∘ₗ (𝓣.repColorModule μ g) := by
apply LinearMap.ext
intro x
simp [repColorModule_colorModuleCast_apply]
@[simp]
lemma rep_mapIso (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) :
(𝓣.rep g) ∘ₗ (𝓣.mapIso e h).toLinearMap = (𝓣.mapIso e h).toLinearMap ∘ₗ 𝓣.rep g := by
apply PiTensorProduct.ext
apply MultilinearMap.ext
intro x
simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, LinearEquiv.coe_coe,
Function.comp_apply]
erw [mapIso_tprod]
simp [rep, repColorModule_colorModuleCast_apply]
change (PiTensorProduct.map fun x => (𝓣.repColorModule (cY x)) g)
((PiTensorProduct.tprod R) fun i => (𝓣.colorModuleCast _) (x (e.symm i))) =
(𝓣.mapIso e h) ((PiTensorProduct.map _) ((PiTensorProduct.tprod R) x))
rw [PiTensorProduct.map_tprod, PiTensorProduct.map_tprod]
rw [mapIso_tprod]
apply congrArg
funext i
subst h
simp [repColorModule_colorModuleCast_apply]
@[simp]
lemma rep_mapIso_apply (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) (x : 𝓣.Tensor cX) :
g • (𝓣.mapIso e h x) = (𝓣.mapIso e h) (g • x) := by
trans ((𝓣.rep g) ∘ₗ (𝓣.mapIso e h).toLinearMap) x
rfl
simp
@[simp]
lemma rep_tprod (g : G) (f : (i : X) → 𝓣.ColorModule (cX i)) :
g • (PiTensorProduct.tprod R f) = PiTensorProduct.tprod R (fun x =>
𝓣.repColorModule (cX x) g (f x)) := by
simp [rep]
change (PiTensorProduct.map _) ((PiTensorProduct.tprod R) f) = _
rw [PiTensorProduct.map_tprod]
/-!
## Group acting on tensor products
-/
lemma rep_tensoratorEquiv (g : G) :
(𝓣.tensoratorEquiv cX cY) ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g)) = 𝓣.rep g ∘ₗ
(𝓣.tensoratorEquiv cX cY).toLinearMap := by
apply tensorProd_piTensorProd_ext
intro p q
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, map_tmul, rep_tprod,
tensoratorEquiv_tmul_tprod]
apply congrArg
funext x
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl
lemma rep_tensoratorEquiv_apply (g : G) (x : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY) :
(𝓣.tensoratorEquiv cX cY) ((TensorProduct.map (𝓣.rep g) (𝓣.rep g)) x)
= (𝓣.rep g) ((𝓣.tensoratorEquiv cX cY) x) := by
trans ((𝓣.tensoratorEquiv cX cY) ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g))) x
rfl
rw [rep_tensoratorEquiv]
rfl
lemma rep_tensoratorEquiv_tmul (g : G) (x : 𝓣.Tensor cX) (y : 𝓣.Tensor cY) :
(𝓣.tensoratorEquiv cX cY) ((g • x) ⊗ₜ[R] (g • y)) =
g • ((𝓣.tensoratorEquiv cX cY) (x ⊗ₜ[R] y)) := by
nth_rewrite 1 [← rep_tensoratorEquiv_apply]
rfl
/-!
## Group acting on contraction
-/
@[simp]
lemma contrAll_rep {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e) (g : G) :
𝓣.contrAll e h ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g)) = 𝓣.contrAll e h := by
apply TensorProduct.ext'
refine fun x ↦ PiTensorProduct.induction_on' x ?_ (by
intro a b hx hy y
simp [map_add, add_tmul, hx, hy])
intro rx fx
refine fun y ↦ PiTensorProduct.induction_on' y ?_ (by
intro a b hx hy
simp at hx hy
simp [map_add, tmul_add, hx, hy])
intro ry fy
simp [contrAll, TensorProduct.smul_tmul]
apply congrArg
apply congrArg
simp [contrAll']
apply congrArg
simp [pairProd]
change (PiTensorProduct.map _) ((PiTensorProduct.map₂ _ _) _) =
(PiTensorProduct.map _) ((PiTensorProduct.map₂ _ _) _)
rw [PiTensorProduct.map₂_tprod_tprod, PiTensorProduct.map₂_tprod_tprod, PiTensorProduct.map_tprod,
PiTensorProduct.map_tprod]
simp only [mk_apply]
apply congrArg
funext x
rw [← repColorModule_colorModuleCast_apply]
nth_rewrite 2 [← 𝓣.contrDual_inv (c x) g]
rfl
@[simp]
lemma contrAll_rep_apply {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e)
(g : G) (x : 𝓣.Tensor c ⊗ 𝓣.Tensor d) :
𝓣.contrAll e h (TensorProduct.map (𝓣.rep g) (𝓣.rep g) x) = 𝓣.contrAll e h x := by
change (𝓣.contrAll e h ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g))) x = _
rw [contrAll_rep]
@[simp]
lemma contrAll_rep_tmul {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃ Y) (h : c = 𝓣.τ ∘ d ∘ e)
(g : G) (x : 𝓣.Tensor c) (y : 𝓣.Tensor d) :
𝓣.contrAll e h ((g • x) ⊗ₜ[R] (g • y)) = 𝓣.contrAll e h (x ⊗ₜ[R] y) := by
nth_rewrite 2 [← contrAll_rep_apply]
rfl
end GroupTensorStructure
end

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

@ -1,661 +0,0 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import Mathlib.Logic.Function.CompTypeclasses
import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.BigOperators
import Mathlib.Logic.Equiv.Fin
import Mathlib.Tactic.FinCases
import Mathlib.Logic.Equiv.Fintype
/-!
# Real Lorentz Tensors
In this file we define real Lorentz tensors.
We implicitly follow the definition of a modular operad.
This will relation should be made explicit in the future.
## References
-- For modular operads see: [Raynor][raynor2021graphical]
-/
/-! TODO: Do complex tensors, with Van der Waerden notation for fermions. -/
/-! TODO: Generalize to maps into Lorentz tensors. -/
/-- The possible `colors` of an index for a RealLorentzTensor.
There are two possiblities, `up` and `down`. -/
inductive RealLorentzTensor.Colors where
| up : RealLorentzTensor.Colors
| down : RealLorentzTensor.Colors
/-- The association of colors with indices. For up and down this is `Fin 1 ⊕ Fin d`. -/
def RealLorentzTensor.ColorsIndex (d : ℕ) (μ : RealLorentzTensor.Colors) : Type :=
match μ with
| RealLorentzTensor.Colors.up => Fin 1 ⊕ Fin d
| RealLorentzTensor.Colors.down => Fin 1 ⊕ Fin d
instance (d : ℕ) (μ : RealLorentzTensor.Colors) : Fintype (RealLorentzTensor.ColorsIndex d μ) :=
match μ with
| RealLorentzTensor.Colors.up => instFintypeSum (Fin 1) (Fin d)
| RealLorentzTensor.Colors.down => instFintypeSum (Fin 1) (Fin d)
instance (d : ℕ) (μ : RealLorentzTensor.Colors) : DecidableEq (RealLorentzTensor.ColorsIndex d μ) :=
match μ with
| RealLorentzTensor.Colors.up => instDecidableEqSum
| RealLorentzTensor.Colors.down => instDecidableEqSum
/-- An `IndexValue` is a set of actual values an index can take. e.g. for a
3-tensor (0, 1, 2). -/
def RealLorentzTensor.IndexValue {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) :
Type 0 := (x : X) → RealLorentzTensor.ColorsIndex d (c x)
/-- A Lorentz Tensor defined by its coordinate map. -/
structure RealLorentzTensor (d : ℕ) (X : Type) where
/-- The color associated to each index of the tensor. -/
color : X → RealLorentzTensor.Colors
/-- The coordinate map for the tensor. -/
coord : RealLorentzTensor.IndexValue d color → ℝ
namespace RealLorentzTensor
open Matrix
universe u1
variable {d : ℕ} {X Y Z : Type} (c : X → Colors)
/-!
## Colors
-/
/-- The involution acting on colors. -/
def τ : Colors → Colors
| Colors.up => Colors.down
| Colors.down => Colors.up
/-- The map τ is an involution. -/
@[simp]
lemma τ_involutive : Function.Involutive τ := by
intro x
cases x <;> rfl
lemma color_eq_dual_symm {μ ν : Colors} (h : μ = τ ν) : ν = τ μ :=
(Function.Involutive.eq_iff τ_involutive).mp h.symm
/-- The color associated with an element of `x ∈ X` for a tensor `T`. -/
def ch {X : Type} (x : X) (T : RealLorentzTensor d X) : Colors := T.color x
/-- An equivalence of `ColorsIndex` types given an equality of colors. -/
def colorsIndexCast {d : ℕ} {μ₁ μ₂ : RealLorentzTensor.Colors} (h : μ₁ = μ₂) :
ColorsIndex d μ₁ ≃ ColorsIndex d μ₂ :=
Equiv.cast (congrArg (ColorsIndex d) h)
/-- An equivalence of `ColorsIndex` between that of a color and that of its dual. -/
def colorsIndexDualCastSelf {d : ℕ} {μ : RealLorentzTensor.Colors}:
ColorsIndex d μ ≃ ColorsIndex d (τ μ) where
toFun x :=
match μ with
| RealLorentzTensor.Colors.up => x
| RealLorentzTensor.Colors.down => x
invFun x :=
match μ with
| RealLorentzTensor.Colors.up => x
| RealLorentzTensor.Colors.down => x
left_inv x := by cases μ <;> rfl
right_inv x := by cases μ <;> rfl
/-- An equivalence of `ColorsIndex` types given an equality of a color and the dual of a color. -/
def colorsIndexDualCast {μ ν : Colors} (h : μ = τ ν) :
ColorsIndex d μ ≃ ColorsIndex d ν :=
(colorsIndexCast h).trans colorsIndexDualCastSelf.symm
lemma colorsIndexDualCast_symm {μ ν : Colors} (h : μ = τ ν) :
(colorsIndexDualCast h).symm =
@colorsIndexDualCast d _ _ ((Function.Involutive.eq_iff τ_involutive).mp h.symm) := by
match μ, ν with
| Colors.up, Colors.down => rfl
| Colors.down, Colors.up => rfl
/-!
## Index values
-/
instance [Fintype X] [DecidableEq X] : Fintype (IndexValue d c) := Pi.fintype
instance [Fintype X] : DecidableEq (IndexValue d c) :=
Fintype.decidablePiFintype
/-!
## Induced isomorphisms between IndexValue sets
-/
/-- An isomorphism of the type of index values given an isomorphism of sets. -/
@[simps!]
def indexValueIso (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors} (h : i = j ∘ f) :
IndexValue d i ≃ IndexValue d j :=
(Equiv.piCongrRight (fun μ => colorsIndexCast (congrFun h μ))).trans $
Equiv.piCongrLeft (fun y => RealLorentzTensor.ColorsIndex d (j y)) f
lemma indexValueIso_symm_apply' (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors}
(h : i = j ∘ f) (y : IndexValue d j) (x : X) :
(indexValueIso d f h).symm y x = (colorsIndexCast (congrFun h x)).symm (y (f x)) := by
rfl
@[simp]
lemma indexValueIso_trans (d : ℕ) (f : X ≃ Y) (g : Y ≃ Z) {i : X → Colors}
{j : Y → Colors} {k : Z → Colors} (h : i = j ∘ f) (h' : j = k ∘ g) :
(indexValueIso d f h).trans (indexValueIso d g h') =
indexValueIso d (f.trans g) (by rw [h, h', Function.comp.assoc]; rfl) := by
have h1 : ((indexValueIso d f h).trans (indexValueIso d g h')).symm =
(indexValueIso d (f.trans g) (by rw [h, h', Function.comp.assoc]; rfl)).symm := by
subst h' h
exact Equiv.coe_inj.mp rfl
simpa only [Equiv.symm_symm] using congrArg (fun e => e.symm) h1
lemma indexValueIso_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
(indexValueIso d f h).symm =
indexValueIso d f.symm ((Equiv.eq_comp_symm f j i).mpr (id (Eq.symm h))) := by
ext i : 1
rw [← Equiv.symm_apply_eq]
funext y
rw [indexValueIso_symm_apply', indexValueIso_symm_apply']
simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast]
apply cast_eq_iff_heq.mpr
rw [Equiv.apply_symm_apply]
lemma indexValueIso_eq_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
indexValueIso d f h =
(indexValueIso d f.symm ((Equiv.eq_comp_symm f j i).mpr (id (Eq.symm h)))).symm := by
rw [indexValueIso_symm]
rfl
@[simp]
lemma indexValueIso_refl (d : ℕ) (i : X → Colors) :
indexValueIso d (Equiv.refl X) (rfl : i = i) = Equiv.refl _ := by
rfl
/-!
## Dual isomorphism for index values
-/
/-- The isomorphism between the index values of a color map and its dual. -/
@[simps!]
def indexValueDualIso (d : ℕ) {i j : X → Colors} (h : i = τ ∘ j) :
IndexValue d i ≃ IndexValue d j :=
(Equiv.piCongrRight (fun μ => colorsIndexDualCast (congrFun h μ)))
/-!
## Extensionality
-/
lemma ext {T₁ T₂ : RealLorentzTensor d X} (h : T₁.color = T₂.color)
(h' : T₁.coord = fun i => T₂.coord (indexValueIso d (Equiv.refl X) h i)) :
T₁ = T₂ := by
cases T₁
cases T₂
simp_all only [IndexValue, mk.injEq]
apply And.intro h
simp only at h
subst h
simp only [Equiv.cast_refl, Equiv.coe_refl, CompTriple.comp_eq] at h'
rfl
/-!
## Mapping isomorphisms.
-/
/-- An equivalence of Tensors given an equivalence of underlying sets. -/
@[simps!]
def mapIso (d : ℕ) (f : X ≃ Y) : RealLorentzTensor d X ≃ RealLorentzTensor d Y where
toFun T := {
color := T.color ∘ f.symm,
coord := T.coord ∘ (indexValueIso d f (by simp : T.color = T.color ∘ f.symm ∘ f)).symm}
invFun T := {
color := T.color ∘ f,
coord := T.coord ∘ (indexValueIso d f.symm (by simp : T.color = T.color ∘ f ∘ f.symm)).symm}
left_inv T := by
refine ext ?_ ?_
· simp [Function.comp.assoc]
· funext i
simp only [IndexValue, Function.comp_apply, Function.comp_id]
apply congrArg
funext x
erw [indexValueIso_symm_apply', indexValueIso_symm_apply', indexValueIso_eq_symm,
indexValueIso_symm_apply']
rw [← Equiv.apply_eq_iff_eq_symm_apply]
simp only [Equiv.refl_symm, Equiv.coe_refl, Function.comp_apply, id_eq, colorsIndexCast,
Equiv.cast_symm, Equiv.cast_apply, cast_cast, Equiv.refl_apply]
apply cast_eq_iff_heq.mpr
congr
exact Equiv.symm_apply_apply f x
right_inv T := by
refine ext ?_ ?_
· simp [Function.comp.assoc]
· funext i
simp only [IndexValue, Function.comp_apply, Function.comp_id]
apply congrArg
funext x
erw [indexValueIso_symm_apply', indexValueIso_symm_apply', indexValueIso_eq_symm,
indexValueIso_symm_apply']
rw [← Equiv.apply_eq_iff_eq_symm_apply]
simp only [Equiv.refl_symm, Equiv.coe_refl, Function.comp_apply, id_eq, colorsIndexCast,
Equiv.cast_symm, Equiv.cast_apply, cast_cast, Equiv.refl_apply]
apply cast_eq_iff_heq.mpr
congr
exact Equiv.apply_symm_apply f x
@[simp]
lemma mapIso_trans (f : X ≃ Y) (g : Y ≃ Z) :
(mapIso d f).trans (mapIso d g) = mapIso d (f.trans g) := by
refine Equiv.coe_inj.mp ?_
funext T
refine ext rfl ?_
simp only [Equiv.trans_apply, IndexValue, mapIso_apply_color, Equiv.symm_trans_apply,
indexValueIso_refl, Equiv.refl_apply, mapIso_apply_coord]
funext i
rw [mapIso_apply_coord, mapIso_apply_coord]
apply congrArg
rw [← indexValueIso_trans]
rfl
exact (Equiv.comp_symm_eq f (T.color ∘ ⇑f.symm) T.color).mp rfl
lemma mapIso_symm (f : X ≃ Y) : (mapIso d f).symm = mapIso d f.symm := rfl
lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl
/-!
## Sums
-/
/-- An equivalence that splits elements of `IndexValue d (Sum.elim TX TY)` into two components. -/
def indexValueSumEquiv {X Y : Type} {TX : X → Colors} {TY : Y → Colors} :
IndexValue d (Sum.elim TX TY) ≃ IndexValue d TX × IndexValue d TY where
toFun i := (fun x => i (Sum.inl x), fun x => i (Sum.inr x))
invFun p := fun c => match c with
| Sum.inl x => (p.1 x)
| Sum.inr x => (p.2 x)
left_inv i := by
simp only [IndexValue]
ext1 x
cases x with
| inl val => rfl
| inr val_1 => rfl
right_inv p := rfl
/-- An equivalence between index values formed by commuting sums. -/
def indexValueSumComm {X Y : Type} (Tc : X → Colors) (Sc : Y → Colors) :
IndexValue d (Sum.elim Tc Sc) ≃ IndexValue d (Sum.elim Sc Tc) :=
indexValueIso d (Equiv.sumComm X Y) (by aesop)
/-!
## Marked Lorentz tensors
To define contraction and multiplication of Lorentz tensors we need to mark indices.
-/
/-- A `RealLorentzTensor` with `n` marked indices. -/
def Marked (d : ℕ) (X : Type) (n : ℕ) : Type :=
RealLorentzTensor d (X ⊕ Fin n)
namespace Marked
variable {n m : ℕ}
/-- The marked point. -/
def markedPoint (X : Type) (i : Fin n) : (X ⊕ Fin n) :=
Sum.inr i
/-- The colors of unmarked indices. -/
def unmarkedColor (T : Marked d X n) : X → Colors :=
T.color ∘ Sum.inl
/-- The colors of marked indices. -/
def markedColor (T : Marked d X n) : Fin n → Colors :=
T.color ∘ Sum.inr
/-- The index values restricted to unmarked indices. -/
def UnmarkedIndexValue (T : Marked d X n) : Type :=
IndexValue d T.unmarkedColor
instance [Fintype X] [DecidableEq X] (T : Marked d X n) : Fintype T.UnmarkedIndexValue :=
Pi.fintype
instance [Fintype X] (T : Marked d X n) : DecidableEq T.UnmarkedIndexValue :=
Fintype.decidablePiFintype
/-- The index values restricted to marked indices. -/
def MarkedIndexValue (T : Marked d X n) : Type :=
IndexValue d T.markedColor
instance (T : Marked d X n) : Fintype T.MarkedIndexValue :=
Pi.fintype
instance (T : Marked d X n) : DecidableEq T.MarkedIndexValue :=
Fintype.decidablePiFintype
lemma color_eq_elim (T : Marked d X n) :
T.color = Sum.elim T.unmarkedColor T.markedColor := by
ext1 x
cases' x <;> rfl
/-- An equivalence splitting elements of `IndexValue d T.color` into their two components. -/
def splitIndexValue {T : Marked d X n} :
IndexValue d T.color ≃ T.UnmarkedIndexValue × T.MarkedIndexValue :=
(indexValueIso d (Equiv.refl _) T.color_eq_elim).trans
indexValueSumEquiv
@[simp]
lemma splitIndexValue_sum {T : Marked d X n} [Fintype X] [DecidableEq X]
(P : T.UnmarkedIndexValue × T.MarkedIndexValue → ℝ) :
∑ i, P (splitIndexValue i) = ∑ j, ∑ k, P (j, k) := by
rw [Equiv.sum_comp splitIndexValue, Fintype.sum_prod_type]
/-- Construction of marked index values for the case of 1 marked index. -/
def oneMarkedIndexValue {T : Marked d X 1} :
ColorsIndex d (T.color (markedPoint X 0)) ≃ T.MarkedIndexValue where
toFun x := fun i => match i with
| 0 => x
invFun i := i 0
left_inv x := rfl
right_inv i := by
funext x
fin_cases x
rfl
/-- Construction of marked index values for the case of 2 marked index. -/
def twoMarkedIndexValue (T : Marked d X 2) (x : ColorsIndex d (T.color (markedPoint X 0)))
(y : ColorsIndex d <| T.color <| markedPoint X 1) :
T.MarkedIndexValue := fun i =>
match i with
| 0 => x
| 1 => y
/-- An equivalence of types used to turn the first marked index into an unmarked index. -/
def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Fin n.succ) ≃ (X ⊕ Fin 1) ⊕ Fin n :=
trans (Equiv.sumCongr (Equiv.refl _)
(((Fin.castOrderIso (Nat.succ_eq_one_add n)).toEquiv.trans finSumFinEquiv.symm)))
(Equiv.sumAssoc _ _ _).symm
/-- Unmark the first marked index of a marked tensor. -/
def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ Fin 1) n :=
mapIso d (unmarkFirstSet X n)
/-!
## Marking elements.
-/
section markingElements
variable [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
/-- Splits a type based on an embedding from `Fin n` into elements not in the image of the
embedding, and elements in the image. -/
def markEmbeddingSet {n : ℕ} (f : Fin n ↪ X) :
X ≃ {x // x ∈ (Finset.image f Finset.univ)ᶜ} ⊕ Fin n :=
(Equiv.Set.sumCompl (Set.range ⇑f)).symm.trans <|
(Equiv.sumComm _ _).trans <|
Equiv.sumCongr ((Equiv.subtypeEquivRight (by simp))) <|
(Function.Embedding.toEquivRange f).symm
lemma markEmbeddingSet_on_mem {n : ℕ} (f : Fin n ↪ X) (x : X)
(hx : x ∈ Finset.image f Finset.univ) : markEmbeddingSet f x =
Sum.inr (f.toEquivRange.symm ⟨x, by simpa using hx⟩) := by
rw [markEmbeddingSet]
simp only [Equiv.trans_apply, Equiv.sumComm_apply, Equiv.sumCongr_apply]
rw [Equiv.Set.sumCompl_symm_apply_of_mem]
rfl
lemma markEmbeddingSet_on_not_mem {n : ℕ} (f : Fin n ↪ X) (x : X)
(hx : ¬ x ∈ (Finset.image f Finset.univ)) : markEmbeddingSet f x =
Sum.inl ⟨x, by simpa using hx⟩ := by
rw [markEmbeddingSet]
simp only [Equiv.trans_apply, Equiv.sumComm_apply, Equiv.sumCongr_apply]
rw [Equiv.Set.sumCompl_symm_apply_of_not_mem]
rfl
simpa using hx
/-- Marks the indices of tensor in the image of an embedding. -/
@[simps!]
def markEmbedding {n : ℕ} (f : Fin n ↪ X) :
RealLorentzTensor d X ≃ Marked d {x // x ∈ (Finset.image f Finset.univ)ᶜ} n :=
mapIso d (markEmbeddingSet f)
lemma markEmbeddingSet_on_mem_indexValue_apply {n : ℕ} (f : Fin n ↪ X) (T : RealLorentzTensor d X)
(i : IndexValue d (markEmbedding f T).color) (x : X) (hx : x ∈ (Finset.image f Finset.univ)) :
i (markEmbeddingSet f x) = colorsIndexCast (congrArg ((markEmbedding f) T).color
(markEmbeddingSet_on_mem f x hx).symm)
(i (Sum.inr (f.toEquivRange.symm ⟨x, by simpa using hx⟩))) := by
simp [colorsIndexCast]
symm
apply cast_eq_iff_heq.mpr
rw [markEmbeddingSet_on_mem f x hx]
lemma markEmbeddingSet_on_not_mem_indexValue_apply {n : ℕ}
(f : Fin n ↪ X) (T : RealLorentzTensor d X) (i : IndexValue d (markEmbedding f T).color)
(x : X) (hx : ¬ x ∈ (Finset.image f Finset.univ)) :
i (markEmbeddingSet f x) = colorsIndexCast (congrArg ((markEmbedding f) T).color
(markEmbeddingSet_on_not_mem f x hx).symm) (i (Sum.inl ⟨x, by simpa using hx⟩)) := by
simp [colorsIndexCast]
symm
apply cast_eq_iff_heq.mpr
rw [markEmbeddingSet_on_not_mem f x hx]
/-- An equivalence between the IndexValues for a tensor `T` and the corresponding
tensor with indices maked by an embedding. -/
@[simps!]
def markEmbeddingIndexValue {n : ℕ} (f : Fin n ↪ X) (T : RealLorentzTensor d X) :
IndexValue d T.color ≃ IndexValue d (markEmbedding f T).color :=
indexValueIso d (markEmbeddingSet f) (
(Equiv.comp_symm_eq (markEmbeddingSet f) ((markEmbedding f) T).color T.color).mp rfl)
lemma markEmbeddingIndexValue_apply_symm_on_mem {n : ℕ}
(f : Fin n.succ ↪ X) (T : RealLorentzTensor d X) (i : IndexValue d (markEmbedding f T).color)
(x : X) (hx : x ∈ (Finset.image f Finset.univ)) :
(markEmbeddingIndexValue f T).symm i x = (colorsIndexCast ((congrFun ((Equiv.comp_symm_eq
(markEmbeddingSet f) ((markEmbedding f) T).color T.color).mp rfl) x).trans
(congrArg ((markEmbedding f) T).color (markEmbeddingSet_on_mem f x hx)))).symm
(i (Sum.inr (f.toEquivRange.symm ⟨x, by simpa using hx⟩))) := by
rw [markEmbeddingIndexValue, indexValueIso_symm_apply']
rw [markEmbeddingSet_on_mem_indexValue_apply f T i x hx]
simp [colorsIndexCast]
lemma markEmbeddingIndexValue_apply_symm_on_not_mem {n : ℕ} (f : Fin n.succ ↪ X)
(T : RealLorentzTensor d X) (i : IndexValue d (markEmbedding f T).color) (x : X)
(hx : ¬ x ∈ (Finset.image f Finset.univ)) : (markEmbeddingIndexValue f T).symm i x =
(colorsIndexCast ((congrFun ((Equiv.comp_symm_eq
(markEmbeddingSet f) ((markEmbedding f) T).color T.color).mp rfl) x).trans
((congrArg ((markEmbedding f) T).color (markEmbeddingSet_on_not_mem f x hx))))).symm
(i (Sum.inl ⟨x, by simpa using hx⟩)) := by
rw [markEmbeddingIndexValue, indexValueIso_symm_apply']
rw [markEmbeddingSet_on_not_mem_indexValue_apply f T i x hx]
simp only [Nat.succ_eq_add_one, Function.comp_apply, markEmbedding_apply_color, colorsIndexCast,
Equiv.cast_symm, id_eq, eq_mp_eq_cast, eq_mpr_eq_cast, Equiv.cast_apply, cast_cast, cast_eq,
Equiv.cast_refl, Equiv.refl_symm]
rfl
/-- Given an equivalence of types, an embedding `f` to an embedding `g`, the equivalence
taking the complement of the image of `f` to the complement of the image of `g`. -/
@[simps!]
def equivEmbedCompl (e : X ≃ Y) {f : Fin n ↪ X} {g : Fin n ↪ Y} (he : f.trans e = g) :
{x // x ∈ (Finset.image f Finset.univ)ᶜ} ≃ {y // y ∈ (Finset.image g Finset.univ)ᶜ} :=
(Equiv.subtypeEquivOfSubtype' e).trans <|
(Equiv.subtypeEquivRight (fun x => by simp [← he, Equiv.eq_symm_apply]))
lemma markEmbedding_mapIso_right (e : X ≃ Y) (f : Fin n ↪ X) (g : Fin n ↪ Y) (he : f.trans e = g)
(T : RealLorentzTensor d X) : markEmbedding g (mapIso d e T) =
mapIso d (Equiv.sumCongr (equivEmbedCompl e he) (Equiv.refl (Fin n))) (markEmbedding f T) := by
rw [markEmbedding, markEmbedding]
erw [← Equiv.trans_apply, ← Equiv.trans_apply]
rw [mapIso_trans, mapIso_trans]
apply congrFun
repeat apply congrArg
refine Equiv.ext (fun x => ?_)
simp only [Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_refl]
by_cases hx : x ∈ Finset.image f Finset.univ
· rw [markEmbeddingSet_on_mem f x hx, markEmbeddingSet_on_mem g (e x) (by simpa [← he] using hx)]
subst he
simp only [Sum.map_inr, id_eq, Sum.inr.injEq, Equiv.symm_apply_eq,
Function.Embedding.toEquivRange_apply, Function.Embedding.trans_apply, Equiv.coe_toEmbedding,
Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq]
change x = f.toEquivRange _
rw [Equiv.apply_symm_apply]
· rw [markEmbeddingSet_on_not_mem f x hx,
markEmbeddingSet_on_not_mem g (e x) (by simpa [← he] using hx)]
subst he
rfl
lemma markEmbedding_mapIso_left {n m : ℕ} (e : Fin n ≃ Fin m) (f : Fin n ↪ X) (g : Fin m ↪ X)
(he : e.symm.toEmbedding.trans f = g) (T : RealLorentzTensor d X) :
markEmbedding g T = mapIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by
simpa [← he] using Equiv.forall_congr_left e)) e) (markEmbedding f T) := by
rw [markEmbedding, markEmbedding]
erw [← Equiv.trans_apply]
rw [mapIso_trans]
apply congrFun
repeat apply congrArg
refine Equiv.ext (fun x => ?_)
simp only [Equiv.trans_apply, Equiv.sumCongr_apply]
by_cases hx : x ∈ Finset.image f Finset.univ
· rw [markEmbeddingSet_on_mem f x hx, markEmbeddingSet_on_mem g x (by
simp [← he, hx]
obtain ⟨y, _, hy2⟩ := Finset.mem_image.mp hx
use e y
simpa using hy2)]
subst he
simp [Equiv.symm_apply_eq]
change x = f.toEquivRange _
rw [Equiv.apply_symm_apply]
· rw [markEmbeddingSet_on_not_mem f x hx, markEmbeddingSet_on_not_mem g x (by
simpa [← he, hx] using fun x => not_exists.mp (Finset.mem_image.mpr.mt hx) (e.symm x))]
subst he
rfl
/-!
## Marking a single element
-/
/-- An embedding from `Fin 1` into `X` given an element `x ∈ X`. -/
@[simps!]
def embedSingleton (x : X) : Fin 1 ↪ X :=
⟨![x], fun x y => by fin_cases x; fin_cases y; simp⟩
lemma embedSingleton_toEquivRange_symm (x : X) :
(embedSingleton x).toEquivRange.symm ⟨x, by simp⟩ = 0 := by
exact Fin.fin_one_eq_zero _
/-- Equivalence, taking a tensor to a tensor with a single marked index. -/
@[simps!]
def markSingle (x : X) : RealLorentzTensor d X ≃ Marked d {x' // x' ≠ x} 1 :=
(markEmbedding (embedSingleton x)).trans
(mapIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by simp)) (Equiv.refl _)))
/-- Equivalence between index values of a tensor and the corresponding tensor with a single
marked index. -/
@[simps!]
def markSingleIndexValue (T : RealLorentzTensor d X) (x : X) :
IndexValue d T.color ≃ IndexValue d (markSingle x T).color :=
(markEmbeddingIndexValue (embedSingleton x) T).trans <|
indexValueIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by simp)) (Equiv.refl _))
(by funext x_1; simp)
/-- Given an equivalence of types, taking `x` to `y` the corresponding equivalence of
subtypes of elements not equal to `x` and not equal to `y` respectively. -/
@[simps!]
def equivSingleCompl (e : X ≃ Y) {x : X} {y : Y} (he : e x = y) :
{x' // x' ≠ x} ≃ {y' // y' ≠ y} :=
(Equiv.subtypeEquivOfSubtype' e).trans <|
Equiv.subtypeEquivRight (fun a => by simp [Equiv.symm_apply_eq, he])
lemma markSingle_mapIso (e : X ≃ Y) (x : X) (y : Y) (he : e x = y)
(T : RealLorentzTensor d X) : markSingle y (mapIso d e T) =
mapIso d (Equiv.sumCongr (equivSingleCompl e he) (Equiv.refl _)) (markSingle x T) := by
rw [markSingle, Equiv.trans_apply]
rw [markEmbedding_mapIso_right e (embedSingleton x) (embedSingleton y)
(Function.Embedding.ext_iff.mp (fun a => by simpa using he)), markSingle, markEmbedding]
erw [← Equiv.trans_apply, ← Equiv.trans_apply, ← Equiv.trans_apply]
rw [mapIso_trans, mapIso_trans, mapIso_trans, mapIso_trans]
apply congrFun
repeat apply congrArg
refine Equiv.ext fun x => ?_
simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.sumCongr_trans,
Equiv.trans_refl, Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_trans, Equiv.coe_refl,
Sum.map_map, CompTriple.comp_eq]
subst he
rfl
/-!
## Marking two elements
-/
/-- An embedding from `Fin 2` given two inequivalent elements. -/
@[simps!]
def embedDoubleton (x y : X) (h : x ≠ y) : Fin 2 ↪ X :=
⟨![x, y], fun a b => by
fin_cases a <;> fin_cases b <;> simp [h]
exact h.symm⟩
end markingElements
end Marked
/-!
## Contraction of indices
-/
open Marked
/-- The contraction of the marked indices in a tensor with two marked indices. -/
def contr {X : Type} (T : Marked d X 2) (h : T.markedColor 0 = τ (T.markedColor 1)) :
RealLorentzTensor d X where
color := T.unmarkedColor
coord := fun i =>
∑ x, T.coord (splitIndexValue.symm (i, T.twoMarkedIndexValue x $ colorsIndexDualCast h x))
/-! TODO: Following the ethos of modular operads, prove properties of contraction. -/
/-! TODO: Use `contr` to generalize to any pair of marked index. -/
/-!
## Rising and lowering indices
Rising or lowering an index corresponds to changing the color of that index.
-/
/-! TODO: Define the rising and lowering of indices using contraction with the metric. -/
/-!
## Graphical species and Lorentz tensors
-/
/-! TODO: From Lorentz tensors graphical species. -/
/-! TODO: Show that the action of the Lorentz group defines an action on the graphical species. -/
end RealLorentzTensor

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

@ -1,401 +0,0 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.SpaceTime.LorentzTensor.Real.Basic
import HepLean.SpaceTime.LorentzTensor.Real.LorentzAction
import HepLean.SpaceTime.LorentzTensor.Real.Multiplication
/-!
# Constructors for real Lorentz tensors
In this file we will constructors of real Lorentz tensors from real numbers,
vectors and matrices.
We will derive properties of these constructors.
-/
namespace RealLorentzTensor
/-!
# Tensors from and to the reals
An important point that we shall see here is that there is a well defined map
to the real numbers, i.e. which is invariant under transformations of mapIso.
-/
/-- An equivalence from Real tensors on an empty set to `ℝ`. -/
@[simps!]
def toReal (d : ℕ) {X : Type} (h : IsEmpty X) : RealLorentzTensor d X ≃ ℝ where
toFun := fun T => T.coord (IsEmpty.elim h)
invFun := fun r => {
color := fun x => IsEmpty.elim h x,
coord := fun _ => r}
left_inv T := by
refine ext ?_ ?_
funext x
exact IsEmpty.elim h x
funext a
change T.coord (IsEmpty.elim h) = _
apply congrArg
funext x
exact IsEmpty.elim h x
right_inv x := rfl
/-- The real number obtained from a tensor is invariant under `mapIso`. -/
lemma toReal_mapIso (d : ℕ) {X Y : Type} (h : IsEmpty X) (f : X ≃ Y) :
(mapIso d f).trans (toReal d (Equiv.isEmpty f.symm)) = toReal d h := by
apply Equiv.ext
intro x
simp only [Equiv.trans_apply, toReal_apply, mapIso_apply_color, mapIso_apply_coord]
apply congrArg
funext x
exact IsEmpty.elim h x
/-!
# Tensors from reals, vectors and matrices
Note that that these definitions are not equivariant with respect to an
action of the Lorentz group. They are provided for constructive purposes.
-/
/-- A marked 1-tensor with a single up index constructed from a vector.
Note: This is not the same as rising indices on `ofVecDown`. -/
def ofVecUp {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
Marked d Empty 1 where
color := fun _ => Colors.up
coord := fun i => v <| i <| Sum.inr <| 0
/-- A marked 1-tensor with a single down index constructed from a vector.
Note: This is not the same as lowering indices on `ofVecUp`. -/
def ofVecDown {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
Marked d Empty 1 where
color := fun _ => Colors.down
coord := fun i => v <| i <| Sum.inr <| 0
/-- A tensor with two up indices constructed from a matrix.
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
def ofMatUpUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
Marked d Empty 2 where
color := fun _ => Colors.up
coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1))
/-- A tensor with two down indices constructed from a matrix.
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
def ofMatDownDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
Marked d Empty 2 where
color := fun _ => Colors.down
coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1))
/-- A marked 2-tensor with the first index up and the second index down.
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
@[simps!]
def ofMatUpDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
Marked d Empty 2 where
color := fun i => match i with
| Sum.inr 0 => Colors.up
| Sum.inr 1 => Colors.down
coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1))
/-- A marked 2-tensor with the first index down and the second index up.
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
def ofMatDownUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
Marked d Empty 2 where
color := fun i => match i with
| Sum.inr 0 => Colors.down
| Sum.inr 1 => Colors.up
coord := fun i => m (i (Sum.inr 0)) (i (Sum.inr 1))
/-!
## Equivalence of `IndexValue` for constructors
-/
/-- Index values for `ofVecUp v` are equivalent to elements of `Fin 1 ⊕ Fin d`. -/
def ofVecUpIndexValue (v : Fin 1 ⊕ Fin d → ℝ) :
IndexValue d (ofVecUp v).color ≃ (Fin 1 ⊕ Fin d) where
toFun i := i (Sum.inr 0)
invFun x := fun i => match i with
| Sum.inr 0 => x
left_inv i := by
funext y
match y with
| Sum.inr 0 => rfl
right_inv x := rfl
/-- Index values for `ofVecDown v` are equivalent to elements of `Fin 1 ⊕ Fin d`. -/
def ofVecDownIndexValue (v : Fin 1 ⊕ Fin d → ℝ) :
IndexValue d (ofVecDown v).color ≃ (Fin 1 ⊕ Fin d) where
toFun i := i (Sum.inr 0)
invFun x := fun i => match i with
| Sum.inr 0 => x
left_inv i := by
funext y
match y with
| Sum.inr 0 => rfl
right_inv x := rfl
/-- Index values for `ofMatUpUp v` are equivalent to elements of
`(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
def ofMatUpUpIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
IndexValue d (ofMatUpUp M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
toFun i := (i (Sum.inr 0), i (Sum.inr 1))
invFun x := fun i => match i with
| Sum.inr 0 => x.1
| Sum.inr 1 => x.2
left_inv i := by
funext y
match y with
| Sum.inr 0 => rfl
| Sum.inr 1 => rfl
right_inv x := rfl
/-- Index values for `ofMatDownDown v` are equivalent to elements of
`(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
def ofMatDownDownIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
IndexValue d (ofMatDownDown M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
toFun i := (i (Sum.inr 0), i (Sum.inr 1))
invFun x := fun i => match i with
| Sum.inr 0 => x.1
| Sum.inr 1 => x.2
left_inv i := by
funext y
match y with
| Sum.inr 0 => rfl
| Sum.inr 1 => rfl
right_inv x := rfl
/-- Index values for `ofMatUpDown v` are equivalent to elements of
`(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
def ofMatUpDownIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
IndexValue d (ofMatUpDown M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
toFun i := (i (Sum.inr 0), i (Sum.inr 1))
invFun x := fun i => match i with
| Sum.inr 0 => x.1
| Sum.inr 1 => x.2
left_inv i := by
funext y
match y with
| Sum.inr 0 => rfl
| Sum.inr 1 => rfl
right_inv x := rfl
/-- Index values for `ofMatDownUp v` are equivalent to elements of
`(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)`. -/
def ofMatDownUpIndexValue (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
IndexValue d (ofMatDownUp M).color ≃ (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) where
toFun i := (i (Sum.inr 0), i (Sum.inr 1))
invFun x := fun i => match i with
| Sum.inr 0 => x.1
| Sum.inr 1 => x.2
left_inv i := by
funext y
match y with
| Sum.inr 0 => rfl
| Sum.inr 1 => rfl
right_inv x := rfl
/-!
## Contraction of indices of tensors from matrices
-/
open Matrix
open Marked
/-- Contracting the indices of `ofMatUpDown` returns the trace of the matrix. -/
lemma contr_ofMatUpDown_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
contr (ofMatUpDown M) (by rfl) = (toReal d instIsEmptyEmpty).symm M.trace := by
refine ext ?_ rfl
· funext i
exact Empty.elim i
/-- Contracting the indices of `ofMatDownUp` returns the trace of the matrix. -/
lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
contr (ofMatDownUp M) (by rfl) = (toReal d instIsEmptyEmpty).symm M.trace := by
refine ext ?_ rfl
· funext i
exact Empty.elim i
/-!
## Multiplication of tensors from vectors and matrices
-/
/-- Multiplying `ofVecUp` with `ofVecDown` gives the dot product. -/
@[simp]
lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
mul (ofVecUp v₁) (ofVecDown v₂) rfl = (toReal d instIsEmptySum).symm (v₁ ⬝ᵥ v₂) := by
refine ext ?_ rfl
· funext i
exact IsEmpty.elim instIsEmptySum i
/-- 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
refine ext ?_ rfl
· funext i
exact IsEmpty.elim instIsEmptySum i
lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
(v : Fin 1 ⊕ Fin d → ℝ) :
mapIso d ((Equiv.sumEmpty (Empty ⊕ Fin 1) Empty))
(mul (unmarkFirst $ ofMatUpDown M) (ofVecUp v) rfl) = ofVecUp (M *ᵥ v) := by
refine ext ?_ rfl
· funext i
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, mapIso_apply_color, mul_color, Equiv.symm_symm]
fin_cases i
rfl
lemma mul_ofMatDownUp_ofVecDown_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
(v : Fin 1 ⊕ Fin d → ℝ) :
mapIso d (Equiv.sumEmpty (Empty ⊕ Fin 1) Empty)
(mul (unmarkFirst $ ofMatDownUp M) (ofVecDown v) rfl) = ofVecDown (M *ᵥ v) := by
refine ext ?_ rfl
· funext i
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, mapIso_apply_color, mul_color, Equiv.symm_symm]
fin_cases i
rfl
/-!
## The Lorentz action on constructors
-/
section lorentzAction
variable {d : ℕ} {X : Type} [Fintype X] [DecidableEq X] (T : RealLorentzTensor d X) (c : X → Colors)
variable (Λ Λ' : LorentzGroup d)
open Matrix
/-- The action of the Lorentz group on `ofReal v` is trivial. -/
@[simp]
lemma lorentzAction_toReal (h : IsEmpty X) (r : ℝ) :
Λ • (toReal d h).symm r = (toReal d h).symm r :=
lorentzAction_on_isEmpty Λ ((toReal d h).symm r)
/-- The action of the Lorentz group on `ofVecUp v` is by vector multiplication. -/
@[simp]
lemma lorentzAction_ofVecUp (v : Fin 1 ⊕ Fin d → ℝ) :
Λ • ofVecUp v = ofVecUp (Λ *ᵥ v) := by
refine ext rfl ?_
funext i
erw [lorentzAction_smul_coord]
simp only [ofVecUp, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
Finset.prod_empty, one_mul]
rw [mulVec]
simp only [Fin.isValue, dotProduct, Finset.univ_unique, Fin.default_eq_zero,
Finset.sum_singleton]
erw [Finset.sum_equiv (ofVecUpIndexValue v)]
intro i
simp_all only [Finset.mem_univ, Fin.isValue, Equiv.coe_fn_mk]
intro j _
simp_all only [Finset.mem_univ, Fin.isValue, Finset.prod_singleton, indexValueIso_refl]
rfl
/-- The action of the Lorentz group on `ofVecDown v` is
by vector multiplication of the transpose-inverse. -/
@[simp]
lemma lorentzAction_ofVecDown (v : Fin 1 ⊕ Fin d → ℝ) :
Λ • ofVecDown v = ofVecDown ((LorentzGroup.transpose Λ⁻¹) *ᵥ v) := by
refine ext rfl ?_
funext i
erw [lorentzAction_smul_coord]
simp only [ofVecDown, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
Finset.prod_empty, one_mul, lorentzGroupIsGroup_inv]
rw [mulVec]
simp only [Fin.isValue, dotProduct, Finset.univ_unique, Fin.default_eq_zero,
Finset.sum_singleton]
erw [Finset.sum_equiv (ofVecUpIndexValue v)]
intro i
simp_all only [Finset.mem_univ, Fin.isValue, Equiv.coe_fn_mk]
intro j _
simp_all only [Finset.mem_univ, Fin.isValue, Finset.prod_singleton, indexValueIso_refl]
rfl
@[simp]
lemma lorentzAction_ofMatUpUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
Λ • ofMatUpUp M = ofMatUpUp (Λ.1 * M * (LorentzGroup.transpose Λ).1) := by
refine ext rfl ?_
funext i
erw [lorentzAction_smul_coord]
erw [← Equiv.sum_comp (ofMatUpUpIndexValue M).symm]
simp only [ofMatUpUp, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
Finset.prod_empty, one_mul, mul_apply]
erw [Finset.sum_product]
rw [Finset.sum_comm]
refine Finset.sum_congr rfl (fun x _ => ?_)
rw [Finset.sum_mul]
refine Finset.sum_congr rfl (fun y _ => ?_)
simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue]
exact mul_right_comm _ _ _
@[simp]
lemma lorentzAction_ofMatDownDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
Λ • ofMatDownDown M = ofMatDownDown ((LorentzGroup.transpose Λ⁻¹).1 * M * (Λ⁻¹).1) := by
refine ext rfl ?_
funext i
erw [lorentzAction_smul_coord]
erw [← Equiv.sum_comp (ofMatDownDownIndexValue M).symm]
simp only [ofMatDownDown, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
Finset.prod_empty, one_mul, mul_apply]
erw [Finset.sum_product]
rw [Finset.sum_comm]
refine Finset.sum_congr rfl (fun x _ => ?_)
rw [Finset.sum_mul]
refine Finset.sum_congr rfl (fun y _ => ?_)
simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue]
exact mul_right_comm _ _ _
@[simp]
lemma lorentzAction_ofMatUpDown (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
Λ • ofMatUpDown M = ofMatUpDown (Λ.1 * M * (Λ⁻¹).1) := by
refine ext rfl ?_
funext i
erw [lorentzAction_smul_coord]
erw [← Equiv.sum_comp (ofMatUpDownIndexValue M).symm]
simp only [ofMatUpDown, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
Finset.prod_empty, one_mul, mul_apply]
erw [Finset.sum_product]
rw [Finset.sum_comm]
refine Finset.sum_congr rfl (fun x _ => ?_)
rw [Finset.sum_mul]
refine Finset.sum_congr rfl (fun y _ => ?_)
simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue]
exact mul_right_comm _ _ _
@[simp]
lemma lorentzAction_ofMatDownUp (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
Λ • ofMatDownUp M =
ofMatDownUp ((LorentzGroup.transpose Λ⁻¹).1 * M * (LorentzGroup.transpose Λ).1) := by
refine ext rfl ?_
funext i
erw [lorentzAction_smul_coord]
erw [← Equiv.sum_comp (ofMatDownUpIndexValue M).symm]
simp only [ofMatDownUp, IndexValue, Fin.isValue, Fintype.prod_sum_type, Finset.univ_eq_empty,
Finset.prod_empty, one_mul, mul_apply]
erw [Finset.sum_product]
rw [Finset.sum_comm]
refine Finset.sum_congr rfl (fun x _ => ?_)
rw [Finset.sum_mul]
refine Finset.sum_congr rfl (fun y _ => ?_)
simp only [Fin.prod_univ_two, Fin.isValue, indexValueIso_refl, IndexValue]
exact mul_right_comm _ _ _
end lorentzAction
end RealLorentzTensor

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

@ -1,444 +0,0 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.SpaceTime.LorentzTensor.Real.Basic
import HepLean.SpaceTime.LorentzGroup.Basic
/-!
# Lorentz group action on Real Lorentz Tensors
We define the action of the Lorentz group on Real Lorentz Tensors.
The Lorentz action is currently only defined for finite and decidable types `X`.
-/
namespace RealLorentzTensor
variable {d : ℕ} {X Y : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
(T : RealLorentzTensor d X) (c : X → Colors) (Λ Λ' : LorentzGroup d) {μ : Colors}
open LorentzGroup BigOperators Marked
/-- Monoid homomorphism from the Lorentz group to matrices indexed by `ColorsIndex d μ` for a
color `μ`.
This can be thought of as the representation of the Lorentz group for that color index. -/
def colorMatrix (μ : Colors) : LorentzGroup d →* Matrix (ColorsIndex d μ) (ColorsIndex d μ) ℝ where
toFun Λ := match μ with
| .up => fun i j => Λ.1 i j
| .down => fun i j => (LorentzGroup.transpose Λ⁻¹).1 i j
map_one' := by
match μ with
| .up =>
simp only [lorentzGroupIsGroup_one_coe]
ext i j
simp only [OfNat.ofNat, One.one, ColorsIndex]
congr
| .down =>
simp only [transpose, inv_one, lorentzGroupIsGroup_one_coe, Matrix.transpose_one]
ext i j
simp only [OfNat.ofNat, One.one, ColorsIndex]
congr
map_mul' Λ Λ' := by
match μ with
| .up =>
ext i j
simp only [lorentzGroupIsGroup_mul_coe]
| .down =>
ext i j
simp only [transpose, mul_inv_rev, lorentzGroupIsGroup_inv, lorentzGroupIsGroup_mul_coe,
Matrix.transpose_mul, Matrix.transpose_apply]
rfl
lemma colorMatrix_cast {μ ν : Colors} (h : μ = ν) (Λ : LorentzGroup d) :
colorMatrix μ Λ =
Matrix.reindex (colorsIndexCast h).symm (colorsIndexCast h).symm (colorMatrix ν Λ) := by
subst h
rfl
lemma colorMatrix_dual_cast {μ : Colors} (Λ : LorentzGroup d) :
colorMatrix (τ μ) Λ = Matrix.reindex (colorsIndexDualCastSelf) (colorsIndexDualCastSelf)
(colorMatrix μ (LorentzGroup.transpose Λ⁻¹)) := by
match μ with
| .up => rfl
| .down =>
ext i j
simp only [τ, colorMatrix, MonoidHom.coe_mk, OneHom.coe_mk, colorsIndexDualCastSelf, transpose,
lorentzGroupIsGroup_inv, Matrix.transpose_apply, minkowskiMetric.dual_transpose,
minkowskiMetric.dual_dual, Matrix.reindex_apply, Equiv.coe_fn_symm_mk, Matrix.submatrix_apply]
lemma colorMatrix_transpose {μ : Colors} (Λ : LorentzGroup d) :
colorMatrix μ (LorentzGroup.transpose Λ) = (colorMatrix μ Λ).transpose := by
match μ with
| .up => rfl
| .down =>
ext i j
simp only [colorMatrix, transpose, lorentzGroupIsGroup_inv, Matrix.transpose_apply,
MonoidHom.coe_mk, OneHom.coe_mk, minkowskiMetric.dual_transpose]
/-!
## Lorentz group to tensor representation matrices.
-/
/-- The matrix representation of the Lorentz group given a color of index. -/
@[simps!]
def toTensorRepMat {c : X → Colors} :
LorentzGroup d →* Matrix (IndexValue d c) (IndexValue d c) ℝ where
toFun Λ := fun i j => ∏ x, colorMatrix (c x) Λ (i x) (j x)
map_one' := by
ext i j
by_cases hij : i = j
· subst hij
simp only [map_one, Matrix.one_apply_eq, Finset.prod_const_one]
· obtain ⟨x, hijx⟩ := Function.ne_iff.mp hij
simp only [map_one]
rw [@Finset.prod_eq_zero _ _ _ _ _ x]
exact Eq.symm (Matrix.one_apply_ne' fun a => hij (id (Eq.symm a)))
exact Finset.mem_univ x
exact Matrix.one_apply_ne' (id (Ne.symm hijx))
map_mul' Λ Λ' := by
ext i j
rw [Matrix.mul_apply]
trans ∑ (k : IndexValue d c), ∏ x,
(colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x))
have h1 : ∑ (k : IndexValue d c), ∏ x,
(colorMatrix (c x) Λ (i x) (k x)) * (colorMatrix (c x) Λ' (k x) (j x)) =
∏ x, ∑ y, (colorMatrix (c x) Λ (i x) y) * (colorMatrix (c x) Λ' y (j x)) := by
rw [Finset.prod_sum]
simp only [Finset.prod_attach_univ, Finset.sum_univ_pi]
rfl
rw [h1]
simp only [map_mul]
rfl
refine Finset.sum_congr rfl (fun k _ => ?_)
rw [Finset.prod_mul_distrib]
lemma toTensorRepMat_mul' (i j : IndexValue d c) :
toTensorRepMat (Λ * Λ') i j = ∑ (k : IndexValue d c),
∏ x, colorMatrix (c x) Λ (i x) (k x) * colorMatrix (c x) Λ' (k x) (j x) := by
simp [Matrix.mul_apply, IndexValue]
refine Finset.sum_congr rfl (fun k _ => ?_)
rw [Finset.prod_mul_distrib]
rfl
lemma toTensorRepMat_of_indexValueSumEquiv {cX : X → Colors} {cY : Y → Colors}
(i j : IndexValue d (Sum.elim cX cY)) :
toTensorRepMat Λ i j = toTensorRepMat Λ (indexValueSumEquiv i).1 (indexValueSumEquiv j).1 *
toTensorRepMat Λ (indexValueSumEquiv i).2 (indexValueSumEquiv j).2 :=
Fintype.prod_sum_type fun x => (colorMatrix (Sum.elim cX cY x)) Λ (i x) (j x)
lemma toTensorRepMat_of_indexValueSumEquiv' {cX : X → Colors} {cY : Y → Colors}
(i j : IndexValue d cX) (k l : IndexValue d cY) :
toTensorRepMat Λ i j * toTensorRepMat Λ k l =
toTensorRepMat Λ (indexValueSumEquiv.symm (i, k)) (indexValueSumEquiv.symm (j, l)) :=
(Fintype.prod_sum_type fun x => (colorMatrix (Sum.elim cX cY x)) Λ
(indexValueSumEquiv.symm (i, k) x) (indexValueSumEquiv.symm (j, l) x)).symm
/-!
## Tensor representation matrices and marked tensors.
-/
lemma toTensorRepMat_of_splitIndexValue' (T : Marked d X n)
(i j : T.UnmarkedIndexValue) (k l : T.MarkedIndexValue) :
toTensorRepMat Λ i j * toTensorRepMat Λ k l =
toTensorRepMat Λ (splitIndexValue.symm (i, k)) (splitIndexValue.symm (j, l)) :=
(Fintype.prod_sum_type fun x =>
(colorMatrix (T.color x)) Λ (splitIndexValue.symm (i, k) x) (splitIndexValue.symm (j, l) x)).symm
lemma toTensorRepMat_oneMarkedIndexValue_dual (T : Marked d X 1) (S : Marked d Y 1)
(h : T.markedColor 0 = τ (S.markedColor 0)) (x : ColorsIndex d (T.markedColor 0))
(k : S.MarkedIndexValue) :
toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k =
toTensorRepMat Λ⁻¹ (oneMarkedIndexValue
$ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k)
(oneMarkedIndexValue x) := by
rw [toTensorRepMat_apply, toTensorRepMat_apply]
erw [Finset.prod_singleton, Finset.prod_singleton]
simp only [Fin.zero_eta, Fin.isValue, lorentzGroupIsGroup_inv]
rw [colorMatrix_cast h, colorMatrix_dual_cast]
rw [Matrix.reindex_apply, Matrix.reindex_apply]
simp only [Fin.isValue, lorentzGroupIsGroup_inv, minkowskiMetric.dual_dual, Subtype.coe_eta,
Equiv.symm_symm, Matrix.submatrix_apply]
rw [colorMatrix_transpose]
simp only [Fin.isValue, Matrix.transpose_apply]
apply congrArg
simp only [Fin.isValue, oneMarkedIndexValue, colorsIndexDualCast, Equiv.coe_fn_symm_mk,
Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.coe_fn_mk, Equiv.apply_symm_apply,
Equiv.symm_apply_apply]
lemma toTensorRepMap_sum_dual (T : Marked d X 1) (S : Marked d Y 1)
(h : T.markedColor 0 = τ (S.markedColor 0)) (j : T.MarkedIndexValue) (k : S.MarkedIndexValue) :
∑ x, toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k
* toTensorRepMat Λ (oneMarkedIndexValue x) j =
toTensorRepMat 1
(oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k) j := by
trans ∑ x, toTensorRepMat Λ⁻¹ (oneMarkedIndexValue$ (colorsIndexDualCast h).symm $
oneMarkedIndexValue.symm k) (oneMarkedIndexValue x) * toTensorRepMat Λ (oneMarkedIndexValue x) j
apply Finset.sum_congr rfl (fun x _ => ?_)
rw [toTensorRepMat_oneMarkedIndexValue_dual]
rw [← Equiv.sum_comp oneMarkedIndexValue.symm]
change ∑ i, toTensorRepMat Λ⁻¹ (oneMarkedIndexValue $ (colorsIndexDualCast h).symm $
oneMarkedIndexValue.symm k) i * toTensorRepMat Λ i j = _
rw [← Matrix.mul_apply, ← toTensorRepMat.map_mul, inv_mul_self Λ]
lemma toTensorRepMat_one_coord_sum (T : Marked d X n) (i : T.UnmarkedIndexValue)
(k : T.MarkedIndexValue) : T.coord (splitIndexValue.symm (i, k)) = ∑ j, toTensorRepMat 1 k j *
T.coord (splitIndexValue.symm (i, j)) := by
erw [Finset.sum_eq_single_of_mem k]
simp only [IndexValue, map_one, Matrix.one_apply_eq, one_mul]
exact Finset.mem_univ k
intro j _ hjk
simp [hjk, IndexValue]
exact Or.inl (Matrix.one_apply_ne' hjk)
/-!
## Definition of the Lorentz group action on Real Lorentz Tensors.
-/
/-- Action of the Lorentz group on `X`-indexed Real Lorentz Tensors. -/
@[simps!]
instance lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) where
smul Λ T := {color := T.color,
coord := fun i => ∑ j, toTensorRepMat Λ i j * T.coord j}
one_smul T := by
refine ext rfl ?_
funext i
simp only [HSMul.hSMul, map_one]
erw [Finset.sum_eq_single_of_mem i]
simp only [Matrix.one_apply_eq, one_mul, IndexValue]
rfl
exact Finset.mem_univ i
exact fun j _ hij => mul_eq_zero.mpr (Or.inl (Matrix.one_apply_ne' hij))
mul_smul Λ Λ' T := by
refine ext rfl ?_
simp only [HSMul.hSMul]
funext i
have h1 : ∑ j : IndexValue d T.color, toTensorRepMat (Λ * Λ') i j
* T.coord j = ∑ j : IndexValue d T.color, ∑ (k : IndexValue d T.color),
(∏ x, ((colorMatrix (T.color x) Λ (i x) (k x)) *
(colorMatrix (T.color x) Λ' (k x) (j x)))) * T.coord j := by
refine Finset.sum_congr rfl (fun j _ => ?_)
rw [toTensorRepMat_mul', Finset.sum_mul]
rw [h1]
rw [Finset.sum_comm]
refine Finset.sum_congr rfl (fun j _ => ?_)
rw [Finset.mul_sum]
refine Finset.sum_congr rfl (fun k _ => ?_)
simp only [toTensorRepMat, IndexValue]
rw [← mul_assoc]
congr
rw [Finset.prod_mul_distrib]
rfl
lemma lorentzAction_smul_coord' {d : ℕ} {X : Type} [Fintype X] [DecidableEq X] (Λ : ↑(𝓛 d))
(T : RealLorentzTensor d X) (i : IndexValue d T.color) :
(Λ • T).coord i = ∑ j : IndexValue d T.color, toTensorRepMat Λ i j * T.coord j := by
rfl
/-!
## Properties of the Lorentz action.
-/
/-- The action on an empty Lorentz tensor is trivial. -/
lemma lorentzAction_on_isEmpty [IsEmpty X] (Λ : LorentzGroup d) (T : RealLorentzTensor d X) :
Λ • T = T := by
refine ext rfl ?_
funext i
erw [lorentzAction_smul_coord]
simp only [Finset.univ_unique, Finset.univ_eq_empty, Finset.prod_empty, one_mul,
Finset.sum_singleton, toTensorRepMat_apply]
simp only [IndexValue, Unique.eq_default, Finset.univ_unique, Finset.sum_const,
Finset.card_singleton, one_smul]
/-- The Lorentz action commutes with `mapIso`. -/
lemma lorentzAction_mapIso (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzTensor d X) :
mapIso d f (Λ • T) = Λ • (mapIso d f T) := by
refine ext rfl ?_
funext i
rw [mapIso_apply_coord]
rw [lorentzAction_smul_coord', lorentzAction_smul_coord']
let is : IndexValue d T.color ≃ IndexValue d ((mapIso d f) T).color :=
indexValueIso d f ((Equiv.comp_symm_eq f ((mapIso d f) T).color T.color).mp rfl)
rw [← Equiv.sum_comp is]
refine Finset.sum_congr rfl (fun j _ => ?_)
rw [mapIso_apply_coord]
refine Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl
· simp only [IndexValue, toTensorRepMat, MonoidHom.coe_mk, OneHom.coe_mk, mapIso_apply_color,
indexValueIso_refl]
rw [← Equiv.prod_comp f]
apply Finset.prod_congr rfl (fun x _ => ?_)
have h1 : (T.color (f.symm (f x))) = T.color x := by
simp only [Equiv.symm_apply_apply]
rw [colorMatrix_cast h1]
apply congrArg
simp only [is]
erw [indexValueIso_eq_symm, indexValueIso_symm_apply']
simp only [colorsIndexCast, Function.comp_apply, mapIso_apply_color, Equiv.cast_refl,
Equiv.refl_symm, Equiv.refl_apply, Equiv.cast_apply]
symm
refine cast_eq_iff_heq.mpr ?_
congr
exact Equiv.symm_apply_apply f x
· apply congrArg
exact (Equiv.apply_eq_iff_eq_symm_apply (indexValueIso d f (mapIso.proof_1 d f T))).mp rfl
/-!
## The Lorentz action on marked tensors.
-/
@[simps!]
instance : MulAction (LorentzGroup d) (Marked d X n) := lorentzAction
/-- Action of the Lorentz group on just marked indices. -/
@[simps!]
def markedLorentzAction : MulAction (LorentzGroup d) (Marked d X n) where
smul Λ T := {
color := T.color,
coord := fun i => ∑ j, toTensorRepMat Λ (splitIndexValue i).2 j *
T.coord (splitIndexValue.symm ((splitIndexValue i).1, j))}
one_smul T := by
refine ext rfl ?_
funext i
simp only [HSMul.hSMul, map_one]
erw [Finset.sum_eq_single_of_mem (splitIndexValue i).2]
erw [Matrix.one_apply_eq (splitIndexValue i).2]
simp only [IndexValue, one_mul, indexValueIso_refl, Equiv.refl_apply]
apply congrArg
exact Equiv.symm_apply_apply splitIndexValue i
exact Finset.mem_univ (splitIndexValue i).2
exact fun j _ hij => mul_eq_zero.mpr (Or.inl (Matrix.one_apply_ne' hij))
mul_smul Λ Λ' T := by
refine ext rfl ?_
simp only [HSMul.hSMul]
funext i
have h1 : ∑ (j : T.MarkedIndexValue), toTensorRepMat (Λ * Λ') (splitIndexValue i).2 j
* T.coord (splitIndexValue.symm ((splitIndexValue i).1, j)) =
∑ (j : T.MarkedIndexValue), ∑ (k : T.MarkedIndexValue),
(∏ x, ((colorMatrix (T.markedColor x) Λ ((splitIndexValue i).2 x) (k x)) *
(colorMatrix (T.markedColor x) Λ' (k x) (j x)))) *
T.coord (splitIndexValue.symm ((splitIndexValue i).1, j)) := by
refine Finset.sum_congr rfl (fun j _ => ?_)
rw [toTensorRepMat_mul', Finset.sum_mul]
rfl
erw [h1]
rw [Finset.sum_comm]
refine Finset.sum_congr rfl (fun j _ => ?_)
rw [Finset.mul_sum]
refine Finset.sum_congr rfl (fun k _ => ?_)
simp only [toTensorRepMat, IndexValue]
rw [← mul_assoc]
congr
rw [Finset.prod_mul_distrib]
rfl
/-- Action of the Lorentz group on just unmarked indices. -/
@[simps!]
def unmarkedLorentzAction : MulAction (LorentzGroup d) (Marked d X n) where
smul Λ T := {
color := T.color,
coord := fun i => ∑ j, toTensorRepMat Λ (splitIndexValue i).1 j *
T.coord (splitIndexValue.symm (j, (splitIndexValue i).2))}
one_smul T := by
refine ext rfl ?_
funext i
simp only [HSMul.hSMul, map_one]
erw [Finset.sum_eq_single_of_mem (splitIndexValue i).1]
erw [Matrix.one_apply_eq (splitIndexValue i).1]
simp only [IndexValue, one_mul, indexValueIso_refl, Equiv.refl_apply]
apply congrArg
exact Equiv.symm_apply_apply splitIndexValue i
exact Finset.mem_univ (splitIndexValue i).1
exact fun j _ hij => mul_eq_zero.mpr (Or.inl (Matrix.one_apply_ne' hij))
mul_smul Λ Λ' T := by
refine ext rfl ?_
simp only [HSMul.hSMul]
funext i
have h1 : ∑ (j : T.UnmarkedIndexValue), toTensorRepMat (Λ * Λ') (splitIndexValue i).1 j
* T.coord (splitIndexValue.symm (j, (splitIndexValue i).2)) =
∑ (j : T.UnmarkedIndexValue), ∑ (k : T.UnmarkedIndexValue),
(∏ x, ((colorMatrix (T.unmarkedColor x) Λ ((splitIndexValue i).1 x) (k x)) *
(colorMatrix (T.unmarkedColor x) Λ' (k x) (j x)))) *
T.coord (splitIndexValue.symm (j, (splitIndexValue i).2)) := by
refine Finset.sum_congr rfl (fun j _ => ?_)
rw [toTensorRepMat_mul', Finset.sum_mul]
rfl
erw [h1]
rw [Finset.sum_comm]
refine Finset.sum_congr rfl (fun j _ => ?_)
rw [Finset.mul_sum]
refine Finset.sum_congr rfl (fun k _ => ?_)
simp only [toTensorRepMat, IndexValue]
rw [← mul_assoc]
congr
rw [Finset.prod_mul_distrib]
rfl
/-- Notation for `markedLorentzAction.smul`. -/
scoped[RealLorentzTensor] infixr:73 " •ₘ " => markedLorentzAction.smul
/-- Notation for `unmarkedLorentzAction.smul`. -/
scoped[RealLorentzTensor] infixr:73 " •ᵤₘ " => unmarkedLorentzAction.smul
/-- Acting on unmarked and then marked indices is equivalent to acting on all indices. -/
lemma marked_unmarked_action_eq_action (T : Marked d X n) : Λ •ₘ (Λ •ᵤₘ T) = Λ • T := by
refine ext rfl ?_
funext i
change ∑ j, toTensorRepMat Λ (splitIndexValue i).2 j *
(∑ k, toTensorRepMat Λ (splitIndexValue i).1 k * T.coord (splitIndexValue.symm (k, j))) = _
trans ∑ j, ∑ k, (toTensorRepMat Λ (splitIndexValue i).2 j *
toTensorRepMat Λ (splitIndexValue i).1 k) * T.coord (splitIndexValue.symm (k, j))
apply Finset.sum_congr rfl (fun j _ => ?_)
rw [Finset.mul_sum]
apply Finset.sum_congr rfl (fun k _ => ?_)
exact Eq.symm (mul_assoc _ _ _)
trans ∑ j, ∑ k, (toTensorRepMat Λ i (splitIndexValue.symm (k, j))
* T.coord (splitIndexValue.symm (k, j)))
apply Finset.sum_congr rfl (fun j _ => (Finset.sum_congr rfl (fun k _ => ?_)))
rw [mul_comm (toTensorRepMat _ _ _), toTensorRepMat_of_splitIndexValue']
simp only [IndexValue, Finset.mem_univ, Prod.mk.eta, Equiv.symm_apply_apply]
trans ∑ p, (toTensorRepMat Λ i p * T.coord p)
rw [← Equiv.sum_comp splitIndexValue.symm, Fintype.sum_prod_type, Finset.sum_comm]
rfl
rfl
/-- Acting on marked and then unmarked indices is equivalent to acting on all indices. -/
lemma unmarked_marked_action_eq_action (T : Marked d X n) : Λ •ᵤₘ (Λ •ₘ T) = Λ • T := by
refine ext rfl ?_
funext i
change ∑ j, toTensorRepMat Λ (splitIndexValue i).1 j *
(∑ k, toTensorRepMat Λ (splitIndexValue i).2 k * T.coord (splitIndexValue.symm (j, k))) = _
trans ∑ j, ∑ k, (toTensorRepMat Λ (splitIndexValue i).1 j *
toTensorRepMat Λ (splitIndexValue i).2 k) * T.coord (splitIndexValue.symm (j, k))
apply Finset.sum_congr rfl (fun j _ => ?_)
rw [Finset.mul_sum]
apply Finset.sum_congr rfl (fun k _ => ?_)
exact Eq.symm (mul_assoc _ _ _)
trans ∑ j, ∑ k, (toTensorRepMat Λ i (splitIndexValue.symm (j, k))
* T.coord (splitIndexValue.symm (j, k)))
apply Finset.sum_congr rfl (fun j _ => (Finset.sum_congr rfl (fun k _ => ?_)))
rw [toTensorRepMat_of_splitIndexValue']
simp only [IndexValue, Finset.mem_univ, Prod.mk.eta, Equiv.symm_apply_apply]
trans ∑ p, (toTensorRepMat Λ i p * T.coord p)
rw [← Equiv.sum_comp splitIndexValue.symm, Fintype.sum_prod_type]
rfl
rfl
/-- The marked and unmarked actions commute. -/
lemma marked_unmarked_action_comm (T : Marked d X n) : Λ •ᵤₘ (Λ •ₘ T) = Λ •ₘ (Λ •ᵤₘ T) := by
rw [unmarked_marked_action_eq_action, marked_unmarked_action_eq_action]
/-! TODO: Show that the Lorentz action commutes with contraction. -/
/-! TODO: Show that the Lorentz action commutes with rising and lowering indices. -/
end RealLorentzTensor

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

@ -1,485 +0,0 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.SpaceTime.LorentzTensor.Real.Basic
import HepLean.SpaceTime.LorentzTensor.Real.LorentzAction
/-!
# Multiplication of Real Lorentz Tensors along an index
We define the multiplication of two singularly marked Lorentz tensors along the
marked index. This is equivalent to contracting two Lorentz tensors.
We prove various results about this multiplication.
-/
/-! TODO: Set up a good notation for the multiplication. -/
namespace RealLorentzTensor
variable {d : ℕ} {X Y : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
(T : RealLorentzTensor d X) (c : X → Colors) (Λ Λ' : LorentzGroup d) {μ : Colors}
open Marked
/-- The contraction of the marked indices of two tensors each with one marked index, which
is dual to the others. The contraction is done via
`φ^μ ψ_μ = φ^0 ψ_0 + φ^1 ψ_1 + ...`. -/
@[simps!]
def mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
(h : T.markedColor 0 = τ (S.markedColor 0)) :
RealLorentzTensor d (X ⊕ Y) where
color := Sum.elim T.unmarkedColor S.unmarkedColor
coord := fun i => ∑ x,
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, oneMarkedIndexValue x)) *
S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2,
oneMarkedIndexValue $ colorsIndexDualCast h x))
/-- 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}
(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}
(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
rfl
lemma mulFstArg_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
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}
(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 :=
splitIndexValue.symm ((indexValueSumEquiv i).2, oneMarkedIndexValue $ colorsIndexDualCast h x)
/-!
## Expressions for multiplication
-/
/-! 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)
(h : T.markedColor 0 = τ (S.markedColor 0)) :
(mul 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
funext i
rw [← Equiv.sum_comp (colorsIndexDualCast h)]
apply Finset.sum_congr rfl (fun x _ => ?_)
congr
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)
(h : T.markedColor 0 = τ (S.markedColor 0)) :
(mul 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
funext i
rw [← Equiv.sum_comp (oneMarkedIndexValue)]
rfl
lemma mul_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,
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 [← Equiv.sum_comp (oneMarkedIndexValue)]
apply Finset.sum_congr rfl (fun x _ => ?_)
congr
exact Eq.symm (colorsIndexDualCast_symm h)
/-!
## Properties of multiplication
-/
/-- Multiplication is well behaved with regard to swapping tensors. -/
lemma mul_symm {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
(h : T.markedColor 0 = τ (S.markedColor 0)) :
mapIso d (Equiv.sumComm X Y) (mul T S h) = mul S T (color_eq_dual_symm h) := by
refine ext ?_ ?_
· funext a
cases a with
| inl _ => rfl
| inr _ => rfl
· funext i
rw [mul_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)
(g : Y ≃ Z) (h : T.markedColor 0 = τ (S.markedColor 0)) :
mapIso d (Equiv.sumCongr f g) (mul T S h) = mul (mapIso d (Equiv.sumCongr f (Equiv.refl _)) T)
(mapIso d (Equiv.sumCongr g (Equiv.refl _)) S) h := by
refine ext ?_ ?_
· funext a
cases a with
| inl _ => rfl
| inr _ => rfl
· funext i
rw [mapIso_apply_coord, mul_coord, mul_coord]
refine Fintype.sum_congr _ _ (fun x => ?_)
rw [mapIso_apply_coord, mapIso_apply_coord]
refine Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl
· apply congrArg
exact (Equiv.symm_apply_eq splitIndexValue).mpr rfl
· apply congrArg
exact (Equiv.symm_apply_eq splitIndexValue).mpr rfl
/-!
## Lorentz action and multiplication.
-/
/-- The marked Lorentz Action leaves multiplication invariant. -/
lemma mul_markedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
(h : T.markedColor 0 = τ (S.markedColor 1)) :
mul (Λ •ₘ T) (Λ •ₘ S) h = mul T S h := by
refine ext rfl ?_
funext i
change ∑ x, (∑ j, toTensorRepMat Λ (oneMarkedIndexValue x) j *
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j))) *
(∑ k, toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k *
S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))) = _
trans ∑ x, ∑ j, ∑ k, (toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k
* toTensorRepMat Λ (oneMarkedIndexValue x) j) *
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j))
* S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))
apply Finset.sum_congr rfl (fun x _ => ?_)
rw [Finset.sum_mul_sum]
apply Finset.sum_congr rfl (fun j _ => ?_)
apply Finset.sum_congr rfl (fun k _ => ?_)
ring
rw [Finset.sum_comm]
trans ∑ j, ∑ k, ∑ x, (toTensorRepMat Λ (oneMarkedIndexValue $ colorsIndexDualCast h x) k
* toTensorRepMat Λ (oneMarkedIndexValue x) j) *
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j))
* S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))
apply Finset.sum_congr rfl (fun j _ => ?_)
rw [Finset.sum_comm]
trans ∑ j, ∑ k, (toTensorRepMat 1
(oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k) j) *
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, j))
* S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))
apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_))
rw [← Finset.sum_mul, ← Finset.sum_mul]
erw [toTensorRepMap_sum_dual]
rfl
rw [Finset.sum_comm]
trans ∑ k,
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1,
(oneMarkedIndexValue $ (colorsIndexDualCast h).symm $ oneMarkedIndexValue.symm k)))*
S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2, k))
apply Finset.sum_congr rfl (fun k _ => ?_)
rw [← Finset.sum_mul, ← toTensorRepMat_one_coord_sum T]
rw [← Equiv.sum_comp (oneMarkedIndexValue)]
erw [← Equiv.sum_comp (colorsIndexDualCast h)]
simp
rfl
/-- The unmarked Lorentz Action commutes with multiplication. -/
lemma mul_unmarkedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
(h : T.markedColor 0 = τ (S.markedColor 1)) :
mul (Λ •ᵤₘ T) (Λ •ᵤₘ S) h = Λ • mul T S h := by
refine ext rfl ?_
funext i
change ∑ x, (∑ j, toTensorRepMat Λ (indexValueSumEquiv i).1 j *
T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))*
∑ k, toTensorRepMat Λ (indexValueSumEquiv i).2 k *
S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x)) = _
trans ∑ x, ∑ j, ∑ k, (toTensorRepMat Λ (indexValueSumEquiv i).1 j *
T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))*
toTensorRepMat Λ (indexValueSumEquiv i).2 k *
S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
· apply Finset.sum_congr rfl (fun x _ => ?_)
rw [Finset.sum_mul_sum ]
apply Finset.sum_congr rfl (fun j _ => ?_)
apply Finset.sum_congr rfl (fun k _ => ?_)
ring
rw [Finset.sum_comm]
trans ∑ j, ∑ k, ∑ x, (toTensorRepMat Λ (indexValueSumEquiv i).1 j *
T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))*
toTensorRepMat Λ (indexValueSumEquiv i).2 k *
S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
· exact Finset.sum_congr rfl (fun j _ => Finset.sum_comm)
trans ∑ j, ∑ k,
((toTensorRepMat Λ (indexValueSumEquiv i).1 j) * toTensorRepMat Λ (indexValueSumEquiv i).2 k)
* ∑ x, (T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))
* S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
· apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_))
rw [Finset.mul_sum]
apply Finset.sum_congr rfl (fun x _ => ?_)
ring
trans ∑ j, ∑ k, toTensorRepMat Λ i (indexValueSumEquiv.symm (j, k)) *
∑ x, (T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))
* S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_))
· rw [toTensorRepMat_of_indexValueSumEquiv']
congr
simp only [IndexValue, Finset.mem_univ, Prod.mk.eta, Equiv.symm_apply_apply, mul_color]
trans ∑ p, toTensorRepMat Λ i p *
∑ x, (T.coord (splitIndexValue.symm ((indexValueSumEquiv p).1, oneMarkedIndexValue x)))
* S.coord (splitIndexValue.symm ((indexValueSumEquiv p).2,
oneMarkedIndexValue $ colorsIndexDualCast h x))
· erw [← Equiv.sum_comp indexValueSumEquiv.symm]
exact Eq.symm Fintype.sum_prod_type
rfl
/-- The Lorentz action commutes with multiplication. -/
lemma mul_lorentzAction (T : Marked d X 1) (S : Marked d Y 1)
(h : T.markedColor 0 = τ (S.markedColor 1)) :
mul (Λ • T) (Λ • S) h = Λ • mul T S h := by
simp only [← marked_unmarked_action_eq_action]
rw [mul_markedLorentzAction, mul_unmarkedLorentzAction]
/-!
## Multiplication on selected indices
-/
variable {n m : ℕ} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
{X' Y' Z : Type} [Fintype X'] [DecidableEq X'] [Fintype Y'] [DecidableEq Y']
[Fintype Z] [DecidableEq Z]
/-- 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)
(h : T.color x = τ (S.color y)) : RealLorentzTensor d ({x' // x' ≠ x} ⊕ {y' // y' ≠ y}) :=
mul (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}
(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)
lemma mulSFstArg_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
subst hij; subst hab
rfl
lemma mulSFstArg_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]
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]
swap
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Finset.univ_unique, Fin.default_eq_zero,
Fin.isValue, Finset.image_singleton, embedSingleton_apply, Finset.mem_singleton]
rw [indexValueIso_symm_apply']
erw [Equiv.symm_apply_eq, Equiv.symm_apply_eq]
simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast]
symm
apply cast_eq_iff_heq.mpr
rw [embedSingleton_toEquivRange_symm]
rfl
lemma mulSFstArg_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]
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]
swap
simpa using hc
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}
(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)
lemma mulSSndArg_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]
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]
swap
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Finset.univ_unique, Fin.default_eq_zero,
Fin.isValue, Finset.image_singleton, embedSingleton_apply, Finset.mem_singleton]
rw [indexValueIso_symm_apply']
erw [Equiv.symm_apply_eq, Equiv.symm_apply_eq]
simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast]
symm
apply cast_eq_iff_heq.mpr
rw [embedSingleton_toEquivRange_symm]
rfl
lemma mulSSndArg_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]
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]
swap
simpa using hc
rfl
lemma mulSSndArg_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
subst hij
subst hab
rfl
lemma mulS_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
rfl
lemma mulS_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) =
mapIso d (Equiv.sumCongr (equivSingleCompl eX hx) (equivSingleCompl eY hy))
(mulS T S x y h) := by
rw [mulS, mulS, mul_mapIso]
congr 1 <;> rw [markSingle_mapIso]
lemma mulS_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]
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)
(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]
/-- 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) :
{yz // yz ≠ (Sum.inl ⟨y, hy⟩ : {y'' // y'' ≠ y'} ⊕ {z' // z' ≠ z})} ≃
{y'' // y'' ≠ y' ∧ y'' ≠ y} ⊕ {z' // z' ≠ z} :=
Equiv.subtypeSum.trans <|
Equiv.sumCongr (
(Equiv.subtypeEquivRight (fun a => by
obtain ⟨a, p⟩ := a; simp only [ne_eq, Sum.inl.injEq, Subtype.mk.injEq])).trans
(Equiv.subtypeSubtypeEquivSubtypeInter _ _)) <|
Equiv.subtypeUnivEquiv (fun a => Sum.inr_ne_inl)
/-- 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) :
{yz // yz ≠ (Sum.inr ⟨y', hy.symm⟩ : {z' // z' ≠ z} ⊕ {y'' // y'' ≠ y})} ≃
{z' // z' ≠ z} ⊕ {y'' // y'' ≠ y' ∧ y'' ≠ y} :=
Equiv.subtypeSum.trans <|
Equiv.sumCongr (Equiv.subtypeUnivEquiv (fun a => Sum.inl_ne_inr)) <|
(Equiv.subtypeEquivRight (fun a => by
obtain ⟨a, p⟩ := a; simp only [ne_eq, Sum.inr.injEq, Subtype.mk.injEq])).trans <|
((Equiv.subtypeSubtypeEquivSubtypeInter _ _).trans
(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) :
{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.sumAssoc _ _ _).symm.trans <|
(Equiv.sumCongr (mulSSplitRight hy x).symm (Equiv.refl _))
lemma mulS_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
funext a
match a with
| .inl ⟨.inl _, _⟩ => rfl
| .inl ⟨.inr _, _⟩ => rfl
| .inr _ => rfl
/-- An equivalence of index values associated with the associativity property of multiplication. -/
def mulSAssocIndexValue {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')
/-- 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)
(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 _ _ _) ?_
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')
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'))
swap
rw [mapIso_apply_coord, mulS_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 _ _ _)]
rw [Finset.sum_comm]
refine Finset.sum_congr rfl (fun a _ => Finset.sum_congr rfl (fun b _ => ?_))
rw [mul_assoc]
refine Mathlib.Tactic.Ring.mul_congr rfl (Mathlib.Tactic.Ring.mul_congr ?_ rfl rfl) rfl
apply congrArg
funext c
by_cases hcy : c = y
· subst hcy
rw [mulSSndArg_on_mem, mulSFstArg_on_not_mem, mulSSndArg_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,
colorsIndexCast, Equiv.cast_refl, Equiv.refl_symm]
erw [Equiv.refl_apply]
rfl
exact hcy'
simpa using hcy
end RealLorentzTensor

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

@ -1,195 +0,0 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.SpaceTime.LorentzTensor.Real.Constructors
/-!
# Unit of multiplication of Real Lorentz Tensors
The definition of the unit is akin to the definition given in
[Raynor][raynor2021graphical]
for modular operads.
The main results of this file are:
- `mulUnit_right`: The multiplicative unit acts as a right unit for the multiplication of Lorentz
tensors.
- `mulUnit_left`: The multiplicative unit acts as a left unit for the multiplication of Lorentz
tensors.
- `mulUnit_lorentzAction`: The multiplicative unit is invariant under Lorentz transformations.
-/
namespace RealLorentzTensor
variable {d : ℕ} {X Y : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
(T : RealLorentzTensor d X) (c : X → Colors) (Λ Λ' : LorentzGroup d) {μ : Colors}
open Marked
/-!
## Unit of multiplication
-/
/-- The unit for the multiplication of Lorentz tensors. -/
def mulUnit (d : ℕ) (μ : Colors) : Marked d (Fin 1) 1 :=
match μ with
| .up => mapIso d ((Equiv.emptySum Empty (Fin (1 + 1))).trans finSumFinEquiv.symm)
(ofMatUpDown 1)
| .down => mapIso d ((Equiv.emptySum Empty (Fin (1 + 1))).trans finSumFinEquiv.symm)
(ofMatDownUp 1)
lemma mulUnit_up_coord : (mulUnit d Colors.up).coord = fun i =>
(1 : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (i (Sum.inl 0)) (i (Sum.inr 0)) := by
rfl
lemma mulUnit_down_coord : (mulUnit d Colors.down).coord = fun i =>
(1 : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (i (Sum.inl 0)) (i (Sum.inr 0)) := by
rfl
@[simp]
lemma mulUnit_markedColor (μ : Colors) : (mulUnit d μ).markedColor 0 = τ μ := by
cases μ
case up => rfl
case down => rfl
lemma mulUnit_dual_markedColor (μ : Colors) : τ ((mulUnit d μ).markedColor 0) = μ := by
cases μ
case up => rfl
case down => rfl
@[simp]
lemma mulUnit_unmarkedColor (μ : Colors) : (mulUnit d μ).unmarkedColor 0 = μ := by
cases μ
case up => rfl
case down => rfl
lemma mulUnit_unmarkedColor_eq_dual_marked (μ : Colors) :
(mulUnit d μ).unmarkedColor = τ ∘ (mulUnit d μ).markedColor := by
funext x
fin_cases x
simp only [Fin.zero_eta, Fin.isValue, mulUnit_unmarkedColor, Function.comp_apply,
mulUnit_markedColor]
exact color_eq_dual_symm rfl
lemma mulUnit_coord_diag (μ : Colors) (i : (mulUnit d μ).UnmarkedIndexValue) :
(mulUnit d μ).coord (splitIndexValue.symm (i,
indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked μ) i)) = 1 := by
cases μ
case' up => rw [mulUnit_up_coord]
case' down => rw [mulUnit_down_coord]
all_goals
simp only [mulUnit]
symm
simp_all only [Fin.isValue, Matrix.one_apply]
split
rfl
next h => exact False.elim (h rfl)
lemma mulUnit_coord_off_diag (μ : Colors) (i: (mulUnit d μ).UnmarkedIndexValue)
(b : (mulUnit d μ).MarkedIndexValue)
(hb : b ≠ indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked μ) i) :
(mulUnit d μ).coord (splitIndexValue.symm (i, b)) = 0 := by
match μ with
| Colors.up =>
rw [mulUnit_up_coord]
simp only [mulUnit, Matrix.one_apply, Fin.isValue, ite_eq_right_iff, one_ne_zero, imp_false,
ne_eq]
by_contra h
have h1 : (indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked (Colors.up)) i) = b := by
funext a
fin_cases a
exact h
exact hb (id (Eq.symm h1))
| Colors.down =>
rw [mulUnit_down_coord]
simp only [mulUnit, Matrix.one_apply, Fin.isValue, ite_eq_right_iff, one_ne_zero, imp_false,
ne_eq]
by_contra h
have h1 : (indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked (Colors.down)) i) = b := by
funext a
fin_cases a
exact h
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
refine ext ?_ ?_
· funext a
match a with
| .inl _ => rfl
| .inr 0 =>
simp only [Fin.isValue, mul_color, Sum.elim_inr, mulUnit_unmarkedColor]
exact h.symm
funext i
rw [mul_indexValue_right]
change ∑ j,
T.coord (splitIndexValue.symm ((indexValueSumEquiv i).1, _)) *
(mulUnit d μ).coord (splitIndexValue.symm ((indexValueSumEquiv i).2, j)) = _
let y := indexValueDualIso d (mulUnit_unmarkedColor_eq_dual_marked μ) (indexValueSumEquiv i).2
erw [Finset.sum_eq_single_of_mem y]
rw [mulUnit_coord_diag]
simp only [Fin.isValue, mul_one]
apply congrArg
funext a
match a with
| .inl a =>
change (indexValueSumEquiv i).1 a = _
rfl
| .inr 0 =>
change oneMarkedIndexValue
((colorsIndexDualCast (Eq.trans h (Eq.symm (mulUnit_dual_markedColor μ)))).symm
(oneMarkedIndexValue.symm y)) 0 = _
rw [indexValueIso_eq_symm, indexValueIso_symm_apply']
simp only [Fin.isValue, oneMarkedIndexValue, colorsIndexDualCast, colorsIndexCast,
Equiv.coe_fn_symm_mk, indexValueDualIso_apply, Equiv.trans_apply, Equiv.cast_apply,
Equiv.symm_trans_apply, Equiv.cast_symm, Equiv.symm_symm, Equiv.apply_symm_apply, cast_cast,
Equiv.coe_fn_mk, Equiv.refl_symm, Equiv.coe_refl, Function.comp_apply, id_eq, mul_color,
Sum.elim_inr, Equiv.refl_apply, cast_inj, y]
rfl
exact Finset.mem_univ y
intro b _ hab
rw [mul_eq_zero]
apply Or.inr
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)) =
mapIso d (Equiv.sumComm X (Fin 1)) T := by
rw [← mul_symm, mulUnit_right]
exact h
lemma mulUnit_lorentzAction (μ : Colors) (Λ : LorentzGroup d) :
Λ • mulUnit d μ = mulUnit d μ := by
match μ with
| Colors.up =>
rw [mulUnit]
simp only [Nat.reduceAdd]
rw [← lorentzAction_mapIso]
rw [lorentzAction_ofMatUpDown]
repeat apply congrArg
rw [mul_one]
change (Λ * Λ⁻¹).1 = 1
rw [mul_inv_self Λ]
rfl
| Colors.down =>
rw [mulUnit]
simp only [Nat.reduceAdd]
rw [← lorentzAction_mapIso]
rw [lorentzAction_ofMatDownUp]
repeat apply congrArg
rw [mul_one]
change ((LorentzGroup.transpose Λ⁻¹) * LorentzGroup.transpose Λ).1 = 1
have inv_transpose : (LorentzGroup.transpose Λ⁻¹) = (LorentzGroup.transpose Λ)⁻¹ := by
simp [LorentzGroup.transpose]
rw [inv_transpose]
rw [inv_mul_self]
rfl
end RealLorentzTensor