Endomorphisms of the unit object of a monoidal category commute (Proposition 1.2.7). The proof uses coherence to identify the left and right unitors of the unit object.
The monoid End(𝟙_ C) of endomorphisms of the unit object of a monoidal category is
commutative, packaged as a CommMonoid instance (Proposition 1.2.7).
In a preadditive monoidal category, the endomorphism ring of the unit object is
commutative; this upgrades the ring structure on End(𝟙_ C) to a CommRing.
If an endomorphism f of the unit object squares to zero under composition,
then its tensor square f ⊗ₘ f is the zero morphism.
A monoidal abelian category is monoidally biexact if tensoring on either side
preserves monomorphisms and epimorphisms, and if X ⊗ X being zero forces X to be zero.
This abstracts Proposition 1.13.1 together with the nondegeneracy needed for the proof
that End(𝟙) is reduced.
- whiskerRight_mono {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] (Z : C) : CategoryTheory.Mono (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
- whiskerLeft_mono (Z : C) {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Mono (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)
- whiskerRight_epi {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] (Z : C) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
- whiskerLeft_epi (Z : C) {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)
- isZero_of_tensorObj_self_isZero (X : C) : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj X X) → CategoryTheory.Limits.IsZero X
Instances
Right tensoring by an object preserves zero morphisms in a monoidal preadditive
category, supplying the PreservesZeroMorphisms instance for tensorRight.
Left tensoring by an object preserves zero morphisms in a monoidal preadditive
category, supplying the PreservesZeroMorphisms instance for tensorLeft.
In an abelian braided rigid monoidal category, if X ⊗ X is the zero object then
X itself is zero. The argument uses the zig-zag identity and duals to show that the
left unitor of X vanishes.
Any abelian rigid monoidal preadditive braided category is monoidally biexact. The proof uses duality adjunctions to deduce that left/right tensoring preserves monomorphisms and epimorphisms, and combines this with the nondegeneracy lemma above.
In a monoidally biexact abelian category, the tensor product of two monomorphisms is a monomorphism.
In a monoidally biexact abelian category, the tensor product of two epimorphisms is an epimorphism.
If an epi e : A ⟶ B followed by a mono m : B ⟶ D is the zero morphism, then
the intermediate object B is zero.
In a monoidally biexact abelian category, if f ⊗ₘ f = 0 for an endomorphism f
of the unit, then f = 0. The proof factors f through its abelian image and uses
biexactness to conclude the image is zero.
A monoid-with-zero in which every square-zero element is zero is reduced (has no nonzero nilpotent elements). The proof uses strong induction to reduce nilpotency to the square-zero case.
In a monoidally biexact abelian monoidal category, the endomorphism ring of the unit object is reduced.
Under the standing assumptions (monoidally biexact, Artinian endomorphism ring),
the commutative ring End(𝟙_ C) is semisimple.
Theorem 1.15.1: in any multiring category, End(𝟙) is a semisimple algebra.
This formalization specializes to abelian monoidally biexact categories with an
Artinian endomorphism ring on the unit.