English
For N faithfully flat, Nontrivial(M ⊗R N) ↔ Nontrivial M.
Русский
Для верноподобной N: непустость M ⊗R N эквивалентна непустости M.
LaTeX
$$[simp] \forall N\ [\text{Module }R N], [\text{Module.FaithfullyFlat }R N] : \operatorname{Nontrivial}(M \otimes_R N) \iff \operatorname{Nontrivial}(M)$$
Lean4
/-- If `M` is a faithfully flat module, then for all linear maps `f`, the map `id ⊗ f = 0`, if and only
if `f = 0`. -/
theorem zero_iff_lTensor_zero [h : FaithfullyFlat R M] {N : Type*} [AddCommGroup N] [Module R N] {N' : Type*}
[AddCommGroup N'] [Module R N'] (f : N →ₗ[R] N') : f = 0 ↔ LinearMap.lTensor M f = 0 :=
⟨fun hf => hf.symm ▸ LinearMap.lTensor_zero M, fun hf =>
by
have :=
lTensor_reflects_exact R M f LinearMap.id
(by
rw [LinearMap.exact_iff, hf, LinearMap.range_zero, LinearMap.ker_eq_bot]
apply Module.Flat.lTensor_preserves_injective_linearMap
exact fun _ _ h => h)
ext x; simpa using this (f x)⟩
