Flatness and localization #
In this file we show that localizations are flat, and flatness is a local property (TODO).
Main result #
IsLocalization.flat: a localization of a commutative ring is flat over it.
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)
Equations
- ⋯ = ⋯