reflectsColimits_of_reflectsIsomorphisms

English

If G reflects isomorphisms and has/ preserves colimits of shape J, then G reflects colimits of shape J.

Русский

Если G отражает изоморфизмы и имеет/сохраняет колимиты формы J, тогда G отражает колимиты формы J.

LaTeX

$$$\\bigl[G \\text{ reflectsIsomorphisms} \\land HasColimitsOfShape J C \\land PreservesColimitsOfShape J G\\bigr] \\Rightarrow ReflectsColimitsOfShape J G$$$

Lean4

/-- If `C` has colimits and `G` preserves colimits, then if `G` reflects isomorphisms then it reflects
colimits.
-/
theorem reflectsColimits_of_reflectsIsomorphisms {G : C ⥤ D} [G.ReflectsIsomorphisms] [HasColimitsOfSize.{w', w} C]
    [PreservesColimitsOfSize.{w', w} G] : ReflectsColimitsOfSize.{w', w} G where
  reflectsColimitsOfShape := reflectsColimitsOfShape_of_reflectsIsomorphisms

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