π_comp_cokernelComparison — Mathlib

English

For HasCokernel f and HasCokernel (G.map f), the equality cokernel.π (G.map f) ≫ cokernelComparison f G = G.map (cokernel.π f) holds.

Русский

Для f и G.map f с существующими котокernel-образами: cokernel.π (G.map f) ∘ cokernelComparison f G = G.map (cokernel.π f).

LaTeX

$$$cokernel.\pi (G.map f) \\circ\\ cokernelComparison f G = G.map (cokernel.\pi f)$$$

Lean4

@[reassoc (attr := simp)]
theorem π_comp_cokernelComparison [HasCokernel f] [HasCokernel (G.map f)] :
    cokernel.π (G.map f) ≫ cokernelComparison f G = G.map (cokernel.π _) :=
  cokernel.π_desc _ _ _

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