Theorems · Definition · category theory

CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms

{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → C → CategoryTheory.MorphismProperty C

Given an object G : C, this is the family of morphisms in C given by the inclusions of all subobjects of G. If G is a separator, and C is a Grothendieck abelian category, then any monomorphism in C is a transfinite composition of pushouts of monomorphisms in this family (see generatingMonomorphisms.exists_transfiniteCompositionOfShape).

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Cited by

8 results in Mathlib

Foundations

Depth 38 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category