English
The Jacobson radical of the quotient R/I, as a subset of R/I, equals Module.jacobson R on the quotient, i.e. (jacobson(R/I)) = (Module.jacobson R)(R/I).
Русский
Радикал Якобсона частного кольца R/I равен радикалу Якобсона R, рассмотренного как модуль над R, на факторкольце R/I.
LaTeX
$$$$(\\operatorname{jacobson}(R/I) : \\text{Set}(R/I)) = \\operatorname{Module.jacobson}_R(R/I).$$$$
Lean4
theorem coe_jacobson_quotient (I : Ideal R) [I.IsTwoSided] :
(jacobson (R ⧸ I) : Set (R ⧸ I)) = Module.jacobson R (R ⧸ I) :=
by
let f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := ⟨AddHom.id _, fun _ _ ↦ rfl⟩
rw [jacobson, ← Module.map_jacobson_of_ker_le (f := f) Function.surjective_id]
· apply Set.image_id
· rintro _ rfl; exact zero_mem _
