Extending orthonormal rows to an orthogonal matrix

A real q × p matrix V with V * Vᵀ = 1 has orthonormal rows, and q ≤ p leaves room for p - q more. Extending those rows to an orthonormal basis of ℝ ^ p and reading the basis as the rows of a square matrix exhibits V as the first q rows of an orthogonal matrix.

Dividing an arbitrary M of full row rank by a square factor T of its Gram matrix M * Mᵀ leaves orthonormal rows, so M = T * Q.submatrix _ id for an orthogonal Q. This is the LQ decomposition, and it is what factors a congruence by a matrix of full row rank into a rotation followed by a coordinate selection.

Main results

• Matrix.exists_mul_transpose_eq_one_and_submatrix_castLE_eq — a real matrix with orthonormal rows consists of the first rows of an orthogonal matrix.
• Matrix.exists_mul_transpose_eq_one_and_eq_mul_submatrix_castLE — a real matrix of full row rank is a square factor of its Gram matrix times such a row selection.

theorem Matrix.exists_mul_transpose_eq_one_and_submatrix_castLE_eq {p q : ℕ} (V : Matrix (Fin q) (Fin p) ℝ) (hqp : q ≤ p) (hV : V * V.transpose = 1) : ∃ (Q : Matrix (Fin p) (Fin p) ℝ), Q * Q.transpose = 1 ∧ Q.submatrix (Fin.castLE hqp) id = V

A real matrix with orthonormal rows is a row selection of an orthogonal matrix. If V * Vᵀ = 1 for a q × p matrix V with q ≤ p, then V consists of the first q rows of an orthogonal p × p matrix.

theorem Matrix.exists_mul_transpose_eq_one_and_eq_mul_submatrix_castLE {p q : ℕ} (M : Matrix (Fin q) (Fin p) ℝ) (hqp : q ≤ p) {T : Matrix (Fin q) (Fin q) ℝ} (hTdet : T.det ≠ 0) (hT : T * T.transpose = M * M.transpose) : ∃ (Q : Matrix (Fin p) (Fin p) ℝ), Q * Q.transpose = 1 ∧ M = T * Q.submatrix (Fin.castLE hqp) id

A matrix of full row rank is a square factor of its Gram matrix times a row selection of an orthogonal matrix. If T * Tᵀ = M * Mᵀ with T invertible, then T⁻¹ * M has orthonormal rows, hence selects the first q rows of an orthogonal matrix Q, and M = T * Q.submatrix _ id. This is the LQ decomposition of a matrix of full row rank.