PrimaryCyclicCriterion.lean

1 import PaperICompletion5
2 
3 /-! # Cyclicity of the literal intrinsic primary components
4 Principality is a one-element spanning statement on the actual polynomial
5 module. In particular it is not an assumed primary multiplicity certificate.
6 -/
7 set_option autoImplicit false
8 noncomputable section
9 open scoped Pointwise
10 namespace Komorebi.PaperICompletion6.PrimaryCyclicCriterion
11 open Polynomial
12 open Komorebi.SeedRankBasics
13 open Komorebi.PaperICompletion.CyclicClassification
14 open Komorebi.PaperICompletion3.PrimarySeedFormula
15 open Komorebi.PaperICompletion4.ResidueQuotient
16 open Komorebi.PaperICompletion4.IntrinsicPrimary
17 open Komorebi.PaperICompletion4.OperatorIntrinsicFormula
18 universe u v
19 variable {k : Type u} [Field k] {V : Type v} [AddCommGroup V] [Module k V]
20 
21 /-- The polynomial-module notion is exactly the original orbit notion of cyclicity. -/
22 theorem hasCyclicVector_iff_polynomialModule_cyclic (T : Module.End k V) :
23     Komorebi.SingleOperatorGraph.HasCyclicVector T ↔ Cyclic k[X] (Module.AEval' T) := by
24   rw [hasCyclicVector_iff_exists_surjective, cyclic_iff_exists_surjective_oneSeedMap]
25   constructor
26   · rintro ⟨x, hx⟩
27     exact ⟨Module.AEval'.of T x, hx⟩
28   · rintro ⟨x, hx⟩
29     exact ⟨(Module.AEval'.of T).symm x, hx⟩
30 
31 /-- A submodule of a cyclic polynomial module is cyclic, by principality of its preimage. -/
32 theorem submodule_cyclic_of_hasCyclicVector (T : Module.End k V)
33     (hT : Komorebi.SingleOperatorGraph.HasCyclicVector T)
34     (P : Submodule k[X] (Module.AEval' T)) : Cyclic k[X] P := by
35   obtain ⟨x, hx⟩ := (hasCyclicVector_iff_exists_surjective T).mp hT
36   have hp : P.IsPrincipal := Submodule.IsPrincipal.of_comap (orbitMap T x) hx P
37   exact (cyclic_iff_top_isPrincipal k[X] P).mpr (Module.isPrincipal_submodule_iff.mpr hp)
38 
39 /-- The literal intrinsic primary components of a cyclic operator are cyclic. -/
40 theorem primary_cyclic_of_hasCyclicVector (T : Module.End k V)
41     (hT : Komorebi.SingleOperatorGraph.HasCyclicVector T) (p : k[X]) :
42     Cyclic k[X] (primarySubmodule (Module.AEval' T) p) :=
43   submodule_cyclic_of_hasCyclicVector T hT _
44 
45 /-- A cyclic primary component has intrinsic residue dimension at most one. -/
46 theorem intrinsicMultiplicity_le_one_of_primary_cyclic (T : Module.End k V)
47     (p : k[X]) (hp : Irreducible p)
48     (h : Cyclic k[X] (primarySubmodule (Module.AEval' T) p)) :
49     intrinsicMultiplicity T p ≤ 1 := by
50   classical
51   let : (Ideal.span {p}).IsMaximal := PrincipalIdealRing.isMaximal_of_irreducible hp
52   let : Field (k[X] ⧸ Ideal.span {p}) := Ideal.Quotient.field _
53   let P := primarySubmodule (Module.AEval' T) p
54   let Q : Submodule k[X] P := p • ⊤
55   obtain ⟨x, hx⟩ := h
56   have hs : FamilyGenerates k[X] P (fun _ : Fin 1 => x) := by
57     simpa [FamilyGenerates, Generates, Set.range_const] using hx
58   have hb := residue_finrank_le_card_of_generates (K := k[X] ⧸ Ideal.span {p})
59     Q.mkQ Q.mkQ_surjective (fun _ : Fin 1 => x) hs
60   simpa [intrinsicMultiplicity, P, Q] using hb
61 
62 /-- No nonzero-space cyclicity assertion is needed for a zero component. -/
63 theorem cyclic_of_subsingleton {R : Type*} [Semiring R]
64     {M : Type*} [AddCommMonoid M] [Module R M] [Subsingleton M] : Cyclic R M := by
65   refine ⟨0, ?_⟩
66   exact Subsingleton.elim _ _
67 
68 /-- The original operator is cyclic exactly when every nonzero intrinsic primary component is. -/
69 theorem hasCyclicVector_iff_nonzero_primary_cyclic [FiniteDimensional k V] [Nontrivial V]
70     (T : Module.End k V) :
71     Komorebi.SingleOperatorGraph.HasCyclicVector T ↔
72       ∀ p : k[X], Irreducible p →
73         Nontrivial (primarySubmodule (Module.AEval' T) p) →
74         Cyclic k[X] (primarySubmodule (Module.AEval' T) p) := by
75   constructor
76   · intro h p _ _
77     exact primary_cyclic_of_hasCyclicVector T h p
78   · intro h
79     have hb : ∀ p : k[X], Irreducible p → intrinsicMultiplicity T p ≤ 1 := by
80       intro p hp
81       apply intrinsicMultiplicity_le_one_of_primary_cyclic T p hp
82       cases subsingleton_or_nontrivial (primarySubmodule (Module.AEval' T) p) with
83       | inl hs => let := hs; exact cyclic_of_subsingleton
84       | inr hn => exact h p hp hn
85     have hm : intrinsicSeedMaximum T ≤ 1 := by
86       apply csSup_le (monicPrimaryMultiplicityValues_nonempty T)
87       rintro n ⟨p, _hp, hi, rfl⟩
88       exact hb p hi
89     have hz : intrinsicSeedMaximum T ≠ 0 := by
90       intro he
91       have hr : seedRank (Komorebi.SingleOperatorGraph.operatorAlgebra T) V = 0 := by
92         rw [operator_seedRank_eq_intrinsicSeedMaximum, he]
93         rfl
94       exact not_subsingleton V ((seedRank_eq_zero_iff _ _).mp hr)
95     have hr : seedRank (Komorebi.SingleOperatorGraph.operatorAlgebra T) V = 1 := by
96       rw [operator_seedRank_eq_intrinsicSeedMaximum, show intrinsicSeedMaximum T = 1 by omega]
97       rfl
98     exact (hasCyclicVector_iff_minpoly_eq_charpoly T).mpr
99       ((operatorAlgebra_seedRank_eq_one_iff_minpoly_eq_charpoly T).mp hr)
100 
101 end Komorebi.PaperICompletion6.PrimaryCyclicCriterion

Back to source controls