English
If C has finite products and W contains identities and is stable under these finite products, then the localization functor L preserves finite products indexed by J: i.e., it preserves limits of shape Discrete J.
Русский
Если в C существуют конечные произведения и W содержит тождественности и сохраняется под этими конечными произведениями, то локализационная проекция сохраняет конечные произведения по индексу J: т.е. сохраняет пределы формы Discrete J.
LaTeX
$$$ \\text{PreservesLimitsOfShape }(\\mathrm{Discrete}\\ J)\\ L $$$
Lean4
/-- When `C` has finite products indexed by `J`, `W : MorphismProperty C` contains
identities and is stable by products indexed by `J`,
then any localization functor for `W` preserves finite products indexed by `J`. -/
theorem preservesProductsOfShape (J : Type) [Finite J] [HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] :
PreservesLimitsOfShape (Discrete J) L where
preservesLimit
{F} := preservesLimit_of_preserves_limit_cone (limit.isLimit F) (HasProductsOfShapeAux.isLimitMapCone L W J F)
