cokernel_funext — Mathlib

English

In a concrete category with cokernel f, two maps g,h from cokernel f to K are equal if they agree on all cokernel-π components.

Русский

В конкретной категории с кокернелем f две стрелки g,h: cokernel f → K равны, если они согласованы на всех компонентах π f.

LaTeX

$$$\\forall n,\\ g(\\mathrm{cokernel.π}\; f\\ n) = h(\\mathrm{cokernel.π}\\ f\\ n) \\Rightarrow g=h$$$

Lean4

theorem cokernel_funext {C : Type*} [Category C] [HasZeroMorphisms C] {FC : C → C → Type*} {CC : C → Type*}
    [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {M N K : C} {f : M ⟶ N} [HasCokernel f]
    {g h : cokernel f ⟶ K} (w : ∀ n : ToType N, g (cokernel.π f n) = h (cokernel.π f n)) : g = h :=
  by
  ext x
  simpa using w x

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