map_radical — Mathlib

English

Localization commutes with taking radicals: the radical of the image equals the image of the radical.

Русский

Локализация сохраняет радикал: образ радикала равен радикалу образа.

LaTeX

$$$I.radical.map(\\mathrm{algebraMap}\\;R\\;S)=(I.map(\\mathrm{algebraMap}\\;R\\;S)).radical$$$

Lean4

theorem map_radical (I : Ideal R) : I.radical.map (algebraMap R S) = (I.map (algebraMap R S)).radical :=
  by
  refine (I.map_radical_le (algebraMap R S)).antisymm ?_
  rintro x ⟨n, hn⟩
  obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective M x
  simp only [← IsLocalization.mk'_pow, IsLocalization.mk'_mem_map_algebraMap_iff M] at hn ⊢
  obtain ⟨s, hs, h⟩ := hn
  refine ⟨s, hs, n + 1, by convert I.mul_mem_left (s ^ n * x) h; ring⟩

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