English
Let C be a category with equalizers. If for every Z and all p: X → Z and i: Z → Y with p ≫ i = f and i is mono, i is an isomorphism, then f is extremal epi.
Русский
Пусть C — категория, в которой существуют эквалайзеры. Если для любого объёма Z и любых отображений p: X → Z, i: Z → Y с условием p ∘ i = f и i моно, выполняется, что i является изоморфизмом, то f является экстремальным эпиморфизмом.
LaTeX
$$$[\\text{HasEqualizers } C] \\; \\Rightarrow\\; (\\forall Z\\; \\forall p:X\\to Z\\; \\forall i:Z\\to Y\\; (p\\circ i=f)\\;[Mono\\ i]\\; \\Rightarrow\\; IsIso\\ i) \\Rightarrow ExtremalEpi\\ f$$
Lean4
theorem mk_of_hasEqualizers [HasEqualizers C]
(hf : ∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y) (_ : p ≫ i = f) [Mono i], IsIso i) : ExtremalEpi f
where
left_cancellation {Z} p q
h := by
have := hf (equalizer.lift f h) (equalizer.ι p q) (by simp)
rw [← cancel_epi (equalizer.ι p q), equalizer.condition]
isIso := by tauto
