English
A simple ring is semisimple if and only if it is Artinian, if and only if it has a minimal left ideal.
Русский
Простое кольцо полупрямое эквивалентно полупрямому, если и только если оно артиново, если и только если у него есть минимальный левый идеал.
LaTeX
$$$\\text{IsSimpleRing}(R) \\Rightarrow (\\mathrm{IsSemisimpleRing}(R) \\iff \\mathrm{IsArtinianRing}(R) \\iff \\exists I, \\mathrm{IsAtom}(I))$$$
Lean4
/-- A simple ring is semisimple iff it is Artinian, iff it has a minimal left ideal. -/
theorem tfae [IsSimpleRing R] : List.TFAE [IsSemisimpleRing R, IsArtinianRing R, ∃ I : Ideal R, IsAtom I] :=
by
tfae_have 1 → 2 := fun _ ↦ inferInstance
tfae_have 2 → 3 := fun _ ↦ IsAtomic.exists_atom _
tfae_have 3 → 1 := fun ⟨I, hI⟩ ↦
by
have ⟨_, h⟩ := isSimpleRing_iff_isTwoSided_imp.mp ‹IsSimpleRing R›
simp_rw [← isFullyInvariant_iff_isTwoSided] at h
have := isSimpleModule_iff_isAtom.mpr hI
obtain eq | eq := h _ (.isotypicComponent R R I)
· exact (hI.bot_lt.not_ge <| (le_sSup <| by exact ⟨.refl ..⟩).trans_eq eq).elim
exact .congr (.symm <| .trans (.ofEq _ _ eq) Submodule.topEquiv)
tfae_finish
