English
If rs is a RegularR-sequence in R and S is a faithfully flat R-algebra, then the image rs^S is a Regular sequence in S with respect to any R-module M transported along the base change.
Русский
Если rs — регулярная последовательность в R и S — плоско-файная R-алгебра, то образ rs в S образует регулярную последовательность в S для переноса M по базе.
LaTeX
$$$\text{IsRegular}_R(rs) \Rightarrow \text{IsRegular}_S( rs.map( algebraMap_R^S) ).$$$
Lean4
/-- Let `R` be a commutative ring, `M` be an `R`-module, `S` be a faithfully flat `R`-algebra,
`N` be the base change of `M` to `S`. If `[r₁, …, rₙ]` is a regular `M`-sequence, then its image
in `N` is a regular `N`-sequence. -/
theorem of_faithfullyFlat_of_isBaseChange {f : M →ₗ[R] N} (hf : IsBaseChange S f) {rs : List R} (reg : IsRegular M rs) :
IsRegular N (rs.map (algebraMap R S)) :=
by
refine ⟨reg.1.of_flat_of_isBaseChange hf, ?_⟩
rw [← Ideal.map_ofList]
exact ((hf.map_smul_top_ne_top_iff_of_faithfullyFlat R M _).mpr reg.2.symm).symm
