Triangular matrices

Mathlib's Matrix.BlockTriangular API computes determinants and inverses of triangular matrices, but not their individual diagonal entries. This file supplies the facts that consumers keep needing: on the diagonal, a product of triangular matrices multiplies entrywise, because ∑ k, A i k * B k i has a single surviving term — and consequences of that, such as the diagonal of an inverse. It also proves uniqueness of a lower-triangular Gram factor with positive diagonal, defines upper-unitriangular matrices, and proves that strictly upper-triangular matrices are nilpotent.

The diagonal results are stated directly for Matrix.IsUpperTriangular and Matrix.IsLowerTriangular rather than through membership in the Borel subalgebra, since there is no Lie theory in them. It is Matrix.mul_apply_diag_of_isUpperTriangular that TauCeti.Algebra.Lie.GeneralLinear.Borel consumes in that form, and all of them are available to modules with no business importing Lie-algebra theory.

Main results

• Matrix.BlockTriangular.det_eq_prod_diag — a matrix that is block triangular for an injective ranking of its indices has the product of its diagonal entries as determinant.
• Matrix.mul_apply_diag_of_isUpperTriangular — the diagonal of a product of upper-triangular matrices is the pointwise product of the diagonals.
• Matrix.mul_apply_diag_of_isLowerTriangular — the corresponding formula for lower-triangular matrices.
• Matrix.IsLowerTriangular.eq_one_of_mul_transpose_self_eq_one — a lower-triangular orthogonal matrix with nonnegative diagonal is the identity.
• Matrix.IsLowerTriangular.eq_of_mul_transpose_self_eq — lower-triangular matrices with positive diagonal are determined by their product with their transpose.
• Matrix.IsLowerTriangular.submatrix_castLE_mul_transpose — a leading principal submatrix of a lower-triangular Gram matrix is the Gram matrix of the corresponding submatrix.
• Matrix.pow_apply_diag_of_isUpperTriangular — the diagonal of a power of an upper-triangular matrix is the corresponding power of the diagonal entry.
• Matrix.isUpperUnitriangular_geom_sum_of_isUpperTriangular_of_diag_eq_zero — the geometric series in a strictly upper-triangular matrix is upper unitriangular, for any truncation that is positive whenever the index type is inhabited, and Matrix.isUpperUnitriangular_geom_sum_card_of_isUpperTriangular_of_diag_eq_zero for the truncation at the size of the matrix.
• Matrix.inv_apply_diag_mul_of_isUpperTriangular — on the diagonal, the inverse inverts entrywise: M⁻¹ i i * M i i = 1.
• Matrix.inv_apply_diag_of_isUpperTriangular — where an upper-triangular matrix carries a 1 on the diagonal, so does its inverse.
• Matrix.IsUpperUnitriangular — an upper-triangular matrix with diagonal one.
• Matrix.IsUpperUnitriangular.ext — upper-unitriangular matrices are determined by their entries strictly above the diagonal.
• Matrix.IsUpperUnitriangular.det_eq_one — an upper-unitriangular matrix has determinant one.
• Matrix.isNilpotent_of_isUpperTriangular_of_diag_eq_zero — strict upper triangularity implies nilpotence.
• TauCeti.isUpperTriangular_transvection_iff — a transvection with its off-diagonal entry strictly below the diagonal is upper triangular exactly when its parameter vanishes.
• TauCeti.vecMul_injective_of_submatrix_isUpperTriangular — a rectangular matrix has injective row multiplication when a square column selection is upper triangular with nonzero diagonal.

theorem Matrix.BlockTriangular.det_eq_prod_diag {ι : Type u_3} {α : Type u_4} {S : Type u_5} [Fintype ι] [DecidableEq ι] [LinearOrder α] [CommRing S] {N : Matrix ι ι S} {b : ι → α} (hN : N.BlockTriangular b) (hb : Function.Injective b) : N.det = ∏ i : ι, N i i

A matrix that is block triangular for an injective ranking of its indices has the product of its diagonal entries as determinant: an injective ranking cuts it into singleton blocks.

def Matrix.IsUpperUnitriangular {R : Type u_1} {m : Type u_2} [LT m] [Zero R] [One R] (M : Matrix m m R) : Prop

