preservesColimit_of_reflects_of_preserves

English

If F ⋙ G preserves colimits for K and G reflects colimits for K ⋙ F, then F preserves colimits for K.

Русский

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

LaTeX

$$$[\\mathrm{PreservesColimit}\\,K\\,(F \\;⋙\\; G)] \\land [\\mathrm{ReflectsColimit}\\,(K \\;⋙\\; F)\\,G] \\Rightarrow \\mathrm{PreservesColimit}\\,K\\,F$$$

Lean4

/-- If `F ⋙ G` preserves colimits for `K`, and `G` reflects colimits for `K ⋙ F`,
then `F` preserves colimits for `K`. -/
theorem preservesColimit_of_reflects_of_preserves [PreservesColimit K (F ⋙ G)] [ReflectsColimit (K ⋙ F) G] :
    PreservesColimit K F :=
  ⟨fun {c} h =>
    ⟨by
      apply isColimitOfReflects G
      apply isColimitOfPreserves (F ⋙ G) h⟩⟩

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