English
Let G be a family of objects indexed by ι in a category C, κ a regular cardinal, and h a cardinal-filtered generators data. Then for every j in the index J X, the diagonal presentation object (h.colimitPresentation X).diag.obj j is κ-presentable.
Русский
Пусть G — семейство объектов, индексированное по ι в категории C, κ — регулярный кардинал, и задан некий набор данных о кардинально-фильтрованных генераторах. Тогда для каждого j из индекса J X диагональный презентационный объект (h.colimitPresentation X).diag.obj j является κ-презентируемым.
LaTeX
$$$\forall j : h.J X,\ IsCardinalPresentable(((h.colimitPresentation X).diag.obj j), \kappa) $$$
Lean4
instance (j : h.J X) : IsCardinalPresentable.{w} ((h.colimitPresentation X).diag.obj j) κ :=
by
obtain ⟨i, ⟨e⟩⟩ := h.exists_colimitPresentation_diag_obj_iso X j
have := h.isCardinalPresentable
exact isCardinalPresentable_of_iso e.symm κ