A square matrix is upper unitriangular when it is upper triangular and every diagonal entry is one.

Equations

• M.IsUpperUnitriangular = (M.IsUpperTriangular ∧ ∀ (i : m), M i i = 1)

theorem Matrix.isUpperUnitriangular_def {R : Type u_1} {m : Type u_2} [LT m] [Zero R] [One R] (M : Matrix m m R) : M.IsUpperUnitriangular ↔ M.IsUpperTriangular ∧ ∀ (i : m), M i i = 1

Upper unitriangularity consists of upper triangularity and diagonal entries equal to one.

theorem Matrix.IsUpperUnitriangular.isUpperTriangular {R : Type u_1} {m : Type u_2} [LT m] [Zero R] [One R] {M : Matrix m m R} (hM : M.IsUpperUnitriangular) : M.IsUpperTriangular

An upper-unitriangular matrix is upper triangular.

theorem Matrix.IsUpperUnitriangular.apply_diag {R : Type u_1} {m : Type u_2} [LT m] [Zero R] [One R] {M : Matrix m m R} (hM : M.IsUpperUnitriangular) (i : m) : M i i = 1

Every diagonal entry of an upper-unitriangular matrix is one.

theorem Matrix.IsUpperUnitriangular.ext {R : Type u_1} {m : Type u_2} [LinearOrder m] [Zero R] [One R] {M N : Matrix m m R} (hM : M.IsUpperUnitriangular) (hN : N.IsUpperUnitriangular) (h : ∀ (i j : m), i < j → M i j = N i j) : M = N

Two upper-unitriangular matrices are equal if their entries strictly above the diagonal agree.

theorem Matrix.IsUpperUnitriangular.det_eq_one {R : Type u_1} {m : Type u_2} [Fintype m] [LinearOrder m] [CommRing R] {M : Matrix m m R} (hM : M.IsUpperUnitriangular) : M.det = 1

The determinant of an upper-unitriangular matrix is one.

theorem Matrix.IsUpperUnitriangular.isUnit_det {R : Type u_1} {m : Type u_2} [Fintype m] [LinearOrder m] [CommRing R] {M : Matrix m m R} (hM : M.IsUpperUnitriangular) : IsUnit M.det

The determinant of an upper-unitriangular matrix is a unit.

@[simp]

theorem Matrix.isUpperUnitriangular_one {R : Type u_1} {m : Type u_2} [Preorder m] [DecidableEq m] [Zero R] [One R] : IsUpperUnitriangular 1

The identity matrix is upper unitriangular.

theorem Matrix.IsUpperUnitriangular.map {R : Type u_1} {m : Type u_2} {S : Type u_3} {F : Type u_4} [LT m] [Zero R] [One R] [Zero S] [One S] [FunLike F R S] [ZeroHomClass F R S] [OneHomClass F R S] (f : F) {M : Matrix m m R} (hM : M.IsUpperUnitriangular) : (M.map ⇑f).IsUpperUnitriangular

Applying a zero- and one-preserving map entrywise preserves upper-unitriangular matrices.

theorem Matrix.pow_apply_eq_zero_of_isUpperTriangular_of_diag_eq_zero {S : Type u_3} [Semiring S] {n : ℕ} {M : Matrix (Fin n) (Fin n) S} (htri : M.IsUpperTriangular) (hdiag : ∀ (i : Fin n), M i i = 0) (k : ℕ) (i j : Fin n) (hji : ↑j < ↑i + k) : (M ^ k) i j = 0

For a strictly upper-triangular matrix, (M ^ k) i j = 0 whenever j < i + k.

theorem Matrix.pow_card_eq_zero_of_isUpperTriangular_of_diag_eq_zero {m : Type u_2} {S : Type u_3} [Semiring S] [Fintype m] [LinearOrder m] {M : Matrix m m S} (htri : M.IsUpperTriangular) (hdiag : ∀ (i : m), M i i = 0) : M ^ Fintype.card m = 0

A strictly upper-triangular matrix has power equal to zero at the cardinality of its index type.

