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) [CommRing R] [CommRing S] [Algebra R S] (p : Submonoid R) [IsLocalization p S] : Module.Flat R S

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

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

theorem Module.flat_of_isLocalized_maximal {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (M : Type u_3) [AddCommGroup 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] → AddCommGroup (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], Module.Flat R (Mₚ P)) : Module.Flat R M

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

theorem Module.flat_of_isLocalized_span {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (M : Type u_3) [AddCommGroup 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) → AddCommGroup (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), Module.Flat R (Mₛ r)) : Module.Flat R M

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