English
If a functor reflects limits, then it reflects limits at the smallest universe as well.
Русский
Если функтор отражает пределы, он отражает пределы в наименьшей вселенной.
LaTeX
$$$\\mathrm{ReflectsLimitsOfSize}\\,F \\Rightarrow \\mathrm{ReflectsLimitsOfSize}\\,0\\,0\\,F$$$
Lean4
/-- If the limit of `F` exists and `G` preserves it, then if `G` reflects isomorphisms then it
reflects the limit of `F`.
-/ -- Porting note: previous behavior of apply pushed instance holes into hypotheses, this errors
theorem reflectsLimit_of_reflectsIsomorphisms (F : J ⥤ C) (G : C ⥤ D) [G.ReflectsIsomorphisms] [HasLimit F]
[PreservesLimit F G] : ReflectsLimit F G where
reflects {c}
t := by
suffices IsIso (IsLimit.lift (limit.isLimit F) c) from ⟨by apply IsLimit.ofPointIso (limit.isLimit F)⟩
change IsIso ((Cones.forget _).map ((limit.isLimit F).liftConeMorphism c))
suffices IsIso (IsLimit.liftConeMorphism (limit.isLimit F) c) from by apply (Cones.forget F).map_isIso _
suffices IsIso ((Cones.functoriality F G).map (IsLimit.liftConeMorphism (limit.isLimit F) c)) from by
apply isIso_of_reflects_iso _ (Cones.functoriality F G)
exact t.hom_isIso (isLimitOfPreserves G (limit.isLimit F)) _
