le_comap_jacobson — Mathlib

English

For a surjective ring homomorphism f: R → R', the Jacobson radical of R is contained in the comap of the Jacobson radical of R' along f.

Русский

Пусть f: R → R' сюръективно. Тогда jacobson(R) ⊆ comap_f(jacobson(R')).

LaTeX

$$$\\operatorname{jacobson}(R) \\le \\operatorname{Ideal.comap}_f\\big(\\operatorname{jacobson}(R')\\big).$$$

Lean4

theorem le_comap_jacobson : jacobson R ≤ Ideal.comap f (jacobson R₂) :=
  Module.le_comap_jacobson f.toSemilinearMap

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