# Projective objects and categories with enough projectives #

An object P is called projective if every morphism out of P factors through every epimorphism.

A category C has enough projectives if every object admits an epimorphism from some projective object.

CategoryTheory.Projective.over X picks an arbitrary such projective object, and CategoryTheory.Projective.π X : CategoryTheory.Projective.over X ⟶ X is the corresponding epimorphism.

Given a morphism f : X ⟶ Y, CategoryTheory.Projective.left f is a projective object over CategoryTheory.Limits.kernel f, and projective.d f : projective.left f ⟶ X is the morphism π (kernel f) ≫ kernel.ι f.

class CategoryTheory.Projective {C : Type u} (P : C) :
• factors : ∀ {E X : C} (f : P X) (e : E X) [inst : ], f',

An object P is called projective if every morphism out of P factors through every epimorphism.

Instances
structure CategoryTheory.ProjectivePresentation {C : Type u} (X : C) :
Type (max u v)
• p : C
• projective :
• f : s.p X
• epi :

A projective presentation of an object X consists of an epimorphism f : P ⟶ X from some projective object P.

Instances For
• presentation : ∀ (X : C),

A category "has enough projectives" if for every object X there is a projective object P and an epimorphism P ↠ X.

Instances
def CategoryTheory.Projective.factorThru {C : Type u} {P : C} {X : C} {E : C} (f : P X) (e : E X) :
P E

An arbitrarily chosen factorisation of a morphism out of a projective object through an epimorphism.

Instances For
@[simp]
theorem CategoryTheory.Projective.factorThru_comp {C : Type u} {P : C} {X : C} {E : C} (f : P X) (e : E X) :
theorem CategoryTheory.Projective.of_iso {C : Type u} {P : C} {Q : C} (i : P Q) (hP : ) :
theorem CategoryTheory.Projective.iso_iff {C : Type u} {P : C} {Q : C} (i : P Q) :

The axiom of choice says that every type is a projective object in Type.

instance CategoryTheory.Projective.instProjectiveSigmaObj {C : Type u} {β : Type v} (g : βC) [∀ (b : β), ] :
instance CategoryTheory.Projective.instProjectiveBiproduct {C : Type u} {β : Type v} (g : βC) [∀ (b : β), ] :
def CategoryTheory.Projective.over {C : Type u} (X : C) :
C

Projective.over X provides an arbitrarily chosen projective object equipped with an epimorphism Projective.π : Projective.over X ⟶ X.

Instances For
def CategoryTheory.Projective.π {C : Type u} (X : C) :

The epimorphism projective.π : projective.over X ⟶ X from the arbitrarily chosen projective object over X.

Instances For
instance CategoryTheory.Projective.π_epi {C : Type u} (X : C) :
def CategoryTheory.Projective.syzygies {C : Type u} {X : C} {Y : C} (f : X Y) :
C

When C has enough projectives, the object projective.syzygies f is an arbitrarily chosen projective object over kernel f.

Instances For
instance CategoryTheory.Projective.instProjectiveSyzygies {C : Type u} {X : C} {Y : C} (f : X Y) :
@[inline, reducible]
abbrev CategoryTheory.Projective.d {C : Type u} {X : C} {Y : C} (f : X Y) :

When C has enough projectives, projective.d f : projective.syzygies f ⟶ X is the composition π (kernel f) ≫ kernel.ι f.

(When C is abelian, we have exact (projective.d f) f.)

Instances For
theorem CategoryTheory.Adjunction.map_projective {C : Type u} {D : Type u'} [] {F : } {G : } (adj : F G) (P : C) (hP : ) :
theorem CategoryTheory.Adjunction.projective_of_map_projective {C : Type u} {D : Type u'} [] {F : } {G : } (adj : F G) (P : C) (hP : CategoryTheory.Projective (F.obj P)) :
def CategoryTheory.Adjunction.mapProjectivePresentation {C : Type u} {D : Type u'} [] {F : } {G : } (adj : F G) (X : C) :

Given an adjunction F ⊣ G such that G preserves epis, F maps a projective presentation of X to a projective presentation of F(X).

Instances For
theorem CategoryTheory.Equivalence.map_projective_iff {C : Type u} {D : Type u'} [] (F : C D) (P : C) :
CategoryTheory.Projective (F.functor.obj P)

Given an equivalence of categories F, a projective presentation of F(X) induces a projective presentation of X.

Instances For
def CategoryTheory.Exact.lift {C : Type u} {P : C} {Q : C} {R : C} {S : C} (h : P R) (f : Q R) (g : R S) (hfg : ) (w : ) :
P Q

Given a projective object P mapping via h into the middle object R of a pair of exact morphisms f : Q ⟶ R and g : R ⟶ S, such that h ≫ g = 0, there is a lift of h to Q.

Instances For
@[simp]
theorem CategoryTheory.Exact.lift_comp {C : Type u} {P : C} {Q : C} {R : C} {S : C} (h : P R) (f : Q R) (g : R S) (hfg : ) (w : ) :