English
FaithfullyFlat R M is equivalent to Flat R M along with the property that for all N, Subsingleton (N ⊗M) → Subsingleton N.
Русский
FaithfullyFlat равносильно Flat вместе со свойством: для всех N, Subsingleton(N ⊗M) → Subsingleton N.
LaTeX
$$$\mathrm{FaithfullyFlat}_R(M) \iff \big( \mathrm{Flat}_R(M) \land \forall N,\operatorname{Subsingleton}(N \otimes_R M) \Rightarrow \operatorname{Subsingleton}(N) \big)$$$
Lean4
/-- Flat descends along faithfully flat ring maps. -/
theorem of_flat_tensorProduct (S : Type*) [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S]
[Module.Flat S (S ⊗[R] M)] : Module.Flat R M :=
by
rw [Module.Flat.iff_lTensor_preserves_injective_linearMap]
intro N P _ _ _ _ f hf
have : Flat R (S ⊗[R] M) := Flat.trans _ S _
rw [← FaithfullyFlat.lTensor_injective_iff_injective R S]
have :
LinearMap.lTensor S (LinearMap.lTensor M f) =
(TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ
LinearMap.lTensor (S ⊗[R] M) f ∘ₗ (TensorProduct.assoc _ _ _ _).symm.toLinearMap :=
by
ext
simp
simpa [this] using Flat.lTensor_preserves_injective_linearMap f hf
