reflectsLimits_of_reflectsIsomorphisms

English

If F ≅ G and F reflects limits of shape J, then G reflects those limits of shape J.

Русский

Если F ≅ G и F отражает пределы формы J, то и G отражает пределы формы J.

LaTeX

$$$\\text{Iso}(F,G) \\Rightarrow [\\mathrm{ReflectsLimitsOfShape}\\,J\\,F] \\Rightarrow [\\mathrm{ReflectsLimitsOfShape}\\,J\\,G]$$$

Lean4

/-- If `C` has limits and `G` preserves limits, then if `G` reflects isomorphisms then it reflects
limits.
-/
theorem reflectsLimits_of_reflectsIsomorphisms {G : C ⥤ D} [G.ReflectsIsomorphisms] [HasLimitsOfSize.{w', w} C]
    [PreservesLimitsOfSize.{w', w} G] : ReflectsLimitsOfSize.{w', w} G where
  reflectsLimitsOfShape := reflectsLimitsOfShape_of_reflectsIsomorphisms

Похожие утверждения