Commit 2024-12-07 06:05 653f17d0

View on Github →

feat(RingTheory/LocalProperties): flatness is a local property (#19085) This PR proves that flat is a local property. Main results:

  1. flat_of_localization_maximal : Let M be a module over CommRing R. If the localization of M at each maximal ideal P is flat over R_p, then M is flat over R.
  2. flat_of_localization_span : Let M be a module over CommRing R and S be a set that spans R. If the localization of M at s : S is flat over Localization.Away s, then M is flat over R.
  3. flat_iff_of_localization : Let R_p a localization of CommRing R and M be a module over R_p. Then M is flat over R if and only if M is flat over R_p

Estimated changes