colimitPresentationCompYoneda — Mathlib

Lean4

/-- An ind-object `X` is the colimit (in `Ind C`!) of the filtered diagram presenting it. -/
noncomputable def colimitPresentationCompYoneda (X : Ind C) : colimit (X.presentation.F ⋙ Ind.yoneda) ≅ X :=
  Ind.inclusion.fullyFaithful.isoEquiv.symm <|
    calc
      (Ind.inclusion C).obj (colimit (X.presentation.F ⋙ Ind.yoneda)) ≅
          colimit (X.presentation.F ⋙ Ind.yoneda ⋙ Ind.inclusion C) :=
        preservesColimitIso _ _
      _ ≅ colimit (X.presentation.F ⋙ yoneda) :=
        (HasColimit.isoOfNatIso (isoWhiskerLeft X.presentation.F Ind.yonedaCompInclusion))
      _ ≅ (Ind.inclusion C).obj X := IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) X.presentation.isColimit

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