epi_iff_forall_injective — Mathlib

English

An arrow f is epi iff for every object Z the map g: Y → Z, given by g ↦ f ∘ g, is injective.

Русский

Стрелка f — эпиморфизм тогда и только тогда, когда для каждого Z отображение g: Y → Z, заданное g ↦ f ∘ g, инъективно.

LaTeX

$$$$\\mathrm{Epi}(f) \\iff \\forall Z, \\operatorname{Injective}(\\lambda g:Y\\to Z, f\\circ g).$$$$

Lean4

/-- `f : X ⟶ Y` is an epimorphism iff for all `Z`, composition of morphisms `Y ⟶ Z` with `f`
is injective. -/
theorem epi_iff_forall_injective {X Y : C} (f : X ⟶ Y) : Epi f ↔ ∀ Z, (fun g : Y ⟶ Z ↦ f ≫ g).Injective :=
  ⟨fun _ _ _ _ hg ↦ (cancel_epi f).1 hg, fun h ↦ ⟨fun _ _ hg ↦ h _ hg⟩⟩

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