class IsSurjectiveFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C D) : Prop

A functor F : C ⥤ D is surjective when every object of D arises as a subquotient of some F.obj X.

• surj (Y : D) : ∃ (X : C) (A : D) (m : A ⟶ F.obj X) (e : A ⟶ Y), CategoryTheory.Mono m ∧ CategoryTheory.Epi e

class QuasiTensorFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (D : Type u₁) [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] : Type (max (max (max u u₁) v) v₁)

A quasi-tensor functor C ⥤ D between abelian monoidal categories: a faithful additive monoidal functor.

• F : CategoryTheory.Functor C D
• monoidal : F.Monoidal
• additive : F.Additive
• faithful : F.Faithful

class SurjectiveQuasiTensorFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (D : Type u₁) [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] extends QuasiTensorFunctor C D : Type (max (max (max u u₁) v) v₁)

A surjective quasi-tensor functor: a quasi-tensor functor whose underlying functor is surjective in the sense that every target object is a subquotient of an image.

• F : CategoryTheory.Functor C D
• monoidal : F.Monoidal
• additive : F.Additive
• faithful : F.Faithful
• surjective : IsSurjectiveFunctor QuasiTensorFunctor.F

class ProjectiveIsInjective (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : Prop

The property that every projective object is also injective; this characterises finite tensor categories, where projectives and injectives coincide.

• injective_of_projective (Q : C) : CategoryTheory.Projective Q → CategoryTheory.Injective Q

theorem projective_is_injective_in_finite_tensor_category {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [ProjectiveIsInjective D] (Q : D) (hQ : CategoryTheory.Projective Q) : CategoryTheory.Injective Q

In a category satisfying ProjectiveIsInjective, every projective object is injective.

theorem defect_dichotomy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.EnoughProjectives C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.RigidCategory D] [CategoryTheory.EnoughProjectives D] (QTF : SurjectiveQuasiTensorFunctor C D) [QuasiTensorFunctor.F.PreservesMonomorphisms] [QuasiTensorFunctor.F.PreservesEpimorphisms] : (∀ (P : C), CategoryTheory.Projective P → CategoryTheory.Projective (QuasiTensorFunctor.F.obj P)) ∨ ∀ (P : C), CategoryTheory.Projective P → ∀ (Q : D), CategoryTheory.Projective Q → ¬CategoryTheory.Limits.IsZero Q → ¬∃ (i : Q ⟶ QuasiTensorFunctor.F.obj P) (r : QuasiTensorFunctor.F.obj P ⟶ Q), CategoryTheory.CategoryStruct.comp i r = CategoryTheory.CategoryStruct.id Q

Defect dichotomy for surjective quasi-tensor functors between finite tensor categories: either every image of a projective is projective, or no projective object in the source maps to a nonzero projective summand in the target.

theorem isZero_of_no_nonzero_projective {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Abelian D] [CategoryTheory.EnoughProjectives D] (h : ∀ (Q : D), CategoryTheory.Projective Q → CategoryTheory.Limits.IsZero Q) (X : D) : CategoryTheory.Limits.IsZero X

In an abelian category with enough projectives, if every projective object is zero then every object is zero.