English
Let M be an Artinian module over a ring R. Then M is semisimple if and only if its Jacobson radical is the zero submodule.
Русский
Пусть M — артинановый модуль над кольцом R. Тогда M разложим по простым модулям тогда и только тогда, когда Якобсонов радикал модуля M равен нулю.
LaTeX
$$$ IsArtinian\\; R\\; M \\Rightarrow \\bigl( IsSemisimpleModule\\; R\\; M \\iff Module.jacobson\\; R\\; M = \\bot \\bigr) $$$
Lean4
theorem isSemisimpleModule_iff_jacobson [IsArtinian R M] : IsSemisimpleModule R M ↔ Module.jacobson R M = ⊥ :=
⟨fun _ ↦ IsSemisimpleModule.jacobson_eq_bot R M, fun h ↦
have ⟨s, hs⟩ := Finset.exists_inf_le (Subtype.val (p := fun m : Submodule R M ↦ IsCoatom m))
have _ (m : s) : IsSimpleModule R (M ⧸ m.1.1) := isSimpleModule_iff_isCoatom.mpr m.1.2
let f : M →ₗ[R] ∀ m : s, M ⧸ m.1.1 := LinearMap.pi fun m ↦ m.1.1.mkQ
.of_injective f <|
LinearMap.ker_eq_bot.mp <|
le_bot_iff.mp fun x hx ↦ by
rw [← h, Module.jacobson, Submodule.mem_sInf]
exact fun m hm ↦
hs ⟨m, hm⟩ <|
Submodule.mem_finsetInf.mpr fun i hi ↦ (Submodule.Quotient.mk_eq_zero i.1).mp <| congr_fun hx ⟨i, hi⟩⟩
