English
Let M be Artinian as an R-module, and let S be a commutative semiring with an R-algebra structure, together with an S-action on M that is compatible through an algebra map S → R which is surjective, i.e., M is an Artinian S-module as well. Then M is Artinian as an S-module.
Русский
Пусть M является артинановым как модуль над R, а S — коммутативное полугруппа-семиринг с структурой алгебра над R, причём действование S на M совместимо через сюръективное отображение алгебраMap S R; тогда M является артинановым как S-модуль.
LaTeX
$$$([CommSemiring\ S], [Algebra\ S\ R], [Module\ S\ M], [IsArtinian\ R\ M], [IsScalarTower\ S\ R\ M], (H : Function.Surjective (algebraMap S\ R))) \\Rightarrow IsArtinian\ S\ M$$$
Lean4
/-- If `M` is an Artinian `R` module, and `S` is an `R`-algebra with a surjective
algebra map, then `M` is an Artinian `S` module.
-/
theorem isArtinian_of_surjective_algebraMap {S : Type*} [CommSemiring S] [Algebra S R] [Module S M] [IsArtinian R M]
[IsScalarTower S R M] (H : Function.Surjective (algebraMap S R)) : IsArtinian S M :=
by
apply (OrderEmbedding.wellFoundedLT (β := Submodule R M))
refine ⟨⟨?_, ?_⟩, ?_⟩
· intro N
refine { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ?_ }
intro c x hx
obtain ⟨r, rfl⟩ := H c
suffices r • x ∈ N by simpa [Algebra.algebraMap_eq_smul_one, smul_assoc]
apply N.smul_mem _ hx
· intro N1 N2 h
rwa [Submodule.ext_iff] at h ⊢
· intro N1 N2
rfl
