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