cokernelComparison_map_desc — Mathlib

English

For HasCokernel f and HasCokernel (G.map f), and h : Y ⟶ Z with f ≫ h = 0, the equation cokernelComparison f G ≫ G.map (cokernel.desc f h w) = cokernel.desc (G.map f) (G.map h) (by ... ) holds.

Русский

При f и G.map f с условиями; для h: Y→Z с f∘h=0, выполняется равенство сравнения котокernel с описанием через h.

LaTeX

$$$cokernelComparison f G \;\circ\\ G.map (cokernel.desc f h w) = cokernel.desc (G.map f) (G.map h) (by \;simp)$$$

Lean4

@[reassoc (attr := simp)]
theorem cokernelComparison_map_desc [HasCokernel f] [HasCokernel (G.map f)] {Z : C} {h : Y ⟶ Z} (w : f ≫ h = 0) :
    cokernelComparison f G ≫ G.map (cokernel.desc _ h w) =
      cokernel.desc _ (G.map h) (by simp only [← G.map_comp, w, Functor.map_zero]) :=
  by ext; simp [← G.map_comp]

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