natIso — Mathlib

English

The colimit of F represents the functor W ↦ cocones on F with cone point W; i.e. there is a natural isomorphism coyoneda.obj(op t.pt) ⋙ ulift ≅ F.cocones.

Русский

Колимит F представляет функтор W ↦ коконы над F с вершиной W; то есть существует естественное изоморфизм coyoneda.obj(op t.pt) ⋙ ulift ≅ F.cocones.

LaTeX

$$$\mathrm{natIso}(h):\; \mathrm{coyoneda.obj}(\mathrm{op}\; t.\mathrm{pt}) \;\circ\; \mathrm{uliftFunctor} \;\cong\; F.\mathrm{cocones}$$$

Lean4

/-- The colimit of `F` represents the functor taking `W` to
  the set of cocones on `F` with cone point `W`. -/
def natIso (h : IsColimit t) : coyoneda.obj (op t.pt) ⋙ uliftFunctor.{u₁} ≅ F.cocones :=
  NatIso.ofComponents (IsColimit.homIso h)

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