LinearPrimaryEigenspace.lean

1 import PaperICompletion4
2 import Mathlib.RingTheory.Polynomial.Quotient
3 import Mathlib.LinearAlgebra.Dimension.Free
4 
5 /-! # Linear primary multiplicity is actual geometric multiplicity
6 The polynomial scalar quotient is identified with the literal cokernel of p(T).
7 For p = X - C a, evaluation identifies its residue field with the base field.
8 Rank-nullity then computes the dimension of the actual eigenspace, without
9 any diagonalizability hypothesis.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 open scoped Pointwise
14 namespace Komorebi.PaperICompletion5.LinearPrimaryEigenspace
15 open Polynomial
16 open Komorebi.PaperICompletion4.ResidueQuotient
17 open Komorebi.PaperICompletion4.IntrinsicPrimary
18 open Komorebi.PaperICompletion4.OperatorIntrinsicFormula
19 universe u v
20 variable {k : Type u} [Field k]
21 variable {V : Type v} [AddCommGroup V] [Module k V]
22 
23 /-- The original vector, followed by the actual cokernel quotient. -/
24 def polynomialCokernelMap (T : Module.End k V) (p : k[X]) :
25     Module.AEval' T →ₗ[k] V ⧸ LinearMap.range (aeval T p) :=
26   (LinearMap.range (aeval T p)).mkQ.comp (Module.AEval'.of T).symm.toLinearMap
27 
28 /-- No finite-dimensional hypothesis is required for this quotient map. -/
29 theorem polynomialCokernelMap_surjective (T : Module.End k V) (p : k[X]) :
30     Function.Surjective (polynomialCokernelMap T p) :=
31   (LinearMap.range (aeval T p)).mkQ_surjective.comp (Module.AEval'.of T).symm.surjective
32 
33 /-- The kernel is exactly the actual polynomial scalar image. -/
34 theorem polynomialCokernelMap_ker (T : Module.End k V) (p : k[X]) :
35     (polynomialCokernelMap T p).ker =
36       (p • (⊤ : Submodule k[X] (Module.AEval' T))).restrictScalars k := by
37   ext x
38   change Submodule.Quotient.mk ((Module.AEval'.of T).symm x) =
39     (0 : V ⧸ LinearMap.range (aeval T p)) ↔
40       x ∈ p • (⊤ : Submodule k[X] (Module.AEval' T))
41   rw [Submodule.Quotient.mk_eq_zero, LinearMap.mem_range, mem_scalarImage_iff]
42   rfl
43 
44 /-- The natural base-field-linear equivalence from polynomial quotient to cokernel. -/
45 def polynomialQuotientEquivCokernel (T : Module.End k V) (p : k[X]) :
46     ScalarQuotient (Module.AEval' T) p ≃ₗ[k] V ⧸ LinearMap.range (aeval T p) :=
47   (Submodule.Quotient.restrictScalarsEquiv k
48     (p • (⊤ : Submodule k[X] (Module.AEval' T)))).symm.trans
49     ((Submodule.quotEquivOfEq _ _ (polynomialCokernelMap_ker T p).symm).trans
50       ((polynomialCokernelMap T p).quotKerEquivOfSurjective
51         (polynomialCokernelMap_surjective T p)))
52 
53 /-- The equivalence preserves the literal representative in the original vector space. -/
54 theorem polynomialQuotientEquivCokernel_mk (T : Module.End k V) (p : k[X]) (x : V) :
55     polynomialQuotientEquivCokernel T p (Submodule.Quotient.mk (Module.AEval'.of T x)) =
56       Submodule.Quotient.mk x := by
57   rfl
58 
59 /-- Endomorphisms have equal nullity and cokernel dimension in finite dimension. -/
60 theorem finrank_cokernel_eq_finrank_kernel [FiniteDimensional k V] (S : Module.End k V) :
61     Module.finrank k (V ⧸ LinearMap.range S) = Module.finrank k (LinearMap.ker S) := by
62   have hq := (LinearMap.range S).finrank_quotient_add_finrank
63   have hk := S.finrank_range_add_finrank_ker
64   omega
65 
66 /-- Evaluation identifies the linear residue field with a one-dimensional base-field space. -/
67 theorem linearResidue_finrank (a : k) :
68     Module.finrank k (k[X] ⧸ Ideal.span {X - C a}) = 1 := by
69   simpa using (quotientSpanXSubCAlgEquiv a).toLinearEquiv.finrank_eq
70 
71 /-- Linear primary multiplicity equals the dimension of the actual eigenspace.
72 This holds over any field and includes non-diagonalizable operators. -/
73 theorem intrinsicMultiplicity_X_sub_C_eq_eigenspace [FiniteDimensional k V]
74     (T : Module.End k V) (a : k) :
75     intrinsicMultiplicity T (X - C a) = Module.finrank k (T.eigenspace a) := by
76   let p : k[X] := X - C a
77   let : (Ideal.span {p}).IsMaximal :=
78     PrincipalIdealRing.isMaximal_of_irreducible (irreducible_X_sub_C a)
79   let : Field (k[X] ⧸ Ideal.span {p}) := Ideal.Quotient.field _
80   let : IsArtinian k[X] (Module.AEval' T) := isArtinian_of_tower k inferInstance
81   have hd : Module.finrank (k[X] ⧸ Ideal.span {p}) (IntrinsicPrimaryQuotient T p) =
82       Module.finrank k (IntrinsicPrimaryQuotient T p) := by
83     have h := Module.finrank_mul_finrank k (k[X] ⧸ Ideal.span {p})
84       (IntrinsicPrimaryQuotient T p)
85     simpa only [p, linearResidue_finrank, one_mul] using h
86   have heval : aeval T p = T - a • 1 := by
87     simp [p, Algebra.algebraMap_eq_smul_one]
88   calc
89     intrinsicMultiplicity T (X - C a) =
90         Module.finrank k (IntrinsicPrimaryQuotient T p) := hd
91     _ = Module.finrank k (ScalarQuotient (Module.AEval' T) p) :=
92       ((primaryQuotientEquivGlobal (Module.AEval' T) p).restrictScalars k).finrank_eq
93     _ = Module.finrank k (V ⧸ LinearMap.range (aeval T p)) :=
94       (polynomialQuotientEquivCokernel T p).finrank_eq
95     _ = Module.finrank k (LinearMap.ker (aeval T p)) :=
96       finrank_cokernel_eq_finrank_kernel (aeval T p)
97     _ = Module.finrank k (T.eigenspace a) := by rw [heval, Module.End.eigenspace_def]
98 
99 end Komorebi.PaperICompletion5.LinearPrimaryEigenspace

Back to source controls