preservesFiniteColimits_of_reflects_of_preserves

English

If F ∘ G preserves finite colimits and G reflects finite colimits, then F preserves finite colimits.

Русский

Если F ∘ G сохраняет конечные колимиты и G отражает конечные колимиты, тогда F сохраняет конечные колимиты.

LaTeX

$$$\mathrm{PreservesFiniteColimits}(F \circ G) \land \mathrm{ReflectsFiniteColimits}(G) \Rightarrow \mathrm{PreservesFiniteColimits}(F)$$$

Lean4

/-- If `F ⋙ G` preserves finite colimits and `G` reflects finite colimits, then `F` preserves finite
colimits.
-/
theorem preservesFiniteColimits_of_reflects_of_preserves (F : C ⥤ D) (G : D ⥤ E) [PreservesFiniteColimits (F ⋙ G)]
    [ReflectsFiniteColimits G] : PreservesFiniteColimits F where
  preservesFiniteColimits _ _ _ := preservesColimitsOfShape_of_reflects_of_preserves F G

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