cokernelIsoOfEq_inv_comp_desc — Mathlib

English

In the inverse direction, (cokernelIsoOfEq h).inv ≫ cokernel.desc _ e he = cokernel.desc _ e (by simp [← h, he]).

Русский

В отношении противолежащего направления: (cokernelIsoOfEq h).inv ≫ cokernel.desc _ e he = cokernel.desc _ e (by simp [← h, he]).

LaTeX

$$$(cokernelIsoOfEq(h)).inv \circ cokernel.desc\_f e he = cokernel.desc\_f e (by simp [\Leftarrow h, he])$$$

Lean4

@[reassoc (attr := simp)]
theorem cokernelIsoOfEq_inv_comp_desc {Z} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) (e : Y ⟶ Z) (he) :
    (cokernelIsoOfEq h).inv ≫ cokernel.desc _ e he = cokernel.desc _ e (by simp [← h, he]) := by cases h; simp

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