Matrix diagonalizability criterion- Proofs

Stream: maths

[Pranav Shankar]

I'm looking to add the criterion for matrix diagonalizability to mathlib. The criterion has 2 directions: EigenbasisExistsIfDiagonalizable and DiagonalizableIfBasisOfEigenvectorsExists. Are these proofs valid? Can they be added to mathlib?

The first proof is:

import Mathlib
theorem EigenbasisExistsIfDiagonalizable
  {F V : Type*} [Field F] [AddCommGroup V] [Module F V] [FiniteDimensional F V]
  (f : V →ₗ[F] V)
  (defaultBasis : Module.Basis (Fin (Module.finrank F V)) F V)
  (diagonalizable : ∃ (μ : Fin (Module.finrank F V) → F),
            ∃ (P : Matrix (Fin (Module.finrank F V)) (Fin (Module.finrank F V)) F),
            P.det ≠ 0 ∧
            LinearMap.toMatrix defaultBasis defaultBasis f = P * (Matrix.diagonal μ) * P⁻¹) :
            ∃ (b : Module.Basis (Fin (Module.finrank F V)) F V),
            ∀ i, ∃ L : F, f (b i) = L • (b i) := by


  rcases diagonalizable with ⟨μ, P, h_det, h_A_eq⟩

  let A := LinearMap.toMatrix defaultBasis defaultBasis f
  have AP_eq_PD : A * P = P * (Matrix.diagonal μ) := by
    dsimp [A]
    rw [h_A_eq]


    rw [Matrix.mul_assoc, Matrix.mul_assoc]


    rw [Matrix.nonsing_inv_mul P (isUnit_iff_ne_zero.mpr h_det)]


    simp only [Matrix.mul_one]
  have AP_col : ∀ j, (A * P).col j = Matrix.mulVec A (P.col j) := by
    intro j
    ext i
    simp [Matrix.col, Matrix.mulVec, Matrix.mul_apply, dotProduct]
  have PD_col : ∀ j, (P * (Matrix.diagonal μ)).col j = μ j • (P.col j) := by
    intro j
    ext i
    simp [Matrix.col]
    rw [mul_comm]
  have P_inv : IsUnit P.det := isUnit_iff_ne_zero.mpr h_det
  let n := Fin (Module.finrank F V)
  let b_basis : Module.Basis n F V := defaultBasis
  let f_lin := Matrix.toLin b_basis b_basis P
  let g_lin := Matrix.toLin b_basis b_basis P⁻¹
  have h_right : f_lin * g_lin = 1 := by
      apply (LinearMap.toMatrix b_basis b_basis).injective

      simp only [f_lin, g_lin, LinearMap.toMatrix_mul, LinearMap.toMatrix_toLin, LinearMap.toMatrix_one]

      exact Matrix.mul_nonsing_inv P (isUnit_iff_ne_zero.mpr h_det)


  have h_left : g_lin * f_lin = 1 := by
      apply (LinearMap.toMatrix b_basis b_basis).injective
      simp only [f_lin, g_lin, LinearMap.toMatrix_mul, LinearMap.toMatrix_toLin, LinearMap.toMatrix_one]
      -- Apply the identity P⁻¹ * P = 1
      exact Matrix.nonsing_inv_mul P (isUnit_iff_ne_zero.mpr h_det)

  have f_inv : IsUnit f_lin := by
   refine ⟨{
      val := f_lin
      inv := g_lin
      val_inv := h_right
      inv_val := h_left
    }, rfl⟩
  let f_P : V ≃ₗ[F] V := LinearEquiv.ofLinear f_lin g_lin h_right h_left
  let b := b_basis.map f_P
  exists b
  intro i
  exists μ i
  have f_eq_A : f = Matrix.toLin b_basis b_basis A := by
    apply (LinearMap.toMatrix b_basis b_basis).injective
    simp only [LinearMap.toMatrix_toLin]
    dsimp [A]
  rw [f_eq_A]
  apply_fun (Matrix.toLin b_basis b_basis) at AP_eq_PD
  rw [Matrix.toLin_mul b_basis b_basis b_basis] at AP_eq_PD
  rw [Matrix.toLin_mul b_basis b_basis b_basis] at AP_eq_PD
  dsimp [b, f_P]
  rw [← LinearMap.comp_apply]
  dsimp [f_lin]
  rw [← LinearMap.comp_apply]
  rw [AP_eq_PD]
  rw [LinearMap.comp_apply]
  suffices eigen : (Matrix.toLin b_basis b_basis (Matrix.diagonal μ)) (b_basis i) = μ i • b_basis i by
    rw [eigen]
    rw [LinearMap.map_smul]
  apply b_basis.repr.injective
  simp [Matrix.toLin_apply, b_basis.repr_self]
  ext k
  simp [Matrix.mulVec_diagonal]
  simp only [Finsupp.single_apply]
  split_ifs with h_eq
  · subst h_eq
    simp
  · simp [h_eq]

and the second proof is

import Mathlib
theorem DiagonalizableIfBasisOfEigenvectorsExists
  {F V : Type*} [Field F] [AddCommGroup V] [Module F V] [FiniteDimensional F V]
  (f : V →ₗ[F] V) -- Linear operator on V
  (eigenBasis : Module.Basis (Fin (Module.finrank F V)) F V)
  (eigenvector_property : ∀ i, ∃ L : F, f (eigenBasis i) = L • (eigenBasis i)) :
  ∃ D : Matrix (Fin (Module.finrank F V)) (Fin (Module.finrank F V)) F,
    ∃ P : Matrix (Fin (Module.finrank F V)) (Fin (Module.finrank F V)) F,
      (P.det ≠ 0) ∧
      (LinearMap.toMatrix eigenBasis eigenBasis f = P * D * P⁻¹) := by
      have matrix_wrt_eigenbasis_is_diagonal
        (μ : Fin (Module.finrank F V) → F)
        (eigen : ∀ i, f (eigenBasis i) = μ i • eigenBasis i) :
        LinearMap.toMatrix eigenBasis eigenBasis f = Matrix.diagonal μ := by
          ext i j
          simp [LinearMap.toMatrix_apply, eigen, Matrix.diagonal, Finsupp.single_apply]
          by_cases diagOrNot: i = j
          · subst diagOrNot
            simp
          rw [if_neg diagOrNot]
          rw [if_neg (Ne.symm diagOrNot)]

      let μ := fun i => Classical.choose (eigenvector_property i)

      have hμ : ∀ i, f (eigenBasis i) = μ i • eigenBasis i := by
        intro i
        rw [Classical.choose_spec (eigenvector_property i)]

      let D := Matrix.diagonal μ
      let P := (1 : Matrix (Fin (Module.finrank F V)) (Fin (Module.finrank F V)) F)

      use D, P
      constructor

        dsimp [P]

        rw [Matrix.det_one]

        exact one_ne_zero

        dsimp [P]
        simp only [Matrix.one_mul, Matrix.mul_one, inv_one]


        apply matrix_wrt_eigenbasis_is_diagonal
        exact hμ

[Eric Wieser]

Please apply #backticks

[J. J. Issai (project started by GRP)]

Also, "Diagonalization Proofs" means something different in logic and set theory and recursion theory. Please change title to "Matrix Diagonalization proofs".