Theorems · Inductive type · commutative algebra
Algebra.HasGoingUp
(R : Type u_1) → (S : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Prop
An R-algebra S satisfies Algebra.HasGoingUp R S if for every pair of
prime ideals p ≤ q of R with P a prime of S lying above p, there exists a
prime P ≤ Q of S lying above q.
The condition only asks for < which is easier to prove, use
Ideal.exists_ideal_ge_liesOver_of_le for applying it.
- Defined in
- Mathlib.RingTheory.Ideal.HasGoingUp
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by8
Results whose statement or proof uses this declaration.
- Ideal.exists_ideal_ge_liesOver_of_lestatement and proof · cited by 2
- Algebra.HasGoingUp.exists_ideal_ge_liesOver_of_ltstatement and proof · cited by 1
- Algebra.HasGoingUp.iff_specializingMap_primeSpectrumComapstatement and proof · cited by 1
- Ideal.exists_ideal_gt_liesOver_of_ltstatement and proof · cited by 1
- Ideal.exists_ltSeries_of_hasGoingUpstatement and proof · cited by 0
- Algebra.HasGoingUp.casesOnstatement and proof · cited by 0
- Algebra.HasGoingUp.recOnstatement and proof · cited by 0
- Algebra.HasGoingUp.transstatement and proof · cited by 0