Going down

In this file we define a predicate Algebra.HasGoingDown: 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.

Main results

• Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap: going down is equivalent to generalizations lifting along Spec S → Spec R.
• Algebra.HasGoingDown.of_flat: flat algebras satisfy going down.

Note

• For the fact that an integral extension of domains with normal base satisfies going down, see Mathlib/RingTheory/IntegralClosure/GoingDown.lean.

class Algebra.HasGoingDown (R : Type u_1) (S : Type u_2) [CommRing R] [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.

• exists_ideal_le_liesOver_of_lt {p : Ideal R} [p.IsPrime] (Q : Ideal S) [Q.IsPrime] : p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

theorem Ideal.exists_ideal_le_liesOver_of_le {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.HasGoingDown R S] {p q : Ideal R} [p.IsPrime] (Q : Ideal S) [Q.IsPrime] [Q.LiesOver q] (hle : p ≤ q) : ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

theorem Ideal.exists_ideal_lt_liesOver_of_lt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.HasGoingDown R S] {p q : Ideal R} [p.IsPrime] (Q : Ideal S) [Q.IsPrime] [Q.LiesOver q] (hpq : p < q) : ∃ P < Q, P.IsPrime ∧ P.LiesOver p

theorem Ideal.exists_ltSeries_of_hasGoingDown {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.HasGoingDown R S] (l : LTSeries (PrimeSpectrum R)) (P : Ideal S) [P.IsPrime] [lo : P.LiesOver (RelSeries.last l).asIdeal] : ∃ (L : LTSeries (PrimeSpectrum S)), L.length = l.length ∧ RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧ List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = RelSeries.toList l

theorem Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] : HasGoingDown R S ↔ GeneralizingMap (PrimeSpectrum.comap (algebraMap R S))

An R-algebra S has the going down property if and only if generalizations lift along Spec S → Spec R.

theorem Algebra.HasGoingDown.trans (R : Type u_3) (S : Type u_4) [CommRing R] [CommRing S] [Algebra R S] (T : Type u_5) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [HasGoingDown R S] [HasGoingDown S T] : HasGoingDown R T

Stacks Tag 00HX

theorem Algebra.HasGoingDown.of_comap_localRingHom_surjective {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (H : ∀ (P : Ideal S) [inst : P.IsPrime], Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))) : HasGoingDown R S

If for every prime of S, the map Spec Sₚ → Spec Rₚ is surjective, the algebra satisfies going down.

instance Algebra.HasGoingDown.of_flat {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] : HasGoingDown R S

Flat algebras satisfy the going down property.