cokernelZeroIsoTarget_hom — Mathlib

English

For any f, g with f ≫ g = 0, the composition colimit.ι (parallelPair f 0) WalkingParallelPair.zero ≫ cokernel.desc f g h equals 0.

Русский

Для любых f, g с f ≫ g = 0 композиция colimit.ι (parallelPair f 0) WalkingParallelPair.zero ≫ cokernel.desc f g h равна 0.

LaTeX

$$$\text{If } f:\,X\to Y, g:\,Y\to Z, h:f\to g=0\Rightarrow (colimit.ι(\parallelPair f 0)\WalkingParallelPair.zero) \;\gg\; cokernel.desc f g h = 0$$$

Lean4

@[simp]
theorem cokernelZeroIsoTarget_hom : cokernelZeroIsoTarget.hom = cokernel.desc (0 : X ⟶ Y) (𝟙 Y) (by simp) := by ext;
  simp [cokernelZeroIsoTarget]

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