map_jacobson_of_bijective — Mathlib

English

If f is bijective, then map f preserves Jacobson radical: map f I.jacobson = (map f I).jacobson.

Русский

Если отображение f биективно, то сохраняется радикал Якобиана: map f I.jacobson = (map f I).jacobson.

LaTeX

$$$\operatorname{map}_f I^{\mathrm{jacobson}} = (\operatorname{map}_f I)^{\mathrm{jacobson}}$$$

Lean4

theorem map_jacobson_of_bijective {f : R →+* S} (hf : Function.Bijective f) : map f I.jacobson = (map f I).jacobson :=
  map_jacobson_of_surjective hf.right (le_trans (le_of_eq ((RingHom.injective_iff_ker_eq_bot f).1 hf.left)) bot_le)

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