Injective objects and categories with enough injectives

An object J is injective iff every morphism into J can be obtained by extending a monomorphism.

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

An object J is injective iff every morphism into J can be obtained by extending a monomorphism.

• factors {X Y : C} (g : X ⟶ J) (f : X ⟶ Y) [Mono f] : ∃ (h : Y ⟶ J), CategoryStruct.comp f h = g

  An object J is injective iff every morphism into J can be obtained by extending a monomorphism.

@[reducible, inline]

abbrev CategoryTheory.isInjective (C : Type u₁) [Category.{v₁, u₁} C] : ObjectProperty C

The ObjectProperty C corresponding to the notion of injective objects in C.

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

structure CategoryTheory.InjectivePresentation {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : Type (max u₁ v₁)

An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

• J : C

  An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

• injective : Injective self.J

  An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

• f : X ⟶ self.J

  An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

• mono : Mono self.f

  An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

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

A category "has enough injectives" if every object has an injective presentation, i.e. if for every object X there is an injective object J and a monomorphism X ↪ J.

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

  A category "has enough injectives" if every object has an injective presentation, i.e. if for every object X there is an injective object J and a monomorphism X ↪ J.

noncomputable def CategoryTheory.Injective.factorThru {C : Type u₁} [Category.{v₁, u₁} C] {J X Y : C} [Injective J] (g : X ⟶ J) (f : X ⟶ Y) [Mono f] : Y ⟶ J

Let J be injective and g a morphism into J, then g can be factored through any monomorphism.

@[simp]

theorem CategoryTheory.Injective.comp_factorThru {C : Type u₁} [Category.{v₁, u₁} C] {J X Y : C} [Injective J] (g : X ⟶ J) (f : X ⟶ Y) [Mono f] : CategoryStruct.comp f (factorThru g f) = g

@[simp]

theorem CategoryTheory.Injective.comp_factorThru_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J X Y : C} [Injective J] (g : X ⟶ J) (f : X ⟶ Y) [Mono f] {Z : C} (h : J ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (factorThru g f) h) = CategoryStruct.comp g h

instance CategoryTheory.Injective.zero_injective {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] : Injective 0

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

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

instance CategoryTheory.Injective.instOfNonempty (X : Type u₁) [Nonempty X] : Injective X

The axiom of choice says that every nonempty type is an injective object in Type.

instance CategoryTheory.Injective.Type.enoughInjectives : EnoughInjectives (Type u₁)

instance CategoryTheory.Injective.instProd {C : Type u₁} [Category.{v₁, u₁} C] {P Q : C} [Limits.HasBinaryProduct P Q] [Injective P] [Injective Q] : Injective (P ⨯ Q)

instance CategoryTheory.Injective.instPiObj {C : Type u₁} [Category.{v₁, u₁} C] {β : Type v} (c : β → C) [Limits.HasProduct c] [∀ (b : β), Injective (c b)] : Injective (∏ᶜ c)

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

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

instance CategoryTheory.Injective.instUnopOfProjectiveOpposite {C : Type u₁} [Category.{v₁, u₁} C] {P : Cᵒᵖ} [Projective P] : Injective (Opposite.unop P)

instance CategoryTheory.Injective.instProjectiveUnopOfOpposite {C : Type u₁} [Category.{v₁, u₁} C] {J : Cᵒᵖ} [Injective J] : Projective (Opposite.unop J)

instance CategoryTheory.Injective.instProjectiveOppositeOp {C : Type u₁} [Category.{v₁, u₁} C] {J : C} [Injective J] : Projective (Opposite.op J)

instance CategoryTheory.Injective.instOppositeOpOfProjective {C : Type u₁} [Category.{v₁, u₁} C] {P : C} [Projective P] : Injective (Opposite.op P)

theorem CategoryTheory.Injective.injective_iff_projective_op {C : Type u₁} [Category.{v₁, u₁} C] {J : C} : Injective J ↔ Projective (Opposite.op J)

theorem CategoryTheory.Injective.projective_iff_injective_op {C : Type u₁} [Category.{v₁, u₁} C] {P : C} : Projective P ↔ Injective (Opposite.op P)

theorem CategoryTheory.Injective.injective_iff_preservesEpimorphisms_yoneda_obj {C : Type u₁} [Category.{v₁, u₁} C] (J : C) : Injective J ↔ (yoneda.obj J).PreservesEpimorphisms

theorem CategoryTheory.Injective.injective_of_adjoint {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} [L.PreservesMonomorphisms] (adj : L ⊣ R) (J : D) [Injective J] : Injective (R.obj J)

theorem CategoryTheory.Injective.exists_presentation {C : Type u₁} [Category.{v₁, u₁} C] [EnoughInjectives C] (X : C) : ∃ (p : InjectivePresentation X), Limits.IsZero X → Limits.IsZero p.J

If C has enough injectives, we may choose an injective presentation of X : C which is given by a zero object when X is a zero object.

noncomputable def CategoryTheory.Injective.under {C : Type u₁} [Category.{v₁, u₁} C] [EnoughInjectives C] (X : C) : C

