hasColimits_of_coreflective — Mathlib

English

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

Русский

Если C имеет колимиты, то любая подкатегория D с ядром-флективной имеет колимиты.

LaTeX

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

Lean4

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

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