English
Let I be an ideal of a commutative ring R. Then I equals its Jacobson radical if and only if the Jacobson radical of the quotient ring R/I is the zero ideal.
Русский
Пусть I — идеал коммутативного кольца R. Тогда I равно своему радикалу Якобсона тогда и только тогда, когда радикал Якобсона кольца- namely радикал Якобсона факторкольца R/I равен нулю.
LaTeX
$$$I\,\mathrm{jacobson} = I \quad\Longleftrightarrow\quad \mathrm{jacobson}(\bot : \mathrm{Ideal}(R / I)) = \bot$$$
Lean4
/-- An ideal `I` of `R` is equal to its Jacobson radical if and only if
the Jacobson radical of the quotient ring `R/I` is the zero ideal -/
theorem jacobson_eq_iff_jacobson_quotient_eq_bot : I.jacobson = I ↔ jacobson (⊥ : Ideal (R ⧸ I)) = ⊥ :=
by
have hf : Function.Surjective (Ideal.Quotient.mk I) := Submodule.Quotient.mk_surjective I
constructor
· intro h
replace h := congr_arg (Ideal.map (Ideal.Quotient.mk I)) h
rw [map_jacobson_of_surjective hf (le_of_eq mk_ker)] at h
simpa using h
· intro h
replace h := congr_arg (comap (Ideal.Quotient.mk I)) h
rw [comap_jacobson_of_surjective hf, ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at h
simpa using h
