mathlib3 documentation


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.

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

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₁} [category_theory.category C] {J X Y : C} [category_theory.injective J] (g : X J) (f : X Y) [category_theory.mono f] :

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

@[protected, instance]

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

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

Instances for category_theory.injective.under

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

Instances for category_theory.injective.ι

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

Instances for category_theory.injective.syzygies

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

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

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


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