isColimitTautologicalCocone — Mathlib

Lean4

/-- The tautological cocone with point `P` is a colimit cocone, exhibiting `P` as a colimit of
    representables.

    Proposition 2.6.3(i) in [Kashiwara2006] -/
def isColimitTautologicalCocone (P : Cᵒᵖ ⥤ Type v₁) : IsColimit (tautologicalCocone P) :=
  let e :
    functorToRepresentables.{v₁} P ≅
      ((CategoryOfElements.costructuredArrowYonedaEquivalence P).functor ⋙ CostructuredArrow.proj yoneda P ⋙ yoneda) :=
    NatIso.ofComponents (fun e ↦ NatIso.ofComponents (fun X ↦ Equiv.ulift.toIso))
  (IsColimit.whiskerEquivalenceEquiv (CategoryOfElements.costructuredArrowYonedaEquivalence P)).2
    ((IsColimit.precomposeHomEquiv e _).1 (colimitOfRepresentable.{v₁} P))

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