English
The standard radical and Jacobson radical of an ideal I coincide if and only if the nilradical and Jacobson radical of the quotient ring R/I coincide.
Русский
Стандартный радикал и радикал Якобсона идеала I совпадают тогда и только тогда, когда нильрадикал и радикал Якобсона частного кольца R/I совпадают.
LaTeX
$$$I.\mathrm{radical} = I.\mathrm{jacobson} \;\;\Longleftrightarrow\;\; \mathrm{radical}(\bot : \mathrm{Ideal}(R / I)) = \mathrm{jacobson}(\bot)$$$
Lean4
/-- The standard radical and Jacobson radical of an ideal `I` of `R` are equal if and only if
the nilradical and Jacobson radical of the quotient ring `R/I` coincide -/
theorem radical_eq_jacobson_iff_radical_quotient_eq_jacobson_bot :
I.radical = I.jacobson ↔ radical (⊥ : Ideal (R ⧸ I)) = jacobson ⊥ :=
by
have hf : Function.Surjective (Ideal.Quotient.mk I) := Submodule.Quotient.mk_surjective I
constructor
· intro h
have := congr_arg (map (Ideal.Quotient.mk I)) h
rw [map_radical_of_surjective hf (le_of_eq mk_ker), map_jacobson_of_surjective hf (le_of_eq mk_ker)] at this
simpa using this
· intro h
have := congr_arg (comap (Ideal.Quotient.mk I)) h
rw [comap_radical, comap_jacobson_of_surjective hf, ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at this
simpa using this
