English
For a local ring R and a finitely generated R-module M, IsRegular M rs is equivalent to IsWeaklyRegular M rs when rs is contained in the maximal ideal, i.e., the regularity criterion reduces to a local criterion.
Русский
Для локального кольца R и модуля M с конечной генерацией, IsRegular M rs эквивалентна IsWeaklyRegular M rs при условии rs ⊆ максимальная идеал, что сводит критерий регулярности к локальному критерию.
LaTeX
$$$[IsLocalRing\\ R] \\Rightarrow (IsRegular(M, rs) \\leftrightarrow IsWeaklyRegular(M, rs))$ при $rs \\subseteq \\mathfrak{m}$$$
Lean4
theorem _root_.IsLocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal [IsLocalRing R] [Nontrivial M]
[Module.Finite R M] {rs : List R} (h : ∀ r ∈ rs, r ∈ IsLocalRing.maximalIdeal R) :
IsRegular M rs ↔ IsWeaklyRegular M rs :=
have H h' := bot_ne_top.symm <| annihilator_eq_top_iff.mp <| Eq.trans annihilator_top h'
isRegular_iff_isWeaklyRegular_of_subset_jacobson_annihilator fun r hr =>
IsLocalRing.jacobson_eq_maximalIdeal (Module.annihilator R M) H ▸ h r hr
