1. Physlib
  2. Mathematics
  3. SchurTriangulation
Imports
/- Copyright (c) 2025 Gordon Hsu. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gordon Hsu -/ module public import Mathlib.LinearAlgebra.Eigenspace.Triangularizable public import Mathlib.Analysis.InnerProductSpace.Adjoint

Schur triangulation

Schur triangulation is more commonly known as Schur decomposition or Schur triangularization, but "triangulation" makes the API more readable. It states that a square matrix over an algebraically closed field, e.g., ℂ, is unitarily similar to an upper triangular matrix.

Main definitions

    Matrix.schur_triangulation : a matrix A : Matrix n n 𝕜 with 𝕜 being algebraically closed can be decomposed as A = U * T * star U where U is unitary and T is upper triangular.

    Matrix.schurTriangulationUnitary : the unitary matrix U as previously stated.

    Matrix.schurTriangulation : the upper triangular matrix T as previously stated.

    Some auxiliary definitions are not meant to be used directly, but LinearMap.SchurTriangulationAux.of contains the main algorithm for the triangulation procedure.

@[expose] public section

subNat' i h subtracts m from i. This is an alternative form of Fin.subNat.

@[inline] def Fin.subNat' (i : Fin (m + n)) (h : ¬ i < m) : Fin n := subNat m (Fin.cast (m.add_comm n) i) (Nat.ge_of_not_lt h)

An alternative form of Equiv.sumEquivSigmaBool where Bool.casesOn is replaced by cond.

def sumEquivSigmalCond : Fin m ⊕ Fin n ≃ Σ b, cond b (Fin m) (Fin n) := calc Fin m ⊕ Fin n _ ≃ Fin n ⊕ Fin m := sumComm .. _ ≃ Σ b, bif b then (Fin m) else (Fin n) := sumEquivSigmaBool .. _ ≃ Σ b, cond b (Fin m) (Fin n) := sigmaCongrRight (fun | true | false => Equiv.refl _)

The composition of finSumFinEquiv and Equiv.sumEquivSigmalCond used by LinearMap.SchurTriangulationAux.of.

def finAddEquivSigmaCond : Fin (m + n) ≃ Σ b, cond b (Fin m) (Fin n) := finSumFinEquiv.symm.trans sumEquivSigmalCond
lemma finAddEquivSigmaCond_true (h : i < m) : finAddEquivSigmaCond i = ⟨true, i, h⟩ := congrArg sumEquivSigmalCond <| finSumFinEquiv_symm_apply_castAdd ⟨i, h⟩lemma finAddEquivSigmaCond_false (h : ¬ i < m) : finAddEquivSigmaCond i = ⟨false, i.subNat' h⟩ := let j : Fin n := i.subNat' h calc finAddEquivSigmaCond i _ = finAddEquivSigmaCond (Fin.natAdd m j) := suffices m + (i - m) = i from congrArg _ (Fin.ext this.symm) Nat.add_sub_of_le (Nat.le_of_not_gt h) _ = ⟨false, i.subNat' h⟩ := congrArg sumEquivSigmalCond <| finSumFinEquiv_symm_apply_natAdd j

The type family parameterized by Bool is finite if each type variant is finite.

instance [M : Fintype m] [N : Fintype n] (b : Bool) : Fintype (cond b m n) := b.rec N M

The type family parameterized by Bool has decidable equality if each type variant is decidable.

set_option backward.isDefEq.respectTransparency false ininstance [DecidableEq m] [DecidableEq n] : DecidableEq (Σ b, cond b m n) | ⟨true, _⟩, ⟨false, _⟩ | ⟨false, _⟩, ⟨true, _⟩ => isFalse nofun | ⟨false, i⟩, ⟨false, j⟩ | ⟨true, i⟩, ⟨true, j⟩ => if h : i = j then isTrue (Sigma.eq rfl h) else isFalse fun | rfl => h rfl

The property of a matrix being upper triangular. See also Matrix.det_of_upperTriangular.

abbrev IsUpperTriangular [LT n] [CommRing R] (A : Matrix n n R) := A.BlockTriangular id

The subtype of upper triangular matrices.

abbrev UpperTriangular (n R) [LT n] [CommRing R] := { A : Matrix n n R // A.IsUpperTriangular }

Don't use this definition directly. Instead, use Matrix.schurTriangulationBasis, Matrix.schurTriangulationUnitary, and Matrix.schurTriangulation. See also LinearMap.SchurTriangulationAux.of and Matrix.schurTriangulationAux.

The dimension of the inner product space E.

An orthonormal basis of E that induces an upper triangular form for f.

structure SchurTriangulationAux (f : Module.End 𝕜 E) where dim : ℕ hdim : Module.finrank 𝕜 E = dim basis : OrthonormalBasis (Fin dim) 𝕜 E upperTriangular : (toMatrix basis.toBasis basis.toBasis f).IsUpperTriangular

Schur's recursive triangulation procedure

Given a linear endomorphism f on a non-trivial finite-dimensional vector space E over an algebraically closed field 𝕜, one can always pick an eigenvalue μ of f whose corresponding eigenspace V is non-trivial. Given that E is also an inner product space, let bV and bW be orthonormal bases for V and Vᗮ respectively. Then, the collection of vectors in bV and bW forms an orthonormal basis bE for E, as the direct sum of V and Vᗮ is an internal decomposition of E. The matrix representation of f with respect to bE satisfies $$ \sideset{\mathrm{bE}}{\mathrm{bE}}{[f]} = \begin{bmatrix} \sideset{\mathrm{bV}}{\mathrm{bV}}{[f]} & \sideset{\mathrm{bW}}{\mathrm{bV}}{[f]} \ \sideset{\mathrm{bV}}{\mathrm{bW}}{[f]} & \sideset{\mathrm{bW}}{\mathrm{bW}}{[f]} \end{bmatrix} = \begin{bmatrix} \mu I & □ \ 0 & \sideset{\mathrm{bW}}{\mathrm{bW}}{[f]} \end{bmatrix}, $$ which is upper triangular as long as $\sideset{\mathrm{bW}}{\mathrm{bW}}{[f]}$ is. Finally, one observes that the recursion from $\sideset{\mathrm{bE}}{\mathrm{bE}}{[f]}$ to $\sideset{\mathrm{bW}}{\mathrm{bW}}{[f]}$ is well-founded, as the dimension of bW is smaller than that of bE because bV is non-trivial.

However, in order to leverage DirectSum.IsInternal.collectedOrthonormalBasis, the type Σ b, cond b (Fin m) (Fin n) has to be used instead of the more natural Fin m ⊕ Fin n while their equivalence is propositionally established by Equiv.sumEquivSigmalCond.

Don't use this definition directly. This is the key algorithm behind Matrix.schur_triangulation.

set_option maxHeartbeats 800000 in set_option maxRecDepth 2000 in set_option backward.isDefEq.respectTransparency false inAll goals completed! 🐙 _ = toMatrixOrthonormal bW g i' j' := (g.toMatrixOrthonormal_apply_apply ..).symm _ = 0 := hg (Nat.sub_lt_sub_right (Nat.le_of_not_lt hj) hji) } else haveI : Subsingleton E := not_nontrivial_iff_subsingleton.mp hE { dim := 0 hdim := Module.finrank_zero_of_subsingleton basis := (Basis.empty E).toOrthonormalBasis ⟨nofun, nofun⟩ upperTriangular := nofun } termination_by Module.finrank 𝕜 E decreasing_by All goals completed! 🐙

Schur triangulation, Schur decomposition for matrices over an algebraically closed field. In particular, a complex matrix can be converted to upper-triangular form by a change of basis. In other words, any complex matrix is unitarily similar to an upper triangular matrix.

All goals completed! 🐙