epi_image_of_epi — Mathlib

English

If f: X → Y has an image, and image inclusion is epi, and factorThroughImage is epi, then image.ι f is epi.

Русский

Если у f существует образ, и инъекция образа является эпиморфизмом, и factorThroughImage является эпиморфизмом, то image.ι f — эпиморфизм.

LaTeX

$$$ [HasImage(f)] \\; Epi(image.f) \\Rightarrow Epi(image.ι(f)) $$$

Lean4

theorem epi_image_of_epi {X Y : C} (f : X ⟶ Y) [HasImage f] [E : Epi f] : Epi (image.ι f) :=
  by
  rw [← image.fac f] at E
  exact epi_of_epi (factorThruImage f) (image.ι f)

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