Essential dimension of symmetric groups

AbbreviationThe function field \(\mathbb{C}(x_1, \dots, x_n)\)#✓fully proved

For \(n \in \mathbb{N}\), the function field \(\mathbb{C}(x_1, \dots, x_n)\) is the fraction field of the polynomial ring \(\mathbb{C}[x_1, \dots, x_n]\) in \(n\) indeterminates.

abbrev rootsField (n : ℕ) : Type :=
  FractionRing (MvPolynomial (Fin n) ℂ)

Used by 23

Used byThe roots generate the function field · Elementary symmetric polynomials evaluated at the roots · Polynomials in the roots · The coefficients are algebraically independent · The roots are algebraically independent · The coefficients of the general polynomial · Coefficients in the coefficient field · Coefficients indexed by degree · Essential dimension of the symmetric group · Trivial upper bound for the essential dimension of \(S_n\) · Coefficient field of the general polynomial · General polynomial · Rational functions are algebraic over the polynomial subalgebra · Distinct linear factors are coprime · Descent of the general polynomial extension · The trivial descent · The roots of the general polynomial generate the function field · The roots \(x_i\) · The roots \(x_i\) are pairwise distinct · Each \(x_i\) is a root of the general polynomial · The product of the linear factors \(X - x_i\) is separable · Transcendence degree of the coefficient field · Transcendence degree of \(\mathbb{C}(x_1, \dots, x_n)\)

DefinitionThe roots \(x_i\)#✓fully proved

For \(n \in \mathbb{N}\) and \(i \in \{1, \dots, n\}\), \(x_i\) is the \(i\)-th indeterminate of the polynomial ring \(\mathbb{C}[x_1, \dots, x_n]\), viewed as an element of its fraction field, the function field \(\mathbb{C}(x_1, \dots, x_n)\).

These elements are the roots of the general polynomial.

noncomputable def root (n : ℕ) (i : Fin n) : rootsField n :=
  algebraMap (MvPolynomial (Fin n) ℂ) (rootsField n) (X i)

Uses 1 · Used by 11

Statement usesThe function field \(\mathbb{C}(x_1, \dots, x_n)\)

Used byThe roots generate the function field · Elementary symmetric polynomials evaluated at the roots · Polynomials in the roots · The roots are algebraically independent · Rational functions are algebraic over the polynomial subalgebra · The trivial descent · The roots of the general polynomial generate the function field · The roots \(x_i\) are pairwise distinct · Each \(x_i\) is a root of the general polynomial · The product of the linear factors \(X - x_i\) is separable · Transcendence degree of \(\mathbb{C}(x_1, \dots, x_n)\)

DefinitionThe coefficients of the general polynomial#✓fully proved

For \(0 \le i < n\), the coefficient \(a_{i+1}\) is the \((i+1)\)-st elementary symmetric function of \(x_1, \dots, x_n\), as an element of the function field \(\mathbb{C}(x_1, \dots, x_n)\).

noncomputable def coeff (n : ℕ) (i : Fin n) : rootsField n :=
  algebraMap (MvPolynomial (Fin n) ℂ) (rootsField n)
    (esymm (Fin n) ℂ (i.val + 1))

Uses 1 · Used by 6

Statement usesThe function field \(\mathbb{C}(x_1, \dots, x_n)\)

Used byThe coefficients are algebraically independent · Coefficients in the coefficient field · Coefficient field of the general polynomial · The trivial descent · Each \(x_i\) is a root of the general polynomial · Transcendence degree of the coefficient field

DefinitionCoefficient field of the general polynomial#✓fully proved

For a natural number \(n\), let \(\mathbb{C}(x_1, \dots, x_n)\) be the field of rational functions in \(n\) indeterminates and, for \(1 \le k \le n\), let \(a_k\) be the \(k\)-th elementary symmetric function of \(x_1, \dots, x_n\). The coefficient field \(\mathbb{C}(a_1, \dots, a_n)\) is the intermediate field of \(\mathbb{C} \subseteq \mathbb{C}(x_1, \dots, x_n)\) generated over \(\mathbb{C}\) by \(a_1, \dots, a_n\).

noncomputable def generalBaseField (n : ℕ) :
    IntermediateField ℂ (rootsField n) :=
  IntermediateField.adjoin ℂ (Set.range (coeff n))

Uses 2 · Used by 9

