Hessenberg similarity certificates

Matrix.Hessenberg.Similarity A certifies a similarity relation between the square matrix A and an upper Hessenberg matrix.

Main definitions

• Matrix.Hessenberg.Similarity: the certificate structure.

Main results

• Matrix.Hessenberg.Similarity.charpoly_eq: The characteristic polynomial of A is equal to the characteristic polynomial of its Hessenberg matrix.

structure Matrix.Hessenberg.Similarity {m : Type u_1} {R : Type u_2} [CommRing R] [Fintype m] [LinearOrder m] [SuccOrder m] (A : Matrix m m R) : Type (max u_1 u_2)

A certificate of a Hessenberg similarity of A consisting of a permutation σ of its rows and columns, a lower triangular matrix L with nonzero diagonal and an upper Hessenberg matrix H satisfying A.reindex σ σ * L = L * H.

NB: The certificate does not represent the standard Hessenberg reduction where the transformation matrix L is orthogonal.

• L : Matrix m m R

  The transformation matrix.

• σ : Equiv.Perm m

  The row / column permutation on A.

• H : Matrix m m R

  The upper Hessenberg matrix.

• mul_eq_mul : (reindex self.σ self.σ) A * self.L = self.L * self.H
• isLowerTriangular : self.L.IsLowerTriangular
• diag_ne_zero (i : m) : self.L.diag i ≠ 0
• isUpperHessenberg : self.H.IsUpperHessenberg

@[simp]

theorem Matrix.Hessenberg.Similarity.charpoly_eq {m : Type u_1} {R : Type u_2} [CommRing R] [Fintype m] [DecidableEq m] [LinearOrder m] [SuccOrder m] [IsDomain R] {A : Matrix m m R} (cert : Similarity A) : cert.H.charpoly = A.charpoly