Extending matrices on configurations by one coordinate

Matrix.extendLast extends a matrix indexed by Fin m → ι to one indexed by Fin (m + 1) → ι, for a finite type ι, acting as the identity on the last coordinate. It is the Kronecker product 1 ⊗ₖ X, reindexed along Fin.snocEquiv. The construction composes Mathlib's tensor-product inclusion, Kronecker algebra equivalence, and matrix reindexing equivalence.

def Matrix.extendLast {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] [DecidableEq ι] {m : ℕ} : Matrix (Fin m → ι) (Fin m → ι) R →ₐ[R] Matrix (Fin (m + 1) → ι) (Fin (m + 1) → ι) R

A matrix on m coordinates with values in ι as a matrix on m + 1 coordinates, acting as the identity on the last one: the Kronecker product 1 ⊗ₖ X, reindexed along Fin.snocEquiv. Its entry at s and t is the entry of the original matrix at their first m coordinates when their last coordinates agree, and 0 otherwise.

Equations

• Matrix.extendLast = (↑(Matrix.reindexAlgEquiv R R (Fin.snocEquiv fun (x : Fin (m + 1)) => ι))).comp ((↑(Matrix.kroneckerAlgEquiv ι (Fin m → ι) R)).comp Algebra.TensorProduct.includeRight)

theorem Matrix.extendLast_eq {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] [DecidableEq ι] {m : ℕ} (X : Matrix (Fin m → ι) (Fin m → ι) R) : extendLast X = (reindex (Fin.snocEquiv fun (x : Fin (m + 1)) => ι) (Fin.snocEquiv fun (x : Fin (m + 1)) => ι)) (kroneckerMap (fun (x1 x2 : R) => x1 * x2) 1 X)

extendLast X is the Kronecker product of the identity on the last coordinate with X.

@[simp]

theorem Matrix.extendLast_apply {R : Type u_1} {ι : Type u_2} [CommSemiring R] [Fintype ι] [DecidableEq ι] {m : ℕ} (X : Matrix (Fin m → ι) (Fin m → ι) R) (s t : Fin (m + 1) → ι) : extendLast X s t = if s (Fin.last m) = t (Fin.last m) then X (Fin.init s) (Fin.init t) else 0