ScalarExtension.lean

1 import PaperICompletion5
2 import Mathlib.LinearAlgebra.Charpoly.BaseChange
3 import Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
4 import Mathlib.RingTheory.Flat.Basic
5 import Mathlib.RingTheory.PowerBasis
6 
7 /-! # Actual scalar extension of finite-dimensional operators
8 The extension is the literal tensor-product endomorphism `T.baseChange K`.
9 No minimal-polynomial preservation or descent certificate is an input.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace Komorebi.PaperICompletion6.ScalarExtension
14 open Polynomial TensorProduct
15 open scoped TensorProduct
16 universe u v w
17 variable {k : Type u} [Field k] {V : Type v} [AddCommGroup V] [Module k V]
18 variable (K : Type w) [Field K] [Algebra k K]
19 
20 /-- The endomorphism map provided by the universal property is literal base change. -/
21 theorem tensor_endHom_eq_baseChange :
22     (TensorProduct.isBaseChange k V K).endHom = LinearMap.baseChangeHom k K V V := by
23   apply LinearMap.ext
24   intro T
25   apply (TensorProduct.isBaseChange k V K).algHom_ext
26   intro x
27   simpa using (TensorProduct.isBaseChange k V K).endHom_comp_apply T x
28 
29 /-- The full endomorphism space commutes with scalar extension in finite dimension. -/
30 theorem isBaseChange_endomorphisms [FiniteDimensional k V] :
31     IsBaseChange K (LinearMap.baseChangeHom k K V V) := by
32   rw [← tensor_endHom_eq_baseChange K]
33   exact (TensorProduct.isBaseChange k V K).end
34 
35 /-- Linear independence of actual operators survives field extension. -/
36 theorem linearIndependent_baseChange [FiniteDimensional k V] {ι : Type*}
37     {f : ι → Module.End k V} (hf : LinearIndependent k f) :
38     LinearIndependent K (fun i => (f i).baseChange K) := by
39   have h := (Module.Flat.linearIndependent_one_tmul (S := K) hf).map'
40     (isBaseChange_endomorphisms (V := V) K).equiv.toLinearMap
41     (LinearMap.ker_eq_bot.mpr (isBaseChange_endomorphisms (V := V) K).equiv.injective)
42   simpa [Function.comp_def] using h
43 
44 /-- Powers below the original minimal degree remain independent over the extended field. -/
45 theorem linearIndependent_baseChange_powers [FiniteDimensional k V] (T : Module.End k V) :
46     LinearIndependent K
47       (fun i : Fin (minpoly k T).natDegree => (T.baseChange K) ^ (i : ℕ)) := by
48   simpa only [LinearMap.baseChange_pow] using
49     linearIndependent_baseChange K (linearIndependent_pow (K := k) T)
50 
51 /-- Evaluating mapped coefficients agrees with extending the evaluated operator. -/
52 theorem aeval_map_baseChange (T : Module.End k V) (p : k[X]) :
53     aeval (T.baseChange K) (p.map (algebraMap k K)) = (aeval T p).baseChange K := by
54   rw [aeval_map_algebraMap]
55   exact aeval_algHom_apply (Module.End.baseChangeHom k K V) T p
56 
57 /-- The minimal polynomial itself commutes with every field extension. -/
58 theorem minpoly_baseChange [FiniteDimensional k V] (T : Module.End k V) :
59     minpoly K (T.baseChange K) = (minpoly k T).map (algebraMap k K) := by
60   refine minpoly.eq_of_linearIndependent K (T.baseChange K)
61     ((minpoly.monic (LinearMap.isIntegral T)).map _) ?_
62     (minpoly k T).natDegree ?_ ?_
63   · rw [aeval_map_baseChange, minpoly.aeval, LinearMap.baseChange_zero]
64   · rw [Polynomial.degree_map_eq_of_injective (algebraMap k K).injective,
65       Polynomial.degree_eq_natDegree (minpoly.ne_zero (LinearMap.isIntegral T))]
66   · exact linearIndependent_baseChange_powers K T
67 
68 /-- Minimal-polynomial degree is unchanged by any field extension. -/
69 theorem minpoly_natDegree_baseChange [FiniteDimensional k V] (T : Module.End k V) :
70     (minpoly K (T.baseChange K)).natDegree = (minpoly k T).natDegree := by
71   rw [minpoly_baseChange, Polynomial.natDegree_map_eq_of_injective (algebraMap k K).injective]
72 
73 /-- Equality of minimal and characteristic polynomials is both preserved and reflected. -/
74 theorem minpoly_eq_charpoly_baseChange_iff [FiniteDimensional k V] (T : Module.End k V) :
75     minpoly K (T.baseChange K) = (T.baseChange K).charpoly ↔ minpoly k T = T.charpoly := by
76   rw [minpoly_baseChange, LinearMap.charpoly_baseChange]
77   exact (Polynomial.map_injective (algebraMap k K) (algebraMap k K).injective).eq_iff
78 
79 /-- Cyclicity is preserved and reflected for the actual tensor-product operator. -/
80 theorem hasCyclicVector_baseChange_iff [FiniteDimensional k V] (T : Module.End k V) :
81     Komorebi.SingleOperatorGraph.HasCyclicVector (T.baseChange K) ↔
82       Komorebi.SingleOperatorGraph.HasCyclicVector T := by
83   rw [Komorebi.PaperICompletion.CyclicClassification.hasCyclicVector_iff_minpoly_eq_charpoly,
84     Komorebi.PaperICompletion.CyclicClassification.hasCyclicVector_iff_minpoly_eq_charpoly]
85   exact minpoly_eq_charpoly_baseChange_iff K T
86 
87 /-- The base-changed space is nonzero whenever the original vector space is nonzero. -/
88 theorem baseChange_nontrivial [Nontrivial V] : Nontrivial (K ⊗[k] V) :=
89   Function.Injective.nontrivial (Module.Flat.tensorProduct_mk_injective k V K)
90 
91 /-- The manuscript's clause after extension, over any algebraically closed extension field. -/
92 theorem hasCyclicVector_iff_extended_spectral_multiplicities_one
93     [FiniteDimensional k V] [Nontrivial V] [IsAlgClosed K] (T : Module.End k V) :
94     Komorebi.SingleOperatorGraph.HasCyclicVector T ↔
95       ∀ a : K, a ∈ spectrum K (T.baseChange K) →
96         Module.finrank K (Module.End.eigenspace (T.baseChange K) a) = 1 := by
97   let : Nontrivial (K ⊗[k] V) := baseChange_nontrivial (V := V) K
98   exact (hasCyclicVector_baseChange_iff K T).symm.trans
99     (Komorebi.PaperICompletion5.CyclicGeometricCriterion.hasCyclicVector_iff_all_spectral_multiplicities_one (T.baseChange K))
100 
101 end Komorebi.PaperICompletion6.ScalarExtension

Back to source controls