English
If colimit functor preserves monos, a morphism f between cocone points compatible with a mono natural transformation φ is itself mono.
Русский
Если колимит-функтор сохраняет моно morphisms, морфизм f между точками коконотов совместим с мономорфизмами φ и т.д., тогда f моно.
LaTeX
$$$[HasColimitsOfShape J C] \\land [(colim : (J ⥤ C) ⥤ C).PreservesMonomorphisms] \\Rightarrow \\text{Mono}(f)$ under compatibility hf$$
Lean4
/-- Assume that `colim : (J ⥤ C) ⥤ C` preserves monomorphisms, and
`φ : X₁ ⟶ X₂` is a monomorphism in `J ⥤ C`, then if `f : c₁.pt ⟶ c₂.pt` is a morphism
between the points of colimit cocones for `X₁` and `X₂` in such a way that `f`
identifies to `colim.map φ`, then `f` is a monomorphism. -/
theorem map_mono' [HasColimitsOfShape J C] [(colim : (J ⥤ C) ⥤ C).PreservesMonomorphisms] {X₁ X₂ : J ⥤ C} (φ : X₁ ⟶ X₂)
[Mono φ] {c₁ : Cocone X₁} (hc₁ : IsColimit c₁) {c₂ : Cocone X₂} (hc₂ : IsColimit c₂) (f : c₁.pt ⟶ c₂.pt)
(hf : ∀ j, c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j) : Mono f :=
by
refine ((MorphismProperty.monomorphisms C).arrow_mk_iso_iff ?_).2 (inferInstanceAs (Mono (colim.map φ)))
exact
Arrow.isoMk (IsColimit.coconePointUniqueUpToIso hc₁ (colimit.isColimit _))
(IsColimit.coconePointUniqueUpToIso hc₂ (colimit.isColimit _))
(hc₁.hom_ext
(fun j ↦ by
dsimp
rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc, colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]))
