isIso_limMap_π — Mathlib

English

For a cone c with a limit, the map limMap c.π is an isomorphism.

Русский

Для предела конуса c отображение limMap c.π является изоморфизмом.

LaTeX

$$$\mathrm{IsIso}(\mathrm{limMap}(c.\pi))$$$

Lean4

theorem isIso_limMap_π {F : J ⥤ C} [HasLimit F] {c : Cone F} (hc : IsLimit c) : IsIso (limMap c.π) :=
  by
  suffices
    limMap c.π =
      ((limit.isLimit _).conePointUniqueUpToIso (isLimitConstCone J c.pt) ≪≫
          hc.conePointUniqueUpToIso (limit.isLimit _)).hom
    by rw [this]; infer_instance
  ext j
  simp only [limMap_π, Functor.const_obj_obj, limit.cone_x, constCone_pt, Iso.trans_hom, assoc,
    limit.conePointUniqueUpToIso_hom_comp]
  congr 1
  simp [← Iso.inv_comp_eq_id]

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