existsUnique — Mathlib

English

Let s be a Cofork over f,g with IsColimit. For any W, and any k: Y→W with f ≫ k = g ≫ k, there exists a unique d: s.pt ⟶ W such that Cofork.π s ≫ d = k.

Русский

Пусть s — кофор над f,g с IsColimit. Для любого W и любого k: Y→W с f ≫ k = g ≫ k существует единственный d: s.pt ⟶ W такой, что Cofork.π s ≫ d = k.

LaTeX

$$$\\exists! d:\\; s.pt \\to W,\\; Cofork.π s \\to d = k$$$

Lean4

theorem existsUnique {s : Cofork f g} (hs : IsColimit s) {W : C} (k : Y ⟶ W) (h : f ≫ k = g ≫ k) :
    ∃! d : s.pt ⟶ W, Cofork.π s ≫ d = k :=
  ⟨hs.desc <| Cofork.ofπ _ h, hs.fac _ _, fun _ hm =>
    Cofork.IsColimit.hom_ext hs <| hm.symm ▸ (hs.fac (Cofork.ofπ _ h) WalkingParallelPair.one).symm⟩

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