OperatorIntrinsicFormula.lean

1 import PaperICompletion4.GroupedPrimary
2 
3 /-! # Intrinsic primary multiplicities of the actual operator
4 Each primary multiplicity is the residue-field dimension of X_p/p(T)X_p.
5 It is identified with each presentation fibre, not just their maximum.
6 -/
7 set_option autoImplicit false
8 noncomputable section
9 open scoped Pointwise
10 namespace Komorebi.PaperICompletion4.OperatorIntrinsicFormula
11 open Polynomial
12 open Komorebi.PaperICompletion3.PrimarySeedFormula
13 open Komorebi.PaperICompletion3.OperatorPrimaryAPI
14 open Komorebi.PaperICompletion4.ResidueQuotient
15 open Komorebi.PaperICompletion4.IntrinsicPrimary
16 open Komorebi.PaperICompletion4.GroupedPrimary
17 open Komorebi.SeedRankBasics
18 universe u v
19 variable {k : Type u} [Field k]
20 variable {V : Type v} [AddCommGroup V] [Module k V]
21 
22 /-- The literal intrinsic quotient of the actual polynomial module. -/
23 abbrev IntrinsicPrimaryQuotient (T : Module.End k V) (p : k[X]) :=
24   ScalarQuotient (primarySubmodule (Module.AEval' T) p) p
25 
26 /-- Intrinsic multiplicity is residue-field dimension, not base-field dimension. -/
27 def intrinsicMultiplicity (T : Module.End k V) (p : k[X]) : ℕ :=
28   Module.finrank (k[X] ⧸ Ideal.span {p}) (IntrinsicPrimaryQuotient T p)
29 
30 /-- The underlying primary condition is the paper's actual p(T)-annihilation condition. -/
31 theorem operator_primary_membership (T : Module.End k V) (p : k[X]) (x : V) :
32     Module.AEval'.of T x ∈ primarySubmodule (Module.AEval' T) p ↔
33       ∃ n : ℕ, ((aeval T p) ^ n) x = 0 := by
34   change (∃ n : ℕ, ((aeval T) (p ^ n)) x = 0) ↔ _
35   simp only [map_pow]
36 
37 /-- Scalar-image membership agrees with the literal image of p(T) on V. -/
38 theorem operator_scalarImage_membership (T : Module.End k V) (p : k[X]) (x : V) :
39     Module.AEval'.of T x ∈ p • (⊤ : Submodule k[X] (Module.AEval' T)) ↔
40       ∃ y : V, (aeval T p) y = x := by
41   rw [mem_scalarImage_iff]
42   rfl
43 
44 /-- The grouped elementary divisors are the actual intrinsic primary component. -/
45 def operatorPrimaryComponentEquiv {T : Module.End k V} (D : PrimaryPresentation T)
46     (p : k[X]) (hp : Irreducible p) :
47     primarySubmodule (Module.AEval' T) p ≃ₗ[k[X]]
48       ((i : {i : D.Index // D.label i = Ideal.span {p}}) →
49         k[X] ⧸ Ideal.span {D.prime i ^ D.exponent i}) :=
50   (primaryCongr p D.equiv).trans (groupedPrimaryEquiv D.prime D.irreducible D.exponent p hp)
51 
52 /-- Any actual primary presentation identifies the intrinsic quotient with its residue fibre. -/
53 def operatorPrimaryQuotientEquiv [FiniteDimensional k V]
54     {T : Module.End k V} (D : PrimaryPresentation T) (p : k[X]) (hp : Irreducible p) :
55     IntrinsicPrimaryQuotient T p ≃ₗ[k[X] ⧸ Ideal.span {p}]
56       ({i : D.Index // D.label i = Ideal.span {p}} → k[X] ⧸ Ideal.span {p}) := by
57   let : IsArtinian k[X] (Module.AEval' T) := isArtinian_of_tower k inferInstance
58   exact (primaryQuotientEquivGlobal (Module.AEval' T) p).trans
59     ((scalarQuotientCongr p D.equiv).trans
60       (primaryProductQuotientEquiv D.prime D.irreducible D.exponent D.positive p hp))
61 
62 /-- The intrinsic dimension equals the number of blocks in each primary fibre. -/
63 theorem intrinsicMultiplicity_eq_fiber [FiniteDimensional k V]
64     {T : Module.End k V} (D : PrimaryPresentation T) (p : k[X]) (hp : Irreducible p) :
65     intrinsicMultiplicity T p = fiberMultiplicity D.label (Ideal.span {p}) := by
66   classical
67   let : (Ideal.span {p}).IsMaximal := PrincipalIdealRing.isMaximal_of_irreducible hp
68   let : Field (k[X] ⧸ Ideal.span {p}) := Ideal.Quotient.field _
69   have h := (operatorPrimaryQuotientEquiv D p hp).finrank_eq
70   simpa [intrinsicMultiplicity, fiberMultiplicity, Module.finrank_pi,
71     ← Nat.card_eq_fintype_card] using h
72 
73 /-- Any actual primary decomposition of the intrinsic component has the intrinsic count.
74 This also applies to decompositions not obtained by grouping a presentation of V. -/
75 theorem intrinsicMultiplicity_eq_card_of_component_decomposition
76     {ι : Type v} [Fintype ι] (T : Module.End k V) (p : k[X]) (hp : Irreducible p)
77     (q : ι → k[X]) (hq : ∀ i, Irreducible (q i)) (e : ι → ℕ) (he : ∀ i, 0 < e i)
78     (hlabel : ∀ i, Ideal.span {q i} = Ideal.span {p})
79     (f : primarySubmodule (Module.AEval' T) p ≃ₗ[k[X]]
80       ((i : ι) → k[X] ⧸ Ideal.span {q i ^ e i})) :
81     intrinsicMultiplicity T p = Fintype.card ι := by
82   classical
83   let : (Ideal.span {p}).IsMaximal := PrincipalIdealRing.isMaximal_of_irreducible hp
84   let : Field (k[X] ⧸ Ideal.span {p}) := Ideal.Quotient.field _
85   have E := (scalarQuotientCongr p f).trans (primaryProductQuotientEquiv q hq e he p hp)
86   have h := E.finrank_eq
87   have hc : intrinsicMultiplicity T p =
88       Fintype.card {i : ι // Ideal.span {q i} = Ideal.span {p}} := by
89     simpa [intrinsicMultiplicity, Module.finrank_pi, ← Nat.card_eq_fintype_card] using h
90   exact hc.trans (Fintype.card_congr (Equiv.subtypeUnivEquiv hlabel))
91 
92 /-- Every individual fibre multiplicity, not merely its maximum, is presentation invariant. -/
93 theorem primary_fiber_presentation_invariant [FiniteDimensional k V]
94     {T : Module.End k V} (D E : PrimaryPresentation T) (p : k[X]) (hp : Irreducible p) :
95     fiberMultiplicity D.label (Ideal.span {p}) =
96       fiberMultiplicity E.label (Ideal.span {p}) :=
97   (intrinsicMultiplicity_eq_fiber D p hp).symm.trans
98     (intrinsicMultiplicity_eq_fiber E p hp)
99 
100 /-- A missing primary label contributes zero to the intrinsic quotient dimension. -/
101 theorem intrinsicMultiplicity_eq_zero_of_absent [FiniteDimensional k V]
102     {T : Module.End k V} (D : PrimaryPresentation T) (p : k[X]) (hp : Irreducible p)
103     (h : ∀ i, D.label i ≠ Ideal.span {p}) : intrinsicMultiplicity T p = 0 := by
104   classical
105   rw [intrinsicMultiplicity_eq_fiber D p hp]
106   let : IsEmpty {i : D.Index // D.label i = Ideal.span {p}} :=
107     ⟨fun i ↦ h i.val i.property⟩
108   simp [fiberMultiplicity]
109 
110 /-- The printed primary quotient formula for the canonical seed rank. -/
111 theorem operator_seedFinrank_eq_intrinsic_primary_max [FiniteDimensional k V]
112     {T : Module.End k V} (D : PrimaryPresentation T) :
113     seedFinrank (Komorebi.SingleOperatorGraph.operatorAlgebra T) V =
114       Finset.univ.sup (fun i : D.Index ↦ intrinsicMultiplicity T (D.prime i)) := by
115   rw [D.seedFinrank_eq]
116   unfold PrimaryPresentation.maxCount maxMultiplicity
117   congr 1
118   funext i
119   exact (intrinsicMultiplicity_eq_fiber D (D.prime i) (D.irreducible i)).symm
120 
121 
122 /-- Associated irreducibles define the same intrinsic multiplicity. -/
123 theorem intrinsicMultiplicity_eq_of_span_eq [FiniteDimensional k V]
124     (T : Module.End k V) (p q : k[X]) (hp : Irreducible p) (hq : Irreducible q)
125     (h : Ideal.span {p} = Ideal.span {q}) :
126     intrinsicMultiplicity T p = intrinsicMultiplicity T q := by
127   let D := chosenPrimaryPresentation T
128   rw [intrinsicMultiplicity_eq_fiber D p hp, intrinsicMultiplicity_eq_fiber D q hq, h]
129 
130 /-- Every intrinsic multiplicity is bounded by the canonical seed number. -/
131 theorem intrinsicMultiplicity_le_seedFinrank [FiniteDimensional k V]
132     (T : Module.End k V) (p : k[X]) (hp : Irreducible p) :
133     intrinsicMultiplicity T p ≤ seedFinrank (Komorebi.SingleOperatorGraph.operatorAlgebra T) V := by
134   classical
135   let D := chosenPrimaryPresentation T
136   by_cases h : ∃ i : D.Index, D.label i = Ideal.span {p}
137   · obtain ⟨i, hi⟩ := h
138     rw [intrinsicMultiplicity_eq_fiber D p hp, D.seedFinrank_eq, ← hi]
139     exact fiberMultiplicity_le_max D.label i
140   · rw [intrinsicMultiplicity_eq_zero_of_absent D p hp (by simpa using h)]
141     exact Nat.zero_le _
142 
143 /-- The exact set in the printed maximum: all monic irreducible polynomials. -/
144 def monicPrimaryMultiplicityValues (T : Module.End k V) : Set ℕ :=
145   {n | ∃ p : k[X], p.Monic ∧ Irreducible p ∧ intrinsicMultiplicity T p = n}
146 
147 /-- The zero-dimensional case also has a nonempty value set, containing the value at X. -/
148 theorem monicPrimaryMultiplicityValues_nonempty (T : Module.End k V) :
149     (monicPrimaryMultiplicityValues T).Nonempty :=
150   ⟨intrinsicMultiplicity T X, X, monic_X, irreducible_X, rfl⟩
151 
152 /-- The set of intrinsic primary dimensions is bounded; its supremum is a true finite maximum. -/
153 theorem monicPrimaryMultiplicityValues_bddAbove [FiniteDimensional k V] (T : Module.End k V) :
154     BddAbove (monicPrimaryMultiplicityValues T) := by
155   refine ⟨seedFinrank (Komorebi.SingleOperatorGraph.operatorAlgebra T) V, ?_⟩
156   rintro n ⟨p, _, hp, rfl⟩
157   exact intrinsicMultiplicity_le_seedFinrank T p hp
158 
159 /-- A presentation-free definition of the intrinsic maximum. -/
160 def intrinsicSeedMaximum (T : Module.End k V) : ℕ := sSup (monicPrimaryMultiplicityValues T)
161 
162 /-- The maximum is attained by a monic irreducible, including when every multiplicity is zero. -/
163 theorem intrinsicSeedMaximum_attained [FiniteDimensional k V] (T : Module.End k V) :
164     ∃ p : k[X], p.Monic ∧ Irreducible p ∧ intrinsicMultiplicity T p = intrinsicSeedMaximum T :=
165   Nat.sSup_mem (monicPrimaryMultiplicityValues_nonempty T)
166     (monicPrimaryMultiplicityValues_bddAbove T)
167 
168 /-- The complete printed maximum formula, with no supplied presentation or seed certificate. -/
169 theorem operator_seedFinrank_eq_intrinsicSeedMaximum [FiniteDimensional k V]
170     (T : Module.End k V) :
171     seedFinrank (Komorebi.SingleOperatorGraph.operatorAlgebra T) V = intrinsicSeedMaximum T := by
172   classical
173   let D := chosenPrimaryPresentation T
174   apply le_antisymm
175   · rw [operator_seedFinrank_eq_intrinsic_primary_max D]
176     apply Finset.sup_le
177     intro i _
178     let p := normalize (D.prime i)
179     have hp : Irreducible p := (associated_normalize (D.prime i)).irreducible (D.irreducible i)
180     have hm : p.Monic := Polynomial.monic_normalize (D.irreducible i).ne_zero
181     have heq : intrinsicMultiplicity T p = intrinsicMultiplicity T (D.prime i) :=
182       intrinsicMultiplicity_eq_of_span_eq T p (D.prime i) hp (D.irreducible i)
183         (Ideal.span_singleton_eq_span_singleton.mpr (normalize_associated (D.prime i)))
184     rw [← heq]
185     exact le_csSup (monicPrimaryMultiplicityValues_bddAbove T) ⟨p, hm, hp, rfl⟩
186   · exact csSup_le (monicPrimaryMultiplicityValues_nonempty T)
187       (fun n ⟨p, _, hp, hn⟩ ↦ hn ▸ intrinsicMultiplicity_le_seedFinrank T p hp)
188 
189 /-- Cardinal-valued seed rank equals the same exact intrinsic maximum. -/
190 theorem operator_seedRank_eq_intrinsicSeedMaximum [FiniteDimensional k V]
191     (T : Module.End k V) :
192     seedRank (Komorebi.SingleOperatorGraph.operatorAlgebra T) V =
193       (intrinsicSeedMaximum T : Cardinal) := by
194   let D := chosenPrimaryPresentation T
195   rw [D.seedRank_eq, ← D.seedFinrank_eq, operator_seedFinrank_eq_intrinsicSeedMaximum T]
196 
197 end Komorebi.PaperICompletion4.OperatorIntrinsicFormula

Back to source controls