isColimitEquivIsInitial — Mathlib

English

A cocone c is a colimit cocone if and only if it is initial; i.e., IsColimit c ≃ IsInitial c.

Русский

Кокон является колимитным коконом тогда и только тогда, когда он является инициальным; IsColimit c эквивалентно IsInitial c.

LaTeX

$$$\\text{IsColimit}(c) \\simeq \\text{IsInitial}(c)$$$

Lean4

/-- A cocone is a colimit cocone iff it is initial. -/
def isColimitEquivIsInitial {F : J ⥤ C} (c : Cocone F) : IsColimit c ≃ IsInitial c :=
  IsColimit.isoUniqueCoconeMorphism.toEquiv.trans
    { toFun := fun _ => IsInitial.ofUnique _
      invFun := fun h s => ⟨⟨IsInitial.to h s⟩, fun a => IsInitial.hom_ext h a _⟩
      left_inv := by cat_disch
      right_inv := by cat_disch }

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