theorem FiniteMorphismDimension.PrimeSpectrum.comap_strictMono_of_isIntegral {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] [Algebra.IsIntegral B A] : StrictMono (PrimeSpectrum.comap (algebraMap B A))

For an integral extension B → A, the induced map on prime spectra is strictly monotone, so chains in Spec A descend to chains in Spec B.

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

An integral extension B → A satisfies dim A ≤ dim B, via strict monotonicity of Spec on chains.

theorem FiniteMorphismDimension.exists_lift_chain {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] [Algebra.IsIntegral B A] (hinj : Function.Injective ⇑(algebraMap B A)) (n : ℕ) (f : Fin (n + 1) → PrimeSpectrum B) (hf : ∀ (i : Fin n), f i.castSucc < f i.succ) : ∃ (g : Fin (n + 1) → PrimeSpectrum A), (∀ (i : Fin (n + 1)), PrimeSpectrum.comap (algebraMap B A) (g i) = f i) ∧ ∀ (i : Fin n), g i.castSucc < g i.succ

Going-up: an injective integral extension lifts any strict chain of primes in B to a strict chain in A with prescribed comap images.

theorem FiniteMorphismDimension.ringKrullDim_ge_of_injective_integral {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] [Algebra.IsIntegral B A] (hinj : Function.Injective ⇑(algebraMap B A)) : ringKrullDim B ≤ ringKrullDim A

Combined with going-up: an injective integral extension also satisfies dim B ≤ dim A, so an integral surjection preserves Krull dimension.

theorem FiniteMorphismDimension.ringKrullDim_eq_of_injective_finite {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] [Module.Finite B A] (hinj : Function.Injective ⇑(algebraMap B A)) : ringKrullDim A = ringKrullDim B

Lem 10, Lec 5: a finite injective morphism preserves Krull dimension, i.e. dim X = dim Y for a finite surjection X → Y.