# 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₁} [] (J : C) :

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) [inst : ], ∃ (h : Y J),

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

Instances
theorem CategoryTheory.Injective.factors {C : Type u₁} [] {J : C} [self : ] {X : C} {Y : C} (g : X J) (f : X Y) :
∃ (h : Y J),

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

theorem CategoryTheory.Limits.IsZero.injective {C : Type u₁} [] {X : C} (h : ) :
structure CategoryTheory.InjectivePresentation {C : Type u₁} [] (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 : CategoryTheory.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 : CategoryTheory.Mono self.f

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

Instances For
theorem CategoryTheory.InjectivePresentation.injective {C : Type u₁} [] {X : C} (self : ) :

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

theorem CategoryTheory.InjectivePresentation.mono {C : Type u₁} [] {X : C} (self : ) :

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

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),

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.

Instances
theorem CategoryTheory.EnoughInjectives.presentation {C : Type u₁} [] [self : ] (X : C) :

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.

def CategoryTheory.Injective.factorThru {C : Type u₁} [] {J : C} {X : C} {Y : C} (g : X J) (f : X Y) :
Y J

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

Equations
• = .choose
Instances For
@[simp]
theorem CategoryTheory.Injective.comp_factorThru {C : Type u₁} [] {J : C} {X : C} {Y : C} (g : X J) (f : X Y) :
Equations
• =
theorem CategoryTheory.Injective.of_iso {C : Type u₁} [] {P : C} {Q : C} (i : P Q) (hP : ) :
theorem CategoryTheory.Injective.iso_iff {C : Type u₁} [] {P : C} {Q : C} (i : P Q) :

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

Equations
• =
instance CategoryTheory.Injective.instProd {C : Type u₁} [] {P : C} {Q : C} :
Equations
• =
instance CategoryTheory.Injective.instPiObj {C : Type u₁} [] {β : Type v} (c : βC) [∀ (b : β), ] :
Equations
• =
instance CategoryTheory.Injective.instBiprod {C : Type u₁} [] {P : C} {Q : C} :
Equations
• =
instance CategoryTheory.Injective.instBiproduct {C : Type u₁} [] {β : Type v} (c : βC) [∀ (b : β), ] :
Equations
• =
Equations
• =
Equations
• =
Equations
• =
Equations
• =
theorem CategoryTheory.Injective.injective_iff_preservesEpimorphisms_yoneda_obj {C : Type u₁} [] (J : C) :
(CategoryTheory.yoneda.obj J).PreservesEpimorphisms
theorem CategoryTheory.Injective.injective_of_adjoint {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } [L.PreservesMonomorphisms] (adj : L R) (J : D) :
def CategoryTheory.Injective.under {C : Type u₁} [] (X : C) :
C

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

Equations
• = .some.J
Instances For
instance CategoryTheory.Injective.injective_under {C : Type u₁} [] (X : C) :
Equations
• =
def CategoryTheory.Injective.ι {C : Type u₁} [] (X : C) :

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

Equations
• = .some.f
Instances For
instance CategoryTheory.Injective.ι_mono {C : Type u₁} [] (X : C) :
Equations
• =
def CategoryTheory.Injective.syzygies {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
C

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

Equations
Instances For
instance CategoryTheory.Injective.instSyzygies {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
Equations
• =
@[reducible, inline]
abbrev CategoryTheory.Injective.d {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

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).)

Equations
Instances For
Equations
• =
Equations
• =
theorem CategoryTheory.Adjunction.map_injective {C : Type u₁} [] {D : Type u_1} [] {F : } {G : } (adj : F G) [F.PreservesMonomorphisms] (I : D) (hI : ) :
theorem CategoryTheory.Adjunction.injective_of_map_injective {C : Type u₁} [] {D : Type u_1} [] {F : } {G : } (adj : F G) [G.Full] [G.Faithful] (I : D) (hI : CategoryTheory.Injective (G.obj I)) :
def CategoryTheory.Adjunction.mapInjectivePresentation {C : Type u₁} [] {D : Type u_1} [] {F : } {G : } (adj : F G) [F.PreservesMonomorphisms] (X : D) :

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

Equations
• adj.mapInjectivePresentation X I = { J := G.obj I.J, injective := , f := G.map I.f, mono := }
Instances For
def CategoryTheory.Adjunction.injectivePresentationOfMap {C : Type u₁} [] {D : Type u_1} [] {F : } {G : } (adj : F G) [F.PreservesMonomorphisms] [F.ReflectsMonomorphisms] (X : C) (I : CategoryTheory.InjectivePresentation (F.obj 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.

Equations
• adj.injectivePresentationOfMap X I = { J := G.obj I.J, injective := , f := (adj.homEquiv X I.J) I.f, mono := }
Instances For
theorem CategoryTheory.EnoughInjectives.of_adjunction {C : Type u₁} {D : Type u₂} [] [] {L : } {R : } (adj : L R) [L.PreservesMonomorphisms] [L.ReflectsMonomorphisms] :

Lemma 3.8

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

An equivalence of categories transfers enough injectives.

theorem CategoryTheory.Equivalence.map_injective_iff {C : Type u₁} [] {D : Type u_1} [] (F : C D) (P : C) :
CategoryTheory.Injective (F.functor.obj P)

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

Equations
• F.injectivePresentationOfMapInjectivePresentation X I = F.toAdjunction.injectivePresentationOfMap X I
Instances For
theorem CategoryTheory.Equivalence.enoughInjectives_iff {C : Type u₁} [] {D : Type u_1} [] (F : C D) :