flat_iff_of_isLocalization — Mathlib

English

For a localization S of R, a module M is flat over S if and only if it is flat over R.

Русский

Для локализации S кольца R модуль M плосок над S тогда и только тогда, когда он плосок над R.

LaTeX

$$$\\text{Flat}(S,M) \\iff \\text{Flat}(R,M)$$$

Lean4

theorem flat_iff_of_isLocalization : Flat S M ↔ Flat R M :=
  have := isLocalizedModule_id p M S
  have := IsLocalization.flat S p
  ⟨fun _ ↦ .trans R S M, fun _ ↦ .of_isLocalizedModule S p .id⟩

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