hasLimits_of_coreflective — Mathlib

English

If C has size- limits and R coreflective, then D has size- limits.

Русский

Если C имеет пределы заданного размера и R(corefle) — ядроотражатель, тогда D имеет пределы заданного размера.

LaTeX

$$$\\operatorname{HasLimitsOfSize}_{v,u} C \\Rightarrow (\\text{Coreflective } R \\Rightarrow \\operatorname{HasLimitsOfSize}_{v,u} D).$$$

Lean4

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

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