English
If a diagram H: K ⥤ Over (colimit F) is filtered and has a colimit expressed via isColimit, then there exists an index k with a limit after evaluation, mirroring the colimit's computation.
Русский
Если диаграмма H: K ⥤ Over (colimit F) финально упорядочена и имеет предел, выражаемый через isColimit, то существует индекс k, для которого предел после оценки существует.
LaTeX
$$$[IsFiltered K] \\Rightarrow \\exists k, Nonempty\\,\\left(\\lim\\_{\\mathcal{G}} \\mathsf{yoneda.obj}(H.obj k)\\right)$$$
Lean4
theorem exists_nonempty_limit_obj_of_isColimit [IsFiltered K] {c : Cocone H} (hc : IsColimit c) (T : Over (colimit F))
(hT : c.pt ≅ T) (h : Nonempty <| limit <| 𝒢 ⋙ yoneda.obj T) : ∃ k, Nonempty <| limit <| 𝒢 ⋙ yoneda.obj (H.obj k) :=
by
refine exists_nonempty_limit_obj_of_colimit F G H ?_
suffices T ≅ colimit H from Nonempty.map (lim.map (whiskerLeft 𝒢 (yoneda.map this.hom))) h
refine hT.symm ≪≫ IsColimit.coconePointUniqueUpToIso hc (colimit.isColimit _)
