The unit tensors

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

The unit tensor associated with a color c.

Equations

• TensorSpecies.unitTensor c = TensorSpecies.Tensor.fromConstPair (S.unit.app { as := c })

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

theorem TensorSpecies.unit_app_eq_dual_unit_app {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} (c : S.C) : S.unit.app { as := c } = CategoryTheory.CategoryStruct.comp (S.unit.app { as := S.τ c }) (CategoryTheory.CategoryStruct.comp (β_ (S.FD.obj { as := S.τ (S.τ c) }) (S.FD.obj { as := S.τ c })).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (S.FD.obj { as := S.τ c }) (S.FD.map (CategoryTheory.Discrete.eqToHom ⋯))))

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

The unit tensor is symmetric on dualing the color.

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

theorem TensorSpecies.unit_fromSingleTContrFromPairT_eq_fromSingleT {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} (x : ↑(S.FD.obj { as := c }).V) : Tensor.fromSingleTContrFromPairT x ((CategoryTheory.ConcreteCategory.hom (S.unit.app { as := c }).hom) 1) = Tensor.fromSingleT x

@[simp]

theorem TensorSpecies.contrT_single_unitTensor {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} (x : S.Tensor ![c]) : (Tensor.contrT 1 0 1 ⋯) ((Tensor.prodT x) (unitTensor c)) = (Tensor.permT id ⋯) x

This lemma represents the de-categorification of S.contr_unit.

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

@[simp]

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