isLimit_iff_isIso_limMap_π — Mathlib

English

Same as above for a simplified instance, that limMap c.π is an isomorphism when c is a limit.

Русский

То же самое для упрощенного случая: limMap c.π — изоморфизм, если c является пределом.

LaTeX

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

Lean4

theorem isLimit_iff_isIso_limMap_π {F : J ⥤ C} [HasLimit F] (c : Cone F) : Nonempty (IsLimit c) ↔ IsIso (limMap c.π) :=
  ⟨fun ⟨h⟩ => IsLimit.isIso_limMap_π h, fun _ => ⟨c.isLimitOfIsIsoLimMapπ⟩⟩

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