explicitCokernelDesc_unique — Mathlib

English

If explicitCokernelπ f ≫ e = g and g = explicitCokernelDesc w, then e = explicitCokernelDesc w.

Русский

Если explicitCokernelπ f ≫ e = g и g = explicitCokernelDesc w, то e = explicitCokernelDesc w.

LaTeX

$$$explicitCokernelπ f \\\\circ e = g \\\\Rightarrow e = explicitCokernelDesc(w).$$$

Lean4

theorem explicitCokernelDesc_unique {X Y Z : SemiNormedGrp.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (w : f ≫ g = 0)
    (e : explicitCokernel f ⟶ Z) (he : explicitCokernelπ f ≫ e = g) : e = explicitCokernelDesc w :=
  by
  apply (isColimitCokernelCocone f).uniq (Cofork.ofπ g (by simp [w]))
  rintro (_ | _)
  · convert w.symm
    simp
  · exact he

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