English
Under Noetherian hypothesis, weak regularity is preserved under permutation of rs, provided each element lies in the Jacobson radical of the annihilator; hence IsWeaklyRegular is invariant under rs' perm rs.
Русский
При гипотезе Нётерова законы сохраняются при перестановке rs, если каждое r лежит в радикале Якобсона аннигиллятора; из этого следует, что IsWeaklyRegular неизменна при перестановке rs.
LaTeX
$$$[IsNoetherian\\ R\\ M] \\Rightarrow IsWeaklyRegular(M, rs) \\Rightarrow rs' \\text{ perm rs} \\Rightarrow IsWeaklyRegular(M, rs')$$$
Lean4
theorem of_perm_of_subset_jacobson_annihilator [IsNoetherian R M] {rs rs' : List R} (h1 : IsWeaklyRegular M rs)
(h2 : List.Perm rs rs') (h3 : ∀ r ∈ rs, r ∈ (Module.annihilator R M).jacobson) : IsWeaklyRegular M rs' :=
h1.prototype_perm h2 fun r _ _ h h' =>
eq_bot_of_eq_pointwise_smul_of_mem_jacobson_annihilator (IsNoetherian.noetherian _) h'
(Ideal.jacobson_mono
(le_trans (LinearMap.annihilator_le_of_surjective (R := R) _ (mkQ_surjective _))
(LinearMap.annihilator_le_of_injective _ (injective_subtype _)))
(h3 r (h.subset List.mem_cons_self)))
