Chevalley's theorem with complexity bound

⚠ For general usage, see Mathlib/RingTheory/Spectrum/Prime/Chevalley.lean.

Chevalley's theorem states that if f : R → S is a finitely presented ring hom between commutative rings, then the image of a constructible set in Spec S is a constructible set in Spec R.

Constructible sets in the prime spectrum of R[X] are made of closed sets in the prime spectrum (using unions, intersections, and complements), which are themselves made from a family of polynomials.

We say a closed set has complexity at most M if it can be written as the zero locus of a family of at most M polynomials each of degree at most M. We say a constructible set has complexity at most M if it can be written as (C₁ ∪ ... ∪ Cₖ) \ D where k ≤ M, C₁, ..., Cₖ are closed sets of complexity at most M and D is a closed set.

This file proves a complexity-aware version of Chevalley's theorem, namely that a constructible set of complexity at most M in Spec R[X₁, ..., Xₘ] gets mapped under f : R[Y₁, ..., Yₙ] → R[X₁, ..., Xₘ] to a constructible set of complexity O_{M, m, n}(1) in Spec R[Y₁, ..., Yₙ].

The bound O_{M, m, n}(1) we find is of tower type.

Sketch proof

We first show the result in the case of C : R → R[X]. We prove this by induction on the number of components of the form (C₁ ∪ ... ∪ Cₖ) \ D, then by induction again on the number of polynomials used to describe (C₁ ∪ ... ∪ Cₖ). See the (private) lemma chevalley_polynomialC.

Secondly, we prove the result in the case of C : R → R[X₁, ..., Xₘ] by composing the first result with itself m times. See the (private) lemma chevalley_mvPolynomialC.

Note that, if composing the first result for C : R → R[X₁] and C : R[X₁] → R[X₁, X₂] naïvely, the second map C : R[X₁] → R[X₁, X₂] won't see the X₁-degree of the polynomials used to describe the constructible set in Spec R[X₁]. One therefore needs to track a subgroup of the ring which all coefficients of all used polynomials lie in.

Finally, we deduce the result for any f : R[Y₁, ..., Yₙ] → R[X₁, ..., Xₘ] by decomposing it into two maps C : R[Y₁, ..., Yₙ] → R[X₁, ..., Xₘ, Y₁, ..., Yₙ] and σ : R[X₁, ..., Xₘ, Y₁, ..., Yₙ] → R[X₁, ..., Xₘ]. See chevalley_mvPolynomial_mvPolynomial.

Main reference

The structure of the proof follows https://stacks.math.columbia.edu/tag/00FE, although they do not give an explicit bound on the complexity.

The C : R → R[X] case

theorem ChevalleyThm.chevalley_polynomialC {R : Type u_6} [CommRing R] (M : Submodule ℤ R) (hM : 1 ∈ M) (S : PrimeSpectrum.ConstructibleSetData (Polynomial R)) (hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M) : ∃ (T : PrimeSpectrum.ConstructibleSetData R), PrimeSpectrum.comap Polynomial.C '' S.toSet = T.toSet ∧ ∀ C ∈ T, C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound

The C : R → R[X] case of Chevalley's theorem with complexity bound.

The C : R → R[X₁, ..., Xₘ] case

@[irreducible]

def ChevalleyThm.MvPolynomialC.numBound (k : ℕ) (D : ℕ → ℕ) : ℕ → ℕ

The bound on the number of polynomials used to describe the constructible set appearing in the case of C : R → R[X₁, ..., Xₘ] of Chevalley's theorem with complexity bound.

@[irreducible]

def ChevalleyThm.MvPolynomialC.degBound (k : ℕ) (D : ℕ → ℕ) : ℕ → ℕ

The bound on the degree of the polynomials used to describe the constructible set appearing in the case of C : R → R[X₁, ..., Xₘ] of Chevalley's theorem with complexity bound.

@[simp]

theorem ChevalleyThm.MvPolynomialC.degBound_zero (k : ℕ) (D : ℕ → ℕ) : degBound k D 0 = 1

@[simp]

theorem ChevalleyThm.MvPolynomialC.numBound_zero (k : ℕ) (D : ℕ → ℕ) : numBound k D 0 = k

@[simp]

theorem ChevalleyThm.MvPolynomialC.degBound_succ (k : ℕ) (D : ℕ → ℕ) (n : ℕ) : degBound k D (n + 1) = numBound k D (n + 1) ^ numBound k D (n + 1) * degBound k D n

@[simp]

