English
If M is Artinian as an R-module, then for any rs, IsRegular M rs forces rs to be the empty list; i.e., regularity cannot occur nontrivially in Artinian settings.
Русский
Если M является артиновым как модуль над R, то из IsRegular M rs следует, что rs = [], то есть регулярность не встречается ненулевой образом в артиновом окружении.
LaTeX
$$$[IsArtinian(R,M)]\\; \\Rightarrow\\; IsRegular(M, rs) \\Rightarrow rs = []$$$
Lean4
theorem eq_nil_of_isRegular_on_artinian [IsArtinian R M] : {rs : List R} → IsRegular M rs → rs = []
| [], _ => rfl
| r :: rs, h =>
by
rw [isRegular_iff, ne_comm, ← lt_top_iff_ne_top, Ideal.ofList_cons, sup_smul, ideal_span_singleton_smul,
isWeaklyRegular_cons_iff] at h
refine absurd ?_ (ne_of_lt (lt_of_le_of_lt le_sup_left h.right))
exact
Eq.trans (Submodule.map_top _) <|
LinearMap.range_eq_top.mpr <| surjective_of_injective_endomorphism (LinearMap.lsmul R M r) h.left.left
