desc — Mathlib

English

Describes a unique morphism from the cowedge to X determined by a compatible family f_j.

Русский

Определяется единственный морфизм из cowedge в X, задаваемый совместимой семейством f_j.

LaTeX

$$$\\text{Cowedge.IsColimit.desc}\\ hc\\ f hf : c.pt \\to X$$$

Lean4

/-- Construct a morphism from the coend using its universal property. -/
def desc (hc : IsColimit c) {X : C} (f : ∀ j, (F.obj (op j)).obj j ⟶ X)
    (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j) : c.pt ⟶ X :=
  Multicofork.IsColimit.desc hc f (fun _ ↦ hf _)

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