English
If C has colimits of shape J and R: D → C is reflective, then D has colimits of shape J.
Русский
Если C имеет колимиты по форме J и R: D → C является отражательной, то D имеет колимиты по форме J.
LaTeX
$$$\\text{Reflective}(R) \\wedge \\operatorname{HasColimitsOfShape}(J,C) \\Rightarrow \\operatorname{HasColimitsOfShape}(J,D).$$$
Lean4
/-- If `C` has colimits of shape `J` then any reflective subcategory has colimits of shape `J`. -/
theorem hasColimitsOfShape_of_reflective (R : D ⥤ C) [Reflective R] [HasColimitsOfShape J C] : HasColimitsOfShape J D
where
has_colimit := fun F => by
let c := (monadicLeftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
letI : PreservesColimitsOfShape J _ := (monadicAdjunction R).leftAdjoint_preservesColimits.1
let t : IsColimit c := isColimitOfPreserves (monadicLeftAdjoint R) (colimit.isColimit _)
apply HasColimit.mk ⟨_, (IsColimit.precomposeInvEquiv _ _).symm t⟩
apply (isoWhiskerLeft F (asIso (monadicAdjunction R).counit) :) ≪≫ F.rightUnitor