Statement usesThe coefficients of the general polynomial · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Used byCoefficients in the coefficient field · Coefficients indexed by degree · Trivial upper bound for the essential dimension of \(S_n\) · General polynomial · Descent of the general polynomial extension · The trivial descent · The roots of the general polynomial generate the function field · Each \(x_i\) is a root of the general polynomial · Transcendence degree of the coefficient field

DefinitionCoefficients in the coefficient field#✓fully proved

For \(0 \le i < n\), the coefficient \(a_{i+1}\), the \((i+1)\)-st elementary symmetric function of \(x_1, \dots, x_n\), regarded as an element of the coefficient field \(\mathbb{C}(a_1, \dots, a_n)\).

noncomputable def coeffElem (n : ℕ) (i : Fin n) : ↥(generalBaseField n) :=
  ⟨coeff n i, by exact (IntermediateField.subset_adjoin ℂ _) (Set.mem_range_self i)⟩

Uses 3 · Used by 4

Statement usesThe coefficients of the general polynomial · Coefficient field of the general polynomial · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Used byCoefficients indexed by degree · The trivial descent · Each \(x_i\) is a root of the general polynomial · Transcendence degree of the coefficient field

TheoremThe roots \(x_i\) are pairwise distinct#✓fully proved

For every \(n \in \mathbb{N}\), the elements \(x_1, \dots, x_n\) of the function field \(\mathbb{C}(x_1, \dots, x_n)\) are pairwise distinct: \(x_i = x_j\) implies \(i = j\).

theorem root_injective (n : ℕ) : Function.Injective (root n)

Uses 2 · Used by 2

Statement usesThe roots \(x_i\) · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Used byThe product of the linear factors \(X - x_i\) is separable · Transcendence degree of \(\mathbb{C}(x_1, \dots, x_n)\)

TheoremAlgebraic independence of the elementary symmetric polynomials#✓fully proved

For every natural number \(n\), the elementary symmetric polynomials \(e_1, \dots, e_n \in \mathbb{C}[X_1, \dots, X_n]\) are algebraically independent over \(\mathbb{C}\).

This follows from the fundamental theorem of symmetric polynomials.

theorem algebraicIndependent_esymm (n : ℕ) :
    AlgebraicIndependent ℂ
      (fun i : Fin n => esymm (Fin n) ℂ (i.val + 1) :
        Fin n → MvPolynomial (Fin n) ℂ)

Used by 1

Used byThe coefficients are algebraically independent

TheoremInjective algebra maps preserve algebraic independence#✓fully proved

Let \(A\) and \(B\) be commutative \(\mathbb{C}\)-algebras, let \(f : A \to B\) be an injective \(\mathbb{C}\)-algebra homomorphism, and let \((x_i)_{i \in \iota}\) be a family in \(A\) that is algebraically independent over \(\mathbb{C}\). Then the family \((f(x_i))_{i \in \iota}\) is algebraically independent over \(\mathbb{C}\).

theorem algebraicIndependent_map {ι : Type*} {A B : Type*}
    [CommRing A] [CommRing B] [Algebra ℂ A] [Algebra ℂ B]
    {x : ι → A} (hx : AlgebraicIndependent ℂ x) (f : A →ₐ[ℂ] B)
    (hf : Function.Injective f) :
    AlgebraicIndependent ℂ (f ∘ x)

Used by 2

Used byThe coefficients are algebraically independent · The roots are algebraically independent

TheoremThe coefficients are algebraically independent#✓fully proved

For every natural number \(n\), the coefficients \(a_1, \dots, a_n\) of the general polynomial, the elementary symmetric functions of \(x_1, \dots, x_n\), are algebraically independent over \(\mathbb{C}\) in the function field \(\mathbb{C}(x_1, \dots, x_n)\).

theorem algebraicIndependent_coeff (n : ℕ) :
    AlgebraicIndependent ℂ (coeff n)

Uses 4 · Used by 1

Statement usesThe coefficients of the general polynomial · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Proof usesAlgebraic independence of the elementary symmetric polynomials · Injective algebra maps preserve algebraic independence

Used byTranscendence degree of the coefficient field

TheoremThe roots are algebraically independent#✓fully proved

For every natural number \(n\), the roots \(x_1, \dots, x_n\) are algebraically independent over \(\mathbb{C}\) in the function field \(\mathbb{C}(x_1, \dots, x_n)\).

