English
Let R and S be rings and f: R → S be a ring isomorphism. If I is a prime ideal of R, then the image f(I) is a prime ideal of S.
Русский
Пусть R и S — кольца, и f: R → S — кольцо-изоморфизм. Если I — простой идеал R, то образ f(I) — простой идеал S.
LaTeX
$$$\\text{Let } f:\\;R \\cong S \\text{ be a ring isomorphism and } I \\lhd R\\text{ with } I \\text{ prime}.\\\\\\map f I \\text{ is prime in } S.$$$
Lean4
/-- A ring isomorphism sends a prime ideal to a prime ideal. -/
instance map_isPrime_of_equiv {F' : Type*} [EquivLike F' R S] [RingEquivClass F' R S] (f : F') {I : Ideal R}
[IsPrime I] : IsPrime (map f I) :=
by
have h : I.map f = I.map ((f : R ≃+* S) : R →+* S) := rfl
rw [h, map_comap_of_equiv (f : R ≃+* S)]
exact Ideal.IsPrime.comap (RingEquiv.symm (f : R ≃+* S))
