English
The application of tensorKerEquiv is compatible with the underlying map; evaluating on x yields the same result as the direct application.
Русский
Применение tensorKerEquiv согласовано с базовым отображением; при вычислении на x получаем тот же результат, что и прямое приложение.
LaTeX
$$tensorKerEquiv_apply [Module.Flat R M] (x) : (tensorKer S M f x) = ...$$
Lean4
/-- If `M` is `R`-flat, the canonical map `M ⊗[R] eq(f, g) →ₗ[S] eq (𝟙 ⊗ f, 𝟙 ⊗ g)` is an
isomorphism. -/
def tensorEqLocusEquiv [Module.Flat R M] :
M ⊗[R] eqLocus f g ≃ₗ[S] eqLocus (AlgebraTensorModule.lTensor S M f) (AlgebraTensorModule.lTensor S M g) :=
LinearEquiv.ofLinear (LinearMap.tensorEqLocus S M f g) (LinearMap.tensorEqLocusInv S M f g) (by ext; simp)
(by
ext m x
apply (Module.Flat.lTensor_preserves_injective_linearMap (eqLocus f g).subtype (eqLocus f g).injective_subtype)
simp)
