GeometricSeedFormula.lean

1 import PaperICompletion5.LinearPrimaryEigenspace
2 import Mathlib.FieldTheory.IsAlgClosed.Basic
3 
4 /-! # The geometric seed formula for arbitrary operators
5 No eigenbasis, diagonalization or multiplicity certificate is an input.
6 The spectrum is the actual algebraic spectrum. Empty spectral maxima are zero.
7 -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace Komorebi.PaperICompletion5.GeometricSeedFormula
11 open Polynomial
12 open Komorebi.PaperICompletion4.OperatorIntrinsicFormula
13 open Komorebi.PaperICompletion5.LinearPrimaryEigenspace
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 /-- Geometric multiplicity values over every scalar, including zero off the spectrum. -/
21 def geometricMultiplicityValues (T : Module.End k V) : Set ℕ :=
22   Set.range (fun a : k ↦ Module.finrank k (T.eigenspace a))
23 
24 /-- The all-scalar value set is nonempty, including on a zero space. -/
25 theorem geometricMultiplicityValues_nonempty (T : Module.End k V) :
26     (geometricMultiplicityValues T).Nonempty :=
27   ⟨Module.finrank k (T.eigenspace 0), 0, rfl⟩
28 
29 /-- Each geometric multiplicity is bounded by seed rank, over any field. -/
30 theorem eigenspace_finrank_le_seedFinrank [FiniteDimensional k V]
31     (T : Module.End k V) (a : k) :
32     Module.finrank k (T.eigenspace a) ≤ seedFinrank (operatorAlgebra T) V := by
33   rw [← intrinsicMultiplicity_X_sub_C_eq_eigenspace T a]
34   exact intrinsicMultiplicity_le_seedFinrank T (X - C a) (irreducible_X_sub_C a)
35 
36 /-- The all-scalar supremum is a finite attained maximum. -/
37 theorem geometricMultiplicityValues_bddAbove [FiniteDimensional k V] (T : Module.End k V) :
38     BddAbove (geometricMultiplicityValues T) := by
39   refine ⟨seedFinrank (operatorAlgebra T) V, ?_⟩
40   rintro n ⟨a, rfl⟩
41   exact eigenspace_finrank_le_seedFinrank T a
42 
43 /-- A presentation-free maximum of actual eigenspace dimensions. -/
44 def geometricSeedMaximum (T : Module.End k V) : ℕ := sSup (geometricMultiplicityValues T)
45 
46 /-- A scalar attaining the maximum exists even if the whole space is zero. -/
47 theorem geometricSeedMaximum_attained [FiniteDimensional k V] (T : Module.End k V) :
48     ∃ a : k, Module.finrank k (T.eigenspace a) = geometricSeedMaximum T :=
49   Nat.sSup_mem (geometricMultiplicityValues_nonempty T) (geometricMultiplicityValues_bddAbove T)
50 
51 /-- Over an algebraically closed field, every monic irreducible is a linear factor. -/
52 theorem monic_irreducible_eq_X_sub_C [IsAlgClosed k] (p : k[X])
53     (hm : p.Monic) (hp : Irreducible p) : ∃ a : k, p = X - C a := by
54   refine ⟨-p.coeff 0, ?_⟩
55   simpa [hm.leadingCoeff] using
56     (eq_X_add_C_of_degree_eq_one (IsAlgClosed.degree_eq_one_of_irreducible k hp))
57 
58 /-- The intrinsic primary and geometric value sets are exactly equal. -/
59 theorem primaryValues_eq_geometricValues [FiniteDimensional k V] [IsAlgClosed k]
60     (T : Module.End k V) : monicPrimaryMultiplicityValues T = geometricMultiplicityValues T := by
61   ext n
62   constructor
63   · rintro ⟨p, hm, hp, rfl⟩
64     obtain ⟨a, rfl⟩ := monic_irreducible_eq_X_sub_C p hm hp
65     exact ⟨a, (intrinsicMultiplicity_X_sub_C_eq_eigenspace T a).symm⟩
66   · rintro ⟨a, rfl⟩
67     exact ⟨X - C a, monic_X_sub_C a, irreducible_X_sub_C a,
68       intrinsicMultiplicity_X_sub_C_eq_eigenspace T a⟩
69 
70 /-- Natural-valued seed rank equals the largest actual eigenspace dimension. -/
71 theorem operator_seedFinrank_eq_geometricSeedMaximum
72     [FiniteDimensional k V] [IsAlgClosed k] (T : Module.End k V) :
73     seedFinrank (operatorAlgebra T) V = geometricSeedMaximum T := by
74   rw [operator_seedFinrank_eq_intrinsicSeedMaximum]
75   unfold intrinsicSeedMaximum geometricSeedMaximum
76   rw [primaryValues_eq_geometricValues T]
77 
78 /-- Cardinal-valued seed rank equals the same finite maximum. -/
79 theorem operator_seedRank_eq_geometricSeedMaximum
80     [FiniteDimensional k V] [IsAlgClosed k] (T : Module.End k V) :
81     seedRank (operatorAlgebra T) V = (geometricSeedMaximum T : Cardinal) := by
82   rw [operator_seedRank_eq_intrinsicSeedMaximum,
83     ← operator_seedFinrank_eq_intrinsicSeedMaximum T,
84     operator_seedFinrank_eq_geometricSeedMaximum T]
85 
86 /-- Spectral values use the actual algebraic spectrum, not a supplied list of eigenvalues. -/
87 def spectralMultiplicityValues (T : Module.End k V) : Set ℕ :=
88   {n | ∃ a : k, a ∈ spectrum k T ∧ Module.finrank k (T.eigenspace a) = n}
89 
90 /-- The spectral value set is bounded whether or not it is empty. -/
91 theorem spectralMultiplicityValues_bddAbove [FiniteDimensional k V] (T : Module.End k V) :
92     BddAbove (spectralMultiplicityValues T) := by
93   refine ⟨seedFinrank (operatorAlgebra T) V, ?_⟩
94   rintro n ⟨a, _, rfl⟩
95   exact eigenspace_finrank_le_seedFinrank T a
96 
97 /-- Geometric multiplicity is zero outside the spectrum. -/
98 theorem eigenspace_finrank_eq_zero_of_not_mem_spectrum [FiniteDimensional k V]
99     (T : Module.End k V) (a : k) (ha : a ∉ spectrum k T) :
100     Module.finrank k (T.eigenspace a) = 0 := by
101   have hn : ¬T.HasEigenvalue a := fun h ↦ ha h.mem_spectrum
102   have hb : T.eigenspace a = ⊥ := by
103     simpa only [Module.End.hasEigenvalue_iff, not_not] using hn
104   rw [hb]
105   exact finrank_bot k V
106 
107 /-- The spectral supremum uses the natural-number empty-set convention, namely zero. -/
108 def spectralSeedMaximum (T : Module.End k V) : ℕ := sSup (spectralMultiplicityValues T)
109 
110 /-- Restricting from all scalars to the spectrum removes only zero values. -/
111 theorem geometricSeedMaximum_eq_spectralSeedMaximum [FiniteDimensional k V]
112     (T : Module.End k V) : geometricSeedMaximum T = spectralSeedMaximum T := by
113   apply le_antisymm
114   · apply csSup_le (geometricMultiplicityValues_nonempty T)
115     rintro n ⟨a, rfl⟩
116     by_cases ha : a ∈ spectrum k T
117     · exact le_csSup (spectralMultiplicityValues_bddAbove T) ⟨a, ha, rfl⟩
118     · change Module.finrank k (T.eigenspace a) ≤ spectralSeedMaximum T
119       rw [eigenspace_finrank_eq_zero_of_not_mem_spectrum T a ha]
120       exact Nat.zero_le _
121   · apply csSup_le'
122     rintro n ⟨a, _, rfl⟩
123     exact le_csSup (geometricMultiplicityValues_bddAbove T) ⟨a, rfl⟩
124 
125 /-- The exact printed geometric formula, including the empty-spectrum convention. -/
126 theorem operator_seedFinrank_eq_spectralSeedMaximum
127     [FiniteDimensional k V] [IsAlgClosed k] (T : Module.End k V) :
128     seedFinrank (operatorAlgebra T) V = spectralSeedMaximum T := by
129   rw [operator_seedFinrank_eq_geometricSeedMaximum, geometricSeedMaximum_eq_spectralSeedMaximum]
130 
131 /-- Cardinal-valued version of the printed formula. -/
132 theorem operator_seedRank_eq_spectralSeedMaximum
133     [FiniteDimensional k V] [IsAlgClosed k] (T : Module.End k V) :
134     seedRank (operatorAlgebra T) V = (spectralSeedMaximum T : Cardinal) := by
135   rw [operator_seedRank_eq_geometricSeedMaximum, geometricSeedMaximum_eq_spectralSeedMaximum]
136 
137 end Komorebi.PaperICompletion5.GeometricSeedFormula

Back to source controls