theorem algebraicIndependent_root (n : ℕ) :
    AlgebraicIndependent ℂ (root n)

Uses 3 · Used by 1

Statement usesThe roots \(x_i\) · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Proof usesInjective algebra maps preserve algebraic independence

Used byTranscendence degree of \(\mathbb{C}(x_1, \dots, x_n)\)

TheoremPolynomials in the roots#✓fully proved

For every natural number \(n\) and every polynomial \(p \in \mathbb{C}[X_1, \dots, X_n]\), the image of \(p\) in the function field \(\mathbb{C}(x_1, \dots, x_n)\) lies in the \(\mathbb{C}\)-subalgebra generated by the roots \(x_1, \dots, x_n\).

theorem algebraMap_mem_adjoin_roots (n : ℕ)
    (p : MvPolynomial (Fin n) ℂ) :
    algebraMap (MvPolynomial (Fin n) ℂ) (rootsField n) p ∈
      Algebra.adjoin ℂ (Set.range (root n))

Uses 2 · Used by 2

Statement usesThe roots \(x_i\) · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Used byThe roots generate the function field · Rational functions are algebraic over the polynomial subalgebra

TheoremRational functions are algebraic over the polynomial subalgebra#✓fully proved

For a natural number \(n\), every element of the field \(\mathbb{C}(x_1, \dots, x_n)\) of rational functions in \(n\) indeterminates is algebraic over the \(\mathbb{C}\)-subalgebra generated by \(x_1, \dots, x_n\): it is a ratio of two polynomials in \(x_1, \dots, x_n\).

theorem isAlgebraic_adjoin_roots (n : ℕ) :
    Algebra.IsAlgebraic (Algebra.adjoin ℂ (Set.range (root n)))
      (rootsField n)

Uses 3 · Used by 1

Statement usesThe roots \(x_i\) · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Proof usesPolynomials in the roots

Used byTranscendence degree of \(\mathbb{C}(x_1, \dots, x_n)\)

TheoremTranscendence degree of \(\mathbb{C}(x_1, \dots, x_n)\)#✓fully proved

For every \(n \in \mathbb{N}\), the function field \(\mathbb{C}(x_1, \dots, x_n)\) has transcendence degree \(n\) over \(\mathbb{C}\), as a cardinal.

theorem trdeg_rootsField (n : ℕ) :
    Algebra.trdeg ℂ (rootsField n) = Cardinal.mk (Fin n)

Uses 5 · Used by 1

Statement usesThe function field \(\mathbb{C}(x_1, \dots, x_n)\)

Proof usesThe roots are algebraically independent · Rational functions are algebraic over the polynomial subalgebra · The roots \(x_i\) · The roots \(x_i\) are pairwise distinct

Used byTranscendence degree of the coefficient field

DefinitionNumeric transcendence degree#✓fully proved

For a field \(F\) that is a \(\mathbb{C}\)-algebra, the numeric transcendence degree of \(F\) is its transcendence degree over \(\mathbb{C}\) as a natural number when that degree is finite, and \(0\) when it is infinite.

noncomputable def transDegNat (F : Type) [Field F] [Algebra ℂ F] : ℕ :=
  (Algebra.trdeg ℂ F).toNat

Used by 3

Used byEssential dimension of the symmetric group · Trivial upper bound for the essential dimension of \(S_n\) · Transcendence degree of the coefficient field

TheoremElementary symmetric polynomials evaluated at the roots#✓fully proved

For all natural numbers \(n\) and \(k\), the image of the \(k\)-th elementary symmetric polynomial \(e_k \in \mathbb{C}[X_1, \dots, X_n]\) in the function field \(\mathbb{C}(x_1, \dots, x_n)\) is the \(k\)-th elementary symmetric function of the multiset of roots \(\{x_1, \dots, x_n\}\), that is, the sum of the products \(x_{i_1} \cdots x_{i_k}\) over all \(i_1 < \dots < i_k\).

theorem algebraMap_esymm (n k : ℕ) :
    algebraMap (MvPolynomial (Fin n) ℂ) (rootsField n)
        (esymm (Fin n) ℂ k) =
      (Finset.univ.val.map (root n)).esymm k

Uses 2 · Used by 2

Statement usesThe roots \(x_i\) · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Used byThe trivial descent · Each \(x_i\) is a root of the general polynomial

DefinitionCoefficients indexed by degree#✓fully proved

