# 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) :

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

• factors : ∀ {E X : C} (f : P X) (e : E X) [inst : ], ∃ (f' : P E),
Instances
theorem CategoryTheory.Projective.factors {C : Type u} {P : C} [self : ] {E : C} {X : C} (f : P X) (e : E X) :
∃ (f' : P E),
theorem CategoryTheory.Limits.IsZero.projective {C : Type u} {X : C} (h : ) :
structure CategoryTheory.ProjectivePresentation {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

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

• presentation : ∀ (X : C),
Instances
theorem CategoryTheory.EnoughProjectives.presentation {C : Type u} [self : ] (X : C) :
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.

Equations
• = .choose
Instances For
@[simp]
theorem CategoryTheory.Projective.factorThru_comp_assoc {C : Type u} {P : C} {X : C} {E : C} (f : P X) (e : E X) {Z : C} (h : X Z) :
@[simp]
theorem CategoryTheory.Projective.factorThru_comp {C : Type u} {P : C} {X : C} {E : C} (f : P X) (e : E X) :
Equations
• =
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.

Equations
• =
instance CategoryTheory.Projective.instCoprod {C : Type u} {P : C} {Q : C} :
Equations
• =
instance CategoryTheory.Projective.instSigmaObj {C : Type u} {β : Type v} (g : βC) [∀ (b : β), ] :
Equations
• =
instance CategoryTheory.Projective.instBiprod {C : Type u} {P : C} {Q : C} :
Equations
• =
instance CategoryTheory.Projective.instBiproduct {C : Type u} {β : Type v} (g : βC) [∀ (b : β), ] :
Equations
• =
theorem CategoryTheory.Projective.projective_iff_preservesEpimorphisms_coyoneda_obj {C : Type u} (P : C) :
(CategoryTheory.coyoneda.obj { unop := P }).PreservesEpimorphisms
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.

Equations
• = .some.p
Instances For
Equations
• =
def CategoryTheory.Projective.π {C : Type u} (X : C) :

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

Equations
• = .some.f
Instances For
instance CategoryTheory.Projective.π_epi {C : Type u} (X : C) :
Equations
• =
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.

Equations
Instances For
instance CategoryTheory.Projective.instSyzygies {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
• =
@[reducible, inline]
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.)

Equations
Instances For
theorem CategoryTheory.Adjunction.map_projective {C : Type u} {D : Type u'} [] {F : } {G : } (adj : F G) [G.PreservesEpimorphisms] (P : C) (hP : ) :
theorem CategoryTheory.Adjunction.projective_of_map_projective {C : Type u} {D : Type u'} [] {F : } {G : } (adj : F G) [F.Full] [F.Faithful] (P : C) (hP : CategoryTheory.Projective (F.obj P)) :
def CategoryTheory.Adjunction.mapProjectivePresentation {C : Type u} {D : Type u'} [] {F : } {G : } (adj : F G) [G.PreservesEpimorphisms] (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).

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

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

Equations
• One or more equations did not get rendered due to their size.
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 : ) :