English
If C has shape-J limits and R is coreflective, then D has shape-J limits.
Русский
Если C имеет пределы формы J и R является ядром-отражателем, то D имеет пределы формы J.
LaTeX
$$$\\operatorname{HasLimitsOfShape} J C \\Rightarrow (\\text{Coreflective } R \\Rightarrow \\operatorname{HasLimitsOfShape} J D).$$$
Lean4
/-- If `C` has limits of shape `J` then any coreflective subcategory has limits of shape `J`. -/
theorem hasLimitsOfShape_of_coreflective (R : D ⥤ C) [Coreflective R] [HasLimitsOfShape J C] : HasLimitsOfShape J D
where
has_limit := fun F => by
let c := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
letI : PreservesLimitsOfShape J _ := (comonadicAdjunction R).rightAdjoint_preservesLimits.1
let t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit _)
apply HasLimit.mk ⟨_, (IsLimit.postcomposeHomEquiv _ _).symm t⟩
apply (F.rightUnitor ≪≫ (isoWhiskerLeft F ((asIso (comonadicAdjunction R).unit) :))).symm