Let \(n\) be a natural number, for \(1 \le k \le n\) let \(a_k\) be the \(k\)-th elementary symmetric function of \(x_1, \dots, x_n\) in the function field \(\mathbb{C}(x_1, \dots, x_n)\), and let \(\mathbb{C}(a_1, \dots, a_n)\) be the coefficient field. For each natural number \(k\), the element \(c_k\) of \(\mathbb{C}(a_1, \dots, a_n)\) is defined by \(c_0 = 1\), \(c_k = a_k\) for \(1 \le k \le n\), and \(c_k = 0\) for \(k > n\).

In a variable \(X\), the general polynomial is \(\sum_{k=0}^{n} (-1)^k c_k X^{n-k}\).

noncomputable def coeffNat (n : ℕ) (k : ℕ) : ↥(generalBaseField n) :=
  if h0 : k = 0 then 1
  else if h2 : k ≤ n then
    coeffElem n ⟨k - 1, Nat.sub_one_lt_of_le (Nat.pos_of_ne_zero h0) h2⟩
  else 0

Uses 3 · Used by 3

Statement usesCoefficients in the coefficient field · Coefficient field of the general polynomial · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Used byGeneral polynomial · The trivial descent · Each \(x_i\) is a root of the general polynomial

DefinitionGeneral polynomial#✓fully proved

For a natural number \(n\), let \(x_1, \dots, x_n\) be the indeterminates of the rational function field \(\mathbb{C}(x_1, \dots, x_n)\), let \(a_0 = 1\) and, for \(1 \le k \le n\), let \(a_k\) be the \(k\)-th elementary symmetric function of \(x_1, \dots, x_n\). The general polynomial of degree \(n\) is the polynomial \(\sum_{j=0}^{n} (-1)^j a_j X^{n-j} = X^n - a_1 X^{n-1} + \cdots + (-1)^n a_n\) with coefficients in the coefficient field \(\mathbb{C}(a_1, \dots, a_n)\).

noncomputable def generalPolynomial (n : ℕ) :
    Polynomial (generalBaseField n) :=
  ∑ j ∈ Finset.range (n + 1),
    (-1) ^ j * (Polynomial.C (coeffNat n j) * Polynomial.X ^ (n - j))

Uses 3 · Used by 3

Statement usesCoefficients indexed by degree · Coefficient field of the general polynomial · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Used byThe trivial descent · The roots of the general polynomial generate the function field · Each \(x_i\) is a root of the general polynomial

TheoremDistinct linear factors are coprime#✓fully proved

For a natural number \(n\) and distinct elements \(a \ne b\) of the field \(\mathbb{C}(x_1, \dots, x_n)\) of rational functions in \(n\) indeterminates, the polynomials \(X - a\) and \(X - b\) are coprime in \(\mathbb{C}(x_1, \dots, x_n)[X]\): there are polynomials \(u\) and \(v\) with \(u (X - a) + v (X - b) = 1\).

theorem isCoprime_X_sub_C_of_ne (n : ℕ) {a b : rootsField n} (h : a ≠ b) :
    IsCoprime (Polynomial.X - Polynomial.C a)
      (Polynomial.X - Polynomial.C b)

Uses 1 · Used by 1

Statement usesThe function field \(\mathbb{C}(x_1, \dots, x_n)\)

Used byThe product of the linear factors \(X - x_i\) is separable

TheoremThe product of the linear factors \(X - x_i\) is separable#✓fully proved

For every \(n \in \mathbb{N}\), the polynomial \(\prod_{i=1}^{n} (X - x_i)\) over the function field \(\mathbb{C}(x_1, \dots, x_n)\) is separable.

theorem separable_prod_roots (n : ℕ) :
    (∏ i : Fin n, (Polynomial.X - Polynomial.C (root n i))).Separable

Uses 4 · Used by 1

Statement usesThe roots \(x_i\) · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Proof usesDistinct linear factors are coprime · The roots \(x_i\) are pairwise distinct

Used byThe trivial descent

TheoremThe roots generate the function field#✓fully proved

For every natural number \(n\), the intermediate field of \(\mathbb{C}(x_1, \dots, x_n)\) generated over \(\mathbb{C}\) by the roots \(x_1, \dots, x_n\) is the whole function field \(\mathbb{C}(x_1, \dots, x_n)\).