theorem Matrix.isNilpotent_of_isUpperTriangular_of_diag_eq_zero {m : Type u_2} {S : Type u_3} [Semiring S] [Fintype m] [LinearOrder m] {M : Matrix m m S} (htri : M.IsUpperTriangular) (hdiag : ∀ (i : m), M i i = 0) : IsNilpotent M

A strictly upper-triangular square matrix is nilpotent.

theorem Matrix.mul_apply_diag_of_isUpperTriangular {R : Type u_3} [NonUnitalNonAssocSemiring R] {n : Type u_4} [Fintype n] [LinearOrder n] {A B : Matrix n n R} (hA : A.IsUpperTriangular) (hB : B.IsUpperTriangular) (i : n) : (A * B) i i = A i i * B i i

The diagonal of a product of upper-triangular matrices is the pointwise product of the diagonals.

theorem Matrix.mul_apply_diag_of_isLowerTriangular {R : Type u_3} [NonUnitalNonAssocSemiring R] {n : Type u_4} [Fintype n] [LinearOrder n] {A B : Matrix n n R} (hA : A.IsLowerTriangular) (hB : B.IsLowerTriangular) (i : n) : (A * B) i i = A i i * B i i

The diagonal of a product of lower-triangular matrices is the pointwise product of the diagonals.

theorem Matrix.IsLowerTriangular.submatrix_castLE_mul_transpose {R : Type u_3} [NonUnitalNonAssocSemiring R] {p q : ℕ} {L : Matrix (Fin p) (Fin p) R} (hL : L.IsLowerTriangular) (hqp : q ≤ p) : (L * L.transpose).submatrix (Fin.castLE hqp) (Fin.castLE hqp) = L.submatrix (Fin.castLE hqp) (Fin.castLE hqp) * (L.submatrix (Fin.castLE hqp) (Fin.castLE hqp)).transpose

The leading principal submatrix of a lower-triangular Gram matrix is a Gram matrix. The first q rows of a lower-triangular matrix vanish outside their first q columns, so the leading q × q block of L * Lᵀ sees only the leading q × q block of L.

theorem Matrix.IsLowerTriangular.eq_one_of_mul_transpose_self_eq_one {n : Type u_4} [Fintype n] [LinearOrder n] {K : Type u_5} [CommRing K] [LinearOrder K] [IsStrictOrderedRing K] {Q : Matrix n n K} (hQ : Q.IsLowerTriangular) (hQnonneg : ∀ (i : n), 0 ≤ Q i i) (hQorth : Q * Q.transpose = 1) : Q = 1

A lower-triangular matrix over a linearly ordered commutative ring with nonnegative diagonal whose product with its transpose is the identity is itself the identity.

theorem Matrix.IsLowerTriangular.eq_of_mul_transpose_self_eq {n : Type u_4} [Fintype n] [LinearOrder n] {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {L M : Matrix n n K} (hL : L.IsLowerTriangular) (hM : M.IsLowerTriangular) (hLpos : ∀ (i : n), 0 < L i i) (hMpos : ∀ (i : n), 0 < M i i) (hgram : L * L.transpose = M * M.transpose) : L = M

Lower-triangular matrices over an ordered field with positive diagonal are determined by their Gram matrices L * Lᵀ.

Equivalently, the map L ↦ L * Lᵀ is injective on positive-diagonal lower-triangular matrices. The empty index type is included.

@[simp]

theorem Matrix.pow_apply_diag_of_isUpperTriangular {n : Type u_4} [Fintype n] [LinearOrder n] {T : Type u_5} [Semiring T] {M : Matrix n n T} (hM : M.IsUpperTriangular) (k : ℕ) (i : n) : (M ^ k) i i = M i i ^ k

The diagonal of a power of an upper-triangular matrix is the corresponding power of the diagonal entry.

theorem Matrix.isUpperUnitriangular_geom_sum_of_isUpperTriangular_of_diag_eq_zero {n : Type u_4} [Fintype n] [LinearOrder n] {T : Type u_5} [Semiring T] {M : Matrix n n T} (hM : M.IsUpperTriangular) (hdiag : ∀ (i : n), M i i = 0) {k : ℕ} (hk : Nonempty n → 0 < k) : (∑ j ∈ Finset.range k, M ^ j).IsUpperUnitriangular

A geometric series in a strictly upper-triangular matrix is upper unitriangular, for any truncation k that is positive whenever the index type is inhabited.

Over an empty index type both conditions are vacuous, so nothing is asked of k there.

theorem Matrix.isUpperUnitriangular_geom_sum_card_of_isUpperTriangular_of_diag_eq_zero {n : Type u_4} [Fintype n] [LinearOrder n] {T : Type u_5} [Semiring T] {M : Matrix n n T} (hM : M.IsUpperTriangular) (hdiag : ∀ (i : n), M i i = 0) : (∑ j ∈ Finset.range (Fintype.card n), M ^ j).IsUpperUnitriangular

The geometric series in a strictly upper-triangular matrix, truncated at the size of the matrix, is upper unitriangular.

This is the truncation that appears when inverting 1 - M, being the exponent at which M has already died (Matrix.pow_card_eq_zero_of_isUpperTriangular_of_diag_eq_zero).

theorem Matrix.inv_apply_diag_mul_of_isUpperTriangular {n : Type u_4} [Fintype n] [LinearOrder n] {S : Type u_5} [CommRing S] {M : Matrix n n S} [Invertible M] (hM : M.IsUpperTriangular) (i : n) : M⁻¹ i i * M i i = 1

On the diagonal, the inverse of an invertible upper-triangular matrix inverts entrywise: M⁻¹ i i * M i i = 1.

theorem Matrix.inv_apply_diag_of_isUpperTriangular {n : Type u_4} [Fintype n] [LinearOrder n] {S : Type u_5} [CommRing S] {M : Matrix n n S} [Invertible M] (hM : M.IsUpperTriangular) {i : n} (hdiag : M i i = 1) : M⁻¹ i i = 1

Where an invertible upper-triangular matrix has a 1 on the diagonal, so does its inverse. The hypothesis is needed only at the entry asked about.

theorem Matrix.IsUpperUnitriangular.mul {T : Type u_6} {p : Type u_7} [NonAssocSemiring T] [Fintype p] [LinearOrder p] {M N : Matrix p p T} (hM : M.IsUpperUnitriangular) (hN : N.IsUpperUnitriangular) : (M * N).IsUpperUnitriangular

A product of upper-unitriangular matrices is upper unitriangular.

theorem Matrix.IsUpperUnitriangular.inv {T : Type u_6} {p : Type u_7} [CommRing T] [Fintype p] [LinearOrder p] {M : Matrix p p T} [Invertible M] (hM : M.IsUpperUnitriangular) : M⁻¹.IsUpperUnitriangular

The inverse of an invertible upper-unitriangular matrix is upper unitriangular.

theorem Matrix.IsUpperUnitriangular.isNilpotent_sub_one {T : Type u_6} {p : Type u_7} [Ring T] [Fintype p] [LinearOrder p] {M : Matrix p p T} (hM : M.IsUpperUnitriangular) : IsNilpotent (M - 1)

Subtracting the identity from an upper-unitriangular matrix gives a nilpotent matrix.

@[simp]

theorem TauCeti.isUpperTriangular_transvection_iff {n : Type u_1} [DecidableEq n] [Preorder n] {A : Type u_2} [CommRing A] {i j : n} (hij : j < i) (c : A) : (Matrix.transvection i j c).IsUpperTriangular ↔ c = 0

A transvection whose off-diagonal entry lies strictly below the diagonal is upper triangular exactly when its parameter vanishes. The complementary case, an entry on or above the diagonal, is Mathlib's Matrix.blockTriangular_transvection.

theorem TauCeti.vecMul_injective_of_submatrix_isUpperTriangular {K : Type u_1} {ι : Type u_2} {κ : Type u_3} [Field K] [Fintype ι] [LinearOrder ι] {M : Matrix ι κ K} (e : ι → κ) (hlt : ∀ (i j : ι), j < i → M i (e j) = 0) (hdiag : ∀ (i : ι), M i (e i) ≠ 0) : Function.Injective fun (v : ι → K) => Matrix.vecMul v M

A triangular selection of coordinates makes the rows independent. If some choice e of a coordinate for each row makes the matrix upper triangular - M i (e j) = 0 for j < i - with a nonzero diagonal, then the rows are independent: the selected columns form a square submatrix whose determinant is the product of that diagonal.