reflects_epi_of_reflectsColimit — Mathlib

English

If F reflects colimits, then it reflects epimorphisms.

Русский

Если F отражает колимиты, тогда он отражает эпиморфизмы.

LaTeX

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

Lean4

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

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