Preimage_of_Ideal_under_Ring_Homomorphism_is_Ideal
Provedideal-theoryproofwikiring-homomorphisms
Let be a ring homomorphism. Let be an ideal of . Then is an ideal of such that .
Preamble
import Mathlib.RingTheory.Ideal.Basic
Formal statement
theorem Preimage_of_Ideal_under_Ring_Homomorphism_is_Ideal {R₁ R₂ : Type _} [CommRing R₁] [CommRing R₂] (f : R₁ →+* R₂) (I : Ideal R₂) : ∃ J : Ideal R₁, (↑J : Set R₁) = f ⁻¹' (↑I : Set R₂) := by sorrySource