∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  Function.Surjective ⇑f →
    ∀ {I : Ideal R},
      RingHom.ker f = I →
        ∀ (p : Ideal R) (isPrime : p.IsPrime),
          { asIdeal := p, isPrime := isPrime } ∈ PrimeSpectrum.zeroLocus ↑I → (Ideal.map f p).IsPrime