From 20981bee5dddb366f5bdf4221877eeb89794c85f Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Thu, 23 Sep 2021 00:38:16 +0000 Subject: [PATCH] feat(linear_algebra/charpoly): add linear_map.charpoly (#9279) We add `linear_map.charpoly`, the characteristic polynomial of an endomorphism of a finite free module, and a basic API. --- src/linear_algebra/charpoly.lean | 138 ++++++++++++++++++++++++ src/linear_algebra/charpoly/basic.lean | 16 +++ src/linear_algebra/dimension.lean | 5 + src/linear_algebra/eigenspace.lean | 8 +- src/linear_algebra/free_module_pid.lean | 8 -- 5 files changed, 160 insertions(+), 15 deletions(-) create mode 100644 src/linear_algebra/charpoly.lean diff --git a/src/linear_algebra/charpoly.lean b/src/linear_algebra/charpoly.lean new file mode 100644 index 0000000000000..204e0746036d1 --- /dev/null +++ b/src/linear_algebra/charpoly.lean @@ -0,0 +1,138 @@ +/- +Copyright (c) 2021 Riccardo Brasca. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Riccardo Brasca +-/ + +import linear_algebra.free_module +import linear_algebra.charpoly.coeff +import linear_algebra.matrix.basis + +/-! + +# Characteristic polynomial + +We define the characteristic polynomial of `f : M →ₗ[R] M`, where `M` is a finite and +free `R`-module. + +## Main definition + +* `linear_map.charpoly f` : the characteristic polynomial of `f : M →ₗ[R] M`. + +-/ + +universes u v w + +variables {R : Type u} {M : Type v} [comm_ring R] [nontrivial R] +variables [add_comm_group M] [module R M] [module.free R M] [module.finite R M] (f : M →ₗ[R] M) + +open_locale classical matrix + +noncomputable theory + +open module.free polynomial matrix + +namespace linear_map + +section basic + +/-- The characteristic polynomial of `f : M →ₗ[R] M`. -/ +def charpoly : polynomial R := +(to_matrix (choose_basis R M) (choose_basis R M) f).charpoly + +lemma charpoly_def : + f.charpoly = (to_matrix (choose_basis R M) (choose_basis R M) f).charpoly := rfl + +/-- `charpoly f` is the characteristic polynomial of the matrix of `f` in any basis. -/ +@[simp] lemma charpoly_to_matrix {ι : Type w} [fintype ι] (b : basis ι R M) : + (to_matrix b b f).charpoly = f.charpoly := +begin + set A := to_matrix b b f, + set b' := choose_basis R M, + set ι' := choose_basis_index R M, + set A' := to_matrix b' b' f, + set e := basis.index_equiv b b', + set φ := reindex_linear_equiv R R e e, + set φ₁ := reindex_linear_equiv R R e (equiv.refl ι'), + set φ₂ := reindex_linear_equiv R R (equiv.refl ι') (equiv.refl ι'), + set φ₃ := reindex_linear_equiv R R (equiv.refl ι') e, + set P := b.to_matrix b', + set Q := b'.to_matrix b, + + have hPQ : C.map_matrix (φ₁ P) ⬝ (C.map_matrix (φ₃ Q)) = 1, + { rw [ring_hom.map_matrix_apply, ring_hom.map_matrix_apply, ← matrix.map_mul, ← + @reindex_linear_equiv_mul _ ι' _ _ _ _ R R, basis.to_matrix_mul_to_matrix_flip, + reindex_linear_equiv_one, ← ring_hom.map_matrix_apply, ring_hom.map_one] }, + + calc A.charpoly = (reindex e e A).charpoly : (charpoly_reindex _ _).symm + ... = (scalar ι' X - C.map_matrix (φ A)).det : rfl + ... = (scalar ι' X - C.map_matrix (φ (P ⬝ A' ⬝ Q))).det : + by rw [basis_to_matrix_mul_linear_map_to_matrix_mul_basis_to_matrix] + ... = (scalar ι' X - C.map_matrix (φ₁ P ⬝ φ₂ A' ⬝ φ₃ Q)).det : + by rw [reindex_linear_equiv_mul R R _ _ e, reindex_linear_equiv_mul R R e _ _] + ... = (scalar ι' X - (C.map_matrix (φ₁ P) ⬝ C.map_matrix A' ⬝ C.map_matrix (φ₃ Q))).det : by simp + ... = (scalar ι' X ⬝ C.map_matrix (φ₁ P) ⬝ (C.map_matrix (φ₃ Q)) - + (C.map_matrix (φ₁ P) ⬝ C.map_matrix A' ⬝ C.map_matrix (φ₃ Q))).det : + by { rw [matrix.mul_assoc ((scalar ι') X), hPQ, matrix.mul_one] } + ... = (C.map_matrix (φ₁ P) ⬝ scalar ι' X ⬝ (C.map_matrix (φ₃ Q)) - + (C.map_matrix (φ₁ P) ⬝ C.map_matrix A' ⬝ C.map_matrix (φ₃ Q))).det : by simp + ... = (C.map_matrix (φ₁ P) ⬝ (scalar ι' X - C.map_matrix A') ⬝ C.map_matrix (φ₃ Q)).det : + by rw [← matrix.sub_mul, ← matrix.mul_sub] + ... = (C.map_matrix (φ₁ P)).det * (scalar ι' X - C.map_matrix A').det * + (C.map_matrix (φ₃ Q)).det : by rw [det_mul, det_mul] + ... = (C.map_matrix (φ₁ P)).det * (C.map_matrix (φ₃ Q)).det * + (scalar ι' X - C.map_matrix A').det : by ring + ... = (scalar ι' X - C.map_matrix A').det : by rw [← det_mul, hPQ, det_one, one_mul] + ... = f.charpoly : rfl +end + +end basic + +section coeff + +lemma charpoly_monic : f.charpoly.monic := charpoly_monic _ + +end coeff + +section cayley_hamilton + +/-- The Cayley-Hamilton Theorem, that the characteristic polynomial of a linear map, applied to +the linear map itself, is zero. -/ +lemma aeval_self_charpoly : aeval f f.charpoly = 0 := +begin + apply (linear_equiv.map_eq_zero_iff (alg_equiv_matrix _).to_linear_equiv).1, + rw [alg_equiv.to_linear_equiv_apply, ← alg_equiv.coe_alg_hom, + ← polynomial.aeval_alg_hom_apply _ _ _, charpoly_def], + exact aeval_self_charpoly _, +end + +lemma is_integral : is_integral R f := ⟨f.charpoly, ⟨charpoly_monic f, aeval_self_charpoly f⟩⟩ + +lemma minpoly_dvd_charpoly {K : Type u} {M : Type v} [field K] [add_comm_group M] [module K M] + [finite_dimensional K M] (f : M →ₗ[K] M) : minpoly K f ∣ f.charpoly := +minpoly.dvd _ _ (aeval_self_charpoly f) + +variable {f} + +lemma charpoly_coeff_zero_of_injective (hf : function.injective f) : (minpoly R f).coeff 0 ≠ 0 := +begin + intro h, + obtain ⟨P, hP⟩ := X_dvd_iff.2 h, + have hdegP : P.degree < (minpoly R f).degree, + { rw [hP, mul_comm], + refine degree_lt_degree_mul_X (λ h, _), + rw [h, mul_zero] at hP, + exact minpoly.ne_zero (is_integral f) hP }, + have hPmonic : P.monic, + { suffices : (minpoly R f).monic, + { rwa [monic.def, hP, mul_comm, leading_coeff_mul_X, ← monic.def] at this }, + exact minpoly.monic (is_integral f) }, + have hzero : aeval f (minpoly R f) = 0 := minpoly.aeval _ _, + simp only [hP, mul_eq_comp, ext_iff, hf, aeval_X, map_eq_zero_iff, coe_comp, alg_hom.map_mul, + zero_apply] at hzero, + exact not_le.2 hdegP (minpoly.min _ _ hPmonic (ext hzero)), +end + +end cayley_hamilton + +end linear_map diff --git a/src/linear_algebra/charpoly/basic.lean b/src/linear_algebra/charpoly/basic.lean index ca0d193d01f66..0a0c3f9716776 100644 --- a/src/linear_algebra/charpoly/basic.lean +++ b/src/linear_algebra/charpoly/basic.lean @@ -7,6 +7,7 @@ import tactic.apply_fun import ring_theory.matrix_algebra import ring_theory.polynomial_algebra import linear_algebra.matrix.nonsingular_inverse +import linear_algebra.matrix.reindex import tactic.squeeze /-! @@ -67,12 +68,27 @@ begin split_ifs; simp [h], } end +lemma charmatrix_reindex {m : Type v} [decidable_eq m] [fintype m] (e : n ≃ m) + (M : matrix n n R) : charmatrix (reindex e e M) = reindex e e (charmatrix M) := +begin + ext i j x, + by_cases h : i = j, + all_goals { simp [h] } +end + /-- The characteristic polynomial of a matrix `M` is given by $\det (t I - M)$. -/ def matrix.charpoly (M : matrix n n R) : polynomial R := (charmatrix M).det +lemma matrix.charpoly_reindex {m : Type v} [decidable_eq m] [fintype m] (e : n ≃ m) + (M : matrix n n R) : (reindex e e M).charpoly = M.charpoly := +begin + unfold matrix.charpoly, + rw [charmatrix_reindex, matrix.det_reindex_self] +end + /-- The **Cayley-Hamilton Theorem**, that the characteristic polynomial of a matrix, applied to the matrix itself, is zero. diff --git a/src/linear_algebra/dimension.lean b/src/linear_algebra/dimension.lean index 08f7d8de86478..024b4edbcf4fd 100644 --- a/src/linear_algebra/dimension.lean +++ b/src/linear_algebra/dimension.lean @@ -462,6 +462,11 @@ begin exact le_antisymm w₁ w₂, } end +/-- Given two basis indexed by `ι` and `ι'` of an `R`-module, where `R` satisfies the invariant +basis number property, an equiv `ι ≃ ι' `. -/ +def basis.index_equiv (v : basis ι R M) (v' : basis ι' R M) : ι ≃ ι' := +nonempty.some (cardinal.lift_mk_eq.1 (cardinal.lift_max.2 (mk_eq_mk_of_basis v v'))) + theorem mk_eq_mk_of_basis' {ι' : Type w} (v : basis ι R M) (v' : basis ι' R M) : #ι = #ι' := cardinal.lift_inj.1 $ mk_eq_mk_of_basis v v' diff --git a/src/linear_algebra/eigenspace.lean b/src/linear_algebra/eigenspace.lean index f70ff82e95c1a..54a75fd48379a 100644 --- a/src/linear_algebra/eigenspace.lean +++ b/src/linear_algebra/eigenspace.lean @@ -8,6 +8,7 @@ import field_theory.is_alg_closed.basic import linear_algebra.finsupp import linear_algebra.matrix.to_lin import order.preorder_hom +import linear_algebra.charpoly /-! # Eigenvectors and eigenvalues @@ -130,9 +131,6 @@ end variables [finite_dimensional K V] (f : End K V) -protected theorem is_integral : is_integral K f := -is_integral_of_noetherian (by apply_instance) f - variables {f} {μ : K} theorem has_eigenvalue_of_is_root (h : (minpoly K f).is_root μ) : @@ -518,7 +516,3 @@ end end End end module -variables {K V : Type*} [field K] [add_comm_group V] [module K V] [finite_dimensional K V] - -protected lemma linear_map.is_integral (f : V →ₗ[K] V) : is_integral K f := -module.End.is_integral f diff --git a/src/linear_algebra/free_module_pid.lean b/src/linear_algebra/free_module_pid.lean index 5b4bcfe0a6c0b..47f87bd3507b0 100644 --- a/src/linear_algebra/free_module_pid.lean +++ b/src/linear_algebra/free_module_pid.lean @@ -308,14 +308,6 @@ lemma basis.card_le_card_of_le b.card_le_card_of_linear_independent (b'.linear_independent.map' (submodule.of_le hNO) (N.ker_of_le O _)) -/-- If we have two bases on the same space, their indices are in bijection. -/ -noncomputable def basis.index_equiv {R ι ι' : Type*} [integral_domain R] [module R M] - [fintype ι] [fintype ι'] (b : basis ι R M) (b' : basis ι' R M) : - ι ≃ ι' := -(fintype.card_eq.mp (le_antisymm - (b'.card_le_card_of_linear_independent b.linear_independent) - (b.card_le_card_of_linear_independent b'.linear_independent))).some - /-- If `N` is a submodule in a free, finitely generated module, do induction on adjoining a linear independent element to a submodule. -/ def submodule.induction_on_rank [fintype ι] (b : basis ι R M) (P : submodule R M → Sort*)