English
For any f: N → N', surjectivity of f.lTensor M is equivalent to surjectivity of f, with M faithfully flat.
Русский
При верноподобной M отображение f: N→N' сюръективно тогда и только тогда, когда f.lTensor M сюръективно.
LaTeX
$$[simp] forall f: N → N' [Module.FaithfullyFlat R M] : (Function.Surjective (f.lTensor M)) \iff (Function.Surjective f)$$
Lean4
/-- Faithful flatness is preserved by arbitrary base change. -/
instance (S : Type*) [CommRing S] [Algebra R S] [Module.FaithfullyFlat R M] : Module.FaithfullyFlat S (S ⊗[R] M) :=
by
rw [Module.FaithfullyFlat.iff_flat_and_rTensor_reflects_triviality]
refine ⟨inferInstance, fun N _ _ hN ↦ ?_⟩
let _ : Module R N := Module.compHom N (algebraMap R S)
have : IsScalarTower R S N := IsScalarTower.of_algebraMap_smul fun r ↦ congrFun rfl
have := (AlgebraTensorModule.cancelBaseChange R S S N M).symm.subsingleton
exact FaithfullyFlat.rTensor_reflects_triviality R M N
