comp_preservesFiniteColimits — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The composition of two right exact functors is right exact. -/
theorem comp_preservesFiniteColimits (F : C ⥤ D) (G : D ⥤ E) [PreservesFiniteColimits F] [PreservesFiniteColimits G] :
    PreservesFiniteColimits (F ⋙ G) :=
  ⟨fun _ _ _ => inferInstance⟩

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