preserves_epi_of_preservesColimit

English

If F preserves pushouts, then it preserves epimorphisms.

Русский

Если F сохраняет пушауты, то он сохраняет эпиморфизмы.

LaTeX

$$$\\forall f:X\\to Y,\\ preservesColimit(\\mathrm{span}(f,f)) F \\land \\ epi f \\Rightarrow epi(F.map f)$$$

Lean4

/-- If `F` preserves pushouts, then it preserves epimorphisms. -/
theorem preserves_epi_of_preservesColimit {X Y : C} (f : X ⟶ Y) [PreservesColimit (span f f) F] [Epi f] :
    Epi (F.map f) :=
  by
  have := isColimitPushoutCoconeMapOfIsColimit F _ (PushoutCocone.isColimitMkIdId f)
  simp_rw [F.map_id] at this
  apply PushoutCocone.epi_of_isColimitMkIdId _ this

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