PhysLean Documentation

PhysLean.Relativity.Tensors.TensorSpecies.Contractions.Categorical

Contraction of specific tensor types #

In this file we expand some contractions of given tensors in terms of basic categorical properties of the tensor species.

source
def TensorSpecies.contrOneTwoLeft {S : TensorSpecies} {c1 c2 : S.C} (x : ↑(S.F.obj (IndexNotation.OverColor.mk ![c1])).V) (y : ↑(S.F.obj (IndexNotation.OverColor.mk ![S.τ c1, c2])).V) :
↑(S.F.obj (IndexNotation.OverColor.mk ![c2])).V

Th map built contracting a 1-tensor with a 2-tensor using basic categorical constructions.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TensorSpecies.contrOneTwoLeft_smul_left {S : TensorSpecies} {c1 c2 : S.C} (x : ↑(S.F.obj (IndexNotation.OverColor.mk ![c1])).V) (y : ↑(S.F.obj (IndexNotation.OverColor.mk ![S.τ c1, c2])).V) (r : S.k) :
    contrOneTwoLeft (r • x) y = r • contrOneTwoLeft x y
    source
    @[simp]
    theorem TensorSpecies.contrOneTwoLeft_smul_right {S : TensorSpecies} {c1 c2 : S.C} (x : ↑(S.F.obj (IndexNotation.OverColor.mk ![c1])).V) (y : ↑(S.F.obj (IndexNotation.OverColor.mk ![S.τ c1, c2])).V) (r : S.k) :
    contrOneTwoLeft x (r • y) = r • contrOneTwoLeft x y
    source
    @[simp]
    theorem TensorSpecies.contrOneTwoLeft_add_left {S : TensorSpecies} {c1 c2 : S.C} (x y : ↑(S.F.obj (IndexNotation.OverColor.mk ![c1])).V) (z : ↑(S.F.obj (IndexNotation.OverColor.mk ![S.τ c1, c2])).V) :
    contrOneTwoLeft (x + y) z = contrOneTwoLeft x z + contrOneTwoLeft y z
    source
    @[simp]
    theorem TensorSpecies.contrOneTwoLeft_add_right {S : TensorSpecies} {c1 c2 : S.C} (x : ↑(S.F.obj (IndexNotation.OverColor.mk ![c1])).V) (y z : ↑(S.F.obj (IndexNotation.OverColor.mk ![S.τ c1, c2])).V) :
    contrOneTwoLeft x (y + z) = contrOneTwoLeft x y + contrOneTwoLeft x z
    source
    theorem TensorSpecies.contrOneTwoLeft_tprod_eq {S : TensorSpecies} {c1 c2 : S.C} (fx : (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk ![c1]).left) → ↑(S.FD.obj { as := (IndexNotation.OverColor.mk ![c1]).hom i }).V) (fy : (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk ![S.τ c1, c2]).left) → ↑(S.FD.obj { as := (IndexNotation.OverColor.mk ![S.τ c1, c2]).hom i }).V) :
    contrOneTwoLeft ((PiTensorProduct.tprod S.k) fx) ((PiTensorProduct.tprod S.k) fy) = (CategoryTheory.ConcreteCategory.hom (S.tensorToVec c2).inv.hom) ((CategoryTheory.ConcreteCategory.hom (S.contr.app { as := c1 }).hom) (fx 0 ⊗ₜ[S.k] fy 0) • fy 1)
    source
    theorem TensorSpecies.contr_one_two_left_eq_contrOneTwoLeft_tprod {S : TensorSpecies} {c1 c2 : S.C} (x : ↑(S.F.obj (IndexNotation.OverColor.mk ![c1])).V) (y : ↑(S.F.obj (IndexNotation.OverColor.mk ![S.τ c1, c2])).V) (fx : (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk ![c1]).left) → ↑(S.FD.obj { as := (IndexNotation.OverColor.mk ![c1]).hom i }).V) (fy : (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk ![S.τ c1, c2]).left) → ↑(S.FD.obj { as := (IndexNotation.OverColor.mk ![S.τ c1, c2]).hom i }).V) (hx : x = (PiTensorProduct.tprod S.k) fx) (hy : y = (PiTensorProduct.tprod S.k) fy) :
    (TensorTree.contr 0 0 ⋯ ((TensorTree.tensorNode x).prod (TensorTree.tensorNode y))).tensor = (CategoryTheory.ConcreteCategory.hom (S.F.mapIso (IndexNotation.OverColor.mkIso ⋯)).hom.hom) (contrOneTwoLeft x y)
    source
    theorem TensorSpecies.contr_one_two_left_eq_contrOneTwoLeft {S : TensorSpecies} {c1 c2 : S.C} (x : ↑(S.F.obj (IndexNotation.OverColor.mk ![c1])).V) (y : ↑(S.F.obj (IndexNotation.OverColor.mk ![S.τ c1, c2])).V) :
    (TensorTree.contr 0 0 ⋯ ((TensorTree.tensorNode x).prod (TensorTree.tensorNode y))).tensor = (CategoryTheory.ConcreteCategory.hom (S.F.map (IndexNotation.OverColor.mkIso ⋯).hom).hom) (contrOneTwoLeft x y)
    source
    theorem TensorSpecies.contrOneTwoLeft_tensorTree {S : TensorSpecies} {c1 c2 : S.C} (x : ↑(S.F.obj (IndexNotation.OverColor.mk ![c1])).V) (y : ↑(S.F.obj (IndexNotation.OverColor.mk ![S.τ c1, c2])).V) :
    contrOneTwoLeft x y = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (Equiv.refl (Fin 1)) ⋯) (TensorTree.contr 0 0 ⋯ ((TensorTree.tensorNode x).prod (TensorTree.tensorNode y)))).tensor

    Expanding contrOneTwoLeft as a tensor tree.

    source
    theorem TensorSpecies.contr_two_two_inner_tprod {S : TensorSpecies} (c : S.C) (x : ↑(S.F.obj (IndexNotation.OverColor.mk ![c, c])).V) (fx : (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk ![c, c]).left) → ↑(S.FD.obj { as := (IndexNotation.OverColor.mk ![c, c]).hom i }).V) (y : ↑(S.F.obj (IndexNotation.OverColor.mk ![S.τ c, S.τ c])).V) (fy : (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk ![S.τ c, S.τ c]).left) → ↑(S.FD.obj { as := (IndexNotation.OverColor.mk ![S.τ c, S.τ c]).hom i }).V) (hx : x = (PiTensorProduct.tprod S.k) fx) (hy : y = (PiTensorProduct.tprod S.k) fy) :
    (TensorTree.contr 1 1 ⋯ ((TensorTree.tensorNode x).prod (TensorTree.tensorNode y))).tensor = (CategoryTheory.ConcreteCategory.hom (S.F.map (IndexNotation.OverColor.mkIso ⋯).hom).hom) ((CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.Discrete.pairIsoSep S.FD).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (S.FD.obj { as := c }) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (S.FD.obj { as := S.τ c })).hom).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (S.FD.obj { as := c }) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (S.contr.app { as := c }) (S.FD.obj { as := S.τ c }))).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (S.FD.obj { as := c }) (CategoryTheory.MonoidalCategoryStruct.associator (S.FD.obj { as := c }) (S.FD.obj { as := S.τ c }) (S.FD.obj { as := S.τ c })).inv).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator (S.FD.obj { as := c }) (S.FD.obj { as := c }) (CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := S.τ c }) (S.FD.obj { as := S.τ c }))).hom.hom) ((CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.Discrete.pairIsoSep S.FD).inv.hom) x ⊗ₜ[S.k] (CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.Discrete.pairIsoSep S.FD).inv.hom) y))))))

    Expands the inner contraction of two 2-tensors which are tprods in terms of basic categorical constructions and fields of the tensor species.

    source
    theorem TensorSpecies.contr_two_two_inner {S : TensorSpecies} (c : S.C) (x : ↑(S.F.obj (IndexNotation.OverColor.mk ![c, c])).V) (y : ↑(S.F.obj (IndexNotation.OverColor.mk ![S.τ c, S.τ c])).V) :
    (TensorTree.contr 1 1 ⋯ ((TensorTree.tensorNode x).prod (TensorTree.tensorNode y))).tensor = (CategoryTheory.ConcreteCategory.hom (S.F.map (IndexNotation.OverColor.mkIso ⋯).hom).hom) ((CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.Discrete.pairIsoSep S.FD).hom.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (S.FD.obj { as := c }) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (S.FD.obj { as := S.τ c })).hom).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (S.FD.obj { as := c }) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (S.contr.app { as := c }) (S.FD.obj { as := S.τ c }))).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (S.FD.obj { as := c }) (CategoryTheory.MonoidalCategoryStruct.associator (S.FD.obj { as := c }) (S.FD.obj { as := S.τ c }) (S.FD.obj { as := S.τ c })).inv).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator (S.FD.obj { as := c }) (S.FD.obj { as := c }) (CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := S.τ c }) (S.FD.obj { as := S.τ c }))).hom.hom) ((CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.Discrete.pairIsoSep S.FD).inv.hom) x ⊗ₜ[S.k] (CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.Discrete.pairIsoSep S.FD).inv.hom) y))))))

    Expands the inner contraction of two 2-tensors in terms of basic categorical constructions and fields of the tensor species.