English
If M is flat over R, there is an isomorphism between M ⊗ eqLocus f g and eqLocus(lTensor f, lTensor g), realizing the natural compatibility of tensoring with equalizers.
Русский
Если M плоский над R, существует изоморфизм между M ⊗ eqLocus f g и eqLocus(lTensor f, lTensor g), реализующий естественную совместимость тензорирования с равноположениями.
LaTeX
$$$\text{tensorEqLocusEquiv} : M \otimes_R eqLocus f g \cong_S eqLocus( lTensor_S M f, lTensor_S M g )$$$
Lean4
/-- The canonical map `M ⊗[R] eq(f, g) →ₗ[R] eq(𝟙 ⊗ f, 𝟙 ⊗ g)`. -/
def tensorEqLocus :
M ⊗[R] (LinearMap.eqLocus f g) →ₗ[S]
LinearMap.eqLocus (AlgebraTensorModule.lTensor S M f) (AlgebraTensorModule.lTensor S M g) :=
AlgebraTensorModule.lift (tensorEqLocusBil S M f g)
