epi_snd_of_isLimit — Mathlib

English

If f is epi and s is a pullback cone of f and g that is an IsLimit, then the second projection s.snd is epi.

Русский

Если f — эпиморфизм, а s — конус-пуллбака для f и g, являющийся IsLimit, то вторая проекция s.snd — эпиморфизм.

LaTeX

$$$\\\\forall X,Y,Z, f: X \\\\to Z, g: Y \\\\to Z, [Epi f], {s: PullbackCone f g}, IsLimit s \\\\Rightarrow \\\\mathrm{Epi}(s. snd).$$$

Lean4

theorem epi_snd_of_isLimit [Epi f] {s : PullbackCone f g} (hs : IsLimit s) : Epi s.snd :=
  by
  haveI : Epi (NatTrans.app (limit.cone (cospan f g)).π WalkingCospan.right) := Abelian.epi_pullback_of_epi_f f g
  apply epi_of_epi_fac (IsLimit.conePointUniqueUpToIso_hom_comp (limit.isLimit _) hs _)

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