degree of splitting field

Stream: Is there code for X?

[Suzuka Yu]

Greetings! I wonder if we have

$$\text{if } f \in F[X] \text{ and } deg(f)=n \text{, then } f \text{ has a splitting field } K \text{ over } F \text{ with } [K : F] \leq n!$$

in mathlib. And if not, are there any suggestions on proving it? I did't seem to find many existing theorems in mathlib regarding degree or rank of a field extension (like degree of a simple extension etc.).

Thanks in advance!

[Jz Pan]

@loogle Polynomial.SplittingField, Module.rank

[loogle]

:shrug: nothing found

[Jz Pan]

@loogle Polynomial.SplittingField, Module.finrank

[loogle]

:search: Polynomial.Gal.card_of_separable

[Jz Pan]

I'm afraid that there is none. If it's me, I may prove it by induction. But you need to check the actual definition of docs#Polynomial.SplittingField ...

[Junyan Xu]

Easier to prove f.Gal acts faithfully on the roots of f in the splitting field (there are at most n, and they generate the splitting field).

[Jz Pan]

Junyan Xu said:

Easier to prove f.Gal acts faithfully on the roots of f in the splitting field (there are at most n, and they generate the splitting field).

But what about purely inseparable irreducible polynomials?

[Suzuka Yu]

Jz Pan 发言道：

I'm afraid that there is none. If it's me, I may prove it by induction. But you need to check the actual definition of docs#Polynomial.SplittingField ...

Thanks! indeed I want to do the induction. I tried to follow the proof via adjoining roots one by one.

For instance, if $f$ has roots $\alpha_1, \alpha_2, \dots, \alpha_m$, then

$$[F(\alpha_1, \dots, \alpha_m) : F] = [F(\alpha_1) : F] [F(\alpha_2, \alpha_1) : F(\alpha_1)] \dots \leq n(n-1) \dots = n!$$

But this seems to require lemmas about degree of simple extension ( $[F(\alpha_1) : F] \leq n$ etc. ), do we have anything like this in mathlib?

[Suzuka Yu]

Junyan Xu 发言道：

Easier to prove f.Gal acts faithfully on the roots of f in the splitting field (there are at most n, and they generate the splitting field).

Thanks but could you be more specific? Do you mean $n! \geq |Gal(K/F)| = [K : F]$ (Which might demands $f$ to be separable)?

[Junyan Xu]

Yeah, I missed that you need separability. So my approach needs to use the relative separableClosure to decompose the extension.
For the inductive approach, notice that the construction of SplittingField is already inductive, and it's iterated f.natDegree times. So you can prove bounds for the finrank of docs#Polynomial.SplittingFieldAux inductively and use docs#Polynomial.SplittingField.algEquivSplittingFieldAux.
Some lemmas that will be useful are docs#Polynomial.natDegree_removeFactor, docs#PowerBasis.finrank, docs#AdjoinRoot.powerBasis, docs#Module.finrank_mul_finrank.

[Junyan Xu]

With some sorries

import Mathlib.FieldTheory.SplittingField.Construction

open Polynomial

variable {K : Type*} [Field K] (f : K[X]) (n : ℕ)

