def CategoryTheory.IsSemisimpleObject (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] (X : C) : Prop

class CategoryTheory.IsSemisimpleCategory (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] : Prop

• semisimple (X : C) : IsSemisimpleObject C X

theorem CategoryTheory.isSemisimpleObject_of_iso {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} (i : X ≅ Y) (h : IsSemisimpleObject C Y) : IsSemisimpleObject C X

class CategoryTheory.IsMultitensorCategory (C : Type u) [Category.{v, u} C] [MonoidalCategory C] extends CategoryTheory.RigidCategory C : Type (max u v)

• rightDual (X : C) : HasRightDual X
• leftDual (X : C) : HasLeftDual X

class CategoryTheory.IsMultifusionCategory (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] extends CategoryTheory.IsMultitensorCategory C : Type (max u v)

• rightDual (X : C) : HasRightDual X
• leftDual (X : C) : HasLeftDual X
• isSemisimple : IsSemisimpleCategory C

theorem CategoryTheory.unit_isSemisimpleObject {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [IsSemisimpleCategory C] : IsSemisimpleObject C (MonoidalCategoryStruct.tensorUnit C)

theorem CategoryTheory.isZero_tensor_left {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Preadditive C] [MonoidalPreadditive C] {A B : C} (h : Limits.IsZero A) : Limits.IsZero (MonoidalCategoryStruct.tensorObj A B)

theorem CategoryTheory.isZero_tensor_right {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Preadditive C] [MonoidalPreadditive C] {A B : C} (h : Limits.IsZero B) : Limits.IsZero (MonoidalCategoryStruct.tensorObj A B)

def CategoryTheory.componentObj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {n : ℕ} (f : Fin n → C) (X : C) (i j : Fin n) : C

The (i, j)-component object f i ⊗ X ⊗ f j formed by sandwiching X between two chosen simple summands of the unit.

def CategoryTheory.componentFamily {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {n : ℕ} (f : Fin n → C) (X : C) : Fin n × Fin n → C

The family of all (i, j)-component objects of X, indexed by pairs in Fin n × Fin n.

def CategoryTheory.IsInComponentSubcategory {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {n : ℕ} (f : Fin n → C) (i j : Fin n) : ObjectProperty C

The property that an object lies in the (i, j)-component subcategory: it is isomorphic to f i ⊗ Y ⊗ f j for some Y.

@[reducible, inline]

abbrev CategoryTheory.Definition_1_15_4_ComponentSubcategory {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {n : ℕ} (f : Fin n → C) (i j : Fin n) : Type u

Definition 1.15.4: the component subcategory C_{ij} = 𝟙_i ⊗ C ⊗ 𝟙_j realised as a full subcategory of C.

theorem CategoryTheory.whisker_unitor_calc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} (s : A ⟶ MonoidalCategoryStruct.tensorUnit C) (r : MonoidalCategoryStruct.tensorUnit C ⟶ B) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor A).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A r) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight s B) (MonoidalCategoryStruct.leftUnitor B).hom)) = CategoryStruct.comp s r

Coherence helper: the chain through the unitors and a whiskering collapses to the composition s ≫ r.

theorem CategoryTheory.unitComponent_tensor_zero {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] {n : ℕ} (f : Fin n → C) [Limits.HasBiproduct f] (hiso : MonoidalCategoryStruct.tensorUnit C ≅ ⨁ f) (hsimp : ∀ (i : Fin n), Simple (f i)) {i j : Fin n} (hij : i ≠ j) : Limits.IsZero (MonoidalCategoryStruct.tensorObj (f i) (f j))

If 𝟙_ C decomposes as a sum of distinct simple summands f i, then the cross tensor products f i ⊗ f j with i ≠ j are zero.

noncomputable def CategoryTheory.component_diagonal_unit_iso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] {n : ℕ} (f : Fin n → C) [Limits.HasBiproduct f] (hiso : MonoidalCategoryStruct.tensorUnit C ≅ ⨁ f) (hsimp : ∀ (i : Fin n), Simple (f i)) (i : Fin n) : MonoidalCategoryStruct.tensorObj (f i) (f i) ≅ f i

When 𝟙_ C decomposes as a sum of distinct simple summands f i, each diagonal component f i ⊗ f i is canonically isomorphic to f i.

theorem CategoryTheory.tensor_component_zero {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [Preadditive C] [MonoidalPreadditive C] {n : ℕ} (f : Fin n → C) [Limits.HasBiproduct f] (hiso : MonoidalCategoryStruct.tensorUnit C ≅ ⨁ f) (hsimp : ∀ (i : Fin n), Simple (f i)) (X Y : C) (i j k l : Fin n) (hjk : j ≠ k) : Limits.IsZero (MonoidalCategoryStruct.tensorObj (componentObj f X i j) (componentObj f Y k l))

Proposition 1.15.5 (2): tensor products between component subcategories vanish off the diagonal — C_{ij} ⊗ C_{kl} = 0 unless j = k.

noncomputable def CategoryTheory.tensor_component_compatible {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] {n : ℕ} (f : Fin n → C) [Limits.HasBiproduct f] (hiso : MonoidalCategoryStruct.tensorUnit C ≅ ⨁ f) (hsimp : ∀ (i : Fin n), Simple (f i)) (X Y : C) (i j l : Fin n) : MonoidalCategoryStruct.tensorObj (componentObj f X i j) (componentObj f Y j l) ≅ componentObj f (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X (f j)) Y) i l

Proposition 1.15.5 (2): on the diagonal j = k, the tensor product C_{ij} ⊗ C_{jl} lands in C_{il}, exhibited via an explicit isomorphism.

