English
Let M and N be R-modules, with N nontrivial and flat, and there exists an injective R-linear map from R into M. Then the tensor product M ⊗_R N is nontrivial.
Русский
Пусть M и N — R-модули, N ненулевой и плоский, существует инъективное отображение R → M. Тогда M ⊗_R N ненулевое.
LaTeX
$$$\\forall f\\,\\big( f : R \\to_{\\ell[R]} M \\big),\\;\\text{Injective}(f) \\;\\to\\; \\text{Module.Flat } R N \\;\\to\\; N \\neq 0 \\;\\to\\; M \\otimes_R N \\neq 0$$$
Lean4
/-- If `M`, `N` are `R`-modules, there exists an injective `R`-linear map from `R` to `M`,
and `N` is a nontrivial flat `R`-module, then `M ⊗[R] N` is nontrivial. -/
theorem nontrivial_of_linearMap_injective_of_flat_right (f : R →ₗ[R] M) (h : Function.Injective f) [Module.Flat R N]
[Nontrivial N] : Nontrivial (M ⊗[R] N) :=
Module.Flat.rTensor_preserves_injective_linearMap (M := N) f h |>.comp
(TensorProduct.lid R N).symm.injective |>.nontrivial