theorem adjoin_roots_eq_top (n : ℕ) :
    IntermediateField.adjoin ℂ (Set.range (root n)) = ⊤

Uses 3 · Used by 1

Statement usesThe roots \(x_i\) · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Proof usesPolynomials in the roots

Used byThe roots of the general polynomial generate the function field

TheoremEach \(x_i\) is a root of the general polynomial#✓fully proved

For \(n \in \mathbb{N}\), let \(E_n = \mathbb{C}(x_1, \dots, x_n)\), let \(a_k\) be the \(k\)-th elementary symmetric function of \(x_1, \dots, x_n\), and let \(f_n = X^n - a_1 X^{n-1} + \cdots + (-1)^n a_n\) be the general polynomial, with coefficients in \(F_n = \mathbb{C}(a_1, \dots, a_n) \subseteq E_n\). Then \(f_n(x_i) = 0\) in \(E_n\) for every \(i \in \{1, \dots, n\}\).

theorem root_mem_generalPolynomial_roots (n : ℕ) (i : Fin n) :
    Polynomial.aeval (root n i) (generalPolynomial n) = 0

Uses 8 · Used by 1

Statement usesCoefficient field of the general polynomial · General polynomial · The roots \(x_i\) · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Proof usesElementary symmetric polynomials evaluated at the roots · The coefficients of the general polynomial · Coefficients in the coefficient field · Coefficients indexed by degree

Used byThe roots of the general polynomial generate the function field

TheoremTranscendence degree of the coefficient field#✓fully proved

For \(n \in \mathbb{N}\), let \(a_k\) be the \(k\)-th elementary symmetric function of \(x_1, \dots, x_n\) in \(\mathbb{C}(x_1, \dots, x_n)\). The coefficient field \(F_n = \mathbb{C}(a_1, \dots, a_n)\) of the general polynomial has numeric transcendence degree \(n\) over \(\mathbb{C}\).

theorem transDegNat_generalBaseField (n : ℕ) :
    transDegNat (generalBaseField n) = n

Uses 7 · Used by 1

Statement usesCoefficient field of the general polynomial · The function field \(\mathbb{C}(x_1, \dots, x_n)\) · Numeric transcendence degree

Proof usesThe coefficients are algebraically independent · The coefficients of the general polynomial · Coefficients in the coefficient field · Transcendence degree of \(\mathbb{C}(x_1, \dots, x_n)\)

Used byTrivial upper bound for the essential dimension of \(S_n\)

DefinitionDescent of the general polynomial extension#✓fully proved

For a natural number \(n\), let \(E = \mathbb{C}(x_1, \dots, x_n)\) be the field of rational functions in \(n\) indeterminates and let \(F = \mathbb{C}(a_1, \dots, a_n) \subseteq E\) be the coefficient field of the general polynomial, where \(a_k\) is the \(k\)-th elementary symmetric function of \(x_1, \dots, x_n\). A pair \((F_0, E_0)\) of intermediate fields of \(\mathbb{C} \subseteq E\) is a descent when \(F_0 \subseteq F\), \(F_0 \subseteq E_0\), \(E_0 \cap F = F_0\), the compositum of \(E_0\) and \(F\) is all of \(E\), and there is a nonzero polynomial \(p\) with coefficients in \(F_0\) whose image in \(E[X]\) splits and is separable, such that \(E_0\) is the field generated over \(F_0\) by the roots of \(p\) in \(E\).

Splitting and separability are imposed in \(E\), where they say that the roots of \(p\) are all present and distinct.

def IsDescent (n : ℕ) (F0 E0 : IntermediateField ℂ (rootsField n)) :
    Prop :=
  F0 ≤ generalBaseField n ∧ F0 ≤ E0 ∧
    E0 ⊓ generalBaseField n = F0 ∧ E0 ⊔ generalBaseField n = ⊤ ∧
    ∃ p : Polynomial F0, p ≠ 0 ∧
      (p.map (algebraMap F0 (rootsField n))).Splits ∧
      (p.map (algebraMap F0 (rootsField n))).Separable ∧
      (IntermediateField.adjoin F0
        {x : rootsField n | Polynomial.aeval x p = 0}).restrictScalars
          ℂ = E0

Uses 2 · Used by 3

Statement usesCoefficient field of the general polynomial · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Used byEssential dimension of the symmetric group · Trivial upper bound for the essential dimension of \(S_n\) · The trivial descent

