CompanionSpectrum.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.FiniteModels
6 import Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
7 import Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
8 import Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
9 import Mathlib.Analysis.Complex.Polynomial.Basic
10 import Mathlib.FieldTheory.Separable
11 
12 /-! # The exact characteristic polynomial of the signed companion
13 
14 The first column detects every coefficient of a polynomial of degree below N.
15 Together with Cayley--Hamilton this derives the characteristic polynomial.
16 -/
17 
18 namespace Komorebi.PaperIV
19 noncomputable section
20 open Polynomial
21 
22 /-- The first column of a polynomial in J retains all coefficients below N. -/
23 theorem aeval_signedShiftMatrix_first_column {N : ℕ} (hN : 0 < N)
24     (P : ℂ[X]) (hP : P.natDegree < N) (p : Fin N) :
25     aeval (signedShiftMatrix (R := ℂ) N) P p ⟨0, hN⟩ = P.coeff p.val := by
26   rw [aeval_eq_sum_range' hP]
27   simp only [Matrix.sum_apply, Matrix.smul_apply, smul_eq_mul]
28   rw [Finset.sum_eq_single p.val]
29   · rw [signedShiftMatrix_pow_apply N p.val hN]
30     simp [Nat.mod_eq_of_lt p.isLt, Nat.div_eq_of_lt p.isLt]
31   · intro m hm hmp
32     have hmN : m < N := Finset.mem_range.mp hm
33     rw [signedShiftMatrix_pow_apply N m hN]
34     simp [Nat.mod_eq_of_lt hmN, Ne.symm hmp]
35   · simp [p.isLt]
36 
37 /-- No nonzero polynomial of degree below N annihilates the signed shift. -/
38 theorem signedShiftMatrix_no_small_annihilator {N : ℕ} (hN : 0 < N)
39     (P : ℂ[X]) (hP : P.natDegree < N)
40     (hzero : aeval (signedShiftMatrix (R := ℂ) N) P = 0) : P = 0 := by
41   ext m
42   by_cases hm : m < N
43   · have h := aeval_signedShiftMatrix_first_column hN P hP ⟨m, hm⟩
44     rw [hzero] at h
45     simpa using h.symm
46   · simp [coeff_eq_zero_of_natDegree_lt (show P.natDegree < m by omega)]
47 
48 /-- The signed relation is an actual annihilating polynomial. -/
49 theorem aeval_signedShiftMatrix_X_pow_add_one {N : ℕ} (hN : 0 < N) :
50     aeval (signedShiftMatrix (R := ℂ) N) (X ^ N + 1 : ℂ[X]) = 0 := by
51   simp only [map_add, map_pow, aeval_X, map_one, signedShiftMatrix_pow_order N hN]
52   exact neg_add_cancel 1
53 
54 /-- The companion characteristic polynomial is exactly X^N + 1. -/
55 theorem signedShiftMatrix_charpoly {N : ℕ} (hN : 0 < N) :
56     (signedShiftMatrix (R := ℂ) N).charpoly = (X ^ N + 1 : ℂ[X]) := by
57   let P := (signedShiftMatrix (R := ℂ) N).charpoly
58   have hp : P.IsMonicOfDegree N := by
59     exact ⟨by simp [P], Matrix.charpoly_monic _⟩
60   have hq : (X ^ N + 1 : ℂ[X]).IsMonicOfDegree N := by
61     exact ⟨by simp, by simpa using monic_X_pow_add_C (1 : ℂ) hN.ne'⟩
62   have hdeg := hp.natDegree_sub_lt hN.ne' hq
63   apply sub_eq_zero.mp
64   apply signedShiftMatrix_no_small_annihilator hN _ hdeg
65   rw [map_sub, Matrix.aeval_self_charpoly, aeval_signedShiftMatrix_X_pow_add_one hN,
66     sub_self]
67 
68 /-- The spectrum consists of precisely the Nth roots of minus one. -/
69 theorem signedShiftMatrix_mem_spectrum_iff {N : ℕ} (hN : 0 < N) (eta : ℂ) :
70     eta ∈ spectrum ℂ (signedShiftMatrix (R := ℂ) N) ↔ eta ^ N = -1 := by
71   rw [Matrix.mem_spectrum_iff_isRoot_charpoly, signedShiftMatrix_charpoly hN]
72   simp [IsRoot.def, add_eq_zero_iff_eq_neg]
73 
74 /-- Every characteristic root is simple. -/
75 theorem signedShiftMatrix_charpoly_separable {N : ℕ} (hN : 0 < N) :
76     (signedShiftMatrix (R := ℂ) N).charpoly.Separable := by
77   rw [signedShiftMatrix_charpoly hN]
78   simpa using separable_X_pow_sub_C (-1 : ℂ)
79     (by exact_mod_cast hN.ne') (by norm_num)
80 
81 /-- There are exactly N characteristic roots, counted with multiplicity. -/
82 theorem signedShiftMatrix_charpoly_roots_card {N : ℕ} (hN : 0 < N) :
83     (signedShiftMatrix (R := ℂ) N).charpoly.roots.card = N := by
84   rw [signedShiftMatrix_charpoly hN,
85     (IsAlgClosed.splits _).natDegree_eq_card_roots.symm]
86   simp
87 
88 /-- The root multiset has no repeated elements. -/
89 theorem signedShiftMatrix_charpoly_roots_nodup {N : ℕ} (hN : 0 < N) :
90     (signedShiftMatrix (R := ℂ) N).charpoly.roots.Nodup :=
91   Polynomial.nodup_roots (signedShiftMatrix_charpoly_separable hN)
92 
93 end
94 end Komorebi.PaperIV

Back to source controls