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

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

structure CategoryTheory.ProjectivePresentation {C : Type u} [CategoryTheory.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 : CategoryTheory.Projective self.p
• f : self.p ⟶ X
• epi : CategoryTheory.Epi self.f

theorem CategoryTheory.ProjectivePresentation.projective {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (self : CategoryTheory.ProjectivePresentation X) : CategoryTheory.Projective self.p

theorem CategoryTheory.ProjectivePresentation.epi {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (self : CategoryTheory.ProjectivePresentation X) : CategoryTheory.Epi self.f

class CategoryTheory.EnoughProjectives (C : Type u) [CategoryTheory.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 (CategoryTheory.ProjectivePresentation X)

theorem CategoryTheory.EnoughProjectives.presentation {C : Type u} [CategoryTheory.Category.{v, u} C] [self : CategoryTheory.EnoughProjectives C] (X : C) : Nonempty (CategoryTheory.ProjectivePresentation X)

def CategoryTheory.Projective.factorThru {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {X : C} {E : C} [CategoryTheory.Projective P] (f : P ⟶ X) (e : E ⟶ X) [CategoryTheory.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_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {X : C} {E : C} [CategoryTheory.Projective P] (f : P ⟶ X) (e : E ⟶ X) [CategoryTheory.Epi e] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.factorThru f e) (CategoryTheory.CategoryStruct.comp e h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

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

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

Equations

• ⋯ = ⋯

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

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.Projective.Type.enoughProjectives = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

def CategoryTheory.Projective.over {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnoughProjectives C] (X : C) : CategoryTheory.Projective (CategoryTheory.Projective.over X)

Equations

• ⋯ = ⋯

def CategoryTheory.Projective.π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnoughProjectives C] (X : C) : CategoryTheory.Projective.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnoughProjectives C] (X : C) : CategoryTheory.Epi (CategoryTheory.Projective.π X)

Equations

• ⋯ = ⋯

def CategoryTheory.Projective.syzygies {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnoughProjectives C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnoughProjectives C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] : CategoryTheory.Projective (CategoryTheory.Projective.syzygies f)

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.Projective.d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnoughProjectives C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] : CategoryTheory.Projective.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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [G.PreservesEpimorphisms] (P : C) (hP : CategoryTheory.Projective P) : CategoryTheory.Projective (F.obj P)

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

def CategoryTheory.Adjunction.mapProjectivePresentation {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [G.PreservesEpimorphisms] (X : C) (Y : CategoryTheory.ProjectivePresentation X) : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : C ≌ D) (P : C) : CategoryTheory.Projective (F.functor.obj P) ↔ CategoryTheory.Projective P

def CategoryTheory.Equivalence.projectivePresentationOfMapProjectivePresentation {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : C ≌ D) (X : C) (Y : CategoryTheory.ProjectivePresentation (F.functor.obj X)) : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : C ≌ D) : CategoryTheory.EnoughProjectives C ↔ CategoryTheory.EnoughProjectives D