English
If R ⟂ S is a flat module, the map cone of Under.equalizerFork is preserved by tensorProd with S; i.e., ((tensorProd R S).mapCone (Under.equalizerFork f g)) is a limit cone.
Русский
При плоском модуле S над R отображение конуса через тензорный произведение сохраняется; то есть конус-фазная конструкция является предельной.
LaTeX
$$$ \\text{IsLimit}( (\\text{tensorProd } R S).mapCone(\\text{Under.equalizerFork } f g) )$$$
Lean4
/-- If `S` is `R`-flat, `tensorProd R S` preserves the equalizer of `f` and `g`. -/
noncomputable -- marked noncomputable for performance (only)
def tensorProdMapEqualizerForkIsLimit [Module.Flat R S] {A B : Under R} (f g : A ⟶ B) :
IsLimit ((tensorProd R S).mapCone <| Under.equalizerFork f g) :=
(isLimitMapConeForkEquiv (tensorProd R S) _).symm <|
(IsLimit.equivIsoLimit (equalizerForkTensorProdIso f g).symm) <| Under.equalizerFork'IsLimit _ _
