Documentation

Mathlib.CategoryTheory.Preadditive.Projective.Preserves

Preservation of projective objects #

We define a typeclass Functor.PreservesProjectiveObjects.

We restate the existing result that if F ⊣ G is an adjunction and G preserves monomorphisms, then F preserves projective objects. We show that the converse is true if the domain of F has enough projectives.

source
class CategoryTheory.Functor.PreservesProjectiveObjects {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
Prop

A functor preserves projective objects if it maps projective objects to projective objects.

Instances
    source
    instance CategoryTheory.Functor.projective_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.PreservesProjectiveObjects] (X : C) [Projective X] :
    Projective (F.obj X)

    See Functor.projective_obj_of_projective for a variant taking Projective X as an explicit argument.

    source
    theorem CategoryTheory.Functor.projective_obj_of_projective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.PreservesProjectiveObjects] {X : C} (h : Projective X) :
    Projective (F.obj X)

    See Functor.projective_obj for a variant taking Projective X as a typeclass argument.

    source
    instance CategoryTheory.Functor.preservesProjectiveObjects_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [F.PreservesProjectiveObjects] [G.PreservesProjectiveObjects] :
    (F.comp G).PreservesProjectiveObjects
    source
    theorem CategoryTheory.Functor.preservesProjectiveObjects_of_adjunction_of_preservesEpimorphisms {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] :
    F.PreservesProjectiveObjects
    source
    @[instance 100]
    instance CategoryTheory.Functor.preservesProjectiveObjects_of_isEquivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} [F.IsEquivalence] :
    F.PreservesProjectiveObjects
    source
    theorem CategoryTheory.Functor.preservesEpimorphisms_of_adjunction_of_preservesProjectiveObjects {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [EnoughProjectives C] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.PreservesProjectiveObjects] :
    G.PreservesEpimorphisms