Documentation

Mathlib.CategoryTheory.Preadditive.Projective

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.

theorem CategoryTheory.Projective.factors {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} [self : CategoryTheory.Projective P] {E : C} {X : C} (f : P X) (e : E X) [CategoryTheory.Epi e] :

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

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

Equations

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

Equations
  • =

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

Equations
Instances For

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

Equations
Instances For

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

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

Equations