Characterization of projective objects in terms of lifting properties

An object P is projective iff the morphism 0 ⟶ P has the left lifting property with respect to epimorphisms, projective_iff_llp_epimorphisms_zero.

theorem CategoryTheory.Projective.hasLiftingProperty_of_isZero {C : Type u} [Category.{v, u} C] {Z P X Y : C} (i : Z ⟶ P) (p : X ⟶ Y) [Epi p] [Projective P] (hZ : Limits.IsZero Z) : HasLiftingProperty i p

instance CategoryTheory.Projective.instHasLiftingPropertyOfEpi {C : Type u} [Category.{v, u} C] {X Y P : C} (p : X ⟶ Y) [Epi p] [Projective P] [Limits.HasZeroObject C] (i : 0 ⟶ P) : HasLiftingProperty i p

theorem CategoryTheory.projective_iff_llp_epimorphisms_of_isZero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {P Z : C} (i : Z ⟶ P) (hZ : Limits.IsZero Z) : Projective P ↔ (MorphismProperty.epimorphisms C).llp i

theorem CategoryTheory.projective_iff_llp_epimorphisms_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] (P : C) : Projective P ↔ (MorphismProperty.epimorphisms C).llp 0