reflectsColimitsOfShape_of_reflectsIsomorphisms

English

If G reflects isomorphisms and preserves/has colimits in appropriate sizes, then it reflects colimits of those shapes.

Русский

Если G отражает изоморфизмы и сохраняет колимиты в нужных размерах, то он отражает колимиты соответствующих форм.

LaTeX

$$$\\forall J\\; [G.ReflectsIsomorphisms]\\; [HasColimitsOfSize J\\; C]\\; [PreservesColimitsOfSize J\\; G] \\Rightarrow ReflectsColimitsOfSize J\\, G$$$

Lean4

/-- If `C` has colimits of shape `J` and `G` preserves them, then if `G` reflects isomorphisms then it
reflects colimits of shape `J`.
-/
theorem reflectsColimitsOfShape_of_reflectsIsomorphisms {G : C ⥤ D} [G.ReflectsIsomorphisms] [HasColimitsOfShape J C]
    [PreservesColimitsOfShape J G] : ReflectsColimitsOfShape J G where
  reflectsColimit {F} := reflectsColimit_of_reflectsIsomorphisms F G

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