CyclicClassification.lean

1 import KomorebiVerification.SingleOperatorGraph
2 import Mathlib.Algebra.Module.PID
3 import Mathlib.LinearAlgebra.AnnihilatingPolynomial
4 import Mathlib.RingTheory.AdjoinRoot
5 
6 /-!
7 # The cyclic-vector / minimal-characteristic polynomial bridge
8 
9 Unlike the historical certificate-assembly theorem, these declarations do
10 not accept the desired polynomial equivalence as a hypothesis.  The reverse
11 implication uses Mathlib's proven PID-module annihilator-attainment theorem.
12 All maps are the actual polynomial action of the given endomorphism.
13 -/
14 
15 set_option autoImplicit false
16 noncomputable section
17 
18 namespace Komorebi.PaperICompletion.CyclicClassification
19 open Komorebi.SingleOperatorGraph
20 open Polynomial
21 
22 universe u v
23 variable {k : Type u} [Field k]
24 variable {V : Type v} [AddCommGroup V] [Module k V]
25 
26 /-- The polynomial-module presentation of the orbit of a specified vector. -/
27 def orbitMap (T : Module.End k V) (x : V) : k[X] →ₗ[k[X]] Module.AEval' T :=
28   LinearMap.toSpanSingleton k[X] (Module.AEval' T) (Module.AEval'.of T x)
29 
30 @[simp]
31 theorem orbitMap_apply (T : Module.End k V) (x : V) (p : k[X]) :
32     orbitMap T x p = Module.AEval'.of T (aeval T p x) := rfl
33 
34 /-- The span definition of one seed is equivalent to surjectivity of its actual orbit map. -/
35 theorem singleton_generates_iff_orbitMap_surjective (T : Module.End k V) (x : V) :
36     FamilyGenerates T (fun _ : Fin 1 ↦ x) ↔ Function.Surjective (orbitMap T x) := by
37   have hrange : Set.range (orbitFamily T (fun _ : Fin 1 ↦ x)) =
38       ((evalVector T x).range : Set V) := by
39     ext y
40     constructor
41     · rintro ⟨⟨_i, p⟩, rfl⟩
42       exact ⟨p, rfl⟩
43     · rintro ⟨p, rfl⟩
44       exact ⟨(0, p), rfl⟩
45   change Submodule.span k (Set.range (orbitFamily T (fun _ : Fin 1 ↦ x))) = ⊤ ↔ _
46   rw [hrange, Submodule.span_eq, LinearMap.range_eq_top]
47   rfl
48 
49 /-- Eliminate the arbitrary indexing function from the one-seed predicate. -/
50 theorem hasCyclicVector_iff_exists_surjective (T : Module.End k V) :
51     HasCyclicVector T ↔ ∃ x : V, Function.Surjective (orbitMap T x) := by
52   constructor
53   · rintro ⟨s, hs⟩
54     have heq : s = fun _ : Fin 1 ↦ s 0 := by
55       funext i
56       exact congrArg s (Subsingleton.elim i 0)
57     rw [heq] at hs
58     exact ⟨s 0, (singleton_generates_iff_orbitMap_surjective T (s 0)).mp hs⟩
59   · rintro ⟨x, hx⟩
60     exact ⟨fun _ : Fin 1 ↦ x, (singleton_generates_iff_orbitMap_surjective T x).mpr hx⟩
61 
62 /-- A cyclic vector has exactly the annihilator of the whole polynomial module. -/
63 theorem orbitMap_ker_eq_annihilator_of_surjective
64     (T : Module.End k V) (x : V) (hx : Function.Surjective (orbitMap T x)) :
65     (orbitMap T x).ker = Module.annihilator k[X] (Module.AEval' T) := by
66   ext p
67   change p • Module.AEval'.of T x = 0 ↔
68     p ∈ Module.annihilator k[X] (Module.AEval' T)
69   rw [Module.mem_annihilator]
70   constructor
71   · intro hp y
72     obtain ⟨q, rfl⟩ := hx y
73     change p • (q • Module.AEval'.of T x) = 0
74     rw [smul_smul, mul_comm p q, ← smul_smul, hp, smul_zero]
75   · intro hp
76     exact hp (Module.AEval'.of T x)
77 
78 /-- Identify the orbit's quotient with the minimal-polynomial quotient, from kernel equality. -/
79 def minpolyQuotientEquivOrbit (T : Module.End k V) (x : V)
80     (hx : (orbitMap T x).ker = Module.annihilator k[X] (Module.AEval' T)) :
81     (k[X] ⧸ Ideal.span {minpoly k T}) ≃ₗ[k[X]] (orbitMap T x).range :=
82   (Submodule.quotEquivOfEq _ _
83     ((Polynomial.span_minpoly_eq_annihilator k T).trans hx.symm)).trans
84     (orbitMap T x).quotKerEquivRange
85 
86 /-- The cyclic orbit has dimension equal to the degree of the minimal polynomial. -/
87 theorem orbit_finrank_eq_minpoly_degree (T : Module.End k V) (x : V)
88     (hx : (orbitMap T x).ker = Module.annihilator k[X] (Module.AEval' T)) :
89     Module.finrank k (orbitMap T x).range = (minpoly k T).natDegree := by
90   rw [← ((minpolyQuotientEquivOrbit T x hx).restrictScalars k).finrank_eq]
91   exact finrank_quotient_span_eq_natDegree
92 
93 /-- Cyclicity gives the minimal polynomial its full possible degree. -/
94 theorem minpoly_degree_eq_finrank_of_cyclic [FiniteDimensional k V]
95     (T : Module.End k V) (hT : HasCyclicVector T) :
96     (minpoly k T).natDegree = Module.finrank k V := by
97   obtain ⟨x, hx⟩ := (hasCyclicVector_iff_exists_surjective T).mp hT
98   have hker := orbitMap_ker_eq_annihilator_of_surjective T x hx
99   have hd := orbit_finrank_eq_minpoly_degree T x hker
100   have he : (orbitMap T x).range ≃ₗ[k[X]] Module.AEval' T :=
101     LinearEquiv.ofTop (orbitMap T x).range (LinearMap.range_eq_top.mpr hx)
102   exact hd.symm.trans (((he.restrictScalars k).finrank_eq).trans
103     (Module.AEval'.of T).finrank_eq.symm)
104 
105 /-- The forward minpoly/charpoly bridge, without any canonical-form certificate. -/
106 theorem minpoly_eq_charpoly_of_cyclic [FiniteDimensional k V]
107     (T : Module.End k V) (hT : HasCyclicVector T) :
108     minpoly k T = T.charpoly := by
109   apply (Polynomial.eq_of_monic_of_dvd_of_natDegree_le
110     (minpoly.monic (LinearMap.isIntegral T)) (LinearMap.charpoly_monic T)
111     (LinearMap.minpoly_dvd_charpoly T) ?_).symm
112   rw [LinearMap.charpoly_natDegree, minpoly_degree_eq_finrank_of_cyclic T hT]
113 
114 /-- The PID theorem supplies a vector with the full operator annihilator. -/
115 theorem exists_full_annihilator_vector [FiniteDimensional k V] (T : Module.End k V) :
116     ∃ x : V, (orbitMap T x).ker = Module.annihilator k[X] (Module.AEval' T) := by
117   obtain ⟨x, hx⟩ := Module.exists_ker_toSpanSingleton_eq_annihilator
118     k[X] (Module.AEval' T)
119   exact ⟨(Module.AEval'.of T).symm x, hx⟩
120 
121 /-- Full minimal-polynomial degree forces the attained annihilator orbit to fill the space. -/
122 theorem cyclic_of_minpoly_degree_eq_finrank [FiniteDimensional k V]
123     (T : Module.End k V) (hdegree : (minpoly k T).natDegree = Module.finrank k V) :
124     HasCyclicVector T := by
125   obtain ⟨x, hx⟩ := exists_full_annihilator_vector T
126   have hrank : Module.finrank k (orbitMap T x).range =
127       Module.finrank k (Module.AEval' T) := by
128     rw [orbit_finrank_eq_minpoly_degree T x hx, hdegree, ← (Module.AEval'.of T).finrank_eq]
129   have htop : ((orbitMap T x).range.restrictScalars k) = ⊤ :=
130     Submodule.eq_top_of_finrank_eq hrank
131   have hsurj : Function.Surjective (orbitMap T x) := by
132     intro y
133     have hy : y ∈ (orbitMap T x).range.restrictScalars k := by rw [htop]; trivial
134     exact hy
135   exact (hasCyclicVector_iff_exists_surjective T).mpr ⟨x, hsurj⟩
136 
137 /-- The complete cyclic-vector criterion over an arbitrary field. -/
138 theorem hasCyclicVector_iff_minpoly_eq_charpoly [FiniteDimensional k V]
139     (T : Module.End k V) : HasCyclicVector T ↔ minpoly k T = T.charpoly := by
140   constructor
141   · exact minpoly_eq_charpoly_of_cyclic T
142   · intro hp
143     apply cyclic_of_minpoly_degree_eq_finrank T
144     rw [hp, LinearMap.charpoly_natDegree]
145 
146 /-- The one-seed polynomial predicate agrees with cyclicity for the actual operator algebra. -/
147 theorem hasCyclicVector_iff_operatorAlgebra_cyclic (T : Module.End k V) :
148     HasCyclicVector T ↔ Komorebi.SeedRankBasics.Cyclic (operatorAlgebra T) V := by
149   constructor
150   · rintro ⟨s, hs⟩
151     have heq : s = fun _ : Fin 1 ↦ s 0 := by
152       funext i
153       exact congrArg s (Subsingleton.elim i 0)
154     rw [heq] at hs
155     have h := (familyGenerates_iff_operatorAlgebra_familyGenerates T
156       (fun _ : Fin 1 ↦ s 0)).mp hs
157     exact ⟨s 0, by simpa [Komorebi.SeedRankBasics.FamilyGenerates] using h⟩
158   · rintro ⟨x, hx⟩
159     refine ⟨fun _ : Fin 1 ↦ x, ?_⟩
160     apply (familyGenerates_iff_operatorAlgebra_familyGenerates T _).mpr
161     simpa [Komorebi.SeedRankBasics.FamilyGenerates] using hx
162 
163 /-- Rank-one form of the genuine polynomial criterion; nonzero space is necessary. -/
164 theorem operatorAlgebra_seedRank_eq_one_iff_minpoly_eq_charpoly
165     [FiniteDimensional k V] [Nontrivial V] (T : Module.End k V) :
166     Komorebi.SeedRankBasics.seedRank (operatorAlgebra T) V = 1 ↔
167       minpoly k T = T.charpoly := by
168   let : Module.Finite (operatorAlgebra T) V :=
169     Module.Finite.of_restrictScalars_finite k (operatorAlgebra T) V
170   rw [Komorebi.SeedRankBasics.seedRank_eq_one_iff_cyclic,
171     ← hasCyclicVector_iff_operatorAlgebra_cyclic,
172     hasCyclicVector_iff_minpoly_eq_charpoly]
173 
174 /-- The old four-way assembly no longer needs a polynomial classification input.
175 The seed-number and geometric/block-identification certificates remain explicit. -/
176 theorem cyclic_four_way_without_polynomial_certificate
177     [FiniteDimensional k V] {Λ : Type*}
178     (T : Module.End k V) (R : ℕ)
179     (geometricMultiplicity blockMultiplicity : Λ → ℕ)
180     (hpositive : ∀ eigen, 0 < geometricMultiplicity eigen)
181     (hbound : ∀ eigen, geometricMultiplicity eigen ≤ R)
182     (maxEigen : Λ) (hmax : geometricMultiplicity maxEigen = R)
183     (hLeast : IsLeast {r : ℕ | SeedNumberLE T r} R)
184     (hgeometric_eq_blocks : ∀ eigen,
185       geometricMultiplicity eigen = blockMultiplicity eigen) :
186     (HasCyclicVector T ↔ AllGeometricMultiplicitiesOne geometricMultiplicity) ∧
187       (AllGeometricMultiplicitiesOne geometricMultiplicity ↔
188         OneJordanBlockPerEigenvalue blockMultiplicity) ∧
189       (OneJordanBlockPerEigenvalue blockMultiplicity ↔ minpoly k T = T.charpoly) := by
190   have hfirst : HasCyclicVector T ↔
191       AllGeometricMultiplicitiesOne geometricMultiplicity :=
192     hasCyclicVector_iff_one_block_per_eigenvalue
193       T R geometricMultiplicity hpositive hbound maxEigen hmax hLeast
194   have hmiddle : AllGeometricMultiplicitiesOne geometricMultiplicity ↔
195       OneJordanBlockPerEigenvalue blockMultiplicity := by
196     constructor
197     · intro h eigen
198       rw [← hgeometric_eq_blocks eigen]
199       exact h eigen
200     · intro h eigen
201       rw [hgeometric_eq_blocks eigen]
202       exact h eigen
203   exact ⟨hfirst, hmiddle,
204     hmiddle.symm.trans (hfirst.symm.trans (hasCyclicVector_iff_minpoly_eq_charpoly T))⟩
205 
206 end Komorebi.PaperICompletion.CyclicClassification

Back to source controls