limitCompCoyonedaIsoCone — Mathlib

English

There is a canonical isomorphism between the limit of F ⋙ coyoneda.obj(op X) and the set of natural transformations from the constant functor at X to F.

Русский

Существует каноническое изоморфизм между пределом F ⋙ coyoneda.obj(op X) и множеством натуральных преобразований от константной функтор к F.

LaTeX

$$$\\mathrm{limit}(F \\circ (\\text{coyoneda.obj} (\\mathrm{op}\\ X))) \\cong ((\\mathrm{const}\\ J).obj X \\to F)$$$

Lean4

/-- A cone on `F` with cone point `X` is the same as an element of `lim Hom(X, F·)`. -/
@[simps!]
noncomputable def limitCompCoyonedaIsoCone (F : J ⥤ C) (X : C) :
    limit (F ⋙ coyoneda.obj (op X)) ≅ ((const J).obj X ⟶ F) :=
  ((Types.limitEquivSections _).trans (compCoyonedaSectionsEquiv F X)).toIso

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