instExtremalEpiOfStrongEpi — Mathlib

English

If f is a StrongEpimorphism, then f is an ExtremalEpi.

Русский

Если f является сильной эпиморфией, то она является экстремальной эпиморфией.

LaTeX

$$$\\forall X,Y\\; (f:X\\to Y),\\; [\\text{StrongEpi } f]\\; \\Rightarrow\\; ExtremalEpi\\ f$$

Lean4

instance [StrongEpi f] : ExtremalEpi f where
  isIso {Z} p i fac
    _ := by
    have sq : CommSq p f i (𝟙 Y) := { }
    exact ⟨sq.lift, by simp [← cancel_mono i], by simp⟩

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