# 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) :
• factors : ∀ {X Y : C} (g : X J) (f : X Y) [inst : ], h,

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

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

Instances
structure CategoryTheory.InjectivePresentation {C : Type u₁} [] (X : C) :
Type (max u₁ v₁)
• J : C

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

• injective :

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

• f : X s.J

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

• mono :

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

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

Instances For
• 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.

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

Instances For
@[simp]
theorem CategoryTheory.Injective.comp_factorThru {C : Type u₁} [] {J : C} {X : C} {Y : C} (g : X J) (f : X Y) :
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.

instance CategoryTheory.Injective.instInjectiveProd {C : Type u₁} [] {P : C} {Q : C} :
instance CategoryTheory.Injective.instInjectivePiObj {C : Type u₁} [] {β : Type v} (c : βC) [∀ (b : β), ] :
instance CategoryTheory.Injective.instInjectiveBiprod {C : Type u₁} [] {P : C} {Q : C} :
instance CategoryTheory.Injective.instInjectiveBiproduct {C : Type u₁} [] {β : Type v} (c : βC) [∀ (b : β), ] :
theorem CategoryTheory.Injective.injective_of_adjoint {C : Type u₁} [] {D : Type u₂} [] {L : } {R : } (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.

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

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

Instances For
instance CategoryTheory.Injective.ι_mono {C : Type u₁} [] (X : C) :
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.

Instances For
instance CategoryTheory.Injective.instInjectiveSyzygies {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
@[inline, reducible]
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).)

Instances For
def CategoryTheory.Injective.Exact.desc {C : Type u₁} [] {J : C} {Q : C} {R : C} {S : C} (h : R J) (f : Q R) (g : R S) (hgf : CategoryTheory.Exact g.op f.op) (w : ) :
S J

Given a pair of exact morphism f : Q ⟶ R and g : R ⟶ S and a map h : R ⟶ J to an injective object J such that f ≫ h = 0, then g descents to a map S ⟶ J. See below:

Q --- f --> R --- g --> S
|
| h
v
J

Instances For
@[simp]
theorem CategoryTheory.Injective.Exact.comp_desc {C : Type u₁} [] {J : C} {Q : C} {R : C} {S : C} (h : R J) (f : Q R) (g : R S) (hgf : CategoryTheory.Exact g.op f.op) (w : ) :
= h
theorem CategoryTheory.Adjunction.map_injective {C : Type u₁} [] {D : Type u_1} [] {F : } {G : } (adj : F G) (I : D) (hI : ) :
theorem CategoryTheory.Adjunction.injective_of_map_injective {C : Type u₁} [] {D : Type u_1} [] {F : } {G : } (adj : F G) (I : D) (hI : CategoryTheory.Injective (G.obj I)) :
def CategoryTheory.Adjunction.mapInjectivePresentation {C : Type u₁} [] {D : Type u_1} [] {F : } {G : } (adj : F G) (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).

Instances For
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.

Instances For
theorem CategoryTheory.Equivalence.enoughInjectives_iff {C : Type u₁} [] {D : Type u_1} [] (F : C D) :