existsUnique — Mathlib

English

Let f,g: X → Y be morphisms with HasCoequalizer f g, and for some W and k: Y → W with f ≫ k = g ≫ k, there exists a unique d: coequalizer f g → W such that coequalizer.π f g ≫ d = k.

Русский

Пусть существуют косеквелайзеры f,g: X → Y; для произвольного W и k: Y → W, удовлетворяющего f ≫ k = g ≫ k, существует единственный d: coequalizer f g → W такой, что coequalizer.π f g ≫ d = k.

LaTeX

$$$ \\exists! d: \\mathrm{coequalizer} f g \\to W, \\; \\mathrm{coequalizer}.\\pi f g \\to d = k $$$

Lean4

theorem existsUnique {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) : ∃! d : coequalizer f g ⟶ W, coequalizer.π f g ≫ d = k :=
  Cofork.IsColimit.existsUnique (colimit.isColimit _) _ h

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