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: LetRₚa localization of a commutative ringRandMbe a module overRₚ. ThenMis flat overRif and only ifMis flat overRₚ.Module.flat_of_isLocalized_maximal: LetMbe a module over a commutative ringR. If the localization ofMat each maximal idealPis flat overRₚ, thenMis flat overR.Module.flat_of_isLocalized_span: LetMbe a module over a commutative ringRandSbe a set that spansR. If the localization ofMat eachs : Sis flat overLocalization.Away s, thenMis flat overR.
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