π_desc — Mathlib

English

If f: X → Y is cokernel, and k: Y → W with f ≫ k = 0, then cokernel.π f ≫ cokernel.desc f k h = k for h expressing the zero relation.

Русский

Пусть f: X→Y — коканал, и k: Y→W удовлетворяющее f ≫ k = 0; тогда cokernel.π f ≫ cokernel.desc f k h = k.

LaTeX

$$$\forall f:\; X\to Y,\; \forall k:\; Y\to W,\; (f\;\gg\; k = 0)\Rightarrow cokernel.π f \;\gg\; cokernel.desc f k (f\ggk=0) = k$$$

Lean4

@[reassoc (attr := simp)]
theorem π_desc {W : C} (k : Y ⟶ W) (h : f ≫ k = 0) : cokernel.π f ≫ cokernel.desc f k h = k :=
  (cokernelIsCokernel f).fac (CokernelCofork.ofπ k h) WalkingParallelPair.one

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