Documentation

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms

Monomorphisms in Grothendieck abelian categories #

In this file, we show that in a Grothendieck abelian category, monomorphisms are stable under transfinite composition.

source
instance CategoryTheory.IsGrothendieckAbelian.instIsStableUnderTransfiniteCompositionMonomorphisms {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{w, v, u} C] :
(MorphismProperty.monomorphisms C).IsStableUnderTransfiniteComposition