preservesFiniteProducts — Mathlib

English

If C has finite products and W behaves well with respect to them, then localization preserves finite products: the functor L preserves finite products.

Русский

Если в C существуют конечные произведения, и W благопригодно себя ведёт относительно них, локализация сохраняет конечные произведения: L сохраняет конечные произведения.

LaTeX

$$$ \\text{PreservesFiniteProducts } L$$$

Lean4

/-- When `C` has finite products and `W : MorphismProperty C` contains
identities and is stable by finite products,
then any localization functor for `W` preserves finite products. -/
theorem preservesFiniteProducts : PreservesFiniteProducts L where preserves _ := preservesProductsOfShape L W _

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