English
Under a going-down hypothesis, given prime p ≤ q in R, and Q a prime in S lying over q, there exists a prime P between them with P lying over p and P ≤ Q.
Русский
При условии свойства going-down, для p ≤ q в R и prime-предлагаемого Q в S, лежащего над q, существует простое P между ними с P lies over p и P ≤ Q.
LaTeX
$$$\forall R,S\, [\text{CommRing } R][\text{CommRing } S][\text{Algebra } R S]\; [p,q: \text{Ideal } R] [p.IsPrime][q.IsPrime] (Q: \text{Ideal } S)[Q.IsPrime][Q.LiesOver q] (hle: p \le q) \Rightarrow \exists P \le Q, P.IsPrime \land P.LiesOver p.$$$
Lean4
theorem exists_ideal_le_liesOver_of_le [Algebra.HasGoingDown R S] {p q : Ideal R} [p.IsPrime] [q.IsPrime] (Q : Ideal S)
[Q.IsPrime] [Q.LiesOver q] (hle : p ≤ q) : ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p :=
by
by_cases h : p = q
· subst h
use Q
· have := Q.over_def q
subst this
exact Algebra.HasGoingDown.exists_ideal_le_liesOver_of_lt Q (lt_of_le_of_ne hle h)
