jacobson_quotient_of_le — Mathlib

English

If I ≤ jacobson R, then jacobson(R/I) equals the image of jacobson R under the quotient map by I.

Русский

Пусть I ⊆ jacobson(R). Тогда jacobson(R/I) равен образу jacobson(R) при факторизации по I.

LaTeX

$$$\\operatorname{jacobson}(R/I) = \\operatorname{Submodule.map}(\\operatorname{Ideal.Quotient.mk} I).toSemilinearMap(\\operatorname{jacobson}(R)).$$$

Lean4

theorem jacobson_quotient_of_le {I : Ideal R} [I.IsTwoSided] (le : I ≤ jacobson R) :
    jacobson (R ⧸ I) = Submodule.map (Ideal.Quotient.mk I).toSemilinearMap (jacobson R) :=
  .symm <| Module.map_jacobson_of_ker_le (by exact Ideal.Quotient.mk_surjective) <| by rwa [← I.ker_mkQ] at le

Похожие утверждения