English
If R is an Artinian ring, then R is semiprimary (i.e., J(R) is nilpotent and R/J(R) is semisimple).
Русский
Если R — Артинианово кольцо, то R является полуприварным: радикал Джейкобсона J(R) — nilpotent, а R / J(R) — полносемипринтовое кольцо.
LaTeX
$$$IsArtinianRing\ R \Rightarrow IsSemiprimaryRing\ R$$$
Lean4
instance : IsSemiprimaryRing R
where
isSemisimpleRing := IsArtinianRing.isSemisimpleRing_iff_jacobson.mpr (Ring.jacobson_quotient_jacobson R)
isNilpotent := by
let Jac := Ring.jacobson R
have ⟨n, hn⟩ := IsArtinian.monotone_stabilizes ⟨(Jac ^ ·), @Ideal.pow_le_pow_right _ _ _⟩
have hn : Jac * Jac ^ n = Jac ^ n := by rw [← Ideal.IsTwoSided.pow_succ]; exact (hn _ n.le_succ).symm
use n; by_contra ne
have ⟨N, ⟨eq, ne⟩, min⟩ := wellFounded_lt.has_min {N | Jac * N = N ∧ N ≠ ⊥} ⟨_, hn, ne⟩
have : Jac ^ n * N = N := n.rec (by rw [Jac.pow_zero, N.one_mul]) fun n hn ↦ by rwa [Jac.pow_succ, mul_assoc, eq]
let I x := Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
have hI x : I x ≤ Ideal.span { x } := by rw [Ideal.span, LinearMap.span_singleton_eq_range];
exact LinearMap.map_le_range
have ⟨x, hx⟩ : ∃ x ∈ N, I x ≠ ⊥ := by
contrapose! ne
rw [← this, ← le_bot_iff, Ideal.mul_le]
refine fun ri hi rn hn ↦ ?_
rw [← ne rn hn]
exact ⟨ri, hi, rfl⟩
rw [← Ideal.span_singleton_le_iff_mem] at hx
have : I x = N := by
refine ((hI x).trans hx.1).eq_of_not_lt (min _ ⟨?_, hx.2⟩)
rw [← smul_eq_mul, ← Submodule.map_smul'', smul_eq_mul, hn]
have : Ideal.span { x } = N := le_antisymm hx.1 (this.symm.trans_le <| hI x)
refine (this ▸ ne) ((Submodule.fg_span <| Set.finite_singleton x).eq_bot_of_le_jacobson_smul ?_)
rw [← Ideal.span, this, smul_eq_mul, eq]
