strongEpi_of_regularEpi — Mathlib

English

From a regular epi, deduce a strong epi.

Русский

Из регулярного эпиморфизма следует сильный эпиморфизм.

LaTeX

$$[RegularEpi f] ⇒ [StrongEpi f]$$

Lean4

instance (priority := 100) strongEpi_of_regularEpi (f : X ⟶ Y) [RegularEpi f] : StrongEpi f :=
  StrongEpi.mk'
    (by
      intro A B z hz u v sq
      have : (RegularEpi.left : RegularEpi.W f ⟶ X) ≫ u = RegularEpi.right ≫ u :=
        by
        apply (cancel_mono z).1
        simp only [Category.assoc, sq.w, RegularEpi.w_assoc]
      obtain ⟨t, ht⟩ := RegularEpi.desc' f u this
      exact CommSq.HasLift.mk' ⟨t, ht, (cancel_epi f).1 (by simp only [← Category.assoc, ht, ← sq.w])⟩)

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