surjective_of_epi_of_preservesPushout

English

If f is an epimorphism and the forgetful functor preserves pushouts of shape WalkingSpan, the underlying map of f is surjective.

Русский

Если f является эпиморфизмом и забывающий функтор сохраняет пуш-диаграммы формы WalkingSpan, то базовая функция f сюръективна.

LaTeX

$$$\\operatorname{Epi}(f) \\Rightarrow \\operatorname{Surjective}(((\\mathrm{forget}\\,C).map f))$$$

Lean4

theorem surjective_of_epi_of_preservesPushout {X Y : C} (f : X ⟶ Y) [Epi f]
    [PreservesColimitsOfShape WalkingSpan (forget C)] : Function.Surjective f :=
  (epi_iff_surjective ((forget C).map f)).mp inferInstance

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