hasLimitsOfShape_of_reflective — Mathlib

English

If a category C has limits of shape J and R: D → C is reflective, then D has limits of shape J.

Русский

Если категория C имеет пределы по форме J и R: D ⥤ C является отражательной, то D имеет пределы по форме J.

LaTeX

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

Lean4

/-- If `C` has limits of shape `J` then any reflective subcategory has limits of shape `J`. -/
theorem hasLimitsOfShape_of_reflective [HasLimitsOfShape J C] (R : D ⥤ C) [Reflective R] : HasLimitsOfShape J D :=
  ⟨fun F => hasLimit_of_reflective F R⟩

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