gal_X_pow_sub_C_isSolvable_aux — Mathlib

English

If a ≠ 0 and the polynomial X^n − 1 splits over F, then the Galois group of X^n − C a over F is solvable (with the coefficient a treated as an element of F).

Русский

Если a ≠ 0 и X^n − 1 распадается над F, то Галуа-галуа группы X^n − C a над F разрешим (где коэффициент a трактуется как элемент F).

LaTeX

$$$$\forall n \in \mathbb{N},\ a \in F\setminus\{0\},\ (X^n - 1 : F[X]) \ Splits(\mathrm{id}_F) \Rightarrow IsSolvable\big((X^n - C a).Gal\big)$$$$

Lean4

theorem gal_X_pow_sub_C_isSolvable_aux (n : ℕ) (a : F) (h : (X ^ n - 1 : F[X]).Splits (RingHom.id F)) :
    IsSolvable (X ^ n - C a).Gal := by
  by_cases ha : a = 0
  · rw [ha, C_0, sub_zero]
    exact gal_X_pow_isSolvable n
  have ha' : algebraMap F (X ^ n - C a).SplittingField a ≠ 0 :=
    mt ((injective_iff_map_eq_zero _).mp (RingHom.injective _) a) ha
  by_cases hn : n = 0
  · rw [hn, pow_zero, ← C_1, ← C_sub]
    exact gal_C_isSolvable (1 - a)
  have hn' : 0 < n := pos_iff_ne_zero.mpr hn
  have hn'' : X ^ n - C a ≠ 0 := X_pow_sub_C_ne_zero hn' a
  have hn''' : (X ^ n - 1 : F[X]) ≠ 0 := X_pow_sub_C_ne_zero hn' 1
  have mem_range :
    ∀ {c : (X ^ n - C a).SplittingField}, (c ^ n = 1 → (∃ d, algebraMap F (X ^ n - C a).SplittingField d = c)) :=
    fun {c} hc =>
    RingHom.mem_range.mp
      (minpoly.mem_range_of_degree_eq_one F c
        (h.def.resolve_left hn''' (minpoly.irreducible ((SplittingField.instNormal (X ^ n - C a)).isIntegral c))
          (minpoly.dvd F c (by rwa [map_id, map_sub, sub_eq_zero, aeval_X_pow, aeval_one]))))
  apply isSolvable_of_comm
  intro σ τ
  ext b hb
  rw [mem_rootSet_of_ne hn'', map_sub, aeval_X_pow, aeval_C, sub_eq_zero] at hb
  have hb' : b ≠ 0 := by
    intro hb'
    rw [hb', zero_pow hn] at hb
    exact ha' hb.symm
  have key : ∀ σ : (X ^ n - C a).Gal, ∃ c, σ b = b * algebraMap F _ c :=
    by
    intro σ
    have key : (σ b / b) ^ n = 1 := by rw [div_pow, ← map_pow, hb, σ.commutes, div_self ha']
    obtain ⟨c, hc⟩ := mem_range key
    use c
    rw [hc, mul_div_cancel₀ (σ b) hb']
  obtain ⟨c, hc⟩ := key σ
  obtain ⟨d, hd⟩ := key τ
  rw [σ.mul_apply, τ.mul_apply, hc, map_mul, τ.commutes, hd, map_mul, σ.commutes, hc, mul_assoc, mul_assoc,
    mul_right_inj' hb', mul_comm]

Похожие утверждения