English
In a category with pullbacks, ExtremalEpi f is equivalent to StrongEpi f; moreover, ExtremalEpi f implies StrongEpi f and vice versa when pullbacks exist.
Русский
В категории с пуллбэками экстремальная эпиморфия f эквивалентна сильной эпиморфии f; более того, экстремальная эпиморфия эквивалентна сильной, если существуют пуллбэки.
LaTeX
$$$[HasPullbacks C]\\; \\Rightarrow\\; (ExtremalEpi\\ f \\iff StrongEpi\\ f)$$$
Lean4
theorem extremalEpi_iff_strongEpi_of_hasPullbacks [HasPullbacks C] : ExtremalEpi f ↔ StrongEpi f :=
by
refine ⟨fun _ ↦ ⟨inferInstance, fun A B i _ ↦ ⟨fun {t b} sq ↦ ⟨⟨?_⟩⟩⟩⟩, fun _ ↦ inferInstance⟩
have := ExtremalEpi.isIso f (pullback.lift _ _ sq.w) (pullback.snd _ _) (by simp)
exact
{ l := inv (pullback.snd i b) ≫ pullback.fst _ _
fac_left := by
rw [← cancel_mono i, sq.w, Category.assoc, Category.assoc]
congr 1
rw [← cancel_epi (pullback.snd i b), IsIso.hom_inv_id_assoc, pullback.condition]
fac_right := by simp [pullback.condition] }
