Theorems · Theorem · algebraic geometry

chevalley_mvPolynomial_mvPolynomial

∀ {R : Type u_2} [inst : 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)),
  (∀ C ∈ S, C.n ≤ k) →
    (∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d) →
      (∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d) →
        ∃ T,
          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.

Defined in

Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Cited by

0 results in Mathlib

Foundations

Depth 133 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing