reflectsLimitsOfShape_of_reflectsIsomorphisms

English

If F ≅ G and F reflects limits of a given size, then G reflects those limits.

Русский

Если F ≅ G и F отражает пределы заданного размера, то и G отражает эти пределы.

LaTeX

$$$F \\cong G \\Rightarrow [\\mathrm{ReflectsLimitsOfSize}\\,F] \\Rightarrow [\\mathrm{ReflectsLimitsOfSize}\\,G]$$$

Lean4

/-- If `C` has limits of shape `J` and `G` preserves them, then if `G` reflects isomorphisms then it
reflects limits of shape `J`.
-/
theorem reflectsLimitsOfShape_of_reflectsIsomorphisms {G : C ⥤ D} [G.ReflectsIsomorphisms] [HasLimitsOfShape J C]
    [PreservesLimitsOfShape J G] : ReflectsLimitsOfShape J G where
  reflectsLimit {F} := reflectsLimit_of_reflectsIsomorphisms F G

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