epi_fst_of_isLimit — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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