reflectsLimits_of_natIso — Mathlib

English

If there is a natural isomorphism h: F ≅ G and F reflects limits of shape J, then G reflects limits of shape J.

Русский

Если существует натуральная изоморфия h: F ≅ G и F отражает пределы формы J, то и G отражает пределы формы J.

LaTeX

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

Lean4

/-- Transfer reflection of limits along a natural isomorphism in the functor. -/
theorem reflectsLimits_of_natIso {F G : C ⥤ D} (h : F ≅ G) [ReflectsLimitsOfSize.{w', w} F] :
    ReflectsLimitsOfSize.{w', w} G where reflectsLimitsOfShape := reflectsLimitsOfShape_of_natIso h

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