SixWayCyclicCriterion.lean

1 import PaperICompletion6.ScalarExtension
2 import PaperICompletion6.PrimaryCyclicCriterion
3 import PaperICompletion6.OneInvariantFactor
4 import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
5 import Mathlib.Tactic.TFAE
6 
7 /-! # The six-way cyclic-matrix criterion
8 Every clause refers to the actual operator, its intrinsic primary components,
9 an actual one-factor presentation, or its literal tensor-product extension.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace Komorebi.PaperICompletion6.SixWayCyclicCriterion
14 open Polynomial
15 open Komorebi.SingleOperatorGraph
16 open Komorebi.SeedRankBasics
17 open Komorebi.PaperICompletion.CyclicClassification
18 open Komorebi.PaperICompletion4.IntrinsicPrimary
19 open Komorebi.PaperICompletion6.ScalarExtension
20 open Komorebi.PaperICompletion6.PrimaryCyclicCriterion
21 open Komorebi.PaperICompletion6.OneInvariantFactor
22 universe u v w
23 variable {k : Type u} [Field k] {V : Type v} [AddCommGroup V] [Module k V]
24 variable [FiniteDimensional k V] [Nontrivial V]
25 
26 /-- All six printed clauses over an arbitrary algebraically closed extension. -/
27 theorem cyclic_six_way (K : Type w) [Field K] [Algebra k K] [IsAlgClosed K]
28     (T : Module.End k V) :
29     List.TFAE [
30       HasCyclicVector T,
31       seedRank (operatorAlgebra T) V = 1,
32       ∀ p : k[X], Irreducible p →
33         Nontrivial (primarySubmodule (Module.AEval' T) p) →
34         Cyclic k[X] (primarySubmodule (Module.AEval' T) p),
35       HasOneInvariantFactor T,
36       minpoly k T = T.charpoly,
37       ∀ a : K, a ∈ spectrum K (T.baseChange K) →
38         Module.finrank K (Module.End.eigenspace (T.baseChange K) a) = 1] := by
39   tfae_have 1 ↔ 5 := hasCyclicVector_iff_minpoly_eq_charpoly T
40   tfae_have 2 ↔ 5 := operatorAlgebra_seedRank_eq_one_iff_minpoly_eq_charpoly T
41   tfae_have 1 ↔ 3 := hasCyclicVector_iff_nonzero_primary_cyclic T
42   tfae_have 1 ↔ 4 := hasCyclicVector_iff_oneInvariantFactor T
43   tfae_have 1 ↔ 6 := hasCyclicVector_iff_extended_spectral_multiplicities_one K T
44   tfae_finish
45 
46 /-- The precise algebraic-closure instance in the manuscript. -/
47 theorem cyclic_six_way_algebraicClosure (T : Module.End k V) :
48     List.TFAE [
49       HasCyclicVector T,
50       seedRank (operatorAlgebra T) V = 1,
51       ∀ p : k[X], Irreducible p →
52         Nontrivial (primarySubmodule (Module.AEval' T) p) →
53         Cyclic k[X] (primarySubmodule (Module.AEval' T) p),
54       HasOneInvariantFactor T,
55       minpoly k T = T.charpoly,
56       ∀ a : AlgebraicClosure k, a ∈ spectrum (AlgebraicClosure k)
57           (T.baseChange (AlgebraicClosure k)) →
58         Module.finrank (AlgebraicClosure k)
59           (Module.End.eigenspace (T.baseChange (AlgebraicClosure k)) a) = 1] :=
60   cyclic_six_way (AlgebraicClosure k) T
61 
62 /-- In any supplied invariant-factor chain, cyclicity forces exactly one factor. -/
63 theorem cyclic_iff_invariantFactor_count_one (T : Module.End k V) {r : ℕ}
64     (p : Fin r → k[X]) (hp : ∀ i, 0 < (p i).natDegree)
65     (hchain : ∀ i j, i ≤ j → p i ∣ p j)
66     (E : Module.AEval' T ≃ₗ[k[X]] ((i : Fin r) → k[X] ⧸ Ideal.span {p i})) :
67     HasCyclicVector T ↔ r = 1 := by
68   have hr := (Komorebi.PaperICompletion3.InvariantFactorCount.invariantFactor_operator_seedRanks T p hp hchain E).2.2
69   have h := (hasCyclicVector_iff_minpoly_eq_charpoly T).trans
70     (operatorAlgebra_seedRank_eq_one_iff_minpoly_eq_charpoly T).symm
71   rw [hr] at h
72   exact h.trans (by norm_cast)
73 
74 end Komorebi.PaperICompletion6.SixWayCyclicCriterion

Back to source controls