Theorems · Theorem · algebraic geometry

ChevalleyThm.chevalley_mvPolynomialC

∀ {R : Type u_2} [inst : CommRing R] {n : ℕ} {M : Submodule ℤ R},
  1 ∈ M →
    ∀ (k : ℕ) (d : Multiset (Fin n)) (S : PrimeSpectrum.ConstructibleSetData (MvPolynomial (Fin n) R)),
      (∀ C ∈ S, C.n ≤ k) →
        (∀ C ∈ S,
            ∀ (j : Fin C.n),
              C.g j ∈
                MvPolynomial.coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (MvPolynomial.degreesLE R (Fin n) d)) →
          ∃ T,
            PrimeSpectrum.comap MvPolynomial.C '' S.toSet = T.toSet ∧
              ∀ C ∈ T,
                C.n ≤ ChevalleyThm.MvPolynomialC.numBound k (fun i => 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧
                  ∀ (i : Fin C.n),
                    C.g i ∈
                      M ^
                        ChevalleyThm.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.

Defined in

Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing