Galois Group

Stream: new members

[Nick Adfor]

1. Determine the Galois group of the splitting field of the polynomial (x^4 - 14x^2 + 9) over the field of rational numbers (ℚ).
2. Determine the possible Galois group of the polynomial (x^7 - 7x + 3).
3. Determine the Galois group of the splitting field of the polynomial (x^8 - 3) over the field of rational numbers (ℚ).

I was trying to formalize the proof of these Galois group problems. But it seems hard as I cannot find some related theorem in mathlib. (Maybe I'm not familiar with mathlib?)

So I want to ask for some help.

[David Ang]

Maybe something in Mathlib.FieldTheory.PolynomialGaloisGroup may help?

[David Ang]

docs4#Polynomial.Gal

[Nick Adfor]

David Ang said:

Maybe something in Mathlib.FieldTheory.PolynomialGaloisGroup may help?

Seems that it doesn't offer a method to calculate a Galois group of a specific polynomial……? (I may think that it is the reason why I have no idea about formalize it.)

[Kevin Buzzard]

Well what does it even mean to compute a Galois group? If I give you a polynomial of degree 1000 and ask you what its Galois group is, and remark that the group has no standard name, then what can your answer be?

[Nick Adfor]

Kevin Buzzard said:

Well what does it even mean to compute a Galois group? If I give you a polynomial of degree 1000 and ask you what its Galois group is, and remark that the group has no standard name, then what can your answer be?

I mean that maybe for these polynomial with small degree (for example less than 10), a calculate method might be needed.

[Nick Adfor]

I may need these theorem to calculate these specific Galois group:

Theorem 3 (Transitivity Theorem):
If the polynomial f(x) is irreducible over the rational numbers and has degree n, then its Galois group is a subgroup of the symmetric group S_n.

Theorem 4 (Discriminant Criterion for S_n and A_n):
If the Galois group contains an odd permutation, then it is the symmetric group S_n; otherwise, it is the alternating group A_n.

Theorem 5 (Dihedral Group as Galois Group):
For a polynomial of the form x^n - a, its Galois group is the dihedral group D_n if and only if n is even and a has no nth root in the rational numbers.

And also, I need a method(theorem) to find splitting field from its root. For example, problem 3 has roots i*3^{1/8}, how can I get the splitting field using theorem in Mathlib?

As it is connected with calculating a specific Galois group, I may think that the theorems above are too specific and are not in mathlib. So I quit finding them and try to seek some help here.

[Kevin Buzzard]

I agree that it could be done for small degree, where there are tables of subgroups of symmetric groups, but lean is quite far from a computer algebra package, it's a theorem prover. The things you can formalise are things like "the Galois group is this" as opposed to "what is this Galois group".

There's no reason that lean can't be a formally verified computer algebra package but this would take quite some work.

[Kevin Buzzard]

Theorem 5 is false btw. What's your proof?

[Kevin Buzzard]

Also these theorems are stated informally. It is definitely not true that a Galois group "is" a subgroup of S_n, a Galois group is a group of field automorphisms. It's isomorphic to a subgroup of S_n in typically many ways, and lean will be very pedantic about this sort of thing.

[Kevin Buzzard]

To get a splitting field for a polynomial you use docs#Polynomial.SplittingField

[Nick Adfor]

Kevin Buzzard said:

Also these theorems are stated informally. It is definitely not true that a Galois group "is" a subgroup of S_n, a Galois group is a group of field automorphisms. It's isomorphic to a subgroup of S_n in typically many ways, and lean will be very pedantic about this sort of thing.

https://math.stackexchange.com/questions/85451/what-is-the-galois-group-of-the-splitting-field-of-x8-3-over-mathbbq

Sorry to have a wrong theorem. The original goal is to use theorem 5 to prove problem 3: x^3-8. The correct answer is above. I may want to follow the mse method.

[Kevin Buzzard]

But theorem 5 as stated is nonsense, it's false in both directions. Did you misstate it?

[Scott Carnahan]

Theorem 4 is also false for n > 3.