noncomputable def ChevalleyFiberDim.fiberKrullDim {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] (q : PrimeSpectrum B) : WithBot ℕ∞

The Krull dimension of the fiber of Spec A → Spec B over a prime q ∈ Spec B.

def ChevalleyFiberDim.genericPoint (B : Type u_1) [CommRing B] [IsDomain B] : PrimeSpectrum B

The generic point of Spec B for an integral domain B, given by the zero ideal.

def ChevalleyFiberDim.fiberDimGeInImage {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] (d : ℕ) : Set (PrimeSpectrum B)

The set of primes q in the image of Spec A → Spec B whose fiber has dimension at least d; this is the set whose upper semicontinuity is part of Chevalley's theorem.

theorem ChevalleyFiberDim.fiberKrullDim_generic_eq (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsDomain B] [Algebra B A] : fiberKrullDim (genericPoint B) = ringKrullDim A

The generic fiber of Spec A → Spec B has Krull dimension equal to dim A.

structure ChevalleyFiberDim.DominantFiniteTypeMorphism (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsDomain B] [IsDomain A] [IsNoetherianRing B] [Algebra B A] : Type

The bundled data of a dominant morphism of integral schemes of finite type: the algebra map is injective, the algebra is finite type, and we record the transcendence degree of the function field extension.

• injective : Function.Injective ⇑(algebraMap B A)
• finiteType : Algebra.FiniteType B A
• transDeg : ℕ

theorem ChevalleyFiberDim.fiber_nontrivial_of_in_image {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] {q : PrimeSpectrum B} (hq : q ∈ Set.range (PrimeSpectrum.comap (algebraMap B A))) : Nontrivial (A ⧸ Ideal.map (algebraMap B A) q.asIdeal)

If q ∈ Spec B is in the image of Spec A → Spec B, then the fiber over q is nontrivial (i.e. A / qA ≠ 0).

theorem ChevalleyFiberDim.fiber_dim_usc_image_constructible (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsNoetherianRing B] [Algebra B A] [Algebra.FiniteType B A] : Topology.IsConstructible (Set.range (PrimeSpectrum.comap (algebraMap B A)))

The image of a morphism of finite type between Noetherian affine schemes is constructible (Chevalley, Thm 21.2, Lec 21).

theorem ChevalleyFiberDim.fiberKrullDim_anti {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] {q q' : PrimeSpectrum B} (hle : q.asIdeal ≤ q'.asIdeal) : fiberKrullDim q' ≤ fiberKrullDim q

Fiber dimension is order-reversing: if q ⊆ q', then the fiber over q' has dimension at most that of the fiber over q.

theorem ChevalleyFiberDim.fiberKrullDim_le_generic {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [IsDomain B] [Algebra B A] (q : PrimeSpectrum B) : fiberKrullDim q ≤ fiberKrullDim (genericPoint B)

Every fiber dimension is bounded above by the dimension of the generic fiber.

theorem ChevalleyFiberDim.noether_normalization_descent (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsDomain B] [IsDomain A] [IsNoetherianRing B] [Algebra B A] [Algebra.FiniteType B A] (hf : Function.Injective ⇑(algebraMap B A)) : ∃ (n : ℕ) (b : B) (_ : b ≠ 0) (φ : MvPolynomial (Fin n) (Localization.Away b) →+* Localization.Away ((algebraMap B A) b)), φ.Finite ∧ Function.Injective ⇑φ ∧ φ.comp MvPolynomial.C = Localization.awayMap (algebraMap B A) b ∧ ↑(PrimeSpectrum.basicOpen b) ⊆ Set.range (PrimeSpectrum.comap (algebraMap B A))

Noether normalization descent: for a dominant finite-type morphism between integral domains, after inverting some nonzero b ∈ B, the localized algebra A[b⁻¹] is finite over a polynomial ring B[b⁻¹][x₁,…,xₙ], and the basic open D(b) lies in the image.

theorem ChevalleyFiberDim.lemma33_factorization (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsDomain B] [IsDomain A] [IsNoetherianRing B] [Algebra B A] [Algebra.FiniteType B A] (hf : Function.Injective ⇑(algebraMap B A)) : ∃ (n : ℕ) (b : B) (_ : b ≠ 0) (φ : MvPolynomial (Fin n) (Localization.Away b) →+* Localization.Away ((algebraMap B A) b)), φ.Finite ∧ Function.Injective ⇑φ ∧ φ.comp MvPolynomial.C = Localization.awayMap (algebraMap B A) b ∧ ↑(PrimeSpectrum.basicOpen b) ⊆ Set.range (PrimeSpectrum.comap (algebraMap B A))

Lemma 3.3 factorization: an alias for noether_normalization_descent, exposing the same existence statement under the name used in the textbook.

structure ChevalleyFiberDim.Lemma33Data (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [Algebra B A] : Type (max u_1 u_2)

Packaged data corresponding to the conclusion of Lemma 3.3: a nonzero element b ∈ B, an integer n, a finite injective map from B[b⁻¹][x₁,…,xₙ] into A[b⁻¹] compatible with the algebra map, and the fact that D(b) lies in the image of Spec A → Spec B.

• b : B
• hb : self.b ≠ 0
• n : ℕ
• φ : MvPolynomial (Fin self.n) (Localization.Away self.b) →+* Localization.Away ((algebraMap B A) self.b)
• φ_finite : self.φ.Finite
• φ_injective : Function.Injective ⇑self.φ
• φ_compat : self.φ.comp MvPolynomial.C = Localization.awayMap (algebraMap B A) self.b
• basicOpen_sub_image : ↑(PrimeSpectrum.basicOpen self.b) ⊆ Set.range (PrimeSpectrum.comap (algebraMap B A))

noncomputable def ChevalleyFiberDim.Lemma33Data.ofChevalley (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsDomain B] [IsDomain A] [IsNoetherianRing B] [Algebra B A] [Algebra.FiniteType B A] (hf : Function.Injective ⇑(algebraMap B A)) : Lemma33Data B A

Construct a Lemma33Data witness by unpacking the existence statement of lemma33_factorization.

theorem ChevalleyFiberDim.Lemma33Data.fiber_nontrivial {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] (L : Lemma33Data B A) {q : PrimeSpectrum B} (hq : q ∈ ↑(PrimeSpectrum.basicOpen L.b)) : Nontrivial (A ⧸ Ideal.map (algebraMap B A) q.asIdeal)

Over the basic open D(b) of Lemma33Data, the fibers of Spec A → Spec B are nontrivial.

theorem ChevalleyFiberDim.Lemma33Data.fiberKrullDim_nonneg {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] (L : Lemma33Data B A) {q : PrimeSpectrum B} (hq : q ∈ ↑(PrimeSpectrum.basicOpen L.b)) : 0 ≤ fiberKrullDim q

Over the basic open D(b), the fiber dimensions of Spec A → Spec B are nonnegative.

def ChevalleyFiberDim.fiberDimGe {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] (d : WithBot ℕ∞) : Set (PrimeSpectrum B)

The locus in Spec B where the fiber of Spec A → Spec B has dimension at least d.

theorem ChevalleyFiberDim.fiberDimGeInImage_eq_inter {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] (d : ℕ) : fiberDimGeInImage d = Set.range (PrimeSpectrum.comap (algebraMap B A)) ∩ fiberDimGe ↑d

fiberDimGeInImage d is the intersection of the image with the d-th fiber-dimension locus.

theorem ChevalleyFiberDim.flat_morphism_isOpenMap (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsNoetherianRing B] [Algebra B A] [Algebra.FiniteType B A] [Module.Flat B A] : IsOpenMap (PrimeSpectrum.comap (algebraMap B A))

A flat morphism of finite type between Noetherian schemes is an open map.

noncomputable def ChevalleyFiberDim.doubleQuot_fiber_equiv {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [Algebra B A] {𝔭 q' : PrimeSpectrum B} (hle : 𝔭.asIdeal ≤ q'.asIdeal) : (A ⧸ Ideal.map (algebraMap B A) 𝔭.asIdeal) ⧸ Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap B A) 𝔭.asIdeal)) (Ideal.map (algebraMap B A) q'.asIdeal) ≃+* A ⧸ Ideal.map (algebraMap B A) q'.asIdeal

A ring equivalence comparing the iterated fiber (A/𝔭A)/(q'A) to the fiber A/q'A, used when comparing fiber dimensions along specializations.

theorem ChevalleyFiberDim.chevalley_thm21_2_part1 (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsNoetherianRing B] [Algebra B A] [Algebra.FiniteType B A] : Topology.IsConstructible (Set.range (PrimeSpectrum.comap (algebraMap B A)))

Part 1 of Chevalley's Theorem 21.2 (Lec 21): the image of a morphism of finite type between Noetherian schemes is constructible.

theorem ChevalleyFiberDim.fiberDimGe_isClosed (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsDomain B] [IsDomain A] [IsNoetherianRing B] [Algebra B A] [Algebra.FiniteType B A] (hf : Function.Injective ⇑(algebraMap B A)) (d : ℕ) : IsClosed (fiberDimGe ↑d)

The locus where the fiber dimension is at least d is closed: this is the geometric form of upper semicontinuity of fiber dimension.

theorem ChevalleyFiberDim.chevalley_thm21_2_part2 (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsDomain B] [IsDomain A] [IsNoetherianRing B] [Algebra B A] [Algebra.FiniteType B A] (hf : Function.Injective ⇑(algebraMap B A)) (d : ℕ) : ∃ (Z : Set (PrimeSpectrum B)), IsClosed Z ∧ fiberDimGeInImage d = Set.range (PrimeSpectrum.comap (algebraMap B A)) ∩ Z

Part 2 of Chevalley's Theorem 21.2 (Lec 21): upper semicontinuity of fiber dimension. The locus in the image where fibers have dimension at least d is the trace of a closed set.

theorem ChevalleyFiberDim.chevalley_thm21_2_fiber_dim_lower_bound (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsDomain B] [IsDomain A] [IsNoetherianRing B] [Algebra B A] [Algebra.FiniteType B A] (hf : Function.Injective ⇑(algebraMap B A)) {q : PrimeSpectrum B} (hq : q ∈ Set.range (PrimeSpectrum.comap (algebraMap B A))) : fiberKrullDim q + ringKrullDim B ≥ ringKrullDim A

For dominant morphisms of finite type, every nonempty fiber has dimension at least dim A - dim B.

theorem ChevalleyFiberDim.chevalley_thm21_2_part3 (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsDomain B] [IsDomain A] [IsNoetherianRing B] [Algebra B A] [Algebra.FiniteType B A] (hf : Function.Injective ⇑(algebraMap B A)) : ∃ (b : B), b ≠ 0 ∧ ↑(PrimeSpectrum.basicOpen b) ⊆ Set.range (PrimeSpectrum.comap (algebraMap B A)) ∧ ∀ q ∈ ↑(PrimeSpectrum.basicOpen b), fiberKrullDim q + ringKrullDim B = ringKrullDim A

Part 3 of Chevalley's Theorem 21.2 (Lec 21): if f : Spec A → Spec B has dense image, there is a nonempty open subset U ⊆ Spec B over which every fiber has the expected dimension dim A - dim B.