English
In a semisimple ring, every ideal I is generated by an idempotent element e, i.e., I = span{e} with e^2 = e.
Русский
В полносемпл-кольце каждый идеал порождается идемпотентом: I = span{e}, e^2 = e.
LaTeX
$$$[IsSemisimpleRing(R)]\\; \\Rightarrow\\; \\forall I:\\,\\text{Ideal }R,\\; \\exists e:\\,R,\\; IsIdempotentElem(e) \\land I = \\operatorname{span}\\{e\\}.$$$
Lean4
theorem ideal_eq_span_idempotent [IsSemisimpleRing R] (I : Ideal R) : ∃ e : R, IsIdempotentElem e ∧ I = .span { e } :=
by
obtain ⟨J, h⟩ := exists_isCompl I
obtain ⟨f, idem, rfl⟩ := I.isIdempotentElemEquiv.symm (I.isComplEquivProj ⟨J, h⟩)
exact
⟨f 1, LinearMap.isIdempotentElem_apply_one_iff.mpr idem, by
rw [LinearMap.range_eq_map, ← Ideal.span_one, ← Ideal.submodule_span_eq, LinearMap.map_span, Set.image_one,
Ideal.submodule_span_eq]⟩
