CyclicPolynomial.lean

1 import Mathlib.LinearAlgebra.Charpoly.ToMatrix
2 import Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
3 import Mathlib.Tactic
4 
5 /-! Characteristic polynomials from a proved cyclic basis. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CyclicPolynomial
9 open scoped BigOperators
10 open Polynomial
11 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
12 
13 theorem aeval_apply_eq_sum (F : Module.End K V) (v : V) {p : K[X]} {n : ℕ}
14     (hp : p.natDegree < n) :
15     aeval F p v = ∑ i : Fin n, p.coeff i • (F ^ (i : ℕ)) v := by
16   rw [aeval_eq_sum_range' hp]
17   simp only [LinearMap.sum_apply]
18   exact (Fin.sum_univ_eq_sum_range _ _).symm
19 
20 theorem no_short_annihilator (F : Module.End K V) (v : V) {n : ℕ}
21     (hli : LinearIndependent K (fun i : Fin n => (F ^ (i : ℕ)) v))
22     {p : K[X]} (hp : p.natDegree < n) (hzero : aeval F p v = 0) : p = 0 := by
23   classical
24   rw [aeval_apply_eq_sum F v hp] at hzero
25   have hc := Fintype.linearIndependent_iff.mp hli (fun i => p.coeff i) hzero
26   ext k
27   by_cases hk : k < n
28   · exact hc ⟨k, hk⟩
29   · simp [coeff_eq_zero_of_natDegree_lt (by omega : p.natDegree < k)]
30 
31 theorem charpoly_of_orbit_basis [FiniteDimensional K V] (F : Module.End K V)
32     {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) K V) (v : V)
33     (hb : ∀ i : Fin n, b i = (F ^ (i : ℕ)) v) (c : K)
34     (hclose : (F ^ n) v = c • v) : F.charpoly = X ^ n - C c := by
35   have hdim : Module.finrank K V = n := by simpa using Module.finrank_eq_card_basis b
36   have hli : LinearIndependent K (fun i : Fin n => (F ^ (i : ℕ)) v) := by
37     simpa only [← hb] using b.linearIndependent
38   have hm1 : IsMonicOfDegree F.charpoly n := ⟨by simpa [hdim] using F.charpoly_natDegree, F.charpoly_monic⟩
39   have hm2 : IsMonicOfDegree (X ^ n - C c : K[X]) n :=
40     ⟨natDegree_X_pow_sub_C, monic_X_pow_sub_C c (Nat.ne_of_gt hn)⟩
41   apply sub_eq_zero.mp
42   apply no_short_annihilator F v hli (hm1.natDegree_sub_lt (Nat.ne_of_gt hn) hm2)
43   simp [map_sub, map_pow, aeval_X, aeval_C, F.aeval_self_charpoly, hclose]
44 
45 theorem det_of_orbit_basis [FiniteDimensional K V] (F : Module.End K V)
46     {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) K V) (v : V)
47     (hb : ∀ i : Fin n, b i = (F ^ (i : ℕ)) v) (c : K)
48     (hclose : (F ^ n) v = c • v) : F.det = (-1) ^ (n - 1) * c := by
49   classical
50   rw [← LinearMap.det_toMatrix b F, Matrix.det_eq_sign_charpoly_coeff,
51     LinearMap.charpoly_toMatrix, charpoly_of_orbit_basis F hn b v hb c hclose]
52   simp only [Fintype.card_fin, coeff_sub, coeff_X_pow, coeff_C]
53   have he : n = (n - 1) + 1 := by omega
54   have hs : (-1 : K) ^ n = -((-1 : K) ^ (n - 1)) := by
55     conv_lhs => rw [he, pow_succ]
56     simp
57   simp [Ne.symm hn.ne', hs]
58 
59 theorem eval_charpoly_of_orbit_basis [FiniteDimensional K V] (F : Module.End K V)
60     {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) K V) (v : V)
61     (hb : ∀ i : Fin n, b i = (F ^ (i : ℕ)) v) (c t : K)
62     (hclose : (F ^ n) v = c • v) :
63     (algebraMap K (Module.End K V) t - F).det = t ^ n - c := by
64   rw [← F.eval_charpoly, charpoly_of_orbit_basis F hn b v hb c hclose]
65   simp
66 
67 theorem reverse_cycle_polynomial (n : ℕ) (c : K) :
68     (X ^ n - C c : K[X]).reverse = 1 - C c * X ^ n := by
69   rw [Polynomial.reverse, natDegree_X_pow_sub_C, reflect_sub, reflect_monomial, reflect_C]
70   simp
71 
72 theorem local_polynomial_of_orbit_basis [FiniteDimensional K V] (F : Module.End K V)
73     {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) K V) (v : V)
74     (hb : ∀ i : Fin n, b i = (F ^ (i : ℕ)) v) (c : K)
75     (hclose : (F ^ n) v = c • v) :
76     (LinearMap.toMatrix b b F).charpolyRev = 1 - C c * X ^ n := by
77   classical
78   rw [← Matrix.reverse_charpoly, LinearMap.charpoly_toMatrix,
79     charpoly_of_orbit_basis F hn b v hb c hclose, reverse_cycle_polynomial]
80 
81 end PaperXI.CyclicPolynomial

Back to source controls