Theorems · Theorem · algebraic geometry

ChevalleyThm.chevalley_polynomialC

∀ {R : Type u_6} [inst : CommRing R] (M : Submodule ℤ R),
  1 ∈ M →
    ∀ (S : PrimeSpectrum.ConstructibleSetData (Polynomial R)),
      (∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M) →
        ∃ T,
          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.

Defined in

Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRing