The metric tensors

noncomputable def TensorSpecies.metricTensor {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} (c : S.C) : S.Tensor ![c, c]

The metric tensor associated with a color c.

Equations

• TensorSpecies.metricTensor c = TensorSpecies.Tensor.fromConstPair (S.metric.app { as := c })

theorem TensorSpecies.metricTensor_congr {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c c1 : S.C} (h : c = c1) : metricTensor c = (Tensor.permT id ⋯) (metricTensor c1)

@[simp]

theorem TensorSpecies.metricTensor_invariant {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} (g : G) : g • metricTensor c = metricTensor c

theorem TensorSpecies.permT_fromPairTContr_metric_metric {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} : (Tensor.permT ![1, 0] ⋯) (Tensor.fromPairTContr ((CategoryTheory.ConcreteCategory.hom (S.metric.app { as := c }).hom) 1) ((CategoryTheory.ConcreteCategory.hom (S.metric.app { as := S.τ c }).hom) 1)) = unitTensor c

theorem TensorSpecies.fromPairTContr_metric_metric_eq_permT_unit {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} : Tensor.fromPairTContr ((CategoryTheory.ConcreteCategory.hom (S.metric.app { as := c }).hom) 1) ((CategoryTheory.ConcreteCategory.hom (S.metric.app { as := S.τ c }).hom) 1) = (Tensor.permT ![1, 0] ⋯) (unitTensor c)

@[simp]

theorem TensorSpecies.contrT_metricTensor_metricTensor {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} : (Tensor.contrT 2 1 2 ⋯) ((Tensor.prodT (metricTensor c)) (metricTensor (S.τ c))) = (Tensor.permT ![1, 0] ⋯) (unitTensor c)

The contraction of the metric tensor with its dual gives the unit tensor. This is the de-categorification of S.contr_metric.

theorem TensorSpecies.contrT_metricTensor_metricTensor_eq_dual_unit {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} : (Tensor.contrT 2 1 2 ⋯) ((Tensor.prodT (metricTensor c)) (metricTensor (S.τ c))) = (Tensor.permT ![0, 1] ⋯) (unitTensor (S.τ c))

@[simp]

theorem TensorSpecies.contrT_dual_metricTensor_metricTensor {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} : (Tensor.contrT 2 1 2 ⋯) ((Tensor.prodT (metricTensor (S.τ c))) (metricTensor c)) = (Tensor.permT id ⋯) (unitTensor c)