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} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] [Module.Flat R S] (p : Submonoid S) : 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) → [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.AtPrime P (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.Away (↑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.Away (↑r) M)) : Flat S M

instance instFlatAtPrimeOfIsScalarTower {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] [Module.Flat A B] (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [Algebra (Localization.AtPrime p) (Localization.AtPrime P)] [IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime P)] : Module.Flat (Localization.AtPrime p) (Localization.AtPrime P)

theorem IsSMulRegular.of_isLocalizedModule {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] {K : Type u_6} [AddCommMonoid K] [Module R K] (f : K →ₗ[R] M) [IsLocalizedModule p f] {x : R} (reg : IsSMulRegular K x) : IsSMulRegular M ((algebraMap R S) x)

theorem IsSMulRegular.of_isLocalization {R : Type u_1} (S : Type u_2) [CommSemiring R] [CommSemiring S] [Algebra R S] (p : Submonoid R) [IsLocalization p S] {x : R} (reg : IsSMulRegular R x) : IsSMulRegular S ((algebraMap R S) x)