mathlib documentation


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.

structure category_theory.projective_presentation {C : Type u} [category_theory.category C] (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.


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


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


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

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


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


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


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

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.