Lemmas about primesOver in quotient rings.

theorem Ideal.ncard_primesOver_lt_of_not_le {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (f : S →ₐ[R] T) (Hf : Function.Surjective ⇑f) (P : Ideal R) (P' : Ideal S) [P'.IsPrime] [P'.LiesOver P] (hkP' : ¬RingHom.ker f.toRingHom ≤ P') (H : (P.primesOver S).Finite) : (P.primesOver T).ncard < (P.primesOver S).ncard

Given a prime P of R and an ideal I in an R-algebra S. Suppose we can find a prime P' over P, not containing I, then the number of primes of S / I over P is strictly less than primes of S over P (provided they are finite).

The lemma is stated in terms of surjections for syntactic generality.

theorem Ideal.ncard_primesOver_quotient_singleton_lt_of_notMem {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Ideal R) (e : S) (P' : Ideal S) [P'.IsPrime] [P'.LiesOver P] (heP' : e ∉ P') (H : (P.primesOver S).Finite) : (P.primesOver (S ⧸ span {e})).ncard < (P.primesOver S).ncard