epi_iff_epi_app — Mathlib

English

For a natural transformation f: F ⟶ G, Epi f holds if and only if every component f.app k is epi (assuming HasPushouts).

Русский

Для натурального преобразования f: F ⟶ G условие Epi f выполняется тогда и только тогда, когда каждый компонент f.app k является эпиморфизмом (при условии наличия pushouts).

LaTeX

$$$\\operatorname{Epi} f \\iff \\forall k, \\operatorname{Epi}(f.app k).$$$

Lean4

theorem epi_iff_epi_app : Epi f ↔ ∀ (k : K), Epi (f.app k) :=
  ⟨fun _ ↦ inferInstance, fun _ ↦ epi_of_epi_app _⟩

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