mathlib documentation

category_theory.preadditive.injective

Injective objects and categories with enough injectives #

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

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

Equations
Instances for category_theory.injective.under

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

Equations
Instances for category_theory.injective.ι

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

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
            v
            J
Equations