English
If C has shape-J colimits and R coreflective, then D has shape-J colimits.
Русский
Если C имеет колимиты по форме J и R является coreflective, то D имеет колимиты по форме J.
LaTeX
$$$\\operatorname{HasColimitsOfShape} J C \\Rightarrow (\\text{Coreflective } R \\Rightarrow \\operatorname{HasColimitsOfShape} J D).$$$
Lean4
/-- The coreflector always preserves initial objects. Note this in general doesn't apply to any
other colimit.
-/
theorem rightAdjoint_preservesInitial_of_coreflective (R : D ⥤ C) [Coreflective R] :
PreservesColimitsOfShape (Discrete.{v} PEmpty) (comonadicRightAdjoint R) where
preservesColimit
{K} := by
let F := Functor.empty.{v} D
letI : PreservesColimit (F ⋙ R) (comonadicRightAdjoint R) :=
by
constructor
intro c h
haveI : HasColimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
haveI : HasColimit F := hasColimit_of_coreflective F R
constructor
apply isColimitChangeEmptyCocone D (colimit.isColimit F)
apply (asIso ((comonadicAdjunction R).unit.app _)).trans
apply (comonadicRightAdjoint R).mapIso
letI := comonadicCreatesColimits.{v, v} R
let A := CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit F R
apply (isColimitOfPreserves _ (colimit.isColimit F)).coconePointUniqueUpToIso h
apply preservesColimit_of_iso_diagram _ (Functor.emptyExt (F ⋙ R) _)
