imageToKernel_epi_of_epi_of_zero — Mathlib

English

If g is epi and the left morphism f is arbitrary with f ≫ 0 ≡ 0, then imageToKernel f 0 is epi.

Русский

Если g ⟶ C является эпиморфизмом и f ⟶ B произвольна, то imageToKernel f 0 является эпиморфизмом.

LaTeX

$$Epi (imageToKernel f 0 ⋯)$$

Lean4

/-- `imageToKernel` for `A --f--> B --0--> C`, where `g` is an epi is itself an epi
(i.e. the sequence is exact at `B`).
-/
instance imageToKernel_epi_of_epi_of_zero [HasImages V] [Epi f] : Epi (imageToKernel f (0 : B ⟶ C) (by simp)) :=
  by
  simp only [imageToKernel_zero_right]
  haveI := epi_image_of_epi f
  rw [← imageSubobject_arrow]
  infer_instance

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