English
There is an isomorphism between tensorProdEqualizer f g and Under.equalizerFork' (Algebra.TensorProduct.map (AlgHom.id S S) (toAlgHom f)) and a similar map for g; i.e., tensoring commutes with taking equalizers up to a natural isomorphism.
Русский
Существует изоморфизм между tensorProdEqualizer f g и Under.equalizerFork' соответствующих карт; то есть тензоризация совместима с равенствами через естественный изоморфизм.
LaTeX
$$$ \\text{tensorProdEqualizer } f g \\cong \\text{Under.equalizerFork}'(\\text{Algebra.TensorProduct.map}(\\mathrm{id},\\mathrm{toAlgHom} f), \\text{Algebra.TensorProduct.map}(\\mathrm{id},\\mathrm{toAlgHom} g)) $$$
Lean4
/-- If `S` is `R`-flat, `S ⊗[R] eq(f, g)` is isomorphic to `eq(𝟙 ⊗[R] f, 𝟙 ⊗[R] g)`. -/
-- marked noncomputable for performance (only)
noncomputable def equalizerForkTensorProdIso [Module.Flat R S] {A B : Under R} (f g : A ⟶ B) :
tensorProdEqualizer f g ≅
Under.equalizerFork' (Algebra.TensorProduct.map (AlgHom.id S S) (toAlgHom f))
(Algebra.TensorProduct.map (AlgHom.id S S) (toAlgHom g)) :=
Fork.ext (AlgHom.tensorEqualizerEquiv S S (toAlgHom f) (toAlgHom g)).toUnder <|
by
ext
apply AlgHom.coe_tensorEqualizer
