English
If I is a finitely generated ideal in a commutative ring R and I is idempotent (I^2 = I), then I = R e for some idempotent e ∈ R.
Русский
Если I — конечнопоргенитированный идempotентный идеал кольца R (I^2 = I), то существует идемпотентный элемент e ∈ R такой, что I = R e.
LaTeX
$$$\\text{FG}(I) \\ \land \ I^2 = I \\ \\Rightarrow \\ \\exists e \\in R,\\ e^2 = e \\land I = R e$$$
Lean4
/-- A finitely generated idempotent ideal is generated by an idempotent element -/
theorem isIdempotentElem_iff_of_fg {R : Type*} [CommRing R] (I : Ideal R) (h : I.FG) :
IsIdempotentElem I ↔ ∃ e : R, IsIdempotentElem e ∧ I = R ∙ e :=
by
constructor
· intro e
obtain ⟨r, hr, hr'⟩ :=
Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I I h
(by
rw [smul_eq_mul]
exact e.ge)
simp_rw [smul_eq_mul] at hr'
refine ⟨r, hr' r hr, antisymm ?_ ((Submodule.span_singleton_le_iff_mem _ _).mpr hr)⟩
intro x hx
rw [← hr' x hx]
exact Ideal.mem_span_singleton'.mpr ⟨_, mul_comm _ _⟩
· rintro ⟨e, he, rfl⟩
simp [IsIdempotentElem, Ideal.span_singleton_mul_span_singleton, he.eq]
