mono_inr_of_isColimit — Mathlib

English

If f is any morphism and s is a pushout cocone with IsColimit, then s.inr is mono whenever g is mono.

Русский

Если f произвольный морфизм, а s — пушаут-ко́нок с IsColimit, то s.inr моно, когда g моно.

LaTeX

$$$\\\\forall f,g \\\\in \\\\mathrm{Hom}, [Mono f], {s: PushoutCocone f g}, IsColimit s \\\\Rightarrow \\\\mathrm{Mono}(s.inr).$$$

Lean4

theorem mono_inr_of_isColimit [Mono f] {s : PushoutCocone f g} (hs : IsColimit s) : Mono s.inr :=
  by
  haveI : Mono (NatTrans.app (colimit.cocone (span f g)).ι WalkingCospan.right) := Abelian.mono_pushout_of_mono_f f g
  apply mono_of_mono_fac (IsColimit.comp_coconePointUniqueUpToIso_hom hs (colimit.isColimit _) _)

Похожие утверждения