English
The reflector preserves terminal objects.
Русский
Рефлектор сохраняет терминальные объекты.
LaTeX
$$$\\text{PreservesLimitsOfShape}(\\mathrm{Discrete}\\,\\mathrm{PEmpty}, \\mathrm{monadicLeftAdjoint}\\;R).$$$
Lean4
/-- The reflector always preserves terminal objects. Note this in general doesn't apply to any other
limit.
-/
theorem leftAdjoint_preservesTerminal_of_reflective (R : D ⥤ C) [Reflective R] :
PreservesLimitsOfShape (Discrete.{v} PEmpty) (monadicLeftAdjoint R) where
preservesLimit
{K} := by
let F := Functor.empty.{v} D
letI : PreservesLimit (F ⋙ R) (monadicLeftAdjoint R) :=
by
constructor
intro c h
haveI : HasLimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
haveI : HasLimit F := hasLimit_of_reflective F R
constructor
apply isLimitChangeEmptyCone D (limit.isLimit F)
apply (asIso ((monadicAdjunction R).counit.app _)).symm.trans
apply (monadicLeftAdjoint R).mapIso
letI := monadicCreatesLimits.{v, v} R
let A := CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit F R
apply (isLimitOfPreserves _ (limit.isLimit F)).conePointUniqueUpToIso h
apply preservesLimit_of_iso_diagram _ (Functor.emptyExt (F ⋙ R) _)
