def CategoryTheory.IsRetractOf {C : Type u} [Category.{v, u} C] (Q Y : C) : Prop

Q is a retract of Y in C when there exist morphisms i : Q ⟶ Y and r : Y ⟶ Q with i ≫ r = 𝟙 Q.

theorem CategoryTheory.Projective.of_retract_categorical {C : Type u} [Category.{v, u} C] {Q Y : C} (i : Q ⟶ Y) (r : Y ⟶ Q) (hir : CategoryStruct.comp i r = CategoryStruct.id Q) [hY : Projective Y] : Projective Q

A retract of a projective object is projective.

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

A category satisfies ProjectiveIsInjective when every projective object is also injective.

• injective_of_projective (P : C) : Projective P → Injective P

instance CategoryTheory.projectiveIsInjective_of_rigid (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] [Abelian C] [Injective (MonoidalCategoryStruct.tensorUnit C)] : ProjectiveIsInjective C

In a rigid abelian monoidal category whose unit object is injective, every projective object is injective.

@[instance 100]

instance CategoryTheory.hasProjectiveImpliesInjective_of_rigid (C : Type u) [Category.{v, u} C] [ProjectiveIsInjective C] : HasProjectiveImpliesInjective C

Any category satisfying ProjectiveIsInjective automatically satisfies the mathlib HasProjectiveImpliesInjective typeclass.

instance CategoryTheory.injectiveIsProjective_of_rigid (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] [Abelian C] [Projective (MonoidalCategoryStruct.tensorUnit C)] (I : C) : Injective I → Projective I

In a rigid abelian monoidal category whose unit object is projective, every injective object is projective.

instance CategoryTheory.quasiFrobeniusProperty_of_rigid (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] [Abelian C] [Injective (MonoidalCategoryStruct.tensorUnit C)] [Projective (MonoidalCategoryStruct.tensorUnit C)] : ExactModuleCategory.QuasiFrobeniusProperty C

A rigid abelian monoidal category whose unit is both projective and injective satisfies the quasi-Frobenius property: projectives coincide with injectives.

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

The monoidal category C has a nonzero unit object.

• unit_nonzero : ¬Limits.IsZero (MonoidalCategoryStruct.tensorUnit C)

instance CategoryTheory.hasNonZeroUnit_of_nontrivial_endUnit (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [h : Nontrivial (End (MonoidalCategoryStruct.tensorUnit C))] : HasNonZeroUnit C

If End(𝟙_ C) is nontrivial then the unit object of C is nonzero.

theorem CategoryTheory.exists_nonzero_projective {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] [EnoughProjectives C] [HasNonZeroUnit C] : ∃ (Q : C), Projective Q ∧ ¬Limits.IsZero Q

An abelian monoidal category with enough projectives and a nonzero unit object admits a nonzero projective object: the projective cover of the unit.

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

A functor F : C ⥤ D is surjective (in the sense used here) if every object of D is a subquotient of some F.obj X: there exist a monomorphism into F.obj X and an epimorphism onto Y sharing a common source.

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

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

A quasi-tensor functor between abelian monoidal categories, packaged here as a class: an additive monoidal functor preserving monomorphisms and epimorphisms.

• F : Functor C D
• monoidal : (F k).Monoidal
• additive : (F k).Additive
• preservesMono : (F k).PreservesMonomorphisms
• preservesEpi : (F k).PreservesEpimorphisms

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

A surjective quasi-tensor functor is one whose underlying functor is surjective.

• F : Functor C D
• monoidal : (F k).Monoidal
• additive : (F k).Additive
• preservesMono : (F k).PreservesMonomorphisms
• preservesEpi : (F k).PreservesEpimorphisms
• surjective : (QuasiTensorFunctor.F k).IsSurjective

theorem CategoryTheory.covers_proj_by_proj {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] [EnoughProjectives C] {D : Type u₁} [Category.{v₁, u₁} D] [MonoidalCategory D] [Abelian D] [ProjectiveIsInjective D] (QTF : SurjectiveQuasiTensorFunctor k C D) (Q : D) (hQ_proj : Projective Q) (_hQ_nz : ¬Limits.IsZero Q) : ∃ (P : C), Projective P ∧ IsRetractOf Q ((QuasiTensorFunctor.F k).obj P)

Given a surjective quasi-tensor functor QTF, every nonzero projective object Q of the target is a retract of the image QTF.F.obj P of some projective P in the source.

theorem CategoryTheory.defectDichotomy {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] {D : Type u₁} [Category.{v₁, u₁} D] [MonoidalCategory D] [Abelian D] (QTF : SurjectiveQuasiTensorFunctor k C D) : (∀ (P : C), Projective P → Projective ((QuasiTensorFunctor.F k).obj P)) ∨ ∀ (P : C), Projective P → ∀ (Q : D), Projective Q → ¬Limits.IsZero Q → ¬IsRetractOf Q ((QuasiTensorFunctor.F k).obj P)

Defect dichotomy: for a surjective quasi-tensor functor QTF, either it preserves projectives, or no nonzero projective in the target is a retract of any QTF.F.obj P for P projective.

theorem CategoryTheory.defectDichotomy_not_right {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] [EnoughProjectives C] {D : Type u₁} [Category.{v₁, u₁} D] [MonoidalCategory D] [Abelian D] [ProjectiveIsInjective D] (QTF : SurjectiveQuasiTensorFunctor k C D) (hD_nontrivial : ∃ (Q : D), Projective Q ∧ ¬Limits.IsZero Q) : ¬∀ (P : C), Projective P → ∀ (Q : D), Projective Q → ¬Limits.IsZero Q → ¬IsRetractOf Q ((QuasiTensorFunctor.F k).obj P)

The second alternative of the defect dichotomy is impossible when the target contains a nonzero projective: this follows from covers_proj_by_proj.

theorem CategoryTheory.surjective_quasi_tensor_preserves_projective {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] [EnoughProjectives C] {D : Type u₁} [Category.{v₁, u₁} D] [MonoidalCategory D] [Abelian D] [ProjectiveIsInjective D] (QTF : SurjectiveQuasiTensorFunctor k C D) (hD_nontrivial : ∃ (Q : D), Projective Q ∧ ¬Limits.IsZero Q) (P : C) (hP : Projective P) : Projective ((QuasiTensorFunctor.F k).obj P)

A surjective quasi-tensor functor into a target category with a nonzero projective object (and where projectives are injective) preserves projectives.