CyclicGeometricCriterion.lean

1 import PaperICompletion5.GeometricSeedFormula
2 
3 /-! # The unconditional geometric cyclic criterion over algebraically closed fields
4 The nonzero-space guard is retained when cyclicity is stated as seed rank one.
5 The one-invariant-factor clause is represented by an actual polynomial-module
6 quotient equivalence, not by a supplied numerical invariant-factor count.
7 -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace Komorebi.PaperICompletion5.CyclicGeometricCriterion
11 open Polynomial
12 open Komorebi.PaperICompletion5.GeometricSeedFormula
13 open Komorebi.PaperICompletion.CyclicClassification
14 open Komorebi.SeedRankBasics
15 open Komorebi.SingleOperatorGraph
16 universe u v
17 variable {k : Type u} [Field k]
18 variable {V : Type v} [AddCommGroup V] [Module k V]
19 
20 /-- A spectral value has strictly positive geometric multiplicity. -/
21 theorem eigenspace_finrank_pos_iff_mem_spectrum [FiniteDimensional k V]
22     (T : Module.End k V) (a : k) :
23     0 < Module.finrank k (T.eigenspace a) ↔ a ∈ spectrum k T := by
24   rw [Module.finrank_pos_iff, Submodule.nontrivial_iff_ne_bot,
25     ← Module.End.hasEigenvalue_iff, Module.End.hasEigenvalue_iff_mem_spectrum]
26 
27 /-- The geometric maximum cannot vanish on a nonzero space over an algebraically closed field. -/
28 theorem geometricSeedMaximum_pos [FiniteDimensional k V] [IsAlgClosed k]
29     [Nontrivial V] (T : Module.End k V) : 0 < geometricSeedMaximum T := by
30   by_contra h
31   have hg : geometricSeedMaximum T = 0 := Nat.eq_zero_of_not_pos h
32   have hz : seedRank (operatorAlgebra T) V = 0 := by
33     rw [operator_seedRank_eq_geometricSeedMaximum, hg]
34     rfl
35   exact not_subsingleton V ((seedRank_eq_zero_iff (operatorAlgebra T) V).mp hz)
36 
37 /-- On a nonzero space, a maximum-attaining scalar is an actual spectral value. -/
38 theorem spectralSeedMaximum_attained [FiniteDimensional k V] [IsAlgClosed k]
39     [Nontrivial V] (T : Module.End k V) :
40     ∃ a : k, a ∈ spectrum k T ∧ Module.finrank k (T.eigenspace a) = spectralSeedMaximum T := by
41   obtain ⟨a, ha⟩ := geometricSeedMaximum_attained T
42   refine ⟨a, ?_, ha.trans (geometricSeedMaximum_eq_spectralSeedMaximum T)⟩
43   apply (eigenspace_finrank_pos_iff_mem_spectrum T a).mp
44   rw [ha]
45   exact geometricSeedMaximum_pos T
46 
47 /-- Rank-one maximum is equivalent to multiplicity one at every actual eigenvalue. -/
48 theorem geometricSeedMaximum_eq_one_iff [FiniteDimensional k V] [IsAlgClosed k]
49     [Nontrivial V] (T : Module.End k V) :
50     geometricSeedMaximum T = 1 ↔
51       ∀ a : k, a ∈ spectrum k T → Module.finrank k (T.eigenspace a) = 1 := by
52   constructor
53   · intro h a ha
54     have hpos := (eigenspace_finrank_pos_iff_mem_spectrum T a).mpr ha
55     have hle : Module.finrank k (T.eigenspace a) ≤ geometricSeedMaximum T :=
56       le_csSup (geometricMultiplicityValues_bddAbove T) ⟨a, rfl⟩
57     omega
58   · intro h
59     have hle : geometricSeedMaximum T ≤ 1 := by
60       apply csSup_le (geometricMultiplicityValues_nonempty T)
61       rintro n ⟨a, rfl⟩
62       change Module.finrank k (T.eigenspace a) ≤ 1
63       by_cases ha : a ∈ spectrum k T
64       · rw [h a ha]
65       · rw [eigenspace_finrank_eq_zero_of_not_mem_spectrum T a ha]
66         exact Nat.zero_le _
67     have hp := geometricSeedMaximum_pos T
68     omega
69 
70 /-- Cyclicity and the actual geometric maximum agree, with no spectral certificate. -/
71 theorem hasCyclicVector_iff_geometricSeedMaximum_one
72     [FiniteDimensional k V] [IsAlgClosed k] [Nontrivial V] (T : Module.End k V) :
73     HasCyclicVector T ↔ geometricSeedMaximum T = 1 := by
74   have h := (hasCyclicVector_iff_minpoly_eq_charpoly T).trans
75     (operatorAlgebra_seedRank_eq_one_iff_minpoly_eq_charpoly T).symm
76   rw [operator_seedRank_eq_geometricSeedMaximum] at h
77   exact h.trans (by norm_cast)
78 
79 /-- The full geometric cyclic criterion at native algebraically closed scope. -/
80 theorem hasCyclicVector_iff_all_spectral_multiplicities_one
81     [FiniteDimensional k V] [IsAlgClosed k] [Nontrivial V] (T : Module.End k V) :
82     HasCyclicVector T ↔
83       ∀ a : k, a ∈ spectrum k T → Module.finrank k (T.eigenspace a) = 1 :=
84   (hasCyclicVector_iff_geometricSeedMaximum_one T).trans (geometricSeedMaximum_eq_one_iff T)
85 
86 /-- Polynomial equality has the same unconditional geometric characterization. -/
87 theorem minpoly_eq_charpoly_iff_all_spectral_multiplicities_one
88     [FiniteDimensional k V] [IsAlgClosed k] [Nontrivial V] (T : Module.End k V) :
89     minpoly k T = T.charpoly ↔
90       ∀ a : k, a ∈ spectrum k T → Module.finrank k (T.eigenspace a) = 1 :=
91   (hasCyclicVector_iff_minpoly_eq_charpoly T).symm.trans
92     (hasCyclicVector_iff_all_spectral_multiplicities_one T)
93 
94 /-- A cyclic operator has the actual one-factor polynomial-module presentation. -/
95 def cyclicMinpolyQuotientEquiv (T : Module.End k V) (x : V)
96     (hx : Function.Surjective (orbitMap T x)) :
97     Module.AEval' T ≃ₗ[k[X]] k[X] ⧸ Ideal.span {minpoly k T} :=
98   ((minpolyQuotientEquivOrbit T x (orbitMap_ker_eq_annihilator_of_surjective T x hx)).trans
99     (LinearEquiv.ofTop (orbitMap T x).range (LinearMap.range_eq_top.mpr hx))).symm
100 
101 /-- Cyclicity constructs a one-factor presentation, rather than receiving a count certificate. -/
102 theorem hasCyclicVector_iff_minpoly_quotient_presentation (T : Module.End k V) :
103     HasCyclicVector T ↔ Nonempty (Module.AEval' T ≃ₗ[k[X]] k[X] ⧸ Ideal.span {minpoly k T}) := by
104   constructor
105   · intro h
106     obtain ⟨x, hx⟩ := (hasCyclicVector_iff_exists_surjective T).mp h
107     exact ⟨cyclicMinpolyQuotientEquiv T x hx⟩
108   · rintro ⟨e⟩
109     let z : Module.AEval' T := e.symm (Ideal.Quotient.mk _ 1)
110     apply (hasCyclicVector_iff_exists_surjective T).mpr
111     refine ⟨(Module.AEval'.of T).symm z, ?_⟩
112     intro y
113     obtain ⟨p, hp⟩ := Ideal.Quotient.mk_surjective (e y)
114     refine ⟨p, ?_⟩
115     apply e.injective
116     change e (p • z) = e y
117     rw [e.map_smul]
118     simp only [z, e.apply_symm_apply, Algebra.smul_def, map_one, mul_one]
119     exact hp
120 
121 end Komorebi.PaperICompletion5.CyclicGeometricCriterion

Back to source controls