flat_of_isLocalized_maximal — Mathlib

English

If for every maximal ideal P of S the localized module M_P is flat over R, then M is flat over R.

Русский

Если для каждого максимального идеала P локализация M_P плосна над R, то M плосок над R.

LaTeX

$$$\\forall P\\; [P\\text{ maximal in }S]\\; \\Flat(R, M_P) \\Rightarrow \\Flat(R,M)$$

Lean4

theorem flat_of_isLocalized_maximal (H : ∀ (P : Ideal S) [P.IsMaximal], Flat R (Mₚ P)) : Module.Flat R M :=
  by
  simp_rw [Flat.iff_lTensor_injectiveₛ] at H ⊢
  simp_rw [← AlgebraTensorModule.coe_lTensor (A := S)]
  refine fun _ _ _ N ↦
    injective_of_isLocalized_maximal _ (fun P ↦ AlgebraTensorModule.rTensor R _ (f P)) _
      (fun P ↦ AlgebraTensorModule.rTensor R _ (f P)) _ fun P hP ↦ ?_
  simpa [IsLocalizedModule.map_lTensor] using H P N

Похожие утверждения