InvariantFactorCount.lean

1 import PaperICompletion3.OperatorPrimaryAPI
2 
3 /-!
4 # Exact invariant-factor count
5 
6 The publication's corollary starts with an actual rational canonical
7 presentation. From that presentation and the divisibility chain, the seed
8 count is proved, not accepted as a certificate. Existence of an ordered
9 invariant-factor presentation is not asserted by this module.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 
14 namespace Komorebi.PaperICompletion3.InvariantFactorCount
15 
16 open Polynomial
17 open Komorebi.SeedRankBasics
18 open Komorebi.PaperICompletion3.PrimarySeedFormula
19 
20 universe u v
21 variable {k : Type u} [Field k]
22 
23 /-- A chain of nonconstant invariant factors requires exactly one seed per factor.
24 The empty chain has minimum zero. -/
25 theorem invariantFactorProduct_seedNumber_isLeast {r : ℕ}
26     (f : Fin r → k[X]) (hf : ∀ i, 0 < (f i).natDegree)
27     (hchain : ∀ i j, i ≤ j → f i ∣ f j) :
28     IsLeast {n : ℕ | ∃ s : Fin n → ((i : Fin r) → k[X] ⧸ Ideal.span {f i}),
29       FamilyGenerates k[X] ((i : Fin r) → k[X] ⧸ Ideal.span {f i}) s} r := by
30   classical
31   constructor
32   · refine ⟨coloredSeeds (fun i ↦ Ideal.span {f i}) (fun i ↦ i), ?_⟩
33     apply coloredSeeds_generate
34     intro i j hne heq
35     exact (hne heq).elim
36   · rintro n ⟨s, hs⟩
37     by_cases hr : r = 0
38     · subst r
39       exact Nat.zero_le _
40     · let first : Fin r := ⟨0, Nat.pos_of_ne_zero hr⟩
41       obtain ⟨p, hp, hpf⟩ := Polynomial.exists_irreducible_of_natDegree_pos (hf first)
42       let P : Ideal k[X] := Ideal.span {p}
43       let : P.IsMaximal := PrincipalIdealRing.isMaximal_of_irreducible hp
44       have hIP : ∀ i : Fin r, Ideal.span {f i} ≤ P := by
45         intro i
46         exact Ideal.span_singleton_le_span_singleton.mpr
47           (hpf.trans (hchain first i (Fin.mk_le_mk.mpr (Nat.zero_le _))))
48       have h := fiberMultiplicity_le_of_generates (fun i ↦ Ideal.span {f i})
49         (fun _ : Fin r ↦ P) hIP P s hs
50       simpa [fiberMultiplicity] using h
51 
52 /-- The printed invariant-factor corollary, for the actual polynomial module.
53 Only the displayed decomposition and nonconstant divisibility chain are inputs. -/
54 theorem invariantFactor_operator_seedRanks {V : Type v} [AddCommGroup V] [Module k V]
55     (T : Module.End k V) {r : ℕ}
56     (f : Fin r → k[X]) (hf : ∀ i, 0 < (f i).natDegree)
57     (hchain : ∀ i j, i ≤ j → f i ∣ f j)
58     (E : Module.AEval' T ≃ₗ[k[X]] ((i : Fin r) → k[X] ⧸ Ideal.span {f i})) :
59     IsLeast {n : ℕ | Komorebi.SingleOperatorGraph.SeedNumberLE T n} r ∧
60       seedFinrank (Komorebi.SingleOperatorGraph.operatorAlgebra T) V = r ∧
61       seedRank (Komorebi.SingleOperatorGraph.operatorAlgebra T) V = (r : Cardinal) := by
62   have h := operator_seedNumber_isLeast_of_polynomialModule T r
63     (seedNumber_isLeast_linearEquiv E r (invariantFactorProduct_seedNumber_isLeast f hf hchain))
64   exact ⟨h,
65     Komorebi.SingleOperatorGraph.operatorAlgebra_seedFinrank_eq_of_seedNumber_isLeast T r h,
66     Komorebi.SingleOperatorGraph.operatorAlgebra_seedRank_eq_of_seedNumber_isLeast T r h⟩
67 
68 end Komorebi.PaperICompletion3.InvariantFactorCount

Back to source controls