of_isLocalizedModule — Mathlib

English

Under a flat base change, a weakly regular sequence remains weakly regular after mapping rs through the base change map.

Русский

При плоском переходе базе слабая регулярность последовательности сохраняется после отображения rs через отображение перехода базы.

LaTeX

$$$\text{IsWeaklyRegular}_S( rs.map( algebraMap_R^S) ) \text{ from reg. on } R.$$$

Lean4

theorem of_isLocalizedModule (f : M →ₗ[R] N) [IsLocalizedModule T f] {rs : List R} (reg : IsWeaklyRegular M rs) :
    IsWeaklyRegular N (rs.map (algebraMap R S)) :=
  have : Flat R S := IsLocalization.flat S T
  reg.of_flat_of_isBaseChange (IsLocalizedModule.isBaseChange T S f)

Похожие утверждения