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} [Category.{v, u} C] (P : C) : Prop

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) [Epi e] : ∃ (f' : P ⟶ E), CategoryStruct.comp f' e = f

theorem CategoryTheory.Limits.IsZero.projective {C : Type u} [Category.{v, u} C] {X : C} (h : IsZero X) : Projective X

structure CategoryTheory.ProjectivePresentation {C : Type u} [Category.{v, u} 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.

• p : C
• projective : Projective self.p
• f : self.p ⟶ X
• epi : Epi self.f

class CategoryTheory.EnoughProjectives (C : Type u) [Category.{v, u} C] : Prop

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

• presentation (X : C) : Nonempty (ProjectivePresentation X)

def CategoryTheory.Projective.factorThru {C : Type u} [Category.{v, u} C] {P X E : C} [Projective P] (f : P ⟶ X) (e : E ⟶ X) [Epi e] : P ⟶ E

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

Equations

• CategoryTheory.Projective.factorThru f e = ⋯.choose

@[simp]

theorem CategoryTheory.Projective.factorThru_comp {C : Type u} [Category.{v, u} C] {P X E : C} [Projective P] (f : P ⟶ X) (e : E ⟶ X) [Epi e] : CategoryStruct.comp (factorThru f e) e = f

@[simp]

theorem CategoryTheory.Projective.factorThru_comp_assoc {C : Type u} [Category.{v, u} C] {P X E : C} [Projective P] (f : P ⟶ X) (e : E ⟶ X) [Epi e] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (factorThru f e) (CategoryStruct.comp e h) = CategoryStruct.comp f h

instance CategoryTheory.Projective.zero_projective {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] : Projective 0

theorem CategoryTheory.Projective.of_iso {C : Type u} [Category.{v, u} C] {P Q : C} (i : P ≅ Q) : Projective P → Projective Q

theorem CategoryTheory.Projective.iso_iff {C : Type u} [Category.{v, u} C] {P Q : C} (i : P ≅ Q) : Projective P ↔ Projective Q

instance CategoryTheory.Projective.inst (X : Type u) : Projective X

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

instance CategoryTheory.Projective.Type.enoughProjectives : EnoughProjectives (Type u)

instance CategoryTheory.Projective.instCoprod {C : Type u} [Category.{v, u} C] {P Q : C} [Limits.HasBinaryCoproduct P Q] [Projective P] [Projective Q] : Projective (P ⨿ Q)

instance CategoryTheory.Projective.instSigmaObj {C : Type u} [Category.{v, u} C] {β : Type v} (g : β → C) [Limits.HasCoproduct g] [∀ (b : β), Projective (g b)] : Projective (∐ g)

instance CategoryTheory.Projective.instBiprod {C : Type u} [Category.{v, u} C] {P Q : C} [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproduct P Q] [Projective P] [Projective Q] : Projective (P ⊞ Q)

instance CategoryTheory.Projective.instBiproduct {C : Type u} [Category.{v, u} C] {β : Type v} (g : β → C) [Limits.HasZeroMorphisms C] [Limits.HasBiproduct g] [∀ (b : β), Projective (g b)] : Projective (⨁ g)

theorem CategoryTheory.Projective.projective_iff_preservesEpimorphisms_coyoneda_obj {C : Type u} [Category.{v, u} C] (P : C) : Projective P ↔ (coyoneda.obj (Opposite.op P)).PreservesEpimorphisms

def CategoryTheory.Projective.over {C : Type u} [Category.{v, u} C] [EnoughProjectives C] (X : C) : C

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

Equations

• CategoryTheory.Projective.over X = ⋯.some.p

instance CategoryTheory.Projective.projective_over {C : Type u} [Category.{v, u} C] [EnoughProjectives C] (X : C) : Projective (over X)

def CategoryTheory.Projective.π {C : Type u} [Category.{v, u} C] [EnoughProjectives C] (X : C) : over X ⟶ X

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

Equations

• CategoryTheory.Projective.π X = ⋯.some.f

instance CategoryTheory.Projective.π_epi {C : Type u} [Category.{v, u} C] [EnoughProjectives C] (X : C) : Epi (π X)

def CategoryTheory.Projective.syzygies {C : Type u} [Category.{v, u} C] [EnoughProjectives C] [Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Limits.HasKernel f] : C

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

Equations

• CategoryTheory.Projective.syzygies f = CategoryTheory.Projective.over (CategoryTheory.Limits.kernel f)

instance CategoryTheory.Projective.instSyzygies {C : Type u} [Category.{v, u} C] [EnoughProjectives C] [Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Limits.HasKernel f] : Projective (syzygies f)

@[reducible, inline]

abbrev CategoryTheory.Projective.d {C : Type u} [Category.{v, u} C] [EnoughProjectives C] [Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Limits.HasKernel f] : syzygies f ⟶ X

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

• CategoryTheory.Projective.d f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.π (CategoryTheory.Limits.kernel f)) (CategoryTheory.Limits.kernel.ι f)

theorem CategoryTheory.Adjunction.map_projective {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [G.PreservesEpimorphisms] (P : C) (hP : Projective P) : Projective (F.obj P)

theorem CategoryTheory.Adjunction.projective_of_map_projective {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.Full] [F.Faithful] (P : C) (hP : Projective (F.obj P)) : Projective P

def CategoryTheory.Adjunction.mapProjectivePresentation {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [G.PreservesEpimorphisms] (X : C) (Y : ProjectivePresentation X) : ProjectivePresentation (F.obj X)

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

• adj.mapProjectivePresentation X Y = CategoryTheory.ProjectivePresentation.mk (F.obj Y.p) (F.map Y.f)

theorem CategoryTheory.Equivalence.map_projective_iff {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : C ≌ D) (P : C) : Projective (F.functor.obj P) ↔ Projective P

def CategoryTheory.Equivalence.projectivePresentationOfMapProjectivePresentation {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : C ≌ D) (X : C) (Y : ProjectivePresentation (F.functor.obj X)) : ProjectivePresentation X

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

Equations

• F.projectivePresentationOfMapProjectivePresentation X Y = CategoryTheory.ProjectivePresentation.mk (F.inverse.obj Y.p) (CategoryTheory.CategoryStruct.comp (F.inverse.map Y.f) (F.unitInv.app X))

theorem CategoryTheory.Equivalence.enoughProjectives_iff {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : C ≌ D) : EnoughProjectives C ↔ EnoughProjectives D