English
The class of monomorphisms in a category C is closed under shape-J colimits, provided C has those colimits and colimits preserve monomorphisms. In particular, whenever a diagram consists of monomorphisms, the induced map from the colimit of the domain objects to the colimit of the codomain objects is again a monomorphism.
Русский
Класс мономорфизмов в категории C замкнут по колимитам формы J, если в C существуют такие колимиты и колимиты сохраняют мономорфизмы. То есть для любого диаграммного набора мономорфизмов соответствующая стрелка из колимита доменов в колимит кодомоментов является мономорфизм.
LaTeX
$$$\operatorname{IsStableUnderColimitsOfShape}(J,\operatorname{monomorphisms}(C)).$$$
Lean4
instance isStableUnderColimitsOfShape_monomorphisms [HasColimitsOfShape J C]
[(colim : (J ⥤ C) ⥤ C).PreservesMonomorphisms] : (monomorphisms C).IsStableUnderColimitsOfShape J where
condition X₁ X₂ c₁ c₂ hc₁ hc₂ f hf φ
hφ := by
have (j : J) : Mono (f.app j) := hf _
have := NatTrans.mono_of_mono_app f
apply colim.map_mono' f hc₁ hc₂ φ (by simp [hφ])
