Duality on simple classes

In a rigid monoidal abelian category with additive tensor product the right dual of a simple object is simple (TauCeti.simple_rightDual), so duality acts on the simple isomorphism classes: TauCeti.SimpleClasses.dual sends the class of X to the class of Xᘁ. In a finite semisimple rigid category with simple tensor unit this action is an involution (TauCeti.SimpleClasses.dual_dual, in TauCeti/CategoryTheory/Semisimple/Rigid.lean).

Main declarations

• TauCeti.SimpleClasses.dual: the dual simple class;
• TauCeti.SimpleClasses.dualReprIso: its representative is isomorphic to the right dual of the representative;
• TauCeti.SimpleClasses.dual_classOf and TauCeti.SimpleClasses.eq_dual_iff: characterizations of the dual class.

References

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

noncomputable def TauCeti.SimpleClasses.dual {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] (S : SimpleClasses C) : SimpleClasses C

The dual of a simple class: the class of the right dual of its representative.

noncomputable def TauCeti.SimpleClasses.dualReprIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] (S : SimpleClasses C) : S.dual.repr ≅ S.reprᘁ

The representative of the dual class is isomorphic to the right dual of the representative.

@[simp]

theorem TauCeti.SimpleClasses.dual_classOf {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] (X : C) [CategoryTheory.Simple X] : (classOf X).dual = classOf Xᘁ

The dual of the class of a simple object is the class of its right dual.

theorem TauCeti.SimpleClasses.eq_dual_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] (S T : SimpleClasses C) : T = S.dual ↔ Nonempty (T.repr ≅ S.reprᘁ)

A simple class is the dual of S exactly when its representative is isomorphic to the right dual of the representative of S.