iff_flat_tensorProduct — Mathlib

English

Flatness descends along tensor product with a faithfully flat algebra: M is flat over R iff S ⊗R M is flat over S, given S is a faithfully flat R-algebra.

Русский

Плоскость опускается через тensor-произведение по верноподобной алгебре: M плоско над R тогда и только тогда, когда S ⊗R M плоско над S.

LaTeX

$$$\forall S\,[\text{CommRing } S]\ [\text{Algebra } R S]\ [\mathrm{Module.FaithfullyFlat }R S] : \mathrm{Module.Flat}_S(S \otimes_R M) \iff \mathrm{Module.Flat}_R(M)$$$

Lean4

theorem iff_flat_tensorProduct (S : Type*) [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S] :
    Module.Flat S (S ⊗[R] M) ↔ Module.Flat R M :=
  ⟨fun _ ↦ .of_flat_tensorProduct R M S, fun _ ↦ inferInstance⟩

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