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₁} [CategoryTheory.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) [inst : CategoryTheory.Mono f], ∃ (h : Y ⟶ J), CategoryTheory.CategoryStruct.comp f h = g

  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₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (h : CategoryTheory.Limits.IsZero X) : CategoryTheory.Injective X

structure CategoryTheory.InjectivePresentation {C : Type u₁} [CategoryTheory.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 : 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.

class CategoryTheory.EnoughInjectives (C : Type u₁) [CategoryTheory.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 (CategoryTheory.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.

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

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

Equations

• CategoryTheory.Injective.factorThru g f = Exists.choose ⋯

@[simp]

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

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

Equations

• ⋯ = ⋯

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

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.Injective.Type.enoughInjectives = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

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

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

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

Equations

• CategoryTheory.Injective.under X = (Nonempty.some ⋯).J

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

Equations

• ⋯ = ⋯

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

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

Equations

• CategoryTheory.Injective.ι X = (Nonempty.some ⋯).f

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

Equations

• ⋯ = ⋯

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

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

Equations

• CategoryTheory.Injective.syzygies f = CategoryTheory.Injective.under (CategoryTheory.Limits.cokernel f)

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

Equations

• ⋯ = ⋯

@[inline, reducible]

abbrev CategoryTheory.Injective.d {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.EnoughInjectives C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] : Y ⟶ CategoryTheory.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).)

Equations

• CategoryTheory.Injective.d f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (CategoryTheory.Injective.ι (CategoryTheory.Limits.cokernel f))

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

def CategoryTheory.Injective.Exact.desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasImages Cᵒᵖ] [CategoryTheory.Limits.HasEqualizers Cᵒᵖ] {J : C} {Q : C} {R : C} {S : C} [CategoryTheory.Injective J] (h : R ⟶ J) (f : Q ⟶ R) (g : R ⟶ S) (hgf : CategoryTheory.Exact g.op f.op) (w : CategoryTheory.CategoryStruct.comp 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

• CategoryTheory.Injective.Exact.desc h f g hgf w = (CategoryTheory.Exact.lift h.op g.op f.op hgf ⋯).unop

@[simp]

theorem CategoryTheory.Injective.Exact.comp_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasImages Cᵒᵖ] [CategoryTheory.Limits.HasEqualizers Cᵒᵖ] {J : C} {Q : C} {R : C} {S : C} [CategoryTheory.Injective J] (h : R ⟶ J) (f : Q ⟶ R) (g : R ⟶ S) (hgf : CategoryTheory.Exact g.op f.op) (w : CategoryTheory.CategoryStruct.comp f h = 0) : CategoryTheory.CategoryStruct.comp g (CategoryTheory.Injective.Exact.desc h f g hgf w) = h

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

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

def CategoryTheory.Adjunction.mapInjectivePresentation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [CategoryTheory.Functor.PreservesMonomorphisms F] (X : D) (I : CategoryTheory.InjectivePresentation X) : CategoryTheory.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).

Equations

• CategoryTheory.Adjunction.mapInjectivePresentation adj X I = { J := G.obj I.J, injective := ⋯, f := G.map I.f, mono := ⋯ }

def CategoryTheory.Adjunction.injectivePresentationOfMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [CategoryTheory.Functor.PreservesMonomorphisms F] [CategoryTheory.Functor.ReflectsMonomorphisms F] (X : C) (I : CategoryTheory.InjectivePresentation (F.obj X)) : CategoryTheory.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.

Equations

• CategoryTheory.Adjunction.injectivePresentationOfMap adj X I = { J := G.obj I.J, injective := ⋯, f := (adj.homEquiv X I.J) I.f, mono := ⋯ }

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

Lemma 3.8

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

An equivalence of categories transfers enough injectives.

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

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

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

Equations

• CategoryTheory.Equivalence.injectivePresentationOfMapInjectivePresentation F X I = CategoryTheory.Adjunction.injectivePresentationOfMap F.toAdjunction X I

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