Duals of simple objects

In a rigid monoidal abelian category whose tensor product is additive, the right dual of a simple object is simple. Taking right adjoint mates is a bijection (A ⟶ B) ≃ (Bᘁ ⟶ Aᘁ) reversing composition, with inverse the left adjoint mate, and every object Y is the right dual (ᘁY)ᘁ of its left dual. So a monomorphism f : Y ⟶ Xᘁ is the mate of the epimorphism ᘁf : X ⟶ ᘁY, which out of the simple object X is an isomorphism or zero.

This is what makes duality act on the simple isomorphism classes of a fusion category.

If the tensor unit is simple, the tensor product of two nonzero objects is nonzero (TauCeti.not_isZero_tensorObj). The coevaluation 𝟙_ C ⟶ Y ⊗ Yᘁ of a nonzero object is nonzero, hence a monomorphism out of the simple unit, and whiskering by X keeps it a monomorphism because X ⊗ - is right adjoint to Xᘁ ⊗ -. So X ≅ X ⊗ 𝟙_ C embeds into (X ⊗ Y) ⊗ Yᘁ. Without a simple unit this fails: in a multifusion category two distinct simple summands of the unit have zero tensor product.

For a split simple member of an exact pairing, Frobenius reciprocity and Schur's lemma show that every morphism from the paired tensor product to the unit is a scalar multiple of the evaluation. Both choices of the simple member are available; they control the two categorical trace pairings.

References

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

instance TauCeti.simple_rightDual {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] (X : C) [CategoryTheory.Simple X] : CategoryTheory.Simple Xᘁ

In a rigid monoidal abelian category, the right dual of a simple object is simple.

theorem TauCeti.not_isZero_tensorObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RightRigidCategory C] [CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] {X Y : C} (hX : ¬CategoryTheory.Limits.IsZero X) (hY : ¬CategoryTheory.Limits.IsZero Y) : ¬CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

In a right rigid monoidal preadditive category with kernels and simple tensor unit, the tensor product of two nonzero objects is nonzero.

theorem TauCeti.hom_tensorUnit_eq_smul_evaluation_of_simple_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (k : Type u_1) [Field k] [IsAlgClosed k] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] {X Y : C} [CategoryTheory.ExactPairing X Y] [CategoryTheory.Simple Y] [FiniteDimensional k (Y ⟶ Y)] (f : CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : ∃ (c : k), f = c • ε_ X Y

If the right member of an exact pairing is split simple, every morphism from the paired tensor product to the unit is a scalar multiple of the evaluation.

theorem TauCeti.hom_tensorUnit_eq_smul_evaluation_of_simple_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (k : Type u_1) [Field k] [IsAlgClosed k] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] {X Y : C} [CategoryTheory.ExactPairing X Y] [CategoryTheory.Simple X] [FiniteDimensional k (X ⟶ X)] (f : CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : ∃ (c : k), f = c • ε_ X Y

If the left member of an exact pairing is split simple, every morphism from the paired tensor product to the unit is a scalar multiple of the evaluation.