hasLimits_of_reflective — Mathlib

English

If C has all limits of a given size, and R: D → C is reflective, then D has all limits of that size.

Русский

Если C имеет все пределы заданного размера, и R: D → C является отражательной, то D имеет все пределы этого размера.

LaTeX

$$$\\operatorname{HasLimitsOfSize}_{v,u}(C) \\Rightarrow \\bigl(\\text{Reflective}(R) \\implies \\operatorname{HasLimitsOfSize}_{v,u}(D)\\bigr).$$$

Lean4

/-- If `C` has limits then any reflective subcategory has limits. -/
theorem hasLimits_of_reflective (R : D ⥤ C) [HasLimitsOfSize.{v, u} C] [Reflective R] : HasLimitsOfSize.{v, u} D :=
  ⟨fun _ => hasLimitsOfShape_of_reflective R⟩

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