Documentation

Mathlib.RingTheory.Ideal.HasGoingUp

Going up #

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

This file closely mirrors Mathlib.RingTheory.Ideal.GoingDown.

Main results #

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

Instances
    source
    theorem Ideal.exists_ideal_ge_liesOver_of_le {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.HasGoingUp R S] {p q : Ideal R} [q.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p] (hle : p ≤ q) :
    ∃ (Q : Ideal S), P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q
    source
    theorem Ideal.exists_ideal_gt_liesOver_of_lt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.HasGoingUp R S] {p q : Ideal R} [q.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p] (hpq : p < q) :
    ∃ (Q : Ideal S), P < Q ∧ Q.IsPrime ∧ Q.LiesOver q
    source
    theorem Ideal.exists_ltSeries_of_hasGoingUp {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.HasGoingUp R S] (l : LTSeries (PrimeSpectrum R)) (P : Ideal S) [P.IsPrime] [lo : P.LiesOver (RelSeries.head l).asIdeal] :
    ∃ (L : LTSeries (PrimeSpectrum S)), L.length = l.length ∧ RelSeries.head L = { asIdeal := P, isPrime := ⋯ } ∧ List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = RelSeries.toList l

    This generalizes exists_ideal_over_prime_of_isIntegral_of_isPrime to arbitrary length chains.

    source
    theorem Algebra.HasGoingUp.iff_specializingMap_primeSpectrumComap {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] :
    HasGoingUp R S ↔ SpecializingMap (PrimeSpectrum.comap (algebraMap R S))

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

    source
    theorem Algebra.HasGoingUp.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] [HasGoingUp R S] [HasGoingUp S T] :
    HasGoingUp R T

    Stacks Tag 00HX

    source
    instance Algebra.HasGoingUp.of_isIntegral {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] :
    HasGoingUp R S

    Integral algebras satisfy the going up property.