π_comp_cokernelIsoOfEq_hom — Mathlib

English

For f and g with a cokernel, and when h: f = g, the equation π g ≫ (cokernelIsoOfEq h).hom = π f holds; and similarly for inv.

Русский

Если f и g имеют коканал, и h: f = g, то π g ≫ (cokernelIsoOfEq h).hom = π f и аналогично с inv.

LaTeX

$$$\pi_g \circ (cokernelIsoOfEq(h)).hom = \pi_f$ and $\pi_g \circ (cokernelIsoOfEq(h)).inv = \pi_f$ (согласно h).$$

Lean4

@[reassoc (attr := simp)]
theorem π_comp_cokernelIsoOfEq_hom {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) :
    cokernel.π f ≫ (cokernelIsoOfEq h).hom = cokernel.π g := by cases h; simp

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