Monomorphisms in Grothendieck abelian categories

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

instance CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mono.map_bot_le {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{w, v, u} C] {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} (h : (monomorphisms C).TransfiniteCompositionOfShape J f) (j : J) : Mono (h.F.map (homOfLE ⋯))

theorem CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mono {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{w, v, u} C] {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} (h : (monomorphisms C).TransfiniteCompositionOfShape J f) : Mono f

instance CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.mono_map {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian.{w, v, u} C] {J : Type w} [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] {X Y : C} {f : X ⟶ Y} (h : (monomorphisms C).TransfiniteCompositionOfShape J f) (j j' : J) (f✝ : j ⟶ j') : Mono (h.F.map f✝)

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