English
Regularity is preserved under localization: localizing at a prime p yields a regular sequence image in the localized ring.
Русский
Регулярность сохраняется при локализации: образ регулярной последовательности в локализованном кольце остаётся регулярной.
LaTeX
$$$\text{If } rs\text{ is IsWeaklyRegular over } R\text{ and } rs\subset p, \text{ then } rs\mapsto (algebraMap_R^S)(rs)\text{ is IsWeaklyRegular over } S.$$$
Lean4
/-- Let `R` be a commutative ring, `M` be an `R`-module, `S` be a flat `R`-algebra, `N` be the base
change of `M` to `S`. If `[r₁, …, rₙ]` is a weakly regular `M`-sequence, then its image in `N` is
a weakly regular `N`-sequence. -/
theorem of_flat_of_isBaseChange [Flat R S] {f : M →ₗ[R] N} (hf : IsBaseChange S f) {rs : List R}
(reg : IsWeaklyRegular M rs) : IsWeaklyRegular N (rs.map (algebraMap R S)) := by
induction rs generalizing M N with
| nil => simp
| cons x _ ih =>
simp only [List.map_cons, isWeaklyRegular_cons_iff] at reg ⊢
have e :=
(QuotSMulTop.algebraMapTensorEquivTensorQuotSMulTop x M S).symm ≪≫ₗ
QuotSMulTop.congr ((algebraMap R S) x) hf.equiv
have hg : IsBaseChange S <| e.toLinearMap.restrictScalars R ∘ₗ TensorProduct.mk R S (QuotSMulTop x M) 1 :=
IsBaseChange.of_equiv e (fun _ ↦ by simp)
exact ⟨reg.1.of_flat_of_isBaseChange hf, ih hg reg.2⟩
