mathlib3 documentation

category_theory.preadditive.injective

Injective objects and categories with enough injectives #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[class]
structure category_theory.injective {C : Type u₁} [category_theory.category C] (J : C) :
Prop

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

Instances of this typeclass
source
@[nolint]
structure category_theory.injective_presentation {C : Type u₁} [category_theory.category 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.

Instances for category_theory.injective_presentation
  • category_theory.injective_presentation.has_sizeof_inst
source
@[class]
structure category_theory.enough_injectives (C : Type u₁) [category_theory.category 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.

Instances of this typeclass
source
noncomputable def category_theory.injective.factor_thru {C : Type u₁} [category_theory.category C] {J X Y : C} [category_theory.injective J] (g : X ⟶ J) (f : X ⟶ Y) [category_theory.mono f] :
Y ⟶ J

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

Equations
source
@[simp]
theorem category_theory.injective.comp_factor_thru {C : Type u₁} [category_theory.category C] {J X Y : C} [category_theory.injective J] (g : X ⟶ J) (f : X ⟶ Y) [category_theory.mono f] :
f ≫ category_theory.injective.factor_thru g f = g
source
@[protected, instance]
def category_theory.injective.zero_injective {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] :
category_theory.injective 0
source
theorem category_theory.injective.of_iso {C : Type u₁} [category_theory.category C] {P Q : C} (i : P ≅ Q) (hP : category_theory.injective P) :
category_theory.injective Q
source
theorem category_theory.injective.iso_iff {C : Type u₁} [category_theory.category C] {P Q : C} (i : P ≅ Q) :
category_theory.injective P ↔ category_theory.injective Q
source
@[protected, instance]
def category_theory.injective.injective (X : Type u₁) [nonempty X] :
category_theory.injective X

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

source
@[protected, instance]
def category_theory.injective.Type.enough_injectives  :
category_theory.enough_injectives (Type u₁)
source
@[protected, instance]
def category_theory.injective.category_theory.limits.prod.injective {C : Type u₁} [category_theory.category C] {P Q : C} [category_theory.limits.has_binary_product P Q] [category_theory.injective P] [category_theory.injective Q] :
category_theory.injective (P ⨯ Q)
source
@[protected, instance]
def category_theory.injective.category_theory.limits.pi_obj.injective {C : Type u₁} [category_theory.category C] {β : Type v} (c : β → C) [category_theory.limits.has_product c] [∀ (b : β), category_theory.injective (c b)] :
category_theory.injective (∏ c)
source
@[protected, instance]
def category_theory.injective.category_theory.limits.biprod.injective {C : Type u₁} [category_theory.category C] {P Q : C} [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproduct P Q] [category_theory.injective P] [category_theory.injective Q] :
category_theory.injective (P ⊞ Q)
source
@[protected, instance]
def category_theory.injective.category_theory.limits.biproduct.injective {C : Type u₁} [category_theory.category C] {β : Type v} (c : β → C) [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_biproduct c] [∀ (b : β), category_theory.injective (c b)] :
category_theory.injective (⨁ c)
source
@[protected, instance]
def category_theory.injective.opposite.unop.injective {C : Type u₁} [category_theory.category C] {P : Cᵒᵖ} [category_theory.projective P] :
category_theory.injective (opposite.unop P)
source
@[protected, instance]
def category_theory.injective.opposite.unop.category_theory.projective {C : Type u₁} [category_theory.category C] {J : Cᵒᵖ} [category_theory.injective J] :
category_theory.projective (opposite.unop J)
source
@[protected, instance]
def category_theory.injective.opposite.op.category_theory.projective {C : Type u₁} [category_theory.category C] {J : C} [category_theory.injective J] :
category_theory.projective (opposite.op J)
source
@[protected, instance]
def category_theory.injective.opposite.op.injective {C : Type u₁} [category_theory.category C] {P : C} [category_theory.projective P] :
category_theory.injective (opposite.op P)
source
theorem category_theory.injective.injective_iff_projective_op {C : Type u₁} [category_theory.category C] {J : C} :
category_theory.injective J ↔ category_theory.projective (opposite.op J)
source
theorem category_theory.injective.projective_iff_injective_op {C : Type u₁} [category_theory.category C] {P : C} :
category_theory.projective P ↔ category_theory.injective (opposite.op P)
source
theorem category_theory.injective.injective_iff_preserves_epimorphisms_yoneda_obj {C : Type u₁} [category_theory.category C] (J : C) :
category_theory.injective J ↔ (category_theory.yoneda.obj J).preserves_epimorphisms
source
theorem category_theory.injective.injective_of_adjoint {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {L : C ⥤ D} {R : D ⥤ C} [L.preserves_monomorphisms] (adj : L ⊣ R) (J : D) [category_theory.injective J] :
category_theory.injective (R.obj J)
source
noncomputable def category_theory.injective.under {C : Type u₁} [category_theory.category C] [category_theory.enough_injectives C] (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
source
@[protected, instance]
def category_theory.injective.injective_under {C : Type u₁} [category_theory.category C] [category_theory.enough_injectives C] (X : C) :
category_theory.injective (category_theory.injective.under X)
source
noncomputable def category_theory.injective.ι {C : Type u₁} [category_theory.category C] [category_theory.enough_injectives C] (X : C) :
X ⟶ category_theory.injective.under X

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

Equations
Instances for category_theory.injective.ι
source
@[protected, instance]
def category_theory.injective.ι_mono {C : Type u₁} [category_theory.category C] [category_theory.enough_injectives C] (X : C) :
category_theory.mono (category_theory.injective.ι X)
source
@[protected, instance]
def category_theory.injective.syzygies.injective {C : Type u₁} [category_theory.category C] [category_theory.enough_injectives C] [category_theory.limits.has_zero_morphisms C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_cokernel f] :
category_theory.injective (category_theory.injective.syzygies f)
source
noncomputable def category_theory.injective.syzygies {C : Type u₁} [category_theory.category C] [category_theory.enough_injectives C] [category_theory.limits.has_zero_morphisms C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_cokernel f] :
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
source
@[reducible]
noncomputable def category_theory.injective.d {C : Type u₁} [category_theory.category C] [category_theory.enough_injectives C] [category_theory.limits.has_zero_morphisms C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_cokernel f] :
Y ⟶ category_theory.injective.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).)

source
@[protected, instance]
def category_theory.injective.opposite.category_theory.enough_projectives {C : Type u₁} [category_theory.category C] [category_theory.enough_injectives C] :
category_theory.enough_projectives Cᵒᵖ
source
@[protected, instance]
def category_theory.injective.opposite.category_theory.enough_injectives {C : Type u₁} [category_theory.category C] [category_theory.enough_projectives C] :
category_theory.enough_injectives Cᵒᵖ
source
theorem category_theory.injective.enough_projectives_of_enough_injectives_op {C : Type u₁} [category_theory.category C] [category_theory.enough_injectives Cᵒᵖ] :
category_theory.enough_projectives C
source
theorem category_theory.injective.enough_injectives_of_enough_projectives_op {C : Type u₁} [category_theory.category C] [category_theory.enough_projectives Cᵒᵖ] :
category_theory.enough_injectives C
source
noncomputable def category_theory.injective.exact.desc {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_images Cᵒᵖ] [category_theory.limits.has_equalizers Cᵒᵖ] {J Q R S : C} [category_theory.injective J] (h : R ⟶ J) (f : Q ⟶ R) (g : R ⟶ S) (hgf : category_theory.exact g.op 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
source
@[simp]
theorem category_theory.injective.exact.comp_desc {C : Type u₁} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_images Cᵒᵖ] [category_theory.limits.has_equalizers Cᵒᵖ] {J Q R S : C} [category_theory.injective J] (h : R ⟶ J) (f : Q ⟶ R) (g : R ⟶ S) (hgf : category_theory.exact g.op f.op) (w : f ≫ h = 0) :
g ≫ category_theory.injective.exact.desc h f g hgf w = h
source
theorem category_theory.adjunction.map_injective {C : Type u₁} [category_theory.category C] {D : Type u_1} [category_theory.category D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) [F.preserves_monomorphisms] (I : D) (hI : category_theory.injective I) :
category_theory.injective (G.obj I)
source
theorem category_theory.adjunction.injective_of_map_injective {C : Type u₁} [category_theory.category C] {D : Type u_1} [category_theory.category D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) [category_theory.full G] [category_theory.faithful G] (I : D) (hI : category_theory.injective (G.obj I)) :
category_theory.injective I
source
def category_theory.adjunction.map_injective_presentation {C : Type u₁} [category_theory.category C] {D : Type u_1} [category_theory.category D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) [F.preserves_monomorphisms] (X : D) (I : category_theory.injective_presentation X) :
category_theory.injective_presentation (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).

Equations
source
def category_theory.equivalence.injective_presentation_of_map_injective_presentation {C : Type u₁} [category_theory.category C] {D : Type u_1} [category_theory.category D] (F : C ≌ D) (X : C) (I : category_theory.injective_presentation (F.functor.obj X)) :
category_theory.injective_presentation X

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

Equations
source
theorem category_theory.equivalence.enough_injectives_iff {C : Type u₁} [category_theory.category C] {D : Type u_1} [category_theory.category D] (F : C ≌ D) :
category_theory.enough_injectives C ↔ category_theory.enough_injectives D