English
Let P be an object property closed under isomorphisms. If for every diagram F: J ⥤ C with HasColimit F one has that P(F.obj j) for all j implies P(colimit F), then P is closed under colimits of shape J.
Русский
Пусть P — свойство объектов, замкнутое по изоморфизмам. Если для каждого диаграмма F: J ⥤ C с HasColimit F выполняется, что P(F.obj j) для всех j, тогда P(colimit F), то P замкнуто относительно ко-лимитов формы J.
LaTeX
$$$[P.IsClosedUnderIsomorphisms] \\Rightarrow (\\forall F: J ⥤ C\\,[HasColimit F]\\; (\\forall j, P(F.obj j)) \\Rightarrow P(\\operatorname{colimit} F)) \\Rightarrow \\operatorname{ClosedUnderColimitsOfShape} J P$$
Lean4
theorem closedUnderColimitsOfShape_of_colimit [P.IsClosedUnderIsomorphisms]
(h : ∀ {F : J ⥤ C} [HasColimit F], (∀ j, P (F.obj j)) → P (colimit F)) : ClosedUnderColimitsOfShape J P :=
by
intro F c hc hF
have : HasColimit F := ⟨_, hc⟩
exact P.prop_of_iso ((colimit.isColimit _).coconePointUniqueUpToIso hc) (h hF)
