Krull dimension

TheoremKrull dimension does not increase along integral algebras#✓fully proved

Let \(A\) and \(B\) be commutative rings and let \(B\) be an \(A\)-algebra that is integral over \(A\). Then the Krull dimension of \(B\) is at most the Krull dimension of \(A\).

The structure map \(A \to B\) need not be injective. The inequality comes from incomparability: contracting prime ideals of \(B\) to \(A\) is strictly monotone, so it gives a strictly monotone map from the prime spectrum of \(B\) to the prime spectrum of \(A\).

theorem ringKrullDim_le_of_integral {A B : Type*} [CommRing A] [CommRing B]
    [Algebra A B] [Algebra.IsIntegral A B] : ringKrullDim B ≤ ringKrullDim A

Used by 1

Used byInjective integral maps preserve Krull dimension

TheoremPrime chains lift along injective integral maps#✓fully proved

Every finite chain of prime ideals lifts along an injective integral algebra map.

theorem exists_ltSeries_of_integral_of_injective {A B : Type*} [CommRing A] [CommRing B]
    [Algebra A B] [Algebra.IsIntegral A B] (hinj : Function.Injective (algebraMap A B))
    (p : LTSeries (PrimeSpectrum A)) :
    ∃ q : LTSeries (PrimeSpectrum B),
      q.length = p.length ∧
        List.map (PrimeSpectrum.comap (algebraMap A B)) q.toList = p.toList

Used by 1

Used byKrull dimension does not decrease along injective integral maps

TheoremKrull dimension does not decrease along injective integral maps#✓fully proved

Krull dimension cannot decrease along an injective integral algebra map.

theorem ringKrullDim_ge_of_integral_of_injective {A B : Type*} [CommRing A] [CommRing B]
    [Algebra A B] [Algebra.IsIntegral A B] (hinj : Function.Injective (algebraMap A B)) :
    ringKrullDim A ≤ ringKrullDim B

Uses 1 · Used by 1

Proof usesPrime chains lift along injective integral maps

Used byInjective integral maps preserve Krull dimension

TheoremInjective integral maps preserve Krull dimension#✓fully proved

An injective integral algebra map preserves Krull dimension.

theorem ringKrullDim_eq_of_integral_of_injective {A B : Type*} [CommRing A] [CommRing B]
    [Algebra A B] [Algebra.IsIntegral A B] (hinj : Function.Injective (algebraMap A B)) :
    ringKrullDim B = ringKrullDim A

Uses 2 · Used by 1

Proof usesKrull dimension does not decrease along injective integral maps · Krull dimension does not increase along integral algebras

Used byAdjoining a root of an Eisenstein-like polynomial preserves regularity

TheoremShort prime chains when the completion has dimension at most two#✓fully proved

In a Noetherian local domain whose adic completion has Krull dimension at most 2, any prime strictly below a non-maximal prime is ⊥.

theorem eq_bot_of_lt_of_ne_maximalIdeal_of_ringKrullDim_le_two
    {B : Type u} [CommRing B] [IsDomain B] [IsLocalRing B] [IsNoetherianRing B]
    {R : Type v} [CommRing R] (e : AdicCompletion (maximalIdeal B) B ≃+* R)
    (hR : ringKrullDim R ≤ 2) :
    ∀ 𝔭 𝔮 : Ideal B, 𝔭.IsPrime → 𝔮.IsPrime → 𝔮 ≠ maximalIdeal B → 𝔭 < 𝔮 → 𝔭 = ⊥

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.