Injective.under X provides an arbitrarily chosen injective object equipped with a monomorphism Injective.ι : X ⟶ Injective.under X.

instance CategoryTheory.Injective.injective_under {C : Type u₁} [Category.{v₁, u₁} C] [EnoughInjectives C] (X : C) : Injective (under X)

noncomputable def CategoryTheory.Injective.ι {C : Type u₁} [Category.{v₁, u₁} C] [EnoughInjectives C] (X : C) : X ⟶ under X

The monomorphism Injective.ι : X ⟶ Injective.under X from the arbitrarily chosen injective object under X.

instance CategoryTheory.Injective.ι_mono {C : Type u₁} [Category.{v₁, u₁} C] [EnoughInjectives C] (X : C) : Mono (ι X)

theorem CategoryTheory.Injective.isZero_under {C : Type u₁} [Category.{v₁, u₁} C] [EnoughInjectives C] (X : C) (hX : Limits.IsZero X) : Limits.IsZero (under X)

noncomputable def CategoryTheory.Injective.syzygies {C : Type u₁} [Category.{v₁, u₁} C] [EnoughInjectives C] [Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Limits.HasCokernel f] : C

When C has enough injectives, the object Injective.syzygies f is an arbitrarily chosen injective object under cokernel f.

@[implicit_reducible]

noncomputable instance CategoryTheory.Injective.instSyzygies {C : Type u_2} [Category.{u_1, u_2} C] [EnoughInjectives C] [Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Limits.HasCokernel f] : Injective (syzygies f)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Injective.d {C : Type u₁} [Category.{v₁, u₁} C] [EnoughInjectives C] [Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Limits.HasCokernel f] : Y ⟶ syzygies f

When C has enough injective, Injective.d f : Y ⟶ syzygies f is the composition cokernel.π f ≫ ι (cokernel f).

(When C is abelian, we have exact f (injective.d f).)

instance CategoryTheory.Injective.instEnoughProjectivesOppositeOfEnoughInjectives {C : Type u₁} [Category.{v₁, u₁} C] [EnoughInjectives C] : EnoughProjectives Cᵒᵖ

instance CategoryTheory.Injective.instEnoughInjectivesOppositeOfEnoughProjectives {C : Type u₁} [Category.{v₁, u₁} C] [EnoughProjectives C] : EnoughInjectives Cᵒᵖ

theorem CategoryTheory.Injective.enoughProjectives_of_enoughInjectives_op {C : Type u₁} [Category.{v₁, u₁} C] [EnoughInjectives Cᵒᵖ] : EnoughProjectives C

theorem CategoryTheory.Injective.enoughInjectives_of_enoughProjectives_op {C : Type u₁} [Category.{v₁, u₁} C] [EnoughProjectives Cᵒᵖ] : EnoughInjectives C

theorem CategoryTheory.Adjunction.map_injective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{v_1, u_1} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.PreservesMonomorphisms] (I : D) (hI : Injective I) : Injective (G.obj I)

theorem CategoryTheory.Adjunction.injective_of_map_injective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{v_1, u_1} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [G.Full] [G.Faithful] (I : D) (hI : Injective (G.obj I)) : Injective I

def CategoryTheory.Adjunction.mapInjectivePresentation {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{v_1, u_1} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.PreservesMonomorphisms] (X : D) (I : InjectivePresentation X) : InjectivePresentation (G.obj X)

Given an adjunction F ⊣ G such that F preserves monos, G maps an injective presentation of X to an injective presentation of G(X).

def CategoryTheory.Adjunction.injectivePresentationOfMap {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{v_1, u_1} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.PreservesMonomorphisms] [F.ReflectsMonomorphisms] (X : C) (I : InjectivePresentation (F.obj X)) : InjectivePresentation X

Given an adjunction F ⊣ G such that F preserves monomorphisms and is faithful, then any injective presentation of F(X) can be pulled back to an injective presentation of X. This is similar to mapInjectivePresentation.

theorem CategoryTheory.Functor.injective_of_map_injective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) [F.Full] [F.Faithful] [F.PreservesMonomorphisms] {I : C} (hI : Injective (F.obj I)) : Injective I

theorem CategoryTheory.EnoughInjectives.of_adjunction {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [L.PreservesMonomorphisms] [L.ReflectsMonomorphisms] [EnoughInjectives D] : EnoughInjectives C

Lemma 3.8

theorem CategoryTheory.EnoughInjectives.of_equivalence {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (e : Functor C D) [e.IsEquivalence] [EnoughInjectives D] : EnoughInjectives C

An equivalence of categories transfers enough injectives.

theorem CategoryTheory.Equivalence.map_injective_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : C ≌ D) (P : C) : Injective (F.functor.obj P) ↔ Injective P

def CategoryTheory.Equivalence.injectivePresentationOfMapInjectivePresentation {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : C ≌ D) (X : C) (I : InjectivePresentation (F.functor.obj X)) : InjectivePresentation X

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

theorem CategoryTheory.Equivalence.enoughInjectives_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : C ≌ D) : EnoughInjectives C ↔ EnoughInjectives D

theorem CategoryTheory.Retract.injective {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (h : Retract X Y) [i : Injective Y] : Injective X