Flatness and localization

In this file we show that localizations are flat, and flatness is a local property.

Main result

• IsLocalization.flat: a localization of a commutative ring is flat over it.
• Module.flat_iff_of_isLocalization : Let Rₚ a localization of a commutative ring R and M be a module over Rₚ. Then M is flat over R if and only if M is flat over Rₚ.
• Module.flat_of_isLocalized_maximal : Let M be a module over a commutative ring R. If the localization of M at each maximal ideal P is flat over Rₚ, then M is flat over R.
• Module.flat_of_isLocalized_span : Let M be a module over a commutative ring R and S be a set that spans R. If the localization of M at each s : S is flat over Localization.Away s, then M is flat over R.

theorem IsLocalization.flat {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (p : Submonoid R) [IsLocalization p S] : Module.Flat R S

instance Localization.flat {R : Type u_1} [CommSemiring R] (p : Submonoid R) : Module.Flat R (Localization p)

theorem Module.flat_iff_of_isLocalization {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (p : Submonoid R) [IsLocalization p S] (M : Type u_3) [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] : Flat S M ↔ Flat R M

theorem Module.flat_of_isLocalized_maximal {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (M : Type u_3) [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] (Mₚ : (P : Ideal S) → [inst : P.IsMaximal] → Type u_4) [(P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)] [(P : Ideal S) → [inst : P.IsMaximal] → Module R (Mₚ P)] [(P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)] [∀ (P : Ideal S) [inst : P.IsMaximal], IsScalarTower R S (Mₚ P)] (f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P) [∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (H : ∀ (P : Ideal S) [inst : P.IsMaximal], Flat R (Mₚ P)) : Flat R M

theorem Module.flat_of_localized_maximal {R : Type u_1} [CommSemiring R] (M : Type u_3) [AddCommMonoid M] [Module R M] (h : ∀ (P : Ideal R) [inst : P.IsMaximal], Flat R (LocalizedModule P.primeCompl M)) : Flat R M

theorem Module.flat_of_isLocalized_span {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (M : Type u_3) [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] (s : Set S) (spn : Ideal.span s = ⊤) (Mₛ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₛ r)] [(r : ↑s) → Module R (Mₛ r)] [(r : ↑s) → Module S (Mₛ r)] [∀ (r : ↑s), IsScalarTower R S (Mₛ r)] (g : (r : ↑s) → M →ₗ[S] Mₛ r) [∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (g r)] (H : ∀ (r : ↑s), Flat R (Mₛ r)) : Flat R M

theorem Module.flat_of_localized_span (S : Type u_2) [CommSemiring S] (M : Type u_3) [AddCommMonoid M] [Module S M] (s : Set S) (spn : Ideal.span s = ⊤) (h : ∀ (r : ↑s), Flat S (LocalizedModule (Submonoid.powers ↑r) M)) : Flat S M