English
If R is local and M is finitely generated, IsRegular M rs is equivalent to IsWeaklyRegular M rs when rs lies in the maximal ideal; this reduces a global regularity check to a local one.
Русский
Если R локально и M конечнопорождён, IsRegular M rs эквивалентна IsWeaklyRegular M rs при rs в максимальном идеале; это сводит глобальную проверку регулярности к локальной.
LaTeX
$$$[IsLocalRing R] \\Rightarrow (IsRegular(M, rs) \\iff IsWeaklyRegular(M, rs))$ при $rs \\subseteq \\mathfrak{m}$$$
Lean4
theorem _root_.IsLocalRing.isRegular_of_perm [IsLocalRing R] [IsNoetherian R M] {rs rs' : List R} (h1 : IsRegular M rs)
(h2 : List.Perm rs rs') : IsRegular M rs' := by
obtain ⟨h3, h4⟩ := h1
refine ⟨IsLocalRing.isWeaklyRegular_of_perm_of_subset_maximalIdeal h3 h2 ?_, ?_⟩
· intro x (h6 : x ∈ {r | r ∈ rs})
refine IsLocalRing.le_maximalIdeal ?_ (Ideal.subset_span h6)
exact h4 ∘ Eq.trans (top_smul _).symm ∘ Eq.symm ∘ congrArg (· • ⊤)
· refine ne_of_ne_of_eq h4 (congrArg (Ideal.span · • ⊤) ?_)
exact Set.ext fun _ => h2.mem_iff
