comp_preservesFiniteLimits — Mathlib

English

If F preserves finite limits and G preserves finite limits, then F ⋙ G preserves finite products.

Русский

Если F сохраняет конечные пределы и G сохраняет конечные пределы, то F ⋙ G сохраняет конечные произведения.

LaTeX

$$PreservesFiniteProducts(F ⋙ G) from PreservesFiniteProducts F and PreservesFiniteProducts G$$

Lean4

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

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