colimit_ι_zero_cokernel_desc — Mathlib

English

If h is such that f ≫ h = 0, then cokernel.desc f 0 h = 0.

Русский

Если h удовлетворяет f ≫ h = 0, то cokernel.desc f 0 h = 0.

LaTeX

$$$\forall f:\; X\to Y,\; \forall W:\; \;\forall h,\; f \gg 0 = 0 \Rightarrow cokernel.desc\ f\ 0\ h = 0$$$

Lean4

@[reassoc (attr := simp)]
theorem colimit_ι_zero_cokernel_desc {C : Type*} [Category C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
    (h : f ≫ g = 0) [HasCokernel f] : colimit.ι (parallelPair f 0) WalkingParallelPair.zero ≫ cokernel.desc f g h = 0 :=
  by
  rw [(colimit.w (parallelPair f 0) WalkingParallelPairHom.left).symm]
  simp

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