# 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.

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

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

@[class]
structure category_theory.projective {C : Type u} (P : C) :
Prop
• factors : ∀ {E X : C} (f : P X) (e : E X) [_inst_2 : , ∃ (f' : P E), f' e = f

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

Instances of this typeclass
@[nolint]
structure category_theory.projective_presentation {C : Type u} (X : C) :
Type (max u v)

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

Instances for category_theory.projective_presentation
• category_theory.projective_presentation.has_sizeof_inst
@[class]
structure category_theory.enough_projectives (C : Type u)  :
Prop
• 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 of this typeclass
noncomputable def category_theory.projective.factor_thru {C : Type u} {P X 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.

Equations
@[simp]
theorem category_theory.projective.factor_thru_comp {C : Type u} {P X E : C} (f : P X) (e : E X)  :
@[protected, instance]
theorem category_theory.projective.of_iso {C : Type u} {P Q : C} (i : P Q) (hP : category_theory.projective P) :
theorem category_theory.projective.iso_iff {C : Type u} {P Q : C} (i : P Q) :
@[protected, instance]

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

@[protected, instance]
@[protected, instance]
@[protected, instance]
def category_theory.projective.category_theory.limits.sigma_obj.projective {C : Type u} {β : Type v} (g : β → C) [∀ (b : β), ] :
@[protected, instance]
@[protected, instance]
def category_theory.projective.category_theory.limits.biproduct.projective {C : Type u} {β : Type v} (g : β → C) [∀ (b : β), ] :
noncomputable def category_theory.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.

Equations
Instances for category_theory.projective.over
@[protected, instance]
noncomputable def category_theory.projective.π {C : Type u} (X : C) :

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

Equations
Instances for category_theory.projective.π
@[protected, instance]
def category_theory.projective.π_epi {C : Type u} (X : C) :
@[protected, instance]
noncomputable def category_theory.projective.syzygies {C : Type u} {X 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.

Equations
Instances for category_theory.projective.syzygies
@[reducible]
noncomputable def category_theory.projective.d {C : Type u} {X 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.)

noncomputable def category_theory.exact.lift {C : Type u} {P Q R S : C} (h : P R) (f : Q R) (g : R S) (hfg : g) (w : h g = 0) :
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.

Equations
@[simp]
theorem category_theory.exact.lift_comp {C : Type u} {P Q R S : C} (h : P R) (f : Q R) (g : R S) (hfg : g) (w : h g = 0) :
hfg w f = h