hasColimitsOfShape_of_coreflective

English

If C has shape-J limits and R is coreflective, then D has shape-J limits.

Русский

Если C имеет пределы формы J и R является ядром-отражателем, то D имеет пределы формы J.

LaTeX

$$$\\operatorname{HasLimitsOfShape} J C \\Rightarrow (\\text{Coreflective } R \\Rightarrow \\operatorname{HasLimitsOfShape} J D).$$$

Lean4

/-- If `C` has colimits of shape `J` then any coreflective subcategory has colimits of shape `J`. -/
theorem hasColimitsOfShape_of_coreflective [HasColimitsOfShape J C] (R : D ⥤ C) [Coreflective R] :
    HasColimitsOfShape J D :=
  ⟨fun F => hasColimit_of_coreflective F R⟩

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