mono_inl_of_isColimit — Mathlib

English

Symmetric to Inr: if g is mono and s is a pushout cocone with IsColimit, then s.inl is mono.

Русский

Симметрично к Inr: если g моно и s — пушаут-ко́нок с IsColimit, то s.inl моно.

LaTeX

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

Lean4

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

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