desc_extend — Mathlib

English

For a cocone c and any f: c.pt ⟶ X, the identity desc extended by f equals the composition desc c followed by f.

Русский

Для кокона c и любого f: c.pt ⟶ X, равенство desc F (c.extend f) = desc F c ∘ f выполняется.

LaTeX

$$$\\operatorname{colimit.desc} F (c.\\text{extend} f) = \\operatorname{colimit.desc} F c \\circ f$$$

Lean4

theorem desc_extend (F : J ⥤ C) [HasColimit F] (c : Cocone F) {X : C} (f : c.pt ⟶ X) :
    colimit.desc F (c.extend f) = colimit.desc F c ≫ f := by ext1; rw [← Category.assoc];
  simp
    -- This has the isomorphism pointing in the opposite direction than in `has_limit_of_iso`.
    -- This is intentional; it seems to help with elaboration.

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