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.

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

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

    Instances For

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

      Instances

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

        Equations
        Instances For

          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
              @[reducible, inline]

              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

                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

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

                  Equations
                  Instances For