English
A finitely generated Artinian module over a commutative ring is Noetherian.
Русский
Конечная (генерируемая) Artinian-модуль над коммутативным кольцом — это Noetherian-модуль.
LaTeX
$$$$\text{If } R \text{ is commutative and } M \text{ is finitely generated and Artinian over } R, \text{ then } M \text{ is Noetherian.}$$$$
Lean4
/-- A finitely generated Artinian module over a commutative ring is Noetherian. This is not
necessarily the case over a noncommutative ring, see https://mathoverflow.net/a/61700. -/
theorem isNoetherian_of_finite_isArtinian {R} [CommRing R] [Module R M] [Module.Finite R M] [IsArtinian R M] :
IsNoetherian R M := by
obtain ⟨s, fin, span⟩ := Submodule.fg_def.mp (Module.finite_def.mp ‹_›)
rw [← s.iUnion_of_singleton_coe, Submodule.span_iUnion] at span
rw [← Set.finite_coe_iff] at fin
rw [← isNoetherian_top_iff, ← span]
have _ (i : M) : IsNoetherian R (Submodule.span R { i }) :=
by
rw [LinearMap.span_singleton_eq_range, ← (LinearMap.quotKerEquivRange _).isNoetherian_iff]
let e (I : Ideal R) : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := ⟨.id _, fun _ _ ↦ rfl⟩
rw [(e _).isNoetherian_iff_of_bijective Function.bijective_id]
refine @instIsNoetherianRingOfIsArtinianRing _ _ ?_
rw [IsArtinianRing, ← (e _).isArtinian_iff_of_bijective Function.bijective_id,
(LinearMap.quotKerEquivRange _).isArtinian_iff]
infer_instance
infer_instance
