epi_of_epi_map — Mathlib

English

If F reflects epimorphisms, then epi in the map implies epi in the source.

Русский

Если F отражает эпиморфизмы, то эпиморфизм на отображении влечет за собой эпиморфизм исходного морфизма.

LaTeX

$$[F.ReflectsEpimorphisms] ∧ [Epi (F.map f)] ⇒ [Epi f]$$

Lean4

theorem epi_of_epi_map (F : C ⥤ D) [ReflectsEpimorphisms F] {X Y : C} {f : X ⟶ Y} (h : Epi (F.map f)) : Epi f :=
  ReflectsEpimorphisms.reflects f h

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