TheoremThe roots of the general polynomial generate the function field#✓fully proved

For \(n \in \mathbb{N}\), let \(E_n = \mathbb{C}(x_1, \dots, x_n)\), let \(a_k\) be the \(k\)-th elementary symmetric function of \(x_1, \dots, x_n\), let \(F_n = \mathbb{C}(a_1, \dots, a_n) \subseteq E_n\) be the coefficient field, and let \(f_n = X^n - a_1 X^{n-1} + \cdots + (-1)^n a_n \in F_n[X]\) be the general polynomial. The subfield of \(E_n\) generated over \(F_n\) by all roots of \(f_n\) in \(E_n\) is \(E_n\) itself.

theorem restrictScalars_adjoin_generalPolynomial (n : ℕ) :
    (IntermediateField.adjoin (generalBaseField n)
      {x : rootsField n |
        Polynomial.aeval x (generalPolynomial n) = 0}).restrictScalars
        ℂ = ⊤

Uses 6 · Used by 1

Statement usesCoefficient field of the general polynomial · General polynomial · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Proof usesThe roots generate the function field · The roots \(x_i\) · Each \(x_i\) is a root of the general polynomial

Used byThe trivial descent

TheoremThe trivial descent#✓fully proved

For every natural number \(n\), the pair \((F, E)\) is a descent of the general polynomial extension, where \(E = \mathbb{C}(x_1, \dots, x_n)\) is the field of rational functions in \(n\) indeterminates and \(F = \mathbb{C}(a_1, \dots, a_n)\) is the coefficient field, generated over \(\mathbb{C}\) by the elementary symmetric functions \(a_1, \dots, a_n\) of \(x_1, \dots, x_n\).

The general polynomial serves as the defining polynomial of this descent.

theorem isDescent_generalBaseField (n : ℕ) :
    IsDescent n (generalBaseField n) ⊤

Uses 11 · Used by 1

Statement usesDescent of the general polynomial extension · Coefficient field of the general polynomial · The function field \(\mathbb{C}(x_1, \dots, x_n)\)

Proof usesElementary symmetric polynomials evaluated at the roots · The coefficients of the general polynomial · Coefficients in the coefficient field · Coefficients indexed by degree · General polynomial · The roots of the general polynomial generate the function field · The roots \(x_i\) · The product of the linear factors \(X - x_i\) is separable

Used byTrivial upper bound for the essential dimension of \(S_n\)

DefinitionEssential dimension of the symmetric group#✓fully proved

For a natural number \(n\), let \(\mathbb{C}(x_1, \dots, x_n)\) be the field of rational functions in \(n\) indeterminates. The essential dimension of \(S_n\) over \(\mathbb{C}\), in the general-polynomial parameter sense, is the least natural number \(d\) such that some intermediate field \(F_0\) of \(\mathbb{C} \subseteq \mathbb{C}(x_1, \dots, x_n)\) of transcendence degree at most \(d\) over \(\mathbb{C}\) admits an intermediate field \(E_0\) for which \((F_0, E_0)\) is a descent of the general polynomial extension.

The transcendence degree is read as a natural number (an infinite degree would count as \(0\); this does not occur, since \(F_0\) lies in the coefficient field).

noncomputable def edSn (n : ℕ) : ℕ :=
  sInf {d : ℕ | ∃ F0 E0 : IntermediateField ℂ (rootsField n),
    IsDescent n F0 E0 ∧ transDegNat F0 ≤ d}

Uses 3 · Used by 9

Statement usesDescent of the general polynomial extension · The function field \(\mathbb{C}(x_1, \dots, x_n)\) · Numeric transcendence degree

Used byLower bound for the essential dimension of symmetric groups · Upper bound for the essential dimension of symmetric groups · Essential dimension of the symmetric group on five letters · Essential dimension of the symmetric group on four letters · Trivial upper bound for the essential dimension of \(S_n\) · Essential dimension of the symmetric group on seven letters · Essential dimension of the symmetric group on six letters · Asymptotic essential-dimension ratio of the symmetric groups · The essential-dimension ratio of the symmetric groups is at most one

TheoremTrivial upper bound for the essential dimension of \(S_n\)#✓fully proved

For every natural number \(n\), the essential dimension of the symmetric group \(S_n\) over \(\mathbb{C}\), in the general-polynomial parameter sense, is at most \(n\).

