isIndObject_limit_comp_yoneda — Mathlib

English

If a limit exists for F: J → C, then the Ind-object given by limit(F ⋙ yoneda) is Ind.

Русский

Если предел существует для F: J → C, то Ind-объект $\\mathrm{limit}(F \\cdot \\mathrm{yoneda})$ есть.

LaTeX

$$$\\forall F:\\mathrm{Funct}(J, C)\\,[\\mathrm{HasLimit}\;F]\\;\\Longrightarrow\\; \\mathrm{IsIndObject}(\\mathrm{limit}(F \\odot \\mathrm{yoneda}))$$$

Lean4

/-- If a limit already exists in `C`, then the limit of the image of the diagram under the Yoneda
embedding is an ind-object. -/
theorem isIndObject_limit_comp_yoneda {J : Type u'} [Category.{v'} J] (F : J ⥤ C) [HasLimit F] :
    IsIndObject (limit (F ⋙ yoneda)) :=
  IsIndObject.map (preservesLimitIso yoneda F).hom (isIndObject_yoneda (limit F))

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