English
In a Grothendieck abelian category, let X be an object and F a filtered diagram of subobjects of X indexed by J. If c is a colimit cocone for the corresponding diagram obtained by forgetting structure, and f: c.pt → X is induced by the inclusions (one for each j ∈ J), then f is a monomorphism.
Русский
В абелевой категории Гротендикта существует объект X и фильтрованный диаграммный набор подобъектов F, индексированный множеством J. Пусть c — колимитный конус для соответствующей диаграммы, полученной путём forgetful-функции, и пусть f: c.pt → X индукция по включениям (для каждого j ∈ J). Тогда f является монообразованием.
LaTeX
$$$\mathrm{Mono}(f)$$$
Lean4
/-- If `C` is a Grothendieck abelian category, `X : C`, if `F : J ⥤ MonoOver X` is a
functor from a filtered category `J`, `c` is a colimit cocone for the corresponding
functor `J ⥤ C`, and `f : c.pt ⟶ X` is induced by the inclusions,
then `f` is a monomorphism. -/
theorem mono_of_isColimit_monoOver : Mono f :=
by
let α : F ⋙ MonoOver.forget _ ⋙ Over.forget _ ⟶ (Functor.const _).obj X :=
{ app j := (F.obj j).obj.hom
naturality _ _ f := (F.map f).w }
have := NatTrans.mono_of_mono_app α
exact colim.map_mono' α hc (isColimitConstCocone J X) f (by simpa using hf)
