isIso_colimMap_ι — Mathlib

English

For a cocone c with HasColimit, the map colimMap c.ι is an isomorphism.

Русский

Для кокона c с ко-лимитом отображение colimMap c.ι является изоморфизмом.

LaTeX

$$$\mathrm{IsIso}(\mathrm{colimMap}(c.\iota))$$$

Lean4

theorem isIso_colimMap_ι {F : J ⥤ C} [HasColimit F] {c : Cocone F} (hc : IsColimit c) : IsIso (colimMap c.ι) :=
  by
  suffices
    colimMap c.ι =
      ((colimit.isColimit _).coconePointUniqueUpToIso hc ≪≫
          (isColimitConstCocone J c.pt).coconePointUniqueUpToIso (colimit.isColimit _)).hom
    by rw [this]; infer_instance
  ext j
  simp only [ι_colimMap, Functor.const_obj_obj, colimit.cocone_x, Iso.trans_hom,
    colimit.comp_coconePointUniqueUpToIso_hom_assoc]
  congr 1
  simp [← Iso.comp_inv_eq_id]

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