lemma finrank_splittingFieldAux_le :
    Module.finrank K (SplittingFieldAux n f) ≤ f.natDegree.descFactorial n := by
  induction' n with n ih generalizing K
  · change Module.finrank K K ≤ 1; simp
  have : Fact (Irreducible f.factor) := ⟨irreducible_factor f⟩
  change Module.finrank K (SplittingFieldAux n f.removeFactor) ≤ _
  rw [← Module.finrank_mul_finrank K (AdjoinRoot f.factor)]
  have hf := (irreducible_factor f).ne_zero
  have : f.natDegree ≠ 0 := sorry
  have hf0 : f ≠ 0 := sorry
  have H1 := natDegree_le_of_dvd (factor_dvd_of_natDegree_ne_zero this) hf0
  have H2 := (AdjoinRoot.powerBasis hf).finrank.trans (AdjoinRoot.powerBasis_dim hf)
  refine (mul_le_mul' (H2.trans_le H1) (ih ..)).trans ?_
  rw [natDegree_removeFactor]
  refine LE.le.trans_eq ?_ (Nat.descFactorial_mul_descFactorial (k := 1) n.succ_pos)
  rw [Nat.descFactorial_one, mul_comm, n.add_sub_cancel]

[Antoine Chambert-Loir]

It would be nice to formalize the universal splitting algebra: for a monic degree $n$ polynomial in one variable $f\in k[T]$ over a ring $k$, this is the $k$-algebra $S_f$ defined by generators $z_1,\dots,z_n$ and relations such that $f=(T-z_1)\cdots (T-z_n)$. This algebra is a free module of rank $n!$ over $k$. A reference is the book by Pohst and Zassenhaus, Algorithmic Algebraic Number Theory.

This algebra has discriminant the discriminant of $f$, which implies that it is étale when the discriminant is invertible.

To get a splitting field when $$k$ is a field, just pick a maximal ideal $M$ of this ring, then $K=S_f/M$ will be finite extension of $k$ and its degree is at most $n!$. In fact, one can go further, considering the group of permutations acting as $k$-automorphism of the algebra $S_f$, prove that it acts transitively over the set of maximal ideals of $S_f$, and get the automorphism group of $K/k$ as the stabilizer of the chosen maximal ideal $M$. (There is a nice piece of artinian algebra when $f$ is not separable.)

[Junyan Xu]

The lemma above isn't actually true if n > f.natDegree, in which case the RHS is 0. The following is corrected and sorry-free code:

import Mathlib.FieldTheory.SplittingField.Construction

open Polynomial

variable {K : Type*} [Field K] (f : K[X]) (n : ℕ)

lemma finrank_splittingFieldAux_le (hnf : n ≤ f.natDegree) :
    Module.finrank K (SplittingFieldAux n f) ≤ f.natDegree.descFactorial n := by
  induction' n with n ih generalizing K
  · change Module.finrank K K ≤ 1; simp
  have : Fact (Irreducible f.factor) := ⟨irreducible_factor f⟩
  change Module.finrank K (SplittingFieldAux n f.removeFactor) ≤ _
  rw [← Module.finrank_mul_finrank K (AdjoinRoot f.factor)]
  have hf0 := (irreducible_factor f).ne_zero
  have hf' := (n.succ_pos.trans_le hnf).ne'
  have H1 := natDegree_le_of_dvd (factor_dvd_of_natDegree_ne_zero hf') fun h ↦ hf' <| by
    simp [h]
  have H2 := (AdjoinRoot.powerBasis hf0).finrank.trans (AdjoinRoot.powerBasis_dim hf0)
  refine (mul_le_mul' (H2.trans_le H1) (ih _ ?_)).trans ?_ <;> rw [natDegree_removeFactor]
  · exact Nat.pred_le_pred hnf
  refine LE.le.trans_eq ?_ (Nat.descFactorial_mul_descFactorial (k := 1) n.succ_pos)
  rw [Nat.descFactorial_one, mul_comm, n.add_sub_cancel]

[Suzuka Yu]

Junyan Xu 发言道：

The lemma above isn't actually true if n > f.natDegree, in which case the RHS is 0. The following is corrected and sorry-free code:

import Mathlib.FieldTheory.SplittingField.Construction

open Polynomial

variable {K : Type*} [Field K] (f : K[X]) (n : ℕ)

lemma finrank_splittingFieldAux_le (hnf : n ≤ f.natDegree) :
    Module.finrank K (SplittingFieldAux n f) ≤ f.natDegree.descFactorial n := by
  induction' n with n ih generalizing K
  · change Module.finrank K K ≤ 1; simp
  have : Fact (Irreducible f.factor) := ⟨irreducible_factor f⟩
  change Module.finrank K (SplittingFieldAux n f.removeFactor) ≤ _
  rw [← Module.finrank_mul_finrank K (AdjoinRoot f.factor)]
  have hf0 := (irreducible_factor f).ne_zero
  have hf' := (n.succ_pos.trans_le hnf).ne'
  have H1 := natDegree_le_of_dvd (factor_dvd_of_natDegree_ne_zero hf') fun h ↦ hf' <| by
    simp [h]
  have H2 := (AdjoinRoot.powerBasis hf0).finrank.trans (AdjoinRoot.powerBasis_dim hf0)
  refine (mul_le_mul' (H2.trans_le H1) (ih _ ?_)).trans ?_ <;> rw [natDegree_removeFactor]
  · exact Nat.pred_le_pred hnf
  refine LE.le.trans_eq ?_ (Nat.descFactorial_mul_descFactorial (k := 1) n.succ_pos)
  rw [Nat.descFactorial_one, mul_comm, n.add_sub_cancel]

Amazing! huge thanks!

[Junyan Xu]

It would be nice to formalize the universal splitting algebra

Yeah that would be nice. I believe spanCoeffs in the current construction of AlgebraicClosure is one possible construction of it, but it's difficult to see it's free of the specific rank, unlike with the recursive construction as explained in the book.