The bound comes from the trivial descent, whose parameter field is the coefficient field of the general polynomial, of transcendence degree \(n\).

theorem edSn_le (n : ℕ) : edSn n ≤ n

Uses 7 · Used by 1

Statement usesEssential dimension of the symmetric group

Proof usesDescent of the general polynomial extension · Coefficient field of the general polynomial · The trivial descent · The function field \(\mathbb{C}(x_1, \dots, x_n)\) · Numeric transcendence degree · Transcendence degree of the coefficient field

Used byThe essential-dimension ratio of the symmetric groups is at most one

DefinitionAsymptotic essential-dimension ratio of the symmetric groups#✓fully proved

The catalogue constant \(C_{79}\) is the limit superior, as \(n \to \infty\), of \(\operatorname{ed}_{\mathbb{C}}(S_n) / n\), where \(\operatorname{ed}_{\mathbb{C}}(S_n)\) is the essential dimension of the symmetric group \(S_n\) over \(\mathbb{C}\) in the general-polynomial parameter sense.

noncomputable def essDimRatio : ℝ :=
  Filter.limsup (fun n : ℕ => (edSn n : ℝ) / n) Filter.atTop

Uses 1 · Used by 2

Statement usesEssential dimension of the symmetric group

Used byThe essential-dimension ratio of the symmetric groups is at most one · Lower bound for the asymptotic essential-dimension ratio

TheoremThe essential-dimension ratio of the symmetric groups is at most one#✓fully proved

The constant \(C_{79}\), the limit superior as \(n \to \infty\) of \(\operatorname{ed}_{\mathbb{C}}(S_n) / n\) with the essential dimension of \(S_n\) over \(\mathbb{C}\) taken in the general-polynomial parameter sense, satisfies \(C_{79} \le 1\).

theorem essDimRatio_le_one : essDimRatio ≤ 1

Uses 3

Statement usesAsymptotic essential-dimension ratio of the symmetric groups

Proof usesEssential dimension of the symmetric group · Trivial upper bound for the essential dimension of \(S_n\)

TheoremUpper bound for the essential dimension of symmetric groups#●ready to prove

Write \(\operatorname{ed}(S_n)\) for the essential dimension of the symmetric group \(S_n\) over \(\mathbb{C}\) in the general-polynomial sense: the least transcendence degree over \(\mathbb{C}\) of a subfield \(F_0\) of the coefficient field \(\mathbb{C}(a_1, \dots, a_n)\) of the general polynomial of degree \(n\) over which that polynomial descends up to Tschirnhaus transformation. Then \(\operatorname{ed}(S_n) \le n - 3\) for every natural number \(n \ge 5\).

theorem_wanted buhlerReichstein1997UpperBound_wanted :
    ∀ n ≥ 5, edSn n ≤ n - 3

Sources

• Buhler--Reichstein (1997), the classical Tschirnhaus bound ed_ℂ(Sₙ) ≤ n - 3 for n ≥ 5.

Uses 1

Statement usesEssential dimension of the symmetric group

TheoremLower bound for the essential dimension of symmetric groups#●ready to prove

Write \(\operatorname{ed}(S_n)\) for the essential dimension of the symmetric group \(S_n\) over \(\mathbb{C}\) in the general-polynomial sense: the least transcendence degree over \(\mathbb{C}\) of a subfield \(F_0\) of the coefficient field \(\mathbb{C}(a_1, \dots, a_n)\) of the general polynomial of degree \(n\) over which that polynomial descends up to Tschirnhaus transformation. Then \(\lfloor n/2 \rfloor \le \operatorname{ed}(S_n)\) for every natural number \(n\).

theorem_wanted buhlerReichsteinDuncanLowerBound_wanted :
    ∀ n : ℕ, n / 2 ≤ edSn n

Sources

• Buhler--Reichstein (1997) and Duncan, the lower bound ⌊n/2⌋ ≤ ed_ℂ(Sₙ).

Uses 1

Statement usesEssential dimension of the symmetric group

TheoremLower bound for the asymptotic essential-dimension ratio#●ready to prove

Write \(\operatorname{ed}(S_n)\) for the essential dimension of the symmetric group \(S_n\) over \(\mathbb{C}\) in the general-polynomial sense: the least transcendence degree over \(\mathbb{C}\) of a subfield \(F_0\) of the coefficient field \(\mathbb{C}(a_1, \dots, a_n)\) of the general polynomial of degree \(n\) over which that polynomial descends up to Tschirnhaus transformation. Then \(\limsup_{n \to \infty} \operatorname{ed}(S_n)/n \ge 1/2\).

