English
If J is a shape with filtered colimits and the base category C has AB5 of size J, then monomorphisms are stable under shape-J filtered colimits; in particular, the colimit of a diagram of monomorphisms indexed by a filtered shape remains mono.
Русский
Пусть J имеет фильтрованные колимиты и базовая категория C обладает AB5 по размеру J; тогда мономорфизмы сохраняются под фильтрованными колимитами формы J; следовательно, колимит диаграммы мономорфизмов остаётся мономорфизмом.
LaTeX
$$$\operatorname{IsStableUnderFilteredColimits}(\operatorname{monomorphisms}(C)).$$$
Lean4
instance [HasFilteredColimitsOfSize.{v', u'} C] [AB5OfSize.{v', u'} C] :
IsStableUnderFilteredColimits.{v', u'} (monomorphisms C) where
isStableUnderColimitsOfShape J _ _ := by infer_instance
