English
FaithfullyFlat is preserved under arbitrary base change: if M is faithfully flat over R and S is any R-algebra, then S ⊗R M is faithfully flat over S.
Русский
Верноподобность сохраняется при любом изменении базы: если M верноподобна над R, и S — R-алгебра, то S⊗R M верноподобна над S.
LaTeX
$$$\forall S\ [\text{CommRing } S]\ [\text{Algebra } R S]\ [\text{Module.FaithfullyFlat }R M] \Rightarrow \text{Module.FaithfullyFlat}_S(S \otimes_R M)$$$
Lean4
theorem _root_.IsBaseChange.map_smul_top_ne_top_iff_of_faithfullyFlat (hf : IsBaseChange S f) (I : Ideal R) :
I.map (algebraMap R S) • (⊤ : Submodule S N) ≠ ⊤ ↔ I • (⊤ : Submodule R M) ≠ ⊤ := by
simpa only [← Submodule.subsingleton_quotient_iff_eq_top.not] using
not_congr <|
(tensorQuotEquivQuotSMul N (I.map (algebraMap R S))).symm ≪≫ₗ TensorProduct.comm S N _ ≪≫ₗ hf.tensorEquiv _ ≪≫ₗ
AlgebraTensorModule.congr (I.qoutMapEquivTensorQout S) (.refl R M) ≪≫ₗ
AlgebraTensorModule.assoc R R S S _ M ≪≫ₗ
(TensorProduct.comm R _ M).baseChange R S _ _ ≪≫ₗ
(tensorQuotEquivQuotSMul M I).baseChange R S _ _ |>.subsingleton_congr.trans <|
subsingleton_tensorProduct_iff_right R S
