# 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]
structure category_theory.injective {C : Type u} (J : C) :
Prop
• factors : ∀ {X Y : C} (g : X J) (f : X Y) [_inst_2 : , ∃ (h : Y J), f h = g

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

Instances of this typeclass
@[nolint]
structure category_theory.injective_presentation {C : Type u} (X : C) :
Type (max u v)
• J : C
• injective : . "apply_instance"
• f : X self.J
• mono : . "apply_instance"

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

Instances for category_theory.injective_presentation
• category_theory.injective_presentation.has_sizeof_inst
@[class]
structure category_theory.enough_injectives (C : Type u)  :
Prop
• 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 of this typeclass
noncomputable def category_theory.injective.factor_thru {C : Type u} {J X 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
@[simp]
theorem category_theory.injective.comp_factor_thru {C : Type u} {J X Y : C} (g : X J) (f : X Y)  :
@[protected, instance]
theorem category_theory.injective.of_iso {C : Type u} {P Q : C} (i : P Q) (hP : category_theory.injective P) :
theorem category_theory.injective.iso_iff {C : Type u} {P Q : C} (i : P Q) :
@[protected, instance]

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

@[protected, instance]
@[protected, instance]
@[protected, instance]
def category_theory.injective.category_theory.limits.pi_obj.injective {C : Type u} {β : Type v} (c : β → C) [∀ (b : β), ] :
@[protected, instance]
@[protected, instance]
def category_theory.injective.category_theory.limits.biproduct.injective {C : Type u} {β : Type v} (c : β → C) [∀ (b : β), ] :
@[protected, instance]
@[protected, instance]
noncomputable def category_theory.injective.under {C : Type u} (X : C) :
C

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

Equations
Instances for category_theory.injective.under
@[protected, instance]
noncomputable def category_theory.injective.ι {C : Type u} (X : C) :

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

Equations
Instances for category_theory.injective.ι
@[protected, instance]
def category_theory.injective.ι_mono {C : Type u} (X : C) :
@[protected, instance]
noncomputable def category_theory.injective.syzygies {C : Type u} {X 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 category_theory.injective.syzygies
noncomputable def category_theory.injective.d {C : Type u} {X 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).)

noncomputable def category_theory.injective.exact.desc {C : Type u} {J Q R S : C} (h : R J) (f : Q R) (g : R S) (hgf : f.op) (w : f h = 0) :
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

Equations
@[simp]
theorem category_theory.injective.exact.comp_desc {C : Type u} {J Q R S : C} (h : R J) (f : Q R) (g : R S) (hgf : f.op) (w : f h = 0) :
g hgf w = h