theorem
finite_map_strict_chains
(A : Type u_1)
(B : Type u_2)
[CommRing A]
[CommRing B]
[Algebra A B]
[Module.Finite A B]
(p₁ p₂ : Ideal B)
[p₁.IsPrime]
[p₂.IsPrime]
(h : p₁ < p₂)
:
Lem 8, Lec 4: a finite morphism A → B sends a strict chain of primes
p₁ ⊊ p₂ in B to a strict chain p₁ ∩ A ⊊ p₂ ∩ A in A.