isColimit_iff_isIso_inr — Mathlib

English

If X is initial, then a binary cofan X → Y is colimit iff its right inclusion is an isomorphism.

Русский

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

LaTeX

$$$$ (\exists H: IsColimit\, c) \iff IsIso(c.inr). $$$$

Lean4

theorem isColimit_iff_isIso_inr {X Y : C} (h : IsInitial X) (c : BinaryCofan X Y) :
    Nonempty (IsColimit c) ↔ IsIso c.inr :=
  by
  refine Iff.trans ?_ (BinaryCofan.isColimit_iff_isIso_inl h (BinaryCofan.mk c.inr c.inl))
  exact
    ⟨fun h => ⟨BinaryCofan.isColimitFlip h.some⟩, fun h =>
      ⟨(BinaryCofan.isColimitFlip h.some).ofIsoColimit (isoBinaryCofanMk c).symm⟩⟩

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