PrimarySeedFormula.lean

1 import PaperICompletion.CyclicClassification
2 import Mathlib.Algebra.Polynomial.Module.FiniteDimensional
3 import Mathlib.RingTheory.Ideal.Quotient.Operations
4 
5 /-!
6 # General polynomial-module seed formula: primary products
7 
8 The actual polynomial module is decomposed by the proved PID structure theorem.
9 Chinese remainder coefficients construct shared generators across coprime blocks.
10 Residue fields, rather than base-field eigenvalues, supply the lower bounds.
11 -/
12 set_option autoImplicit false
13 noncomputable section
14 
15 namespace Komorebi.PaperICompletion3.PrimarySeedFormula
16 
17 open Polynomial
18 open Komorebi.SeedRankBasics
19 
20 universe u v w
21 
22 /-- The actual polynomial module of a finite-dimensional operator is torsion. -/
23 theorem operatorModule_isTorsion {k : Type u} [Field k]
24     {V : Type v} [AddCommGroup V] [Module k V] [FiniteDimensional k V]
25     (T : Module.End k V) : Module.IsTorsion k[X] (Module.AEval' T) :=
26   Module.AEval.isTorsion_of_finiteDimensional k V T
27 
28 /-- Primary blocks are constructed from the operator, not supplied by the caller.
29 Exponent-zero summands are allowed by the upstream normal form and are zero modules. -/
30 theorem exists_primaryProduct_equiv {k : Type u} [Field k]
31     {V : Type v} [AddCommGroup V] [Module k V] [FiniteDimensional k V]
32     (T : Module.End k V) :
33     ∃ (ι : Type u) (_ : Fintype ι) (p : ι → k[X])
34       (_ : ∀ i, Irreducible (p i)) (e : ι → ℕ),
35       Nonempty (Module.AEval' T ≃ₗ[k[X]]
36         ((i : ι) → k[X] ⧸ Ideal.span {p i ^ e i})) := by
37   obtain ⟨ι, hι, p, hp, e, ⟨f⟩⟩ := Module.equiv_directSum_of_isTorsion
38     (operatorModule_isTorsion T)
39   exact ⟨ι, hι, p, hp, e, ⟨f.trans DFinsupp.linearEquivFunOnFintype⟩⟩
40 
41 section ResidueLowerBound
42 variable {R : Type u} [CommRing R]
43 variable {M : Type v} [AddCommGroup M] [Module R M]
44 variable {K : Type w} [Field K] [Algebra R K]
45 variable {Y : Type*} [AddCommGroup Y] [Module K Y] [Module R Y]
46   [IsScalarTower R K Y]
47 
48 /-- Every surjective residue-field factor bounds the number of module generators.
49 The residue extension may have degree greater than one over the original base field. -/
50 theorem residue_finrank_le_card_of_generates {ι : Type*} [Fintype ι]
51     (f : M →ₗ[R] Y) (hf : Function.Surjective f)
52     (s : ι → M) (hs : FamilyGenerates R M s) :
53     Module.finrank K Y ≤ Fintype.card ι := by
54   have hspanR : Submodule.span R (Set.range (fun i ↦ f (s i))) = ⊤ := by
55     rw [show Set.range (fun i ↦ f (s i)) = f '' Set.range s from Set.range_comp f s,
56       ← Submodule.map_span, hs, Submodule.map_top, LinearMap.range_eq_top.mpr hf]
57   have hspanK : Submodule.span K (Set.range (fun i ↦ f (s i))) = ⊤ := by
58     apply top_unique
59     intro y _
60     have hy : y ∈ Submodule.span R (Set.range (fun i ↦ f (s i))) := by rw [hspanR]; trivial
61     exact Submodule.span_le_restrictScalars R K _ hy
62   exact finrank_le_of_span_eq_top (R := K) hspanK
63 end ResidueLowerBound
64 
65 section ChineseRemainderGenerators
66 variable {R : Type u} [CommRing R]
67 variable {ι : Type v} [Fintype ι]
68 
69 /-- One vector per color, supported exactly on blocks of that color. -/
70 def coloredSeeds (I : ι → Ideal R) {r : ℕ} (color : ι → Fin r)
71     (j : Fin r) : (i : ι) → R ⧸ I i :=
72   fun i ↦ if color i = j then 1 else 0
73 
74 /-- Blocks sharing a color may share one seed exactly because their
75 quotient ideals are pairwise coprime. The CRT coefficients are constructed. -/
76 theorem coloredSeeds_generate (I : ι → Ideal R) {r : ℕ} (color : ι → Fin r)
77     (hcoprime : ∀ i j, i ≠ j → color i = color j → IsCoprime (I i) (I j)) :
78     FamilyGenerates R ((i : ι) → R ⧸ I i) (coloredSeeds I color) := by
79   classical
80   apply top_unique
81   intro x _
82   have hex : ∀ j : Fin r, ∃ a : R,
83       ∀ i : {i : ι // color i = j}, Ideal.Quotient.mk (I i) a = x i := by
84     intro j
85     apply Ideal.pi_quotient_surjective
86     intro i i' hne
87     exact hcoprime i i' (fun h ↦ hne (Subtype.ext h)) (i.property.trans i'.property.symm)
88   choose a ha using hex
89   have hsum : ∑ j : Fin r, a j • coloredSeeds I color j = x := by
90     funext i
91     simp only [Finset.sum_apply, Pi.smul_apply, coloredSeeds]
92     simp only [smul_ite, smul_zero]
93     simpa [Algebra.smul_def] using ha (color i) ⟨i, rfl⟩
94   rw [← hsum]
95   exact Submodule.sum_mem _ fun j _ ↦ Submodule.smul_mem _ _
96     (Submodule.subset_span (Set.mem_range_self j))
97 end ChineseRemainderGenerators
98 
99 section FiberColors
100 variable {ι : Type u} [Fintype ι] {Λ : Type v}
101 
102 /-- Number of blocks carrying a specified primary label. -/
103 def fiberMultiplicity (label : ι → Λ) (a : Λ) : ℕ :=
104   by
105   classical
106   exact Fintype.card {i : ι // label i = a}
107 
108 /-- Maximum fiber multiplicity, including the empty family with maximum zero. -/
109 def maxMultiplicity (label : ι → Λ) : ℕ :=
110   Finset.univ.sup fun i ↦ fiberMultiplicity label (label i)
111 
112 theorem fiberMultiplicity_le_max (label : ι → Λ) (i : ι) :
113     fiberMultiplicity label (label i) ≤ maxMultiplicity label :=
114   Finset.le_sup (f := fun i ↦ fiberMultiplicity label (label i)) (Finset.mem_univ i)
115 
116 /-- Rank a block within its own primary fiber. -/
117 def fiberColor (label : ι → Λ) (i : ι) : Fin (maxMultiplicity label) := by
118   classical
119   exact ⟨(Fintype.equivFin {j : ι // label j = label i}) ⟨i, rfl⟩,
120     lt_of_lt_of_le (Fin.isLt _) (fiberMultiplicity_le_max label i)⟩
121 
122 /-- Distinct blocks in the same primary fiber receive distinct colors. -/
123 theorem fiberColor_injective_on_fiber (label : ι → Λ) {i j : ι}
124     (hlabel : label i = label j) (hcolor : fiberColor label i = fiberColor label j) : i = j := by
125   classical
126   have hval := congrArg Fin.val hcolor
127   simp only [fiberColor] at hval
128   have transport (a b : Λ) (h : a = b) (z : ι) (hz : label z = a) :
129       ((Fintype.equivFin {x : ι // label x = a}) ⟨z, hz⟩).val =
130       ((Fintype.equivFin {x : ι // label x = b}) ⟨z, hz.trans h⟩).val := by
131     subst b
132     rfl
133   have hcolor' :
134       (Fintype.equivFin {z : ι // label z = label i}) ⟨i, rfl⟩ =
135       (Fintype.equivFin {z : ι // label z = label i}) ⟨j, hlabel.symm⟩ := by
136     apply Fin.ext
137     exact hval.trans (transport (label j) (label i) hlabel.symm j rfl)
138   exact congrArg Subtype.val ((Fintype.equivFin _).injective hcolor')
139 end FiberColors
140 
141 section QuotientFibers
142 variable {R : Type u} [CommRing R]
143 variable {ι : Type v} [Fintype ι]
144 
145 /-- The literal quotient map onto all blocks with a selected residue ideal. -/
146 def residueFiberMap (I P : ι → Ideal R) (hIP : ∀ i, I i ≤ P i) (a : Ideal R) :
147     ((i : ι) → R ⧸ I i) →ₗ[R] ({i : ι // P i = a} → R ⧸ a) :=
148   LinearMap.pi fun i ↦
149     (Ideal.Quotient.factorₐ R ((hIP i).trans_eq i.property)).toLinearMap.comp
150       (LinearMap.proj i.val)
151 
152 omit [Fintype ι] in
153 /-- Every residue-fiber map is onto, including empty fibers. -/
154 theorem residueFiberMap_surjective (I P : ι → Ideal R)
155     (hIP : ∀ i, I i ≤ P i) (a : Ideal R) :
156     Function.Surjective (residueFiberMap I P hIP a) := by
157   classical
158   intro y
159   have hex : ∀ i : {i : ι // P i = a}, ∃ x : R ⧸ I i,
160       Ideal.Quotient.factor ((hIP i).trans_eq i.property) x = y i := by
161     intro i
162     exact Ideal.Quotient.factor_surjective _ (y i)
163   choose x hx using hex
164   refine ⟨fun i ↦ if h : P i = a then x ⟨i, h⟩ else 0, ?_⟩
165   ext i
166   simpa [residueFiberMap, i.property] using hx i
167 
168 /-- A primary residue fiber requires at least its own number of generators. -/
169 theorem fiberMultiplicity_le_of_generates (I P : ι → Ideal R)
170     (hIP : ∀ i, I i ≤ P i) (a : Ideal R) [a.IsMaximal]
171     {κ : Type*} [Fintype κ] (s : κ → ((i : ι) → R ⧸ I i))
172     (hs : FamilyGenerates R ((i : ι) → R ⧸ I i) s) :
173     fiberMultiplicity P a ≤ Fintype.card κ := by
174   classical
175   let : Field (R ⧸ a) := Ideal.Quotient.field a
176   have h := residue_finrank_le_card_of_generates (K := R ⧸ a)
177     (residueFiberMap I P hIP a) (residueFiberMap_surjective I P hIP a) s hs
178   simpa [fiberMultiplicity, Module.finrank_pi, ← Nat.card_eq_fintype_card] using h
179 
180 /-- Exact generator count for finite products of primary quotients.
181 All residue lower bounds and the simultaneous CRT upper bound are proved here. -/
182 theorem primaryProduct_seedNumber_isLeast (I P : ι → Ideal R)
183     (hIP : ∀ i, I i ≤ P i) (hmax : ∀ i, (P i).IsMaximal)
184     (hcoprime : ∀ i j, P i ≠ P j → IsCoprime (I i) (I j)) :
185     IsLeast {r : ℕ | ∃ s : Fin r → ((i : ι) → R ⧸ I i),
186       FamilyGenerates R ((i : ι) → R ⧸ I i) s} (maxMultiplicity P) := by
187   classical
188   constructor
189   · refine ⟨coloredSeeds I (fiberColor P), coloredSeeds_generate I (fiberColor P) ?_⟩
190     intro i j hne hc
191     exact hcoprime i j (fun he ↦ hne (fiberColor_injective_on_fiber P he hc))
192   · rintro r ⟨s, hs⟩
193     apply Finset.sup_le
194     intro i _
195     let : (P i).IsMaximal := hmax i
196     simpa using fiberMultiplicity_le_of_generates I P hIP (P i) s hs
197 end QuotientFibers
198 
199 section PrimePowers
200 variable {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
201 variable {ι : Type v} [Fintype ι]
202 
203 /-- Distinct irreducible principal ideals have coprime powers. -/
204 theorem coprime_primePower_ideals (p q : R) (hp : Irreducible p) (hq : Irreducible q)
205     (hneq : Ideal.span {p} ≠ Ideal.span {q}) (m n : ℕ) :
206     IsCoprime (Ideal.span {p ^ m}) (Ideal.span {q ^ n}) := by
207   apply (Ideal.isCoprime_span_singleton_iff _ _).mpr
208   apply IsCoprime.pow
209   apply hp.coprime_iff_not_dvd.mpr
210   intro hdiv
211   exact hneq (Ideal.span_singleton_eq_span_singleton.mpr
212     ((hp.associated_of_dvd hq hdiv)))
213 
214 /-- Positive exponent prime-power quotients have the exact maximum-primary-fiber seed number. -/
215 theorem primePowerProduct_seedNumber_isLeast (p : ι → R) (hp : ∀ i, Irreducible (p i))
216     (e : ι → ℕ) (he : ∀ i, 0 < e i) :
217     IsLeast {r : ℕ | ∃ s : Fin r → ((i : ι) → R ⧸ Ideal.span {p i ^ e i}),
218       FamilyGenerates R ((i : ι) → R ⧸ Ideal.span {p i ^ e i}) s}
219       (maxMultiplicity fun i ↦ Ideal.span {p i}) := by
220   apply primaryProduct_seedNumber_isLeast
221     (fun i ↦ Ideal.span {p i ^ e i}) (fun i ↦ Ideal.span {p i})
222   · intro i
223     exact Ideal.span_singleton_le_span_singleton.mpr (dvd_pow_self _ (Nat.ne_of_gt (he i)))
224   · intro i
225     exact PrincipalIdealRing.isMaximal_of_irreducible (hp i)
226   · intro i j hne
227     exact coprime_primePower_ideals (p i) (p j) (hp i) (hp j) hne (e i) (e j)
228 end PrimePowers
229 
230 section RemoveZeroBlocks
231 variable {R : Type u} [CommRing R]
232 variable {ι : Type v} [Fintype ι]
233 
234 /-- Exponent-zero blocks are zero modules, not generators to be counted. -/
235 theorem primePower_quotient_subsingleton_of_exponent_zero (p : R) {n : ℕ} (hn : n = 0) :
236     Subsingleton (R ⧸ Ideal.span {p ^ n}) := by
237   subst n
238   simpa only [pow_zero, Ideal.span_singleton_one] using
239     (inferInstance : Subsingleton (R ⧸ (⊤ : Ideal R)))
240 
241 /-- Discard exactly the exponent-zero factors of the upstream primary normal form. -/
242 def dropZeroExponentEquiv (p : ι → R) (e : ι → ℕ) :
243     ((i : ι) → R ⧸ Ideal.span {p i ^ e i}) ≃ₗ[R]
244       ((i : {i : ι // e i ≠ 0}) → R ⧸ Ideal.span {p i ^ e i}) := by
245   classical
246   let f : ((i : ι) → R ⧸ Ideal.span {p i ^ e i}) →ₗ[R]
247       ((i : {i : ι // e i ≠ 0}) → R ⧸ Ideal.span {p i ^ e i}) :=
248     LinearMap.pi fun i ↦ LinearMap.proj i.val
249   apply LinearEquiv.ofBijective f
250   constructor
251   · intro x y hxy
252     ext i
253     by_cases hi : e i = 0
254     · let : Subsingleton (R ⧸ Ideal.span {p i ^ e i}) :=
255         primePower_quotient_subsingleton_of_exponent_zero (p i) hi
256       exact Subsingleton.elim _ _
257     · exact congrFun hxy ⟨i, hi⟩
258   · intro y
259     refine ⟨fun i ↦ if h : e i ≠ 0 then y ⟨i, h⟩ else 0, ?_⟩
260     ext i
261     simp [f, i.property]
262 end RemoveZeroBlocks
263 
264 /-- Every operator has a constructed positive-exponent primary product.
265 Neither a splitting field nor diagonalizability is assumed. -/
266 theorem exists_positive_primaryProduct_equiv {k : Type u} [Field k]
267     {V : Type v} [AddCommGroup V] [Module k V] [FiniteDimensional k V]
268     (T : Module.End k V) :
269     ∃ (ι : Type u) (_ : Fintype ι) (p : ι → k[X])
270       (_ : ∀ i, Irreducible (p i)) (e : ι → ℕ) (_ : ∀ i, 0 < e i),
271       Nonempty (Module.AEval' T ≃ₗ[k[X]]
272         ((i : ι) → k[X] ⧸ Ideal.span {p i ^ e i})) := by
273   classical
274   obtain ⟨ι, _, p, hp, e, ⟨f⟩⟩ := exists_primaryProduct_equiv T
275   exact ⟨{i : ι // e i ≠ 0}, inferInstance, fun i ↦ p i, fun i ↦ hp i,
276     fun i ↦ e i, fun i ↦ Nat.pos_of_ne_zero i.property,
277     ⟨f.trans (dropZeroExponentEquiv p e)⟩⟩
278 
279 section GeneratorTransport
280 variable {R : Type u} [Semiring R]
281 variable {M : Type v} [AddCommGroup M] [Module R M]
282 variable {N : Type w} [AddCommGroup N] [Module R N]
283 
284 /-- Module generators transport along an actual linear equivalence. -/
285 theorem familyGenerates_linearEquiv_iff {ι : Type*} (f : M ≃ₗ[R] N) (s : ι → M) :
286     FamilyGenerates R N (fun i ↦ f (s i)) ↔ FamilyGenerates R M s := by
287   change Submodule.span R (Set.range (fun i ↦ f (s i))) = ⊤ ↔
288     Submodule.span R (Set.range s) = ⊤
289   rw [show Set.range (fun i ↦ f (s i)) = f '' Set.range s from Set.range_comp f s]
290   change Submodule.span R (f.toLinearMap '' Set.range s) = ⊤ ↔ _
291   rw [← Submodule.map_span f.toLinearMap]
292   exact Submodule.map_eq_top_iff
293 
294 /-- The exact finite generator minimum is invariant under linear equivalence. -/
295 theorem seedNumber_isLeast_linearEquiv (f : M ≃ₗ[R] N) (r : ℕ)
296     (h : IsLeast {n : ℕ | ∃ s : Fin n → N, FamilyGenerates R N s} r) :
297     IsLeast {n : ℕ | ∃ s : Fin n → M, FamilyGenerates R M s} r := by
298   constructor
299   · obtain ⟨s, hs⟩ := h.1
300     exact ⟨fun i ↦ f.symm (s i), (familyGenerates_linearEquiv_iff f.symm s).mpr hs⟩
301   · rintro n ⟨s, hs⟩
302     exact h.2 ⟨fun i ↦ f (s i), (familyGenerates_linearEquiv_iff f s).mpr hs⟩
303 end GeneratorTransport
304 
305 section PolynomialOrbitBridge
306 variable {k : Type u} [Field k]
307 variable {V : Type v} [AddCommGroup V] [Module k V]
308 
309 /-- The polynomial submodule span is the paper's literal span of polynomial orbits. -/
310 theorem familyGenerates_iff_polynomialModule {ι : Type*}
311     (T : Module.End k V) (s : ι → V) :
312     Komorebi.SingleOperatorGraph.FamilyGenerates T s ↔
313       FamilyGenerates k[X] (Module.AEval' T) (fun i ↦ Module.AEval'.of T (s i)) := by
314   constructor
315   · intro hs
316     apply top_unique
317     intro y _
318     have hx : (Module.AEval'.of T).symm y ∈
319         Submodule.span k (Set.range (Komorebi.SingleOperatorGraph.orbitFamily T s)) := by
320       rw [hs]; trivial
321     have h : ∀ x ∈ Submodule.span k (Set.range (Komorebi.SingleOperatorGraph.orbitFamily T s)),
322         Module.AEval'.of T x ∈ Submodule.span k[X] (Set.range fun i ↦ Module.AEval'.of T (s i)) := by
323       intro x hx
324       refine Submodule.span_induction ?_ ?_ ?_ ?_ hx
325       · rintro z ⟨⟨i, p⟩, rfl⟩
326         exact Submodule.smul_mem _ p (Submodule.subset_span (Set.mem_range_self i))
327       · simp
328       · intro x y _ _ hx hy
329         simpa using Submodule.add_mem _ hx hy
330       · intro a x _ hx
331         simpa using Submodule.smul_mem
332           ((Submodule.span k[X] (Set.range fun i ↦ Module.AEval'.of T (s i))).restrictScalars k) a hx
333     simpa using h _ hx
334   · intro hs
335     apply top_unique
336     intro x _
337     have hx : Module.AEval'.of T x ∈
338         Submodule.span k[X] (Set.range fun i ↦ Module.AEval'.of T (s i)) := by
339       rw [hs]; trivial
340     have h : ∀ y ∈ Submodule.span k[X] (Set.range fun i ↦ Module.AEval'.of T (s i)),
341         (Module.AEval'.of T).symm y ∈
342           Submodule.span k (Set.range (Komorebi.SingleOperatorGraph.orbitFamily T s)) := by
343       intro y hy
344       refine Submodule.span_induction ?_ ?_ ?_ ?_ hy
345       · rintro y ⟨i, rfl⟩
346         simpa [Komorebi.SingleOperatorGraph.orbitFamily] using
347           (Submodule.subset_span (R := k)
348             (Set.mem_range_self (f := Komorebi.SingleOperatorGraph.orbitFamily T s) (i, 1)))
349       · simp
350       · intro x y _ _ hx hy
351         simpa using Submodule.add_mem _ hx hy
352       · intro p y _ hy
353         exact Komorebi.SingleOperatorGraph.aeval_mem_span_orbit_of_mem T s p hy
354     simpa using h _ hx
355 
356 /-- The module-theoretic minimum equals the existing polynomial-orbit seed minimum. -/
357 theorem operator_seedNumber_isLeast_of_polynomialModule (T : Module.End k V) (r : ℕ)
358     (h : IsLeast {n : ℕ | ∃ s : Fin n → Module.AEval' T,
359       FamilyGenerates k[X] (Module.AEval' T) s} r) :
360     IsLeast {n : ℕ | Komorebi.SingleOperatorGraph.SeedNumberLE T n} r := by
361   constructor
362   · obtain ⟨s, hs⟩ := h.1
363     refine ⟨fun i ↦ (Module.AEval'.of T).symm (s i), ?_⟩
364     apply (familyGenerates_iff_polynomialModule T _).mpr
365     simpa using hs
366   · rintro n ⟨s, hs⟩
367     exact h.2 ⟨fun i ↦ Module.AEval'.of T (s i),
368       (familyGenerates_iff_polynomialModule T s).mp hs⟩
369 end PolynomialOrbitBridge
370 
371 /-- Constructive-in-theorem general primary formula for an arbitrary finite-dimensional
372 operator. All primary data, residue quotients and CRT generators are produced internally. -/
373 theorem exists_operator_primary_seed_formula {k : Type u} [Field k]
374     {V : Type v} [AddCommGroup V] [Module k V] [FiniteDimensional k V]
375     (T : Module.End k V) :
376     ∃ (ι : Type u) (_ : Fintype ι) (p : ι → k[X])
377       (_ : ∀ i, Irreducible (p i)) (e : ι → ℕ) (_ : ∀ i, 0 < e i)
378       (_f : Module.AEval' T ≃ₗ[k[X]] ((i : ι) → k[X] ⧸ Ideal.span {p i ^ e i})),
379       IsLeast {r : ℕ | Komorebi.SingleOperatorGraph.SeedNumberLE T r}
380         (maxMultiplicity fun i ↦ Ideal.span {p i}) ∧
381       seedFinrank (Komorebi.SingleOperatorGraph.operatorAlgebra T) V =
382         maxMultiplicity (fun i ↦ Ideal.span {p i}) ∧
383       seedRank (Komorebi.SingleOperatorGraph.operatorAlgebra T) V =
384         (maxMultiplicity (fun i ↦ Ideal.span {p i}) : Cardinal) := by
385   obtain ⟨ι, hι, p, hp, e, he, ⟨f⟩⟩ := exists_positive_primaryProduct_equiv T
386   have hmodel := primePowerProduct_seedNumber_isLeast p hp e he
387   have hmodule := seedNumber_isLeast_linearEquiv f _ hmodel
388   have h := operator_seedNumber_isLeast_of_polynomialModule T _ hmodule
389   exact ⟨ι, hι, p, hp, e, he, f, h,
390     Komorebi.SingleOperatorGraph.operatorAlgebra_seedFinrank_eq_of_seedNumber_isLeast T _ h,
391     Komorebi.SingleOperatorGraph.operatorAlgebra_seedRank_eq_of_seedNumber_isLeast T _ h⟩
392 
393 end Komorebi.PaperICompletion3.PrimarySeedFormula

Back to source controls