English
If a limit exists in a certain Ind-object construction after Yoneda embedding and indexed by a connected category, then there exists a further index k such that the corresponding limit object is nonempty. This is a step in showing filtered colimits preserve certain structures.
Русский
Если существует предел в построении Ind-объектов после вложения Янгиды и индексируемого связного множества, то найдется индекс k, для которого соответствующий предел не пуст. Это шаг к доказательству сохранения фильтрованных колимитов.
LaTeX
$$$\exists k \; (\text{limit} \rightarrow \text{Yoneda} (H.obj k) ) \neq \varnothing$$$
Lean4
theorem exists_nonempty_limit_obj_of_colimit [IsFiltered K] (h : Nonempty <| limit <| 𝒢 ⋙ yoneda.obj (colimit H)) :
∃ k, Nonempty <| limit <| 𝒢 ⋙ yoneda.obj (H.obj k) :=
by
obtain ⟨t⟩ := h
let t₂ := limMap (compYonedaColimitIsoColimitCompYoneda F G H).hom t
let t₃ := (colimitLimitIso (H ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj 𝒢).flip).inv t₂
obtain ⟨k, y, -⟩ := Types.jointly_surjective'.{v, max u v} t₃
refine ⟨k, ⟨?_⟩⟩
let z := (limitObjIsoLimitCompEvaluation (H ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj 𝒢).flip k).hom y
let y := flipCompEvaluation (H ⋙ yoneda ⋙ (whiskeringLeft _ _ _).obj 𝒢) k
exact (lim.mapIso y).hom z
