OneInvariantFactor.lean

1 import PaperICompletion5
2 import Mathlib.RingTheory.PowerBasis
3 
4 /-! # One invariant factor with an actual companion-matrix basis
5 An actual polynomial-module equivalence yields a basis of the given vector
6 space in which its operator is the usual companion matrix. This is a
7 mathematical construction, not an executable rational-canonical algorithm.
8 -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace Komorebi.PaperICompletion6.OneInvariantFactor
12 open Polynomial
13 open Komorebi.PaperICompletion.CyclicClassification
14 open Komorebi.PaperICompletion5.CyclicGeometricCriterion
15 universe u v
16 variable {k : Type u} [Field k] {V : Type v} [AddCommGroup V] [Module k V]
17 
18 /-- The standard companion matrix, including its empty degree-zero convention. -/
19 def companionMatrix (p : k[X]) : Matrix (Fin p.natDegree) (Fin p.natDegree) k :=
20   fun i j => if (j : ℕ) + 1 = p.natDegree then -p.coeff i
21     else if (i : ℕ) = (j : ℕ) + 1 then 1 else 0
22 
23 /-- Forget only the polynomial scalars in an actual one-factor presentation. -/
24 def quotientVectorEquiv (T : Module.End k V) (p : k[X])
25     (E : Module.AEval' T ≃ₗ[k[X]] k[X] ⧸ Ideal.span {p}) : AdjoinRoot p ≃ₗ[k] V :=
26   (E.symm.restrictScalars k).trans (Module.AEval'.of T).symm
27 
28 /-- The intertwining relation retains the actual operator action. -/
29 theorem quotientVectorEquiv_intertwines (T : Module.End k V) (p : k[X])
30     (E : Module.AEval' T ≃ₗ[k[X]] k[X] ⧸ Ideal.span {p}) (x : AdjoinRoot p) :
31     T (quotientVectorEquiv T p E x) =
32       quotientVectorEquiv T p E (AdjoinRoot.root p * x) := by
33   change T ((Module.AEval'.of T).symm (E.symm x)) =
34     (Module.AEval'.of T).symm (E.symm (AdjoinRoot.root p * x))
35   rw [← Module.AEval'.of_symm_X_smul]
36   congr 1
37   rw [← E.symm.map_smul (X : k[X]) x]
38   rfl
39 
40 /-- The quotient power basis transported to the original space. -/
41 def quotientCompanionBasis (T : Module.End k V) (p : k[X]) (hp : p.Monic)
42     (E : Module.AEval' T ≃ₗ[k[X]] k[X] ⧸ Ideal.span {p}) :
43     Module.Basis (Fin p.natDegree) k V :=
44   (AdjoinRoot.powerBasis' hp).basis.map (quotientVectorEquiv T p E)
45 
46 /-- The matrix in the constructed basis is literally the standard companion matrix. -/
47 theorem toMatrix_quotientCompanionBasis (T : Module.End k V) (p : k[X]) (hp : p.Monic)
48     (E : Module.AEval' T ≃ₗ[k[X]] k[X] ⧸ Ideal.span {p}) :
49     LinearMap.toMatrix (quotientCompanionBasis T p hp E)
50       (quotientCompanionBasis T p hp E) T = companionMatrix p := by
51   let pb := AdjoinRoot.powerBasis' hp
52   let e := quotientVectorEquiv T p E
53   have hconj : e.symm.toLinearMap ∘ₗ (T ∘ₗ e.toLinearMap) =
54       Algebra.lmul k (AdjoinRoot p) pb.gen := by
55     apply LinearMap.ext
56     intro x
57     change e.symm (T (e x)) = AdjoinRoot.root p * x
58     rw [quotientVectorEquiv_intertwines, e.symm_apply_apply]
59   have hpoly : pb.minpolyGen = p := by
60     rw [PowerBasis.minpolyGen_eq]
61     change minpoly k (AdjoinRoot.root p) = p
62     rw [AdjoinRoot.minpoly_root hp.ne_zero]
63     simp [hp.leadingCoeff]
64   change LinearMap.toMatrix (pb.basis.map e) (pb.basis.map e) T = _
65   rw [LinearMap.toMatrix_map_left, LinearMap.toMatrix_map_right, hconj,
66     ← Algebra.leftMulMatrix_apply, PowerBasis.leftMulMatrix]
67   rw [hpoly]
68   rfl
69 
70 /-- An actual one-factor invariant-factor presentation, not a numerical certificate. -/
71 def HasOneInvariantFactor (T : Module.End k V) : Prop :=
72   ∃ p : k[X], p.Monic ∧ 0 < p.natDegree ∧
73     Nonempty (Module.AEval' T ≃ₗ[k[X]] k[X] ⧸ Ideal.span {p})
74 
75 /-- The factor in a monic one-factor presentation is forced to be the minimal polynomial. -/
76 theorem factor_eq_minpoly [FiniteDimensional k V] (T : Module.End k V)
77     (p : k[X]) (hp : p.Monic)
78     (E : Module.AEval' T ≃ₗ[k[X]] k[X] ⧸ Ideal.span {p}) : p = minpoly k T := by
79   have hs : Ideal.span {minpoly k T} = Ideal.span {p} :=
80     (Polynomial.span_minpoly_eq_annihilator k T).trans
81       (E.annihilator_eq.trans Ideal.annihilator_quotient)
82   exact Polynomial.eq_of_monic_of_dvd_of_natDegree_le
83     (minpoly.monic (LinearMap.isIntegral T)) hp
84     (Ideal.span_singleton_le_span_singleton.mp hs.ge)
85     (Polynomial.natDegree_le_of_dvd
86       (Ideal.span_singleton_le_span_singleton.mp hs.le)
87       (minpoly.ne_zero (LinearMap.isIntegral T)))
88 
89 /-- One invariant factor is equivalent to cyclicity of the actual operator. -/
90 theorem hasCyclicVector_iff_oneInvariantFactor [FiniteDimensional k V] [Nontrivial V]
91     (T : Module.End k V) :
92     Komorebi.SingleOperatorGraph.HasCyclicVector T ↔ HasOneInvariantFactor T := by
93   constructor
94   · intro h
95     refine ⟨minpoly k T, minpoly.monic (LinearMap.isIntegral T), ?_,
96       (hasCyclicVector_iff_minpoly_quotient_presentation T).mp h⟩
97     rw [(hasCyclicVector_iff_minpoly_eq_charpoly T).mp h, LinearMap.charpoly_natDegree]
98     exact Module.finrank_pos
99   · rintro ⟨p, hp, _hd, ⟨E⟩⟩
100     apply (hasCyclicVector_iff_minpoly_quotient_presentation T).mpr
101     rw [factor_eq_minpoly T p hp E] at E
102     exact ⟨E⟩
103 
104 /-- A cyclic operator admits a genuine companion-matrix basis for its minimal polynomial. -/
105 theorem exists_companion_basis_of_cyclic [FiniteDimensional k V]
106     (T : Module.End k V) (h : Komorebi.SingleOperatorGraph.HasCyclicVector T) :
107     ∃ b : Module.Basis (Fin (minpoly k T).natDegree) k V,
108       LinearMap.toMatrix b b T = companionMatrix (minpoly k T) := by
109   obtain ⟨E⟩ := (hasCyclicVector_iff_minpoly_quotient_presentation T).mp h
110   exact ⟨quotientCompanionBasis T _ (minpoly.monic (LinearMap.isIntegral T)) E,
111     toMatrix_quotientCompanionBasis T _ (minpoly.monic (LinearMap.isIntegral T)) E⟩
112 
113 end Komorebi.PaperICompletion6.OneInvariantFactor

Back to source controls