Computing Galois group

Stream: mathlib4

[Suzuka Yu]

Greetings! I've been stuck at this "finding the Galois group of the given polynomial over the given field" problem:

$$X^3-10 \text{, over } \mathbb{Q}(\sqrt{-3}). \text{ (and similarly } X^4 - 3 \text{, over }\mathbb{Q}(\sqrt{-3}) \text{)}$$

The first thing I wonder is how can I properly state $\mathbb{Q}(\sqrt{-3})$? I've been thinking noncomputable def K := IntermediateField.adjoin ℚ {I, (√3 : ℂ)} (I didn't find the square root of -3 btw). Another choice is local notation3 "K" => (X^2 + 3 : ℚ[X]).SplittingField, but it does not come with the instance Algebra K ℂ.

With the polynomial defined as noncomputable def f : K[X] := X^3 - 10, I wish to define noncomputable def F := IntermediateField.adjoin K {(Real.rpow 10 (1 / 3) : ℂ)}. Then I want to prove IsSplittingField K F f, and finally (F ≃ₐ[K] F) ≃* (ZMod 3)(which would be identical with f.Gal ≃* (ZMod 3) by definition). However I've achieved nothing, here is what I've tried:

import Mathlib

open Polynomial Complex

noncomputable def K := IntermediateField.adjoin ℚ {I, (√3 : ℂ)}
noncomputable def f : K[X] := X^3 - 10
noncomputable def F := IntermediateField.adjoin K {(Real.rpow 10 (1 / 3) : ℂ)}

