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.

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.

• injective_obj {X : C} : Injective X → Injective (F.obj X)

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.

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.

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

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

@[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

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