desc_epi — Mathlib

English

If k: Y → W is epi, then cokernel.desc f k h is also epi for any h with f ≫ k = 0.

Русский

Если k: Y → W эпиморфизм, то cokernel.desc f k h также эпиморфизм при любом h с f ≫ k = 0.

LaTeX

$$$[Epi\ k] \Rightarrow Epi\ (cokernel.desc f k h)$$$

Lean4

instance desc_epi {W : C} (k : Y ⟶ W) (h : f ≫ k = 0) [Epi k] : Epi (cokernel.desc f k h) :=
  ⟨fun {Z} g g' w => by
    replace w := cokernel.π f ≫= w
    simp only [cokernel.π_desc_assoc] at w
    exact (cancel_epi k).1 w⟩

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