theorem CategoryTheory.rightAdjointMate_unit_endo {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [RigidCategory C] (g : MonoidalCategoryStruct.tensorUnit C ⟶ MonoidalCategoryStruct.tensorUnit C) : gᘁ = g

The right adjoint mate of any endomorphism of the unit 𝟙_ C equals the endomorphism itself, since the unit is canonically self-dual in a rigid category.

noncomputable def CategoryTheory.unitComponent_selfDual {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [RigidCategory C] {n : ℕ} (f : Fin n → C) [Limits.HasBiproduct f] (hiso : MonoidalCategoryStruct.tensorUnit C ≅ ⨁ f) (hsimp : ∀ (i : Fin n), Simple (f i)) (i : Fin n) : f i ≅ (f i)ᘁ

Each simple summand f i of a decomposition of the unit is canonically isomorphic to its own right dual, via the mates of the structural inclusion and projection maps.

def CategoryTheory.rightDualTensorIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (A B : C) : (MonoidalCategoryStruct.tensorObj A B)ᘁ ≅ MonoidalCategoryStruct.tensorObj Bᘁ Aᘁ

The right dual of a tensor product is canonically isomorphic to the reversed tensor product of right duals, (A ⊗ B)ᘁ ≅ Bᘁ ⊗ Aᘁ, constructed via uniqueness of right adjoints.

def CategoryTheory.leftDualTensorIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (A B : C) : ᘁ(MonoidalCategoryStruct.tensorObj A B) ≅ MonoidalCategoryStruct.tensorObj ᘁB ᘁA

The left dual of a tensor product is canonically isomorphic to the reversed tensor product of left duals, ᘁ(A ⊗ B) ≅ ᘁB ⊗ ᘁA, constructed via uniqueness of right adjoints.

def CategoryTheory.leftDualSelfDual {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] {V : C} (selfDual : V ≅ Vᘁ) : ᘁV ≅ V

Given a self-duality isomorphism V ≅ Vᘁ, transport it through left adjoint mates to produce an isomorphism ᘁV ≅ V.

noncomputable def CategoryTheory.rightDual_component {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [RigidCategory C] {n : ℕ} (f : Fin n → C) [Limits.HasBiproduct f] (hiso : MonoidalCategoryStruct.tensorUnit C ≅ ⨁ f) (hsimp : ∀ (i : Fin n), Simple (f i)) (X : C) (i j : Fin n) : (componentObj f X i j)ᘁ ≅ componentObj f Xᘁ j i

The right dual of an (i, j)-component object f i ⊗ X ⊗ f j is identified with the (j, i)-component object on the dual Xᘁ, swapping the indices.

noncomputable def CategoryTheory.leftDual_component {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [RigidCategory C] {n : ℕ} (f : Fin n → C) [Limits.HasBiproduct f] (hiso : MonoidalCategoryStruct.tensorUnit C ≅ ⨁ f) (hsimp : ∀ (i : Fin n), Simple (f i)) (X : C) (i j : Fin n) : ᘁ(componentObj f X i j) ≅ componentObj f (ᘁX) j i

The left dual of an (i, j)-component object f i ⊗ X ⊗ f j is identified with the (j, i)-component object on the left dual ᘁX, swapping the indices.

noncomputable def CategoryTheory.biproductFlattenIso {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasFiniteBiproducts C] {n : ℕ} (g : Fin n → Fin n → C) : (⨁ fun (i : Fin n) => ⨁ fun (j : Fin n) => g i j) ≅ ⨁ fun (p : Fin n × Fin n) => g p.1 p.2

Canonical isomorphism flattening a double biproduct over Fin n × Fin n into a single biproduct indexed by the product type.

theorem CategoryTheory.object_componentDecomposition {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Preadditive C] [MonoidalPreadditive C] [Limits.HasFiniteBiproducts C] {n : ℕ} (f : Fin n → C) [Limits.HasBiproduct f] (hiso : MonoidalCategoryStruct.tensorUnit C ≅ ⨁ f) (hsimp : ∀ (i : Fin n), Simple (f i)) (X : C) : ∃ (x : Limits.HasBiproduct (componentFamily f X)), Nonempty (X ≅ ⨁ componentFamily f X)

Every object X decomposes as a biproduct of its (i, j)-component objects f i ⊗ X ⊗ f j, where f is the chosen decomposition of the unit into simple summands.

def CategoryTheory.rightDualIsoOfIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] {V W : C} (i : V ≅ W) : Wᘁ ≅ Vᘁ

Functoriality of right duals on isomorphisms: an iso V ≅ W gives Wᘁ ≅ Vᘁ via right adjoint mates.

def CategoryTheory.leftDualIsoOfIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] {V W : C} (i : V ≅ W) : ᘁW ≅ ᘁV

Functoriality of left duals on isomorphisms: an iso V ≅ W gives ᘁW ≅ ᘁV via left adjoint mates.

def CategoryTheory.isoRightDualOfLeftDual {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (V : C) : V ≅ (ᘁV)ᘁ

Any object is isomorphic to the right dual of its own left dual, V ≅ (ᘁV)ᘁ, via the uniqueness of right duals on the rigid pairings.

@[reducible]

def CategoryTheory.exactPairing_rightDual_of_braided {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] [BraidedCategory C] (V : C) : ExactPairing Vᘁ V

In a braided rigid category the right dual Vᘁ also forms an exact pairing with V on the other side, obtained by transporting the canonical pairing through the braiding.

def CategoryTheory.leftDualIsoRightDual_of_compatibleDuals {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (V : C) (ep : ExactPairing Vᘁ V) : ᘁV ≅ Vᘁ

Given a compatible exact pairing ExactPairing Vᘁ V, the left and right duals of V are canonically isomorphic, ᘁV ≅ Vᘁ.

def CategoryTheory.doubleDualIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (V : C) (ep : ExactPairing Vᘁ V) : V ≅ Vᘁᘁ

Given a compatible exact pairing ExactPairing Vᘁ V, the object V is canonically isomorphic to its double right dual (Vᘁ)ᘁ.

@[reducible]

noncomputable def CategoryTheory.ExactPairing.ofIsoLeft {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X X' Y : C} (ep : ExactPairing X Y) (f : X ≅ X') : ExactPairing X' Y

Transport an exact pairing ExactPairing X Y along an isomorphism X ≅ X' of the left component to obtain an exact pairing ExactPairing X' Y.

noncomputable def CategoryTheory.leftDual_iso_rightDual_aux {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [IsMultifusionCategory C] (V : C) : ᘁV ≅ Vᘁ

Auxiliary form of Proposition 1.41.1: in a multifusion category the left dual is canonically isomorphic to the right dual.

noncomputable def CategoryTheory.exactPairing_rightDual_of_multifusion {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [IsMultifusionCategory C] (V : C) : ExactPairing Vᘁ V

In a multifusion category, the right dual Vᘁ forms an exact pairing with V on the left as well, yielding a compatible duality.

noncomputable def CategoryTheory.leftDual_iso_rightDual_of_multifusion {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [IsMultifusionCategory C] (V : C) : ᘁV ≅ Vᘁ

In a multifusion category, the left dual is canonically isomorphic to the right dual, obtained by combining leftDualIso with the multifusion exact pairing.

noncomputable def CategoryTheory.prop_1_41_1_leftDualIsoRightDual {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [IsMultifusionCategory C] (V : C) : ᘁV ≅ Vᘁ

Proposition 1.41.1 (first conclusion): in a multifusion category, the functors of taking left and right duals are canonically isomorphic, witnessed object-wise by ᘁV ≅ Vᘁ.

noncomputable def CategoryTheory.prop_1_41_1_doubleDualIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasZeroMorphisms C] [IsMultifusionCategory C] (V : C) : V ≅ Vᘁᘁ

Proposition 1.41.1 (second conclusion): in a multifusion category, every object is canonically isomorphic to its double dual via the multifusion exact pairing.

theorem CategoryTheory.finrank_hom_unit_tensor_dual_eq_finrank_end_aux {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (k : Type w) [Field k] [IsAlgClosed k] [Preadditive C] [Linear k C] [Abelian C] [MonoidalPreadditive C] [MonoidalLinear k C] (V : C) [Simple V] [FiniteDimensional k (V ⟶ V)] [FiniteDimensional k (MonoidalCategoryStruct.tensorUnit C ⟶ MonoidalCategoryStruct.tensorObj V Vᘁ)] : Module.finrank k (MonoidalCategoryStruct.tensorUnit C ⟶ MonoidalCategoryStruct.tensorObj V Vᘁ) = Module.finrank k (V ⟶ V)

Auxiliary fact: for a simple object V in a k-linear rigid abelian category over an algebraically closed field, the k-dimension of 𝟙_ C ⟶ V ⊗ Vᘁ equals the k-dimension of the endomorphism algebra V ⟶ V.

theorem CategoryTheory.isSemisimpleCategory_mono_isSplitMono {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] [Preadditive C] [Abelian C] [IsSemisimpleCategory C] {X Y : C} (f : X ⟶ Y) [Mono f] : IsSplitMono f

Auxiliary fact: in a semisimple abelian category, every monomorphism splits.

theorem CategoryTheory.isSemisimpleCategory_epi_isSplitEpi {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] [Preadditive C] [Abelian C] [IsSemisimpleCategory C] {X Y : C} (f : X ⟶ Y) [Epi f] : IsSplitEpi f

Auxiliary fact: in a semisimple abelian category, every epimorphism splits.

theorem CategoryTheory.isSplitEpi_cokernel_π_of_isSplitMono_aux {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] [Preadditive C] [Abelian C] {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] : IsSplitEpi (Limits.cokernel.π f)

Auxiliary helper: in a preadditive abelian category, the cokernel projection of any split monomorphism is itself a split epimorphism, with explicit splitting via 𝟙 Y - retraction ≫ f.

theorem CategoryTheory.composition_nonzero_of_finrank_one_aux {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (k : Type w) [Field k] [IsAlgClosed k] [Preadditive C] [Linear k C] [Abelian C] [MonoidalPreadditive C] [MonoidalLinear k C] [IsSemisimpleCategory C] [Simple (MonoidalCategoryStruct.tensorUnit C)] {X : C} (f : MonoidalCategoryStruct.tensorUnit C ⟶ X) (g : X ⟶ MonoidalCategoryStruct.tensorUnit C) [FiniteDimensional k (MonoidalCategoryStruct.tensorUnit C ⟶ X)] (hfin : Module.finrank k (MonoidalCategoryStruct.tensorUnit C ⟶ X) = 1) (hf : f ≠ 0) (hg : g ≠ 0) : CategoryStruct.comp f g ≠ 0

Auxiliary lemma: if Hom(𝟙_ C, X) is one-dimensional over an algebraically closed field k and both f : 𝟙_ C ⟶ X and g : X ⟶ 𝟙_ C are nonzero, then the composition f ≫ g is nonzero.

theorem CategoryTheory.coevaluation_ne_zero_of_simple {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] [Preadditive C] [MonoidalPreadditive C] {V : C} [Simple V] : η_ V Vᘁ ≠ 0

The coevaluation η_ V Vᘁ is nonzero for a simple object V in a preadditive monoidal category: otherwise the rigidity triangle would force 𝟙 V = 0, contradicting simplicity.

theorem CategoryTheory.evaluation_ne_zero_of_simple {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] [Preadditive C] [MonoidalPreadditive C] {V : C} [Simple V] : ε_ Vᘁ Vᘁᘁ ≠ 0

The evaluation ε_ Vᘁ (Vᘁ)ᘁ is nonzero for a simple object V: a vanishing evaluation would force 𝟙 Vᘁ = 0 and in turn η_ V Vᘁ = 0, contradicting coevaluation_ne_zero_of_simple.

theorem CategoryTheory.leftQuantumTrace_ne_zero_of_simple_semisimple {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (k : Type w) [Field k] [IsAlgClosed k] [Preadditive C] [Linear k C] [Abelian C] [MonoidalPreadditive C] [MonoidalLinear k C] [IsSemisimpleCategory C] [Simple (MonoidalCategoryStruct.tensorUnit C)] {V : C} [Simple V] [FiniteDimensional k (V ⟶ V)] [FiniteDimensional k (MonoidalCategoryStruct.tensorUnit C ⟶ MonoidalCategoryStruct.tensorObj V Vᘁ)] (a : V ≅ Vᘁᘁ) : TensorCategories.leftQuantumTrace C a.hom ≠ 0

Key technical step in Proposition 1.41.5: for any choice of double-dual isomorphism a : V ≅ (Vᘁ)ᘁ on a simple object in a k-linear semisimple rigid category, the resulting left quantum trace tr_L(a) is nonzero.

theorem CategoryTheory.prop_1_41_5 (k : Type w) [Field k] [IsAlgClosed k] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Preadditive C] [Linear k C] [Abelian C] [MonoidalPreadditive C] [MonoidalLinear k C] [RigidCategory C] [IsSemisimpleCategory C] [Simple (MonoidalCategoryStruct.tensorUnit C)] {V : C} [Simple V] [FiniteDimensional k (V ⟶ V)] [FiniteDimensional k (MonoidalCategoryStruct.tensorUnit C ⟶ MonoidalCategoryStruct.tensorObj V Vᘁ)] (a : V ≅ Vᘁᘁ) : TensorCategories.leftQuantumTrace C a.hom ≠ 0

Proposition 1.41.5: in a semisimple k-linear rigid tensor category with simple unit, the left quantum trace of any double-dual isomorphism on a simple object is nonzero.

theorem CategoryTheory.pivotalDimension_ne_zero_of_simple (k : Type w) [Field k] [IsAlgClosed k] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Preadditive C] [Linear k C] [Abelian C] [MonoidalPreadditive C] [MonoidalLinear k C] [RigidCategory C] [TensorCategories.PivotalCategory C] [IsSemisimpleCategory C] [Simple (MonoidalCategoryStruct.tensorUnit C)] {V : C} [Simple V] [FiniteDimensional k (V ⟶ V)] [FiniteDimensional k (MonoidalCategoryStruct.tensorUnit C ⟶ MonoidalCategoryStruct.tensorObj V Vᘁ)] : TensorCategories.pivotalDimension C V ≠ 0

Corollary of Proposition 1.41.5: the pivotal dimension of any simple object in a pivotal semisimple k-linear tensor category with simple unit is nonzero.

theorem CategoryTheory.evaluation_ne_zero_of_nonzero_obj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Preadditive C] [RightRigidCategory C] [MonoidalPreadditive C] (X : C) (hX : ¬Limits.IsZero X) : ε_ X Xᘁ ≠ 0

Corollary 1.15.9 form: the evaluation ε_ X Xᘁ is nonzero for any nonzero object X in a preadditive right-rigid monoidal category.

theorem CategoryTheory.coevaluation_ne_zero_of_nonzero_obj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Preadditive C] [RightRigidCategory C] [MonoidalPreadditive C] (X : C) (hX : ¬Limits.IsZero X) : η_ X Xᘁ ≠ 0

Corollary 1.15.9 form: the coevaluation η_ X Xᘁ is nonzero for any nonzero object X in a preadditive right-rigid monoidal category.