English
If i is a field homomorphism F → E and a ≠ 0, then (X^n − C a).Splits i implies (X^n − 1).Splits i.
Русский
Пусть i — гомоморфизм полей F → E и a ≠ 0. Если X^n − C a распадается через i, то и X^n − 1 распадается через i.
LaTeX
$$$$\forall i: F \to+* E,\ n:\mathbb{N},\ a \in F\setminus\{0\},\ (X^n - C a).Splits i \Rightarrow (X^n - 1).Splits i$$$$
Lean4
theorem splits_X_pow_sub_one_of_X_pow_sub_C {F : Type*} [Field F] {E : Type*} [Field E] (i : F →+* E) (n : ℕ) {a : F}
(ha : a ≠ 0) (h : (X ^ n - C a).Splits i) : (X ^ n - 1 : F[X]).Splits i :=
by
have ha' : i a ≠ 0 := mt ((injective_iff_map_eq_zero i).mp i.injective a) ha
by_cases hn : n = 0
· rw [hn, pow_zero, sub_self]
exact splits_zero i
have hn' : 0 < n := pos_iff_ne_zero.mpr hn
have hn'' : (X ^ n - C a).degree ≠ 0 := ne_of_eq_of_ne (degree_X_pow_sub_C hn' a) (mt WithBot.coe_eq_coe.mp hn)
obtain ⟨b, hb⟩ := exists_root_of_splits i h hn''
rw [eval₂_sub, eval₂_X_pow, eval₂_C, sub_eq_zero] at hb
have hb' : b ≠ 0 := by
intro hb'
rw [hb', zero_pow hn] at hb
exact ha' hb.symm
let s := ((X ^ n - C a).map i).roots
have hs : _ = _ * (s.map _).prod := eq_prod_roots_of_splits h
rw [leadingCoeff_X_pow_sub_C hn', RingHom.map_one, C_1, one_mul] at hs
have hs' : Multiset.card s = n := (natDegree_eq_card_roots h).symm.trans natDegree_X_pow_sub_C
apply @splits_of_exists_multiset F E _ _ i (X ^ n - 1) (s.map fun c : E => c / b)
rw [leadingCoeff_X_pow_sub_one hn', RingHom.map_one, C_1, one_mul, Multiset.map_map]
have C_mul_C : C (i a⁻¹) * C (i a) = 1 := by rw [← C_mul, ← i.map_mul, inv_mul_cancel₀ ha, i.map_one, C_1]
have key1 : (X ^ n - 1 : F[X]).map i = C (i a⁻¹) * ((X ^ n - C a).map i).comp (C b * X) := by
rw [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, Polynomial.map_one, sub_comp,
pow_comp, X_comp, C_comp, mul_pow, ← C_pow, hb, mul_sub, ← mul_assoc, C_mul_C, one_mul]
have key2 : ((fun q : E[X] => q.comp (C b * X)) ∘ fun c : E => X - C c) = fun c : E => C b * (X - C (c / b)) :=
by
ext1 c
dsimp only [Function.comp_apply]
rw [sub_comp, X_comp, C_comp, mul_sub, ← C_mul, mul_div_cancel₀ c hb']
rw [key1, hs, multiset_prod_comp, Multiset.map_map, key2, Multiset.prod_map_mul,
Function.const_def (α := E) (y := C b), Multiset.map_const, Multiset.prod_replicate, hs', ← C_pow, hb, ← mul_assoc,
C_mul_C, one_mul]
rfl
