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

@@ -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

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.

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'

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

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*)