reflectsColimit_of_reflectsColimitsOfShape

English

If F reflects colimits of shape J, then ReflectsColimit K F holds for any K.

Русский

Если F отражает колимиты по форме J, то ReflectsColimit K F выполняется для любой K.

LaTeX

$$$ \\text{ReflectsColimitsOfShape } J F \\Rightarrow \\text{ReflectsColimit } K F. $$$

Lean4

instance (priority := 100) reflectsColimit_of_reflectsColimitsOfShape (K : J ⥤ C) (F : C ⥤ D)
    [ReflectsColimitsOfShape J F] : ReflectsColimit K F :=
  ReflectsColimitsOfShape.reflectsColimit

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