theorem ChevalleyThm.MvPolynomialC.numBound_succ (k : ℕ) (D : ℕ → ℕ) (n : ℕ) : numBound k D (n + 1) = numBound k D n * degBound k D n * D n

@[irreducible]

theorem ChevalleyThm.MvPolynomialC.degBound_casesOn_succ (k₀ k : ℕ) (D : ℕ → ℕ) (n : ℕ) : degBound k₀ (fun (t : ℕ) => Nat.casesOn t k D) (n + 1) = (k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n

@[irreducible]

theorem ChevalleyThm.MvPolynomialC.numBound_casesOn_succ (k₀ k : ℕ) (D : ℕ → ℕ) (n : ℕ) : numBound k₀ (fun (x : ℕ) => Nat.casesOn x k D) (n + 1) = numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n

@[irreducible]

theorem ChevalleyThm.MvPolynomialC.degBound_le_degBound {k₁ k₂ : ℕ} {D₁ D₂ : ℕ → ℕ} (hk : k₁ ≤ k₂) (n : ℕ) : (∀ i < n, D₁ i ≤ D₂ i) → degBound k₁ D₁ n ≤ degBound k₂ D₂ n

@[irreducible]

theorem ChevalleyThm.MvPolynomialC.numBound_mono {k₁ k₂ : ℕ} {D₁ D₂ : ℕ → ℕ} (hk : k₁ ≤ k₂) (n : ℕ) : (∀ i < n, D₁ i ≤ D₂ i) → numBound k₁ D₁ n ≤ numBound k₂ D₂ n

theorem ChevalleyThm.MvPolynomialC.degBound_pos (k : ℕ) (D : ℕ → ℕ) (n : ℕ) : 0 < degBound k D n

theorem ChevalleyThm.chevalley_mvPolynomialC {R : Type u_2} [CommRing R] {n : ℕ} {M : Submodule ℤ R} (hM : 1 ∈ M) (k : ℕ) (d : Multiset (Fin n)) (S : PrimeSpectrum.ConstructibleSetData (MvPolynomial (Fin n) R)) (hSn : ∀ C ∈ S, C.n ≤ k) (hS : ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ MvPolynomial.coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (MvPolynomial.degreesLE R (Fin n) d)) : ∃ (T : PrimeSpectrum.ConstructibleSetData R), PrimeSpectrum.comap MvPolynomial.C '' S.toSet = T.toSet ∧ ∀ C ∈ T, C.n ≤ MvPolynomialC.numBound k (fun (i : ℕ) => 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ MvPolynomialC.degBound k (fun (i : ℕ) => 1 + Multiset.count i (Multiset.map Fin.val d)) n

The C : R → R[X₁, ..., Xₘ] case of Chevalley's theorem with complexity bound.

The general f : R[Y₁, ..., Yₙ] → R[X₁, ..., Xₘ] case

def ChevalleyThm.numBound (k m n : ℕ) (d : Multiset (Fin m)) : ℕ

The bound on the number of polynomials used to describe the constructible set appearing in Chevalley's theorem with complexity bound.

def ChevalleyThm.degBound (k m n : ℕ) (d : Multiset (Fin m)) : ℕ

The bound on the degree of the polynomials used to describe the constructible set appearing in Chevalley's theorem with complexity bound.

theorem chevalley_mvPolynomial_mvPolynomial {R : Type u_2} [CommRing R] {m n : ℕ} (f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R) (k : ℕ) (d : Multiset (Fin m)) (S : PrimeSpectrum.ConstructibleSetData (MvPolynomial (Fin m) R)) (hSn : ∀ C ∈ S, C.n ≤ k) (hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d) (hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d) : ∃ (T : PrimeSpectrum.ConstructibleSetData (MvPolynomial (Fin n) R)), PrimeSpectrum.comap ↑f '' S.toSet = T.toSet ∧ ∀ C ∈ T, C.n ≤ ChevalleyThm.numBound k m n d ∧ ∀ (i : Fin C.n) (j : Fin n), MvPolynomial.degreeOf j (C.g i) ≤ ChevalleyThm.degBound k m n d

Chevalley's theorem with complexity bound.

A constructible set of complexity at most M in Spec R[X₁, ..., Xₘ] gets mapped under f : R[Y₁, ..., Yₙ] → R[X₁, ..., Xₘ] to a constructible set of complexity O_{M, m, n}(1) in Spec R[Y₁, ..., Yₙ].

See the module doc of Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean for an explanation of this notion of complexity.