lemmastandard

Lower-Bruhat factorization of rational matrices

Factors any rational matrix as lower triangular, partial permutation, lower triangular
reduces matrix shear to a partial permutation
Lemma·lem:lower-lower·§4.1 A matrix decomposition adapted to tape order

Statement (paper)

Every rational m×mm\times m matrix AA of rank aa has a factorization A=E1ΠE2, A=E_1\Pi E_2, where E1,E2E_1,E_2 are invertible lower triangular rational matrices and Π\Pi has exactly aa entries equal to one, with at most one in each row and column, and all remaining entries zero.

In plain English

Every rational m×mm\times m matrix AA of rank aa factors as A=E1ΠE2A=E_1\Pi E_2, where E1,E2E_1,E_2 are invertible lower triangular rational matrices and Π\Pi is a partial permutation matrix with exactly aa ones, at most one per row and column, and zeros elsewhere.

Why it's here

This is a Bruhat-type decomposition in which both outer factors are lower triangular, which suits tape order, where lower triangular maps only use earlier entries. It reduces a general rational matrix to a partial permutation plus lower triangular maps, which the matrix shear cost lemma can then handle.
Classified standard:
This is the classical Bruhat-type (LPU / rook-matrix) decomposition of arbitrary rectangular or rank-deficient matrices over a field, in the version where both outer factors are lower triangular. It is a textbook fact of linear algebra, appearing for instance in Renner's work on Bruhat decompositions of the monoid of all matrices, and the paper uses it as is.

Uses

Nothing else in the paper

Used by

lemMatrix shear via few interchanges

Sources

PaperOpen
Section
§4.1 A matrix decomposition adapted to tape order
Page
—
Label
lem:lower-lower
Line
sections/04-swap.tex:18
Leannot aligned

Phase 2 aligns this node to a Lean declaration.