Metrics in tensor trees

def TensorSpecies.metricTensor (S : TensorSpecies) (c : S.C) : ↑(S.F.obj (IndexNotation.OverColor.mk ![c, c])).V

The metric of a tensor species in a PiTensorProduct.

Equations

• S.metricTensor c = (CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.Discrete.pairIsoSep S.FD).hom.hom) ((CategoryTheory.ConcreteCategory.hom (S.metric.app { as := c }).hom) 1)

theorem TensorSpecies.metricTensor_congr {S : TensorSpecies} {c c' : S.C} (h : c = c') : (TensorTree.tensorNode (S.metricTensor c)).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (Equiv.refl (Fin (Nat.succ 0).succ)) ⋯) (TensorTree.tensorNode (S.metricTensor c'))).tensor

theorem TensorSpecies.pairIsoSep_inv_metricTensor {S : TensorSpecies} (c : S.C) : (CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.Discrete.pairIsoSep S.FD).inv.hom) (S.metricTensor c) = (CategoryTheory.ConcreteCategory.hom (S.metric.app { as := c }).hom) 1

theorem TensorSpecies.contr_metric_braid_unit {S : TensorSpecies} (c : S.C) : (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) (S.metricTensor c) ⊗ₜ[S.k] (CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.Discrete.pairIsoSep S.FD).inv.hom) (S.metricTensor (S.τ c)))))) = (CategoryTheory.ConcreteCategory.hom (β_ (S.FD.obj { as := S.τ c }) (S.FD.obj { as := c })).hom.hom) ((CategoryTheory.ConcreteCategory.hom (S.unit.app { as := c }).hom) 1)

Contraction of a metric tensor with a metric tensor gives the unit. Like S.contr_metric but with the braiding appearing on the side of the unit.

theorem TensorSpecies.metricTensor_contr_dual_metricTensor_perm_cond {S : TensorSpecies} (c : S.C) (x : Fin (Nat.succ 0).succ) : ((Sum.elim ![c, c] ![S.τ c, S.τ c] ∘ ⇑finSumFinEquiv.symm) ∘ Fin.succAbove 1 ∘ Fin.succAbove 1) x = (![S.τ c, c] ∘ ⇑(PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯).symm) x

theorem TensorSpecies.metricTensor_contr_dual_metricTensor_eq_unit {S : TensorSpecies} (c : S.C) : (TensorTree.contr 1 1 ⋯ ((TensorTree.tensorNode (S.metricTensor c)).prod (TensorTree.tensorNode (S.metricTensor (S.τ c))))).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode (S.unitTensor c))).tensor

The contraction of a metric tensor with its dual via the inner indices gives the unit.

theorem TensorSpecies.metricTensor_contr_dual_metricTensor_outer_eq_unit {S : TensorSpecies} (c : S.C) : (TensorTree.contr 0 2 ⋯ ((TensorTree.tensorNode (S.metricTensor c)).prod (TensorTree.tensorNode (S.metricTensor (S.τ c))))).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode (S.unitTensor c))).tensor

The contraction of a metric tensor with its dual via the outer indices gives the unit.