isIso_ι_app_of_isTerminal — Mathlib

English

For a diagram F and cocone c with hc : IsColimit c and X, if X is terminal, then c.ι.app X is an isomorphism.

Русский

Для диаграммы F и кокона c с hc : IsColimit c, если X терминален, то c.ι.app X является изоморфизмом.

LaTeX

$$$\\text{hc : IsColimit } c \\land \\text{IsTerminal } X \\Rightarrow \\IsIso (c.\\ι.app X)$$$

Lean4

theorem isIso_ι_app_of_isTerminal {F : J ⥤ C} {c : Cocone F} (hc : IsColimit c) (X : J) (hX : IsTerminal X) :
    IsIso (c.ι.app X) :=
  by
  change IsIso (coconePointUniqueUpToIso (colimitOfDiagramTerminal hX F) hc).hom
  infer_instance

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