English
Under the flatness assumption, the map cone of the equalizer fork after tensoring is a limit; i.e., tensorProdMapEqualizerForkIsLimit asserts this is a limit.
Русский
При условии плоскости, конус отображения равенства после тензорирования является пределом; перечисляет, что tensorProdMapEqualizerForkIsLimit является пределом.
LaTeX
$$$ \\text{IsLimit}((\\text{tensorProd } R S).mapCone(\\text{Under.equalizerFork } f g))$$$
Lean4
instance [Module.Flat R S] {A B : Under R} (f g : A ⟶ B) : PreservesLimit (parallelPair f g) (tensorProd R S) :=
let c : Fork f g := Under.equalizerFork f g
let hc : IsLimit c := Under.equalizerForkIsLimit f g
let hc' : IsLimit ((tensorProd R S).mapCone c) := tensorProdMapEqualizerForkIsLimit f g
preservesLimit_of_preserves_limit_cone hc hc'
