isWeaklyRegular_of_perm_of_subset_maximalIdeal

English

In an Artinian setting, if IsRegular M rs holds, then rs must be empty; regularity cannot occur nontrivially in Artinian contexts.

Русский

В артиновом контексте, если IsRegular M rs, то rs пуст; регулярность не может возникать ненулевым образом.

LaTeX

$$$[IsArtinian(R,M)] \\Rightarrow IsRegular(M, rs) \\Rightarrow rs = []$$$

Lean4

theorem _root_.IsLocalRing.isWeaklyRegular_of_perm_of_subset_maximalIdeal [IsLocalRing R] [IsNoetherian R M]
    {rs rs' : List R} (h1 : IsWeaklyRegular M rs) (h2 : List.Perm rs rs')
    (h3 : ∀ r ∈ rs, r ∈ IsLocalRing.maximalIdeal R) : IsWeaklyRegular M rs' :=
  IsWeaklyRegular.of_perm_of_subset_jacobson_annihilator h1 h2 fun r hr =>
    IsLocalRing.maximalIdeal_le_jacobson _ (h3 r hr)

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