English
Let R be a ring and M an IsSemisimple R-module. Then the following five properties are equivalent: M is finite as an R-module; M is Noetherian; M is Artinian; M has finite length; and there exists a finite collection of submodules of M, each simple, whose supremum is M and which are independent in the sense of submodule sums.
Русский
Пусть R — кольцо, M — полное разложение как R-модуль. Тогда следующие пять свойств эквивалентны: M конечен как R-модуль; M удовлетворяет условию Нотера; M удовлетворяет условию артинановости; M имеет конечную длину; существует конечное множество подпредметов M, каждый из которых прост, чья супремума равна M и которые независимы по определению независимости по суммам подпредметов.
LaTeX
$$$\\displaystyle \\text{Let } R \\text{ be a ring and } M \\text{ an } R\\text{-module with } M \\text{ semisimple. Then} \\\\ \\\\ \\,\\text{Module.Finite } R M \\iff \\text{IsNoetherian } R M \\iff \\text{IsArtinian } R M \\\\ \\iff \\text{IsFiniteLength } R M \\iff \\\\ \\\\ \\exists s : \\mathcal{P}( \\mathrm{Submodule}_R M ),\\ s.Finite \\wedge \\mathrm{sSupIndep } s \\wedge \\mathrm{sSup } s = \\top \\wedge \\forall m \\in s, \\ \\mathrm{IsSimpleModule} R m.$$$
Lean4
theorem finite_tfae [IsSemisimpleModule R M] :
List.TFAE
[Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M,
∃ s : Set (Submodule R M), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R m] :=
by
rw [isFiniteLength_iff_isNoetherian_isArtinian]
obtain ⟨s, hs⟩ := IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top R M
tfae_have 1 ↔ 2 := ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩
tfae_have 2 → 5 := fun _ ↦ ⟨s, WellFoundedGT.finite_of_sSupIndep hs.1, hs⟩
tfae_have 3 → 5 := fun _ ↦ ⟨s, WellFoundedLT.finite_of_sSupIndep hs.1, hs⟩
tfae_have 5 → 4 := fun ⟨s, fin, _, sSup_eq_top, simple⟩ ↦
by
rw [← isNoetherian_top_iff, ← Submodule.topEquiv.isArtinian_iff, ← sSup_eq_top, sSup_eq_iSup, ← iSup_subtype'']
rw [SetCoe.forall'] at simple
have := fin.to_subtype
exact ⟨isNoetherian_iSup, isArtinian_iSup⟩
tfae_have 4 → 2 := And.left
tfae_have 4 → 3 := And.right
tfae_finish
