reflectsColimits_of_natIso — Mathlib

English

If F ≅ G and F reflects colimits of size, then G reflects colimits of the same size.

Русский

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

LaTeX

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

Lean4

/-- Transfer reflection of colimits along a natural isomorphism in the functor. -/
theorem reflectsColimits_of_natIso {F G : C ⥤ D} (h : F ≅ G) [ReflectsColimitsOfSize.{w, w'} F] :
    ReflectsColimitsOfSize.{w, w'} G where reflectsColimitsOfShape := reflectsColimitsOfShape_of_natIso h

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