English
Let R and S be commutative rings with S flat as an R-algebra. Then the tensor product functor that maps an object over R to its tensor with S preserves limits of the parallel-pair shape (i.e., limits of diagrams shaped like a walking parallel pair). In particular, it preserves pullbacks and equalizers in that setting.
Русский
Пусть R и S — коммутативные кольца, причём S плоско как модуль над R. Тогда функтор тензорного произведения, переводящий объект над R в тензорный продукт с S, сохраняет пределы формы параллельной пары (то есть сохраняет предели вида pullback и equalizer в данной обстановке).
LaTeX
$$$[\\text{Module.Flat } R S] \\Rightarrow \\mathrm{PreservesLimitsOfShape}(\\mathrm{WalkingParallelPair}, \\mathrm{tensorProd}(R,S)).$$$
Lean4
instance [Module.Flat R S] : PreservesLimitsOfShape WalkingParallelPair (tensorProd R S) where
preservesLimit {K} := preservesLimit_of_iso_diagram _ (diagramIsoParallelPair K).symm