theorem_wanted essDimRatioLowerBound_wanted :
    (1 / 2 : ℝ) ≤ essDimRatio

Sources

• catalogue lower row for C₇₉, from the ⌊n/2⌋ lower bound: 1/2 ≤ C₇₉.

Uses 1

Statement usesAsymptotic essential-dimension ratio of the symmetric groups

TheoremEssential dimension of the symmetric group on five letters#●ready to prove

Write \(\operatorname{ed}(S_n)\) for the essential dimension of the symmetric group \(S_n\) over \(\mathbb{C}\) in the general-polynomial sense: the least transcendence degree over \(\mathbb{C}\) of a subfield \(F_0\) of the coefficient field \(\mathbb{C}(a_1, \dots, a_n)\) of the general polynomial of degree \(n\) over which that polynomial descends up to Tschirnhaus transformation. Then \(\operatorname{ed}(S_5) = 2\).

theorem_wanted edSn_five_wanted : edSn 5 = 2

Sources

• Buhler--Reichstein (1997), exact value ed_ℂ(S₅) = 2: their general bounds ⌊5/2⌋ ≤ ed_ℂ(S₅) ≤ 5 - 3 coincide at 2. The classical Bring--Jerrard form X^5 + pX + q is not the descent behind that upper bound here: producing it already requires solving auxiliary equations over an extension of the coefficient field, and normalizing further to X^5 + X + a is again only a scaling over an extension, so neither form witnesses a descent over the original field in the sense of this file (in particular nothing here implies edSn 5 ≤ 1).

Uses 1

Statement usesEssential dimension of the symmetric group

TheoremEssential dimension of the symmetric group on four letters#●ready to prove

Write \(\operatorname{ed}(S_n)\) for the essential dimension of the symmetric group \(S_n\) over \(\mathbb{C}\) in the general-polynomial sense: the least transcendence degree over \(\mathbb{C}\) of a subfield \(F_0\) of the coefficient field \(\mathbb{C}(a_1, \dots, a_n)\) of the general polynomial of degree \(n\) over which that polynomial descends up to Tschirnhaus transformation. Then \(\operatorname{ed}(S_4) = 2\).

theorem_wanted edSn_four_wanted : edSn 4 = 2

Sources

• Buhler--Reichstein (1997), exact value ed_ℂ(S₄) = 2.

Uses 1

Statement usesEssential dimension of the symmetric group

TheoremEssential dimension of the symmetric group on six letters#●ready to prove

Write \(\operatorname{ed}(S_n)\) for the essential dimension of the symmetric group \(S_n\) over \(\mathbb{C}\) in the general-polynomial sense: the least transcendence degree over \(\mathbb{C}\) of a subfield \(F_0\) of the coefficient field \(\mathbb{C}(a_1, \dots, a_n)\) of the general polynomial of degree \(n\) over which that polynomial descends up to Tschirnhaus transformation. Then \(\operatorname{ed}(S_6) = 3\).

theorem_wanted edSn_six_wanted : edSn 6 = 3

Sources

• Buhler--Reichstein (1997), exact value ed_ℂ(S₆) = 3.

Uses 1

Statement usesEssential dimension of the symmetric group

TheoremEssential dimension of the symmetric group on seven letters#●ready to prove

Write \(\operatorname{ed}(S_n)\) for the essential dimension of the symmetric group \(S_n\) over \(\mathbb{C}\) in the general-polynomial sense: the least transcendence degree over \(\mathbb{C}\) of a subfield \(F_0\) of the coefficient field \(\mathbb{C}(a_1, \dots, a_n)\) of the general polynomial of degree \(n\) over which that polynomial descends up to Tschirnhaus transformation. Then \(\operatorname{ed}(S_7) = 4\).

theorem_wanted edSn_seven_wanted : edSn 7 = 4

Sources

• Duncan (2010), Essential dimensions of A₇ and S₇, exact value ed_ℂ(S₇) = 4. Buhler--Reichstein's general bounds give only 3 ≤ ed_ℂ(S₇) ≤ 4 here.

Uses 1

Statement usesEssential dimension of the symmetric group

29 fully proved7 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.