isLimit_iff_isIso_fst — Mathlib

English

If the terminal object is Y and c is a binary fan X → Y, then c is a limit iff its left projection is an isomorphism.

Русский

Если Y является терминальным объектом, а c — двоичный фан X → Y, то c является пределом тогда и только тогда, когда его левая проекция является изоморфизмом.

LaTeX

$$$$ (\exists H: IsLimit\, c) \iff IsIso(c.fst). $$$$

Lean4

theorem isLimit_iff_isIso_fst {X Y : C} (h : IsTerminal Y) (c : BinaryFan X Y) : Nonempty (IsLimit c) ↔ IsIso c.fst :=
  by
  constructor
  · rintro ⟨H⟩
    obtain ⟨l, hl, -⟩ := BinaryFan.IsLimit.lift' H (𝟙 X) (h.from X)
    exact
      ⟨⟨l, BinaryFan.IsLimit.hom_ext H (by simpa [hl, -Category.comp_id] using Category.comp_id _) (h.hom_ext _ _), hl⟩⟩
  · intro
    exact
      ⟨BinaryFan.IsLimit.mk _ (fun f _ => f ≫ inv c.fst) (fun _ _ => by simp) (fun _ _ => h.hom_ext _ _)
          fun _ _ _ e _ => by simp [← e]⟩

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