English
If X: J ⥤ C is mapped by X.map morphisms to mono, J is filtered, then the inclusion maps of the colimit cocone are mono.
Русский
Если X: J ⥤ C обратимо монообразна по всем гомоман помимо J, и J фильтрован, то элементы кокона колимита моно.
LaTeX
$$$[IsFiltered J] \\Rightarrow \\operatorname{Mono}(\\, c.ι.app j_0 \\,)$ under colim preservation conditions$$
Lean4
/-- Assume that `φ : X₁ ⟶ X₂` is a natural transformation in `J ⥤ C` which
consists of epimorphisms, then if `f : c₁.pt ⟶ c₂.pt` is a morphism
between the points of cocones `c₁` and `c₂` for `X₁` and `X₂`, in such
a way that `c₂` is colimit and `f` is compatible with `φ`, then `f` is an epimorphism. -/
theorem map_epi' {X₁ X₂ : J ⥤ C} (φ : X₁ ⟶ X₂) [∀ j, Epi (φ.app j)] (c₁ : Cocone X₁) {c₂ : Cocone X₂}
(hc₂ : IsColimit c₂) (f : c₁.pt ⟶ c₂.pt) (hf : ∀ j, c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j) : Epi f where
left_cancellation {Z} g₁ g₂
h := hc₂.hom_ext (fun j ↦ by rw [← cancel_epi (φ.app j), ← reassoc_of% hf, h, reassoc_of% hf])
