Uniqueness of unitriangular Gram factors

Let ι be a finite partially ordered set. Call a square matrix U indexed by ι unitriangular when its diagonal entries are 1 and U i j = 0 unless j ≤ i. Such a factor is determined by its Gram matrix Uᵀ * U: if U and V are unitriangular and Uᵀ * U = Vᵀ * V, then U = V (TauCeti.eq_of_transpose_mul_self_eq). This is the uniqueness half of the LDLᵀ decomposition with trivial diagonal, for a partial rather than a linear order and over an arbitrary ring.

The entries are recovered row by row, from the top of the order down. In the (j, i) entry ∑ₗ U l j * U l i of the Gram matrix, the term l = i is U i j, and every other nonzero term has i < l, so it involves only rows above i.

A typical use compares two transition matrices that are unitriangular for the dominance order on partitions and have the same Gram matrix, as in the proof of Young's rule.

Main results

• TauCeti.eq_of_transpose_mul_self_eq: unitriangular matrices with the same Gram matrix are equal.

theorem TauCeti.eq_of_transpose_mul_self_eq {ι : Type u_1} {R : Type u_2} [Fintype ι] [PartialOrder ι] [Ring R] {U V : Matrix ι ι R} (hU : ∀ (i j : ι), U i j ≠ 0 → j ≤ i) (hV : ∀ (i j : ι), V i j ≠ 0 → j ≤ i) (hU₁ : ∀ (i : ι), U i i = 1) (hV₁ : ∀ (i : ι), V i i = 1) (h : U.transpose * U = V.transpose * V) : U = V

A unitriangular matrix is determined by its Gram matrix: if U and V have diagonal entries 1, vanish at (i, j) unless j ≤ i for a partial order on the finite index type, and satisfy Uᵀ * U = Vᵀ * V, then U = V.