English
If B is faithfully flat over A and M is any A-module, the canonical map m ↦ 1 ⊗ m from M to B ⊗_A M is injective.
Русский
Если B плоско над A и M произвольный A-модуль, каноническое отображение m ↦ 1 ⊗ m в B ⊗_A M инъективно.
LaTeX
$$Injective(\text{Linear map } M \to B \otimes_A M: m \mapsto 1 \otimes m)$$
Lean4
/-- If `A` is local and `B` is a local and flat `A`-algebra, then `B` is faithfully flat. -/
theorem of_flat_of_isLocalHom [IsLocalRing A] [IsLocalRing B] [Flat A B] [IsLocalHom (algebraMap A B)] :
Module.FaithfullyFlat A B := by
refine ⟨fun m hm ↦ ?_⟩
rw [Ideal.smul_top_eq_map, IsLocalRing.eq_maximalIdeal hm]
by_contra eqt
have :
Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) ≤
Submodule.restrictScalars A (IsLocalRing.maximalIdeal B) :=
((IsLocalRing.local_hom_TFAE (algebraMap A B)).out 0 2).mp ‹_›
rw [eqt, top_le_iff, Submodule.restrictScalars_eq_top_iff] at this
exact Ideal.IsPrime.ne_top' this
