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

If X is a nonzero object of a right-rigid preadditive monoidal category, the coevaluation morphism η_ X Xᘁ : 𝟙_ C ⟶ X ⊗ Xᘁ is nonzero.

theorem TensorCategories.isIso_of_epi_of_simple_src {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} [CategoryTheory.Simple X] (f : X ⟶ Y) [CategoryTheory.Epi f] (hf : f ≠ 0) : CategoryTheory.IsIso f

A nonzero epimorphism out of a simple object in an abelian category is an isomorphism, since its kernel is either zero or all of X.

theorem TensorCategories.rightAdjointMate_epi_of_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RightRigidCategory C] [CategoryTheory.LeftRigidCategory C] [CategoryTheory.MonoidalPreadditive C] {X : C} (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) [CategoryTheory.Mono f] : CategoryTheory.Epi (fᘁ)

In a rigid abelian monoidal preadditive category, if f : X ⟶ 𝟙_ C is a monomorphism then its right adjoint mate Xᘁ ⟶ 𝟙_ C is an epimorphism.

theorem TensorCategories.whiskerLeft_epi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.LeftRigidCategory C] [CategoryTheory.MonoidalPreadditive C] {Y Z : C} (f : Y ⟶ Z) [CategoryTheory.Epi f] (W : C) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W f)

Left whiskering by any object preserves epimorphisms in a left-rigid abelian monoidal preadditive category (Proposition 1.13.1 for left exactness on the left).

theorem TensorCategories.whiskerLeft_rightAdjointMate_epi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RightRigidCategory C] [CategoryTheory.LeftRigidCategory C] [CategoryTheory.MonoidalPreadditive C] {X : C} (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) [CategoryTheory.Mono f] : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (fᘁ))

Left whiskering the right adjoint mate of a mono f : X ⟶ 𝟙_ C by X yields an epimorphism.

theorem TensorCategories.exists_epi_to_tensor_dual {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RightRigidCategory C] [CategoryTheory.LeftRigidCategory C] [CategoryTheory.MonoidalPreadditive C] {X : C} [CategoryTheory.Simple X] (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) [CategoryTheory.Mono f] (hf : f ≠ 0) : ∃ (e : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Xᘁ), CategoryTheory.Epi e ∧ e ≠ 0

If X is simple and f : X ⟶ 𝟙_ C is a nonzero monomorphism, there exists a nonzero epimorphism X ⟶ X ⊗ Xᘁ, obtained from ρ⁻¹ composed with whiskering of the mate of f.

theorem TensorCategories.simple_subobj_unit_retraction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RightRigidCategory C] [CategoryTheory.LeftRigidCategory C] [CategoryTheory.MonoidalPreadditive C] {X : C} [CategoryTheory.Simple X] (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) [CategoryTheory.Mono f] (hf : f ≠ 0) : ∃ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X), g ≠ 0

If X is a simple subobject of the unit (via a nonzero mono f : X ⟶ 𝟙_ C), then there exists a nonzero morphism 𝟙_ C ⟶ X. This produces a candidate retraction of f after passing through End(𝟙).

theorem TensorCategories.exists_simple_subobject {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : C) [CategoryTheory.IsArtinianObject X] (hX : ¬CategoryTheory.Limits.IsZero X) : ∃ (S : C) (_ : CategoryTheory.Simple S) (i : S ⟶ X), CategoryTheory.Mono i ∧ i ≠ 0

Any nonzero Artinian object in an abelian category contains a simple subobject, realized as a nonzero monomorphism S ⟶ X with S simple.

theorem TensorCategories.endUnit_isIso_of_ne_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] (hEnd : ∀ (g : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)), g ≠ 0 → IsUnit g) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (hf : f ≠ 0) : CategoryTheory.IsIso f

Given that every nonzero endomorphism of 𝟙_ C is a unit in End(𝟙_ C), any nonzero endomorphism of the unit is an isomorphism.

theorem TensorCategories.commSemisimpleRing_noNontrivialIdempotents_isUnit (R : Type u_1) [CommRing R] [IsSemisimpleRing R] (htriv : ∀ (e : R), IsIdempotentElem e → e = 0 ∨ e = 1) (g : R) : g ≠ 0 → IsUnit g

A commutative semisimple ring with no nontrivial idempotents is a field, so every nonzero element is a unit. The proof uses the Wedderburn-Artin decomposition into matrix algebras over division rings and rules out factors via idempotents.

theorem TensorCategories.endUnit_trivialIdempotents {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (hIndecomp : CategoryTheory.Indecomposable (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (e : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (he : IsIdempotentElem e) : e = 0 ∨ e = 1

If the unit object is indecomposable, then every idempotent in End(𝟙_ C) is either 0 or 1 (i.e. there are no nontrivial idempotents).

theorem TensorCategories.endUnit_isUnit_of_ne_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [MonoidalBiexact C] [IsArtinianRing (CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))] (hIndecomp : CategoryTheory.Indecomposable (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (g : CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (hg : g ≠ 0) : IsUnit g

Combining semisimplicity of End(𝟙_ C) with indecomposability of the unit, every nonzero endomorphism of the unit object is a unit.

theorem TensorCategories.unitIsSimple (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RightRigidCategory C] [CategoryTheory.LeftRigidCategory C] [CategoryTheory.MonoidalPreadditive C] [MonoidalBiexact C] [IsArtinianRing (CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))] [CategoryTheory.IsArtinianObject (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] (hIndecomp : CategoryTheory.Indecomposable (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) : CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

Theorem 1.15.8 (i): In a ring category with right duals (here modeled by the rigid abelian monoidally biexact setting), the unit object 𝟙_ C is simple.

instance TensorCategories.instSimpleUnitOfUnitIsSimple (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RightRigidCategory C] [CategoryTheory.LeftRigidCategory C] [CategoryTheory.MonoidalPreadditive C] [MonoidalBiexact C] [IsArtinianRing (CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))] [CategoryTheory.IsArtinianObject (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] (hIndecomp : CategoryTheory.Indecomposable (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) : CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

Instance form of unitIsSimple, registering simplicity of 𝟙_ C for typeclass inference whenever an indecomposability hypothesis is supplied.