Documentation

Mathlib.CategoryTheory.Preadditive.Injective.Preserves

Preservation of injective objects #

We define a typeclass Functor.PreservesInjectiveObjects.

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

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

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

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

    See Functor.injective_obj_of_injective for a variant taking Injective X as an explicit argument.

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

    See Functor.injective_obj for a variant taking Injective X as a typeclass argument.

    source
    instance CategoryTheory.Functor.preservesInjectiveObjects_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.PreservesInjectiveObjects] [G.PreservesInjectiveObjects] :
    (F.comp G).PreservesInjectiveObjects
    source
    theorem CategoryTheory.Functor.preservesInjectiveObjects_of_adjunction_of_preservesMonomorphisms {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.PreservesMonomorphisms] :
    G.PreservesInjectiveObjects
    source
    @[instance 100]
    instance CategoryTheory.Functor.preservesInjectiveObjects_of_isEquivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} [F.IsEquivalence] :
    F.PreservesInjectiveObjects
    source
    theorem CategoryTheory.Functor.preservesMonomorphisms_of_adjunction_of_preservesInjectiveObjects {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [EnoughInjectives D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [G.PreservesInjectiveObjects] :
    F.PreservesMonomorphisms