Reduction of a matrix over ℚ to Hessenberg form

reduce computes, for a square matrix A over ℚ, a sequence of row and column swaps, a unit lower triangular matrix L and an upper Hessenberg matrix H such that Aσ * L = L * H, where Aσ := A.submatrix σ σ is A with its rows and columns permuted by the swaps.

Implementation notes

reduce follows steps 1 to 4 of Cohen, Algorithm 2.2.9.

References

• H. Cohen, A Course in Computational Algebraic Number Theory, Algorithm 2.2.9

structure Mathlib.Tactic.Hessenberg.Reduction : Type

A similarity Aσ * L = L * H of a rational matrix A to upper Hessenberg form, where Aσ := A.submatrix σ σ for the arrangement σ of the interchanges.

• swaps : Array (ℕ × ℕ)

  The row and column interchanges, in order. The permutation σ is their product.

• L : Array (Array ℚ)

  The unit lower triangular transform.

• H : Array (Array ℚ)

  The upper Hessenberg form.

def Mathlib.Tactic.Hessenberg.Reduction.perm (d : Reduction) : Array ℕ

The row and column swaps of a Reduction represented as an indexed array. An entry e at index i means that row and column e of the original matrix move to position i.

Equations

• d.perm = Array.foldl (fun (ord : Array ℕ) (x : ℕ × ℕ) => match x with | (a, b) => ord.swapIfInBounds a b) (Array.range d.L.size) d.swaps

def Mathlib.Tactic.Hessenberg.Reduction.arrange {β : Type} [Inhabited β] (d : Reduction) (M : Array (Array β)) : Array (Array β)

Arrange the rows and columns of the matrix M, given as an array of rows, by the interchanges of the reduction: the entry at (i, j) of the result is the entry of M at (d.perm[i], d.perm[j]).

Equations

• d.arrange M = Array.map (fun (i : ℕ) => Array.map (fun (j : ℕ) => M[i]![j]!) d.perm) d.perm

def Mathlib.Tactic.Hessenberg.reduce (n : ℕ) (A : Array (Array ℚ)) : Reduction

Reduce the n × n matrix A over ℚ, given as an array of rows, to upper Hessenberg form by Gaussian elimination with row and column swaps.

Equations

• One or more equations did not get rendered due to their size.