Documentation

TauCeti.LinearAlgebra.Matrix.Step

Matrices with at most one nonzero entry in each column #

A step matrix is a matrix each of whose columns is a scalar multiple of a coordinate vector: the bth column is c b times the t bth coordinate vector, for a target function t and a coefficient function c. Permutation matrices, diagonal matrices and the matrix units are step matrices, and so is the matrix of any linear map that carries each vector of a basis to a multiple of a vector of another basis, a situation common in explicit representation theory.

The property is columnwise, so the row and column index types are allowed to differ: a step matrix in Matrix m n R has target function n → m. The identity and the diagonal matrices are of course square.

This file records the property as Matrix.IsStep and the closure properties that make it useful for computation: a product of step matrices is the step matrix of the composed targets and the coefficients multiplied along the way, and entrywise application of a ring morphism preserves the property. Since each entry of such a product is a single product of table lookups rather than a sum over an index type, identities between explicitly tabulated step matrices reduce to finitely many entrywise identities that need no summation.

The property is stated as the conjunction of the value at the target of each column and the vanishing of that column elsewhere, so that it needs no decidable equality on the rows; the entrywise description by a table lookup is recovered as Matrix.isStep_iff over rows that do have decidable equality.

The target of a column with coefficient zero is unconstrained, so the pair (t, c) is not determined by the matrix; every statement below takes the witnessing pair as data.

The step-matrix API is adapted from the formalization in Tau Ceti PR #6711, the special isogeny of type F₄ in characteristic two on matrices.

Main definitions #

Main results #

source
def Matrix.IsStep {m : Type u_2} {n : Type u_3} {R : Type u_4} [Zero R] (M : Matrix m n R) (t : n → m) (c : n → R) :
Prop

A matrix is a step matrix for a target function t and a coefficient function c when its bth column is c b times the t bth coordinate vector.

Equations
  • M.IsStep t c = ((∀ (b : n), M (t b) b = c b) ∧ ∀ (a : m) (b : n), a ≠ t b → M a b = 0)
Instances For
    source
    theorem Matrix.IsStep.apply_target {m : Type u_2} {n : Type u_3} {R : Type u_4} [Zero R] {M : Matrix m n R} {t : n → m} {c : n → R} (h : M.IsStep t c) (b : n) :
    M (t b) b = c b

    The entry of a step matrix at the target of its column is the coefficient of that column.

    source
    theorem Matrix.IsStep.apply_of_ne {m : Type u_2} {n : Type u_3} {R : Type u_4} [Zero R] {M : Matrix m n R} {t : n → m} {c : n → R} (h : M.IsStep t c) {a : m} {b : n} (hab : a ≠ t b) :
    M a b = 0

    The entry of a step matrix at a row other than the target of its column is zero.

    source
    theorem Matrix.isStep_of_apply_target_of_apply_of_ne {m : Type u_2} {n : Type u_3} {R : Type u_4} [Zero R] {M : Matrix m n R} {t : n → m} {c : n → R} (ht : ∀ (b : n), M (t b) b = c b) (h0 : ∀ (a : m) (b : n), a ≠ t b → M a b = 0) :
    M.IsStep t c

    The introduction form: a matrix that takes the prescribed coefficient at the target of each column and vanishes elsewhere in that column is a step matrix.

    source
    theorem Matrix.isStep_iff {m : Type u_2} {n : Type u_3} {R : Type u_4} [Zero R] {M : Matrix m n R} {t : n → m} {c : n → R} [DecidableEq m] :
    M.IsStep t c ↔ ∀ (a : m) (b : n), M a b = if a = t b then c b else 0

    The entrywise description of a step matrix by a table lookup.

    source
    theorem Matrix.isStep_of_apply {m : Type u_2} {n : Type u_3} {R : Type u_4} [Zero R] {M : Matrix m n R} {t : n → m} {c : n → R} [DecidableEq m] (h : ∀ (a : m) (b : n), M a b = if a = t b then c b else 0) :
    M.IsStep t c

    The introduction form: a matrix whose entries are the table lookups is a step matrix.

    source
    theorem Matrix.IsStep.apply {m : Type u_2} {n : Type u_3} {R : Type u_4} [Zero R] {M : Matrix m n R} {t : n → m} {c : n → R} [DecidableEq m] (h : M.IsStep t c) (a : m) (b : n) :
    M a b = if a = t b then c b else 0

    The elimination form: every entry of a step matrix is a table lookup.

    source
    @[simp]
    theorem Matrix.isStep_diagonal {n : Type u_3} {R : Type u_4} [DecidableEq n] [Zero R] (d : n → R) :
    (diagonal d).IsStep id d

    A diagonal matrix is the step matrix of the identity target and its own diagonal.

    source
    @[simp]
    theorem Matrix.isStep_one {n : Type u_3} {R : Type u_4} [DecidableEq n] [Zero R] [One R] :
    IsStep 1 id 1

    The identity matrix is the step matrix of the identity target and the constant coefficient one.

    source
    theorem Matrix.IsStep.mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_4} [Fintype m] [NonUnitalNonAssocSemiring R] {M : Matrix l m R} {N : Matrix m n R} {t : m → l} {t' : n → m} {c : m → R} {c' : n → R} (hM : M.IsStep t c) (hN : N.IsStep t' c') :
    (M * N).IsStep (t ∘ t') fun (b : n) => c (t' b) * c' b

    A product of step matrices is a step matrix, with the composite target function and with each coefficient the product of the two coefficients met along the way.

    source
    theorem Matrix.IsStep.map {m : Type u_2} {n : Type u_3} {R : Type u_4} {S : Type u_5} [Zero R] [Zero S] {M : Matrix m n R} {t : n → m} {c : n → R} (h : M.IsStep t c) (f : R → S) (hf : f 0 = 0) :
    (M.map f).IsStep t fun (b : n) => f (c b)

    Entrywise application of a zero-preserving map to a step matrix gives the step matrix of the same target and the transformed coefficients. Only the value at zero is used, so no additive or multiplicative structure is required of the map.