hasColimits_of_reflective — Mathlib

English

If C has colimits, then any reflective subcategory D has colimits.

Русский

Если C имеет колимиты, то любая отражательная подкатегория D имеет колимиты.

LaTeX

$$$\\operatorname{HasColimitsOfSize}(C) \\Rightarrow \\bigl(\\text{Reflective}(R) \\Rightarrow \\operatorname{HasColimitsOfSize}(D)\\bigr).$$$

Lean4

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

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