OperatorPrimaryAPI.lean

1 import PaperICompletion3.PrimarySeedFormula
2 
3 /-!
4 # Public operator-primary API
5 
6 A presentation contains an actual polynomial-module equivalence. A proved PID
7 construction produces such a presentation for every finite-dimensional operator.
8 The minimum is independent of the chosen presentation. No eigenbasis, supplied
9 seed-number equality, or polynomial cyclicity bridge is an input.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 
14 namespace Komorebi.PaperICompletion3.OperatorPrimaryAPI
15 
16 open Polynomial
17 open Komorebi.PaperICompletion3.PrimarySeedFormula
18 open Komorebi.SeedRankBasics
19 
20 universe u v
21 variable {k : Type u} [Field k]
22 variable {V : Type v} [AddCommGroup V] [Module k V]
23 
24 /-- A positive-exponent primary presentation of the actual polynomial action. -/
25 structure PrimaryPresentation (T : Module.End k V) where
26   Index : Type u
27   indexFintype : Fintype Index
28   prime : Index → k[X]
29   irreducible : ∀ i, Irreducible (prime i)
30   exponent : Index → ℕ
31   positive : ∀ i, 0 < exponent i
32   equiv : Module.AEval' T ≃ₗ[k[X]] ((i : Index) → k[X] ⧸ Ideal.span {prime i ^ exponent i})
33 
34 attribute [instance] PrimaryPresentation.indexFintype
35 
36 /-- Existence is proved from finite-dimensionality, not assumed. -/
37 theorem primaryPresentation_nonempty [FiniteDimensional k V] (T : Module.End k V) :
38     Nonempty (PrimaryPresentation T) := by
39   obtain ⟨ι, hι, p, hp, e, he, ⟨f⟩⟩ := exists_positive_primaryProduct_equiv T
40   exact ⟨⟨ι, hι, p, hp, e, he, f⟩⟩
41 
42 /-- A mathematically chosen presentation. This is not an executable normal-form algorithm. -/
43 def chosenPrimaryPresentation [FiniteDimensional k V] (T : Module.End k V) :
44     PrimaryPresentation T := Classical.choice (primaryPresentation_nonempty T)
45 
46 /-- Labels are principal ideals, so associated irreducibles are counted together. -/
47 def PrimaryPresentation.label {T : Module.End k V} (D : PrimaryPresentation T) :
48     D.Index → Ideal k[X] := fun i ↦ Ideal.span {D.prime i}
49 
50 /-- Maximum number of positive primary blocks carrying the same irreducible ideal. -/
51 def PrimaryPresentation.maxCount {T : Module.End k V} (D : PrimaryPresentation T) : ℕ :=
52   maxMultiplicity D.label
53 
54 /-- Exact least generator number for any actual primary presentation. -/
55 theorem PrimaryPresentation.seedNumber_isLeast {T : Module.End k V} (D : PrimaryPresentation T) :
56     IsLeast {r : ℕ | Komorebi.SingleOperatorGraph.SeedNumberLE T r} D.maxCount := by
57   exact operator_seedNumber_isLeast_of_polynomialModule T _
58     (seedNumber_isLeast_linearEquiv D.equiv _
59       (primePowerProduct_seedNumber_isLeast D.prime D.irreducible D.exponent D.positive))
60 
61 /-- The presentation formula is the canonical natural-valued seed rank. -/
62 theorem PrimaryPresentation.seedFinrank_eq {T : Module.End k V} (D : PrimaryPresentation T) :
63     seedFinrank (Komorebi.SingleOperatorGraph.operatorAlgebra T) V = D.maxCount :=
64   Komorebi.SingleOperatorGraph.operatorAlgebra_seedFinrank_eq_of_seedNumber_isLeast T _
65     D.seedNumber_isLeast
66 
67 /-- The presentation formula is also the canonical cardinal-valued seed rank. -/
68 theorem PrimaryPresentation.seedRank_eq {T : Module.End k V} (D : PrimaryPresentation T) :
69     seedRank (Komorebi.SingleOperatorGraph.operatorAlgebra T) V = (D.maxCount : Cardinal) :=
70   Komorebi.SingleOperatorGraph.operatorAlgebra_seedRank_eq_of_seedNumber_isLeast T _
71     D.seedNumber_isLeast
72 
73 /-- The maximum is independent of every choice made in the PID presentation. -/
74 theorem PrimaryPresentation.maxCount_eq {T : Module.End k V}
75     (D E : PrimaryPresentation T) : D.maxCount = E.maxCount :=
76   D.seedFinrank_eq.symm.trans E.seedFinrank_eq
77 
78 /-- Operator-derived primary generator count. -/
79 def primaryGeneratorCount [FiniteDimensional k V] (T : Module.End k V) : ℕ :=
80   (chosenPrimaryPresentation T).maxCount
81 
82 /-- No supplied decomposition or seed certificate occurs in this public theorem. -/
83 theorem operator_seedFinrank_eq_primaryGeneratorCount [FiniteDimensional k V]
84     (T : Module.End k V) :
85     seedFinrank (Komorebi.SingleOperatorGraph.operatorAlgebra T) V = primaryGeneratorCount T :=
86   (chosenPrimaryPresentation T).seedFinrank_eq
87 
88 /-- Cardinal form, including the zero-dimensional case. -/
89 theorem operator_seedRank_eq_primaryGeneratorCount [FiniteDimensional k V]
90     (T : Module.End k V) :
91     seedRank (Komorebi.SingleOperatorGraph.operatorAlgebra T) V =
92       (primaryGeneratorCount T : Cardinal) :=
93   (chosenPrimaryPresentation T).seedRank_eq
94 
95 /-- The chosen count is zero exactly for the zero module. -/
96 theorem primaryGeneratorCount_eq_zero_iff [FiniteDimensional k V] (T : Module.End k V) :
97     primaryGeneratorCount T = 0 ↔ Subsingleton V := by
98   rw [← Komorebi.SeedRankBasics.seedRank_eq_zero_iff
99     (Komorebi.SingleOperatorGraph.operatorAlgebra T) V,
100     operator_seedRank_eq_primaryGeneratorCount]
101   norm_cast
102 
103 /-- Any cyclic vector forbids repeated irreducible primary labels. -/
104 theorem PrimaryPresentation.label_injective_of_cyclic {T : Module.End k V}
105     (D : PrimaryPresentation T) (hT : Komorebi.SingleOperatorGraph.HasCyclicVector T) :
106     Function.Injective D.label := by
107   classical
108   obtain ⟨s, hs⟩ := hT
109   have hsModule := (familyGenerates_iff_polynomialModule T s).mp hs
110   have hsProduct := (familyGenerates_linearEquiv_iff D.equiv
111     (fun j ↦ Module.AEval'.of T (s j))).mpr hsModule
112   intro i j hij
113   let : (D.label i).IsMaximal := PrincipalIdealRing.isMaximal_of_irreducible (D.irreducible i)
114   have hIP : ∀ x, Ideal.span {D.prime x ^ D.exponent x} ≤ D.label x := by
115     intro x
116     exact Ideal.span_singleton_le_span_singleton.mpr
117       (dvd_pow_self _ (Nat.ne_of_gt (D.positive x)))
118   have hcard := fiberMultiplicity_le_of_generates
119     (fun x ↦ Ideal.span {D.prime x ^ D.exponent x}) D.label hIP (D.label i) _ hsProduct
120   have hsmall : Nat.card {x : D.Index // D.label x = D.label i} ≤ 1 := by
121     simpa [fiberMultiplicity, ← Nat.card_eq_fintype_card] using hcard
122   have hsub : Subsingleton {x : D.Index // D.label x = D.label i} :=
123     (Fintype.card_le_one_iff_subsingleton).mp (by simpa [Nat.card_eq_fintype_card] using hsmall)
124   exact congrArg Subtype.val (@Subsingleton.elim _ hsub ⟨i, rfl⟩ ⟨j, hij.symm⟩)
125 
126 /-- Distinct primary labels supply a cyclic vector by the literal CRT generator. -/
127 theorem PrimaryPresentation.cyclic_of_label_injective {T : Module.End k V}
128     (D : PrimaryPresentation T) (hD : Function.Injective D.label) :
129     Komorebi.SingleOperatorGraph.HasCyclicVector T := by
130   let I : D.Index → Ideal k[X] := fun i ↦ Ideal.span {D.prime i ^ D.exponent i}
131   let color : D.Index → Fin 1 := fun _ ↦ 0
132   have hgen := coloredSeeds_generate I color (by
133     intro i j hne _
134     exact coprime_primePower_ideals (D.prime i) (D.prime j) (D.irreducible i)
135       (D.irreducible j) (fun h ↦ hne (hD h)) (D.exponent i) (D.exponent j))
136   let s := fun j : Fin 1 ↦ D.equiv.symm (coloredSeeds I color j)
137   have hs : FamilyGenerates k[X] (Module.AEval' T) s :=
138     (familyGenerates_linearEquiv_iff D.equiv.symm (coloredSeeds I color)).mpr hgen
139   refine ⟨fun j ↦ (Module.AEval'.of T).symm (s j), ?_⟩
140   apply (familyGenerates_iff_polynomialModule T _).mpr
141   simpa using hs
142 
143 /-- The primary cyclic criterion is unconditional and includes the zero space. -/
144 theorem PrimaryPresentation.cyclic_iff_label_injective {T : Module.End k V}
145     (D : PrimaryPresentation T) :
146     Komorebi.SingleOperatorGraph.HasCyclicVector T ↔ Function.Injective D.label :=
147   ⟨D.label_injective_of_cyclic, D.cyclic_of_label_injective⟩
148 
149 /-- No repeated irreducible primary factor is equivalent to the polynomial cyclic criterion. -/
150 theorem PrimaryPresentation.label_injective_iff_minpoly_eq_charpoly
151     [FiniteDimensional k V] {T : Module.End k V} (D : PrimaryPresentation T) :
152     Function.Injective D.label ↔ minpoly k T = T.charpoly :=
153   D.cyclic_iff_label_injective.symm.trans
154     (Komorebi.PaperICompletion.CyclicClassification.hasCyclicVector_iff_minpoly_eq_charpoly T)
155 
156 end Komorebi.PaperICompletion3.OperatorPrimaryAPI

Back to source controls