Theorems · Inductive type · commutative algebra
Algebra.HasGoingDown
(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.HasGoingDown R S if for every pair of
prime ideals p ≤ q of R with Q a prime of S lying above q, there exists a
prime P ≤ Q of S lying above p.
The condition only asks for < which is easier to prove, use
Ideal.exists_ideal_le_liesOver_of_le for applying it.
- Defined in
- Mathlib.RingTheory.Ideal.GoingDown
- Cited by
- 11 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 by13
Results whose statement or proof uses this declaration.
- Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComapstatement and proof · cited by 4
- PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentationstatement and proof · cited by 2
- Ideal.exists_ideal_le_liesOver_of_lestatement and proof · cited by 2
- Ideal.exists_ltSeries_of_hasGoingDownstatement and proof · cited by 1
- Ideal.height_eq_height_add_of_liesOver_of_hasGoingDownstatement and proof · cited by 1
- Algebra.HasGoingDown.exists_ideal_le_liesOver_of_ltstatement and proof · cited by 1
- Polynomial.height_map_Cproof · cited by 1
- Ideal.exists_ideal_lt_liesOver_of_ltstatement and proof · cited by 1
- AlgebraicGeometry.Flat.generalizingMapproof · cited by 0
- Algebra.HasGoingDown.casesOnstatement and proof · cited by 0
- Algebra.HasGoingDown.of_comap_localRingHom_surjectivestatement · cited by 0
- Algebra.HasGoingDown.recOnstatement and proof · cited by 0