English
If f is a ring isomorphism, then mapping an ideal forward by f and then mapping back by f’s inverse recovers the original ideal.
Русский
Если f — кольцевой изоморфизм, то отображение вперёд и обратно восстанавливает исходный идеал.
LaTeX
$$$f : R \simeq+* S \Rightarrow (I.map f).map f^{-1} = I$$$
Lean4
/-- If `f : R ≃+* S` is a ring isomorphism and `I : Ideal R`, then `map f.symm (map f I) = I`. -/
@[simp]
theorem map_of_equiv {I : Ideal R} (f : R ≃+* S) : (I.map (f : R →+* S)).map (f.symm : S →+* R) = I := by
rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, map_map, RingEquiv.toRingHom_eq_coe,
RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, map_id]