example : IsSplittingField K F f := {
  splits' := by
    refine (IntermediateField.splits_iff_mem (IsAlgClosed.splits_codomain f)).mpr ?_
    · intro x hx
      have : f ≠ 0 := by
        refine Monic.ne_zero_of_ne (zero_ne_one' K) ?_
        · unfold f
          monicity
          exact Nat.le_max_left 3 0
      simp [this, rootSet, aroots, roots] at hx
      sorry
  adjoin_rootSet' := by
    refine Algebra.eq_top_iff.mpr ?_
    sorry
}

example : (F ≃ₐ[K] F) ≃* (ZMod 3) := sorry

Can anyone give me some guidance? Your help will be highly appreciated!

[Aaron Liu]

I am fairly sure that $\mathbb{Q}(\sqrt{-3})$ does not contain either $\sqrt{-1}$ or $\sqrt{3}$, so your noncomputable def K is wrong. The A square root of -3 is just I * √3.

[Riccardo Brasca]

This is probably doable, but I honestly think we are missing the infrastructure to do it at the moment.

[Riccardo Brasca]

Nothing really prevents it, all the mathematical prerequisites are there, but unless you build a solid API you are going to suffer.

[Riccardo Brasca]

For example, a mathematically correct definition of $\mathbb{Q}(\sqrt{-3})$ is Algebra.adjoin ℚ {(√-3 : ℂ)}, but this is not the same as Polynomial.SplittingField (X^2+3 : ℚ[X]).

[Riccardo Brasca]

I mean, you can prove they're isomorphic, but the isomorphism will be there, and this is annoying.

[Aaron Liu]

I would say use ℚ[X] ⧸ Ideal.span {X ^ 2 + C (3 : ℚ)}, because this works for $(\mathbb{Z} / 5 \mathbb{Z})(\sqrt{3})$ too, without having to have ℂ.

[Riccardo Brasca]

Yes, that's the point. There is a gazilion possible definitions. The answer is that we want a characteristic predicate

[Riccardo Brasca]

We have a solid theory of cyclotomic extensions (including the computation of the Galois group, the discriminant, the ring of integers and so on), and I would suggest to follow the same path.

[Riccardo Brasca]

For your specific example, if you don't mind using big theorems, you can use that $K[\sqrt[3]{10}] / K$, where $K=\mathbb{Q}[\sqrt{-3}]$, is a Kummer extension, then the Galois group is done in mathlib

[Riccardo Brasca]

Everything is in Mathlib.FieldTheory.KummerExtension

[Riccardo Brasca]

Indeed, the best way of defining K is by K := CyclotomicField 3 ℚ.

[Suzuka Yu]

Aaron Liu 发言道：

I am fairly sure that $\mathbb{Q}(\sqrt{-3})$ does not contain either $\sqrt{-1}$ or $\sqrt{3}$, so your noncomputable def K is wrong. The A square root of -3 is just I * √3.

Oops, sorry, silly of me :exhausted:

[Suzuka Yu]

Riccardo Brasca 发言道：

We have a solid theory of cyclotomic extensions (including the computation of the Galois group, the discriminant, the ring of integers and so on), and I would suggest to follow the same path.

Thanks! I'll look into it

[Riccardo Brasca]

Let me see, the first question can be doable really quick using Kummer's extensions

[Riccardo Brasca]

(I didn't have a precise look at the question, my point is that usually computing Galois group can be a pain)

[Riccardo Brasca]

import Mathlib

open Polynomial IsCyclotomicExtension

local notation3 "K" => CyclotomicField 3 ℚ

lemma bar : (X^3 - C (10 : K)).natDegree = 3 := by
  compute_degree!

lemma bar1 : X^3 - C (10 : K) ≠ 0 := by
  intro h
  simpa [h] using bar

lemma foo1 : Irreducible (X^3 - C (10 : K)) := by
  rw [irreducible_iff_roots_eq_zero_of_degree_le_three (by simp [bar]) (by simp [bar])]
  by_contra! H
  obtain ⟨x, hx⟩ := Multiset.exists_mem_of_ne_zero H
  simp only [mem_roots', ne_eq, bar1, not_false_eq_true, IsRoot.def, eval_sub, eval_pow, eval_X,
    eval_C, true_and] at hx
  have : Irreducible (Polynomial.cyclotomic ((3 : ℕ+) : ℕ) ℚ) :=
    cyclotomic.irreducible_rat (by simp)
  have : Algebra.norm ℚ (x^3) = 100 := by
    rw [eq_of_sub_eq_zero hx, show (10 : K) = algebraMap ℚ K 10 by simp, Algebra.norm_algebraMap,
      IsCyclotomicExtension.finrank K (this)]
    simp only [PNat.val_ofNat, Nat.totient_prime Nat.prime_three, Nat.add_one_sub_one]
    norm_num
  rw [map_pow] at this
  sorry

instance : Fact (Irreducible (X^3 - C (10 : K))) := ⟨foo1⟩

open KummerExtension

local notation3 "L" => K[3√ (10 : K)]

lemma foo2 : (primitiveRoots 3 K).Nonempty :=
  ⟨_, (mem_primitiveRoots <| Nat.zero_lt_succ _).2 <| zeta_spec 3 ℚ K⟩

instance : IsSplittingField K L (X ^ 3 - C 10) :=
  isSplittingField_AdjoinRoot_X_pow_sub_C foo2 foo1

local notation3 "G" => L ≃ₐ[K] L

lemma foo3 : IsCyclic G :=
  isCyclic_of_isSplittingField_X_pow_sub_C foo2 foo1 ..

lemma foo4 : Nat.card G = 3 := by
  simp [Nat.card_congr (autEquivZmod foo1 L (zeta_spec 3 ℚ K)).toEquiv]

[Riccardo Brasca]

The only sorry is to prove False having a rational number whose cube is 100, should be easy.

[Riccardo Brasca]

I am not sure this answer your question, but it is a correct mathematical translation of your question.

[Riccardo Brasca]

Here is a sorry free proof. bar2 is not very nice, it should be doable by decide or something like that.

import Mathlib

open Polynomial IsCyclotomicExtension

local notation3 "K" => CyclotomicField 3 ℚ

local notation3 "P" => X^3 - C (10 : K)

lemma bar : natDegree P = 3 := by compute_degree!

lemma bar1 : P ≠ 0 := fun h ↦ by simpa [h] using bar

lemma bar2 (x : ℝ) (hx : x ^ 3 = 100) : Irrational x := by
  refine irrational_nrt_of_notint_nrt 3 100 hx (fun ⟨y, hy⟩ ↦ ?_) (by norm_num)
  rw [hy] at hx
  norm_cast at hx
  have hpos : 0 ≤ y := (Odd.pow_nonneg_iff (n := 3) (by decide)).1 (by simp [hx])
  contrapose! hx
  obtain h | h : y ≤ 4 ∨ 5 ≤ y := by omega
  · apply ne_of_lt
    calc y^3 ≤ 4^3 := by gcongr
     _ < 100 := by norm_num
  · apply ne_of_gt
    calc y^3 ≥ 5^3 := by gcongr
     _ > 100 := by norm_num

lemma foo1 : Irreducible P := by
  rw [irreducible_iff_roots_eq_zero_of_degree_le_three (by simp [bar]) (by simp [bar])]
  by_contra! H
  obtain ⟨x, hx⟩ := Multiset.exists_mem_of_ne_zero H
  simp only [mem_roots', ne_eq, bar1, not_false_eq_true, IsRoot.def, eval_sub, eval_pow, eval_X,
    eval_C, true_and] at hx
  have : Irreducible (cyclotomic ((3 : ℕ+) : ℕ) ℚ) := cyclotomic.irreducible_rat (by simp)
  have : Algebra.norm ℚ (x^3) = 100 := by
    rw [eq_of_sub_eq_zero hx, show (10 : K) = algebraMap ℚ K 10 by simp, Algebra.norm_algebraMap,
      IsCyclotomicExtension.finrank K (this)]
    simp only [PNat.val_ofNat, Nat.totient_prime Nat.prime_three, Nat.add_one_sub_one]
    norm_num
  rw [map_pow] at this
  exact bar2 (Algebra.norm ℚ x) (by norm_cast) (by simp)

instance : Fact (Irreducible P) := ⟨foo1⟩

open KummerExtension

local notation3 "L" => K[3√ (10 : K)]

lemma foo2 : (primitiveRoots 3 K).Nonempty :=
  ⟨_, (mem_primitiveRoots <| Nat.zero_lt_succ _).2 <| zeta_spec 3 ℚ K⟩

instance : IsSplittingField K L (X ^ 3 - C 10) :=
  isSplittingField_AdjoinRoot_X_pow_sub_C foo2 foo1

local notation3 "G" => L ≃ₐ[K] L

noncomputable def f : G ≃* Multiplicative (ZMod 3) := autEquivZmod foo1 L (zeta_spec 3 ℚ K)

[Suzuka Yu]

Riccardo Brasca 发言道：

I am not sure this answer your question, but it is a correct mathematical translation of your question.

Surly it does! Huge thanks!!

[Riccardo Brasca]

On the other hand the second one seems trickier.

[Antoine Chambert-Loir]

Another way of proving bar2 is to argue by contradiction, if $x$ is rational and the multiplicities of all prime factors in $x^100$ are divisible by $10$. (Do we have factorization into prime numbers for rational numbers?)

[Riccardo Brasca]

Yeah, I didn't think about the quickest method. It is just annoying that we have to write anything more than "please Lean tell me that the cubic root of 100 is irrational". For square root we have

unseal Nat.sqrt.iter in
example : Irrational √24 := by decide

and it would be very nice to have something similar for all n-roots of rational numbers.

[Riccardo Brasca]

Or at least roots of integers.

[Kevin Buzzard]

Or both!

[Suzuka Yu]

Riccardo Brasca 发言道：

On the other hand the second one seems trickier.

Greetings! Sorry for the delay getting back here. For the second one, I managed to explicitly write out all roots and the splitting field. Here is my attempt, but I wasn't able to advance further from here:

import Mathlib

/-
**Main Results**
1. `sep_P` : `P = X^4 - C (3 : K)` is separable
2. `root_set` : all roots of `P` (in ℂ, where it splits)
3. `splittingField` : the splitting field of `P`
-/

open Complex Polynomial IntermediateField

local notation3 "K" => ℚ⟮I * √3⟯
local notation3 "P" => X^4 - C (3 : K)
local notation3 "F" => K⟮(√√3 : ℂ)⟯

lemma deg_P : natDegree P = 4 := natDegree_X_pow_sub_C
lemma ne_zero : P ≠ 0 := X_pow_sub_C_ne_zero (n := 4) (by norm_num) 3
lemma monic_P : Monic P := monic_X_pow_sub_C (3 : K) (by norm_num)
lemma sep_P : Separable P := separable_X_pow_sub_C (3 : K) (by norm_num) (by norm_num)

lemma foo : (√√3 : ℂ) ^ 4 = 3 := by
  norm_cast
  rw [pow_mul _ 2 2, Real.sq_sqrt, Real.sq_sqrt]
  · exact zero_le_three
  · exact Real.sqrt_nonneg 3

lemma eq_P : eval₂ (algebraMap K ℂ) √√3 P = 0 := by
  simp only [eval₂_sub, eval₂_X_pow, eval₂_C, IntermediateField.algebraMap_apply, foo]
  exact sub_eq_zero_of_eq rfl

lemma foo' : (I * √√3) ^ 4 = 3 := by
  rw [pow_mul _ 2 2, mul_pow, I_sq, neg_one_mul, neg_sq]
  norm_cast
  rw [Real.sq_sqrt, Real.sq_sqrt]
  · exact zero_le_three
  · exact Real.sqrt_nonneg 3

lemma aux1₁ : {(√√3 : ℂ), (- √√3 : ℂ), I * √√3, - I * √√3} ⊆ (rootSet P ℂ) := by
  intro x hx
  rcases hx with hx | hx | hx | hx
  all_goals rw [hx]; refine mem_rootSet'.mpr ⟨map_ne_zero ne_zero, ?_⟩
  all_goals simp only
    [neg_mul, map_sub, map_pow, aeval_X, aeval_C, IntermediateField.algebraMap_apply]
  · rw [foo]
    exact sub_eq_zero_of_eq rfl
  · rw [neg_pow, pow_mul (-1) 2 2, neg_sq, one_pow, one_pow, one_mul, foo]
    exact sub_eq_zero_of_eq rfl
  · rw [foo']
    exact sub_eq_zero_of_eq rfl
  · rw [neg_pow, pow_mul (-1) 2 2, neg_sq, one_pow, one_pow, one_mul, foo']
    exact sub_eq_zero_of_eq rfl

open scoped Real Pointwise in
lemma aux1₂ : ({(√√3 : ℂ), (- √√3 : ℂ), I * √√3, - I * √√3} : Finset ℂ).card = 4 := by
  have : IsPrimitiveRoot I 4 := by
    convert Complex.isPrimitiveRoot_exp 4 (by norm_num)
    trans cexp (π / 2 * I)
    · simp [Complex.exp_mul_I]
    · congr 1; ring
  calc
    _ = (√√3 • {(1 : ℂ), (-1 : ℂ), I, - I} : Finset ℂ).card := by
      congr
      ext x
      simp [Finset.mem_smul_finset, eq_comm (a := x), mul_comm I]
    _ = (Units.mk0 √√3 (by simp) • {(1 : ℂ), (-1 : ℂ), I, - I} : Finset ℂ).card := by
      rw [Units.smul_mk0]
    _ = ({(1 : ℂ), (-1 : ℂ), I, - I} : Finset ℂ).card :=
      Finset.card_smul_finset _ _
    _ = (nthRootsFinset 4 ℂ).card := by
      congr
      rw [nthRootsFinset, this.nthRoots_eq (α := I) (by simp)]
      ext
      simp only [Finset.mem_insert, Finset.mem_singleton, Multiset.range_succ, Multiset.range_zero,
        Multiset.cons_zero, Multiset.map_cons, I_sq, neg_mul, one_mul, pow_one, I_mul_I,
        Multiset.map_singleton, pow_zero, Multiset.toFinset_cons, Multiset.toFinset_singleton]
      ring_nf
      simp only [I_pow_four]
      rw [← eq_iff_iff]
      ac_rfl
    _ = _ :=
      this.card_nthRootsFinset

lemma aux1₄ : Fintype.card (rootSet P ℂ) = 4 := by
  rw [@card_rootSet_eq_natDegree K _ ℂ _ _ P sep_P (IsAlgClosed.splits_codomain P), deg_P]

lemma aux1₅ : ({(√√3 : ℂ), (- √√3 : ℂ), I * √√3, - I * √√3} : Finset ℂ) = (rootSet P ℂ).toFinset := by
  refine @Finset.eq_of_subset_of_card_le ℂ _ (rootSet P ℂ).toFinset ?_ ?_
  · convert aux1₁
    simp only [neg_mul, Set.subset_toFinset, Finset.coe_insert, Finset.coe_singleton]
  · rw [aux1₂, Set.toFinset_card, aux1₄]

lemma root_set : ({(√√3 : ℂ), (- √√3 : ℂ), I * √√3, - I * √√3}) = (rootSet P ℂ) := by
  rw [← Set.toFinset_inj]
  convert aux1₅
  simp only [neg_mul, Set.toFinset_insert, Set.toFinset_singleton]

lemma aux3₁ : (√√3 : ℂ) ∈ F := IntermediateField.mem_adjoin_simple_self _ _
lemma aux3₂ : I * √3 ∈ F := IntermediateField.algebraMap_mem F ⟨I * √3, IntermediateField.mem_adjoin_simple_self ℚ (I * √3)⟩
lemma aux3₃ : I ∈ F := by
  have := IntermediateField.mul_mem F aux3₁ aux3₁
  norm_cast at this
  rw [← sq, Real.sq_sqrt (by norm_num)] at this
  have := IntermediateField.div_mem F aux3₂ this
  convert this
  norm_num

lemma aux3₄ : ({(√√3 : ℂ), (- √√3 : ℂ), I * √√3, - I * √√3} : Set ℂ) ⊆ F := by
  intro x hx
  rcases hx with h | h | h | h
  all_goals rw [h]
  · exact aux3₁
  · exact neg_mem aux3₁
  · exact IntermediateField.mul_mem F aux3₃ aux3₁
  · rw [neg_mul]
    exact neg_mem <| IntermediateField.mul_mem F aux3₃ aux3₁

lemma splits : Splits (algebraMap K F) P := by
  refine IntermediateField.splits_of_splits (IsAlgClosed.splits_codomain P) ?_
  · rw [← root_set]; exact aux3₄

lemma aux4₁ : K⟮(√√3 : ℂ)⟯ ≤ K⟮↑√√3, -↑√√3, I * ↑√√3, -I * ↑√√3⟯ := by
  have : {(√√3 : ℂ)} ⊆ ({(√√3 : ℂ), (- √√3 : ℂ), I * √√3, - I * √√3} : Set ℂ) := by
    intro x hx
    rw [Set.mem_insert_iff]
    exact (Or.inr hx).symm
  exact adjoin.mono K _ _ this

lemma aux4₂ : K⟮↑√√3, -↑√√3, I * ↑√√3, -I * ↑√√3⟯ ≤ K⟮(√√3 : ℂ)⟯ := by
  suffices (K⟮↑√√3, -↑√√3, I * ↑√√3, -I * ↑√√3⟯ : Set ℂ) ⊆ (F : Set ℂ) from this
  apply (IntermediateField.adjoin_subset_adjoin_iff K (F' := K) (E := ℂ)).2
  constructor
  · intro x hx
    simp only [Set.mem_range, IntermediateField.algebraMap_apply, Subtype.exists, exists_prop,
      exists_eq_right] at hx
    let x' := algebraMap K F ⟨x, hx⟩
    exact Subtype.coe_prop x'
  · exact aux3₄

lemma adjoin_rootSet : adjoin K (rootSet P ℂ) = F := by
  rw [← root_set]
  suffices K⟮↑√√3, -↑√√3, I * ↑√√3, -I * ↑√√3⟯ = F from by rw [this]
  exact le_antisymm aux4₂ aux4₁

lemma splittingField : IsSplittingField K F P := by
  rw [← adjoin_rootSet]
  exact adjoin_rootSet_isSplittingField (L := ℂ) (IsAlgClosed.splits_codomain P)

instance : IntermediateField.FG F := by
  use (rootSet P ℂ).toFinset
  rw [← adjoin_rootSet, Set.coe_toFinset]

lemma aux5₁ : IsIntegral K (√√3 : ℂ) := ⟨P, ⟨monic_P, eq_P⟩⟩

instance : FiniteDimensional K F := adjoin.finiteDimensional aux5₁
instance : Module.Finite K F := inferInstance
noncomputable instance : Fintype (F ≃ₐ[K] F) := AlgEquiv.fintype K F

noncomputable def aux5₂ : F ≃ₐ[K] (SplittingField P) := Polynomial.IsSplittingField.algEquiv F P (h := splittingField)

example : 2 ≤ (minpoly K (√√3 : ℂ)).natDegree := by
  refine (minpoly.two_le_natDegree_iff aux5₁).2 ?_
  simp only [RingHom.mem_range, IntermediateField.algebraMap_apply, Subtype.exists, exists_prop,
    exists_eq_right]
  intro h
  rw [IntermediateField.mem_adjoin_simple_iff] at h
  rcases h with ⟨t, ⟨s, h⟩⟩

  sorry

example : Fintype.card (Gal P) = 4 := by
  rw [Polynomial.Gal.card_of_separable sep_P]
  have h : Module.finrank K (SplittingField P) = Module.finrank K F :=
    LinearEquiv.finrank_eq aux5₂.toLinearEquiv.symm
  rw [h]
  refine @finrank_of_isSplittingField_X_pow_sub_C K _ 4 ?_ 3 (by sorry) F _ _ splittingField

  sorry

[Vasilii Nesterov]

Riccardo Brasca said:

Yeah, I didn't think about the quickest method. It is just annoying that we have to write anything more than "please Lean tell me that the cubic root of 100 is irrational". For square root we have

unseal Nat.sqrt.iter in
example : Irrational √24 := by decide

and it would be very nice to have something similar for all n-roots of rational numbers.

Should it be in the scope of norm_num?

[Vasilii Nesterov]

Btw, I've implemented this in #22794, so it can be done as

example : Irrational (100^(1/3 : ℝ)) := by norm_num