epi_iff_mk_eq_top — Mathlib

English

In a balanced category, a morphism f is epi if and only if Subobject.mk f = ⊤.

Русский

В сбалансированной категории морфизм f эпиморфизм тогда и только тогда, когда Subobject.mk f = ⊤.

LaTeX

$$$\text{Epi } f \iff \operatorname{Subobject}.mk f = \top$$$

Lean4

theorem epi_iff_mk_eq_top [Balanced C] (f : X ⟶ Y) [Mono f] : Epi f ↔ Subobject.mk f = ⊤ :=
  by
  rw [← isIso_iff_mk_eq_top]
  exact ⟨fun _ ↦ isIso_of_mono_of_epi f, fun _ ↦ inferInstance⟩

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