English
If colimit over J preserves monomorphisms and X: J ⥤ C is a natural transformation with epi components, then the induced map between colimit cocones is mono.
Русский
Если колимит по J сохраняет моно morphisms и X: J ⥤ C — натуральное преобразование с мономорфизмами в компонентах, тогда полученная карта между колимитами моно.
LaTeX
$$$[HasColimitsOfShape J C] \\land [(\\text{colim} : (J ⥤ C) ⥤ C).PreservesMonomorphisms] \\Rightarrow \\operatorname{Mono}(f)$ where f is the induced map between colimit points$$
Lean4
/-- If `colim` of shape `J` into an abelian category `C` preserves monomorphisms, then `C` has AB of
shape `J`.
-/
theorem hasExactColimitsOfShape_of_preservesMono [HasColimitsOfShape J C]
[PreservesMonomorphisms (colim (J := J) (C := C))] : HasExactColimitsOfShape J C where
preservesFiniteLimits :=
by
apply (config := { allowSynthFailures := true }) preservesFiniteLimits_of_preservesHomology
· exact preservesHomology_of_preservesMonos_and_cokernels _
· exact additive_of_preservesBinaryBiproducts _
