Duality on the Grothendieck ring of a rigid category

In a right rigid monoidal additive category, taking right duals respects isomorphisms and binary biproducts (TauCeti.rightDualBiprodIso), so it descends to an additive endomorphism TauCeti.SplitK0.dual of the split Grothendieck group, [X] ↦ [Xᘁ]. Since (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ and (𝟙_ C)ᘁ ≅ 𝟙_ C, it is an anti-endomorphism of the Grothendieck ring: dual (x * y) = dual y * dual x and dual 1 = 1.

For a fusion category this is the involution of the Grothendieck ring as a based ring, which permutes the basis of simple classes; that is developed in TauCeti/CategoryTheory/Semisimple/Rigid.lean.

Main declarations

• TauCeti.SplitK0.dual: the duality [X] ↦ [Xᘁ] on split K₀;
• TauCeti.SplitK0.dual_one and TauCeti.SplitK0.dual_mul: it reverses products.

References

• [P. Etingof, S. Gelaki, D. Nikshych, V. Ostrik, Tensor categories][egno15], §4.5

noncomputable def TauCeti.SplitK0.dual {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] [CategoryTheory.RightRigidCategory C] : SplitK0 C →+ SplitK0 C

The duality [X] ↦ [Xᘁ] on the split Grothendieck group of a right rigid monoidal additive category. It reverses products (TauCeti.SplitK0.dual_mul).

@[simp]

theorem TauCeti.SplitK0.dual_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] [CategoryTheory.RightRigidCategory C] (X : C) : dual (of X) = of Xᘁ

The dual of the class of an object is the class of its right dual.

@[simp]

theorem TauCeti.SplitK0.dual_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] [CategoryTheory.RightRigidCategory C] : dual 1 = 1

The duality fixes the unit, since the right dual of the tensor unit is the tensor unit.

@[simp]

theorem TauCeti.SplitK0.dual_mul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] [CategoryTheory.RightRigidCategory C] (x y : SplitK0 C) : dual (x * y) = dual y * dual x

The duality reverses products, since (X ⊗ Y)ᘁ ≅ Yᘁ ⊗ Xᘁ.