Documentation

TauCeti.LinearAlgebra.Matrix.Kronecker.Power

Kronecker powers of matrices #

For a matrix A with rows indexed by m, columns indexed by n and a finite type κ, the Kronecker power Matrix.kroneckerPower κ A is the matrix with rows indexed by κ → m and columns indexed by κ → n whose (v, u) entry is ∏ i, A (v i) (u i). It is the matrix of A acting in every factor of the κ-indexed tensor power, in the monomial bases.

The Kronecker power is multiplicative and commutes with transposition, so if Aᵀ * A = 1 then the Kronecker power satisfies the same identity. The Kronecker power of a diagonal matrix is diagonal, and that of the matrix of an equivalence f is the matrix of the equivalence v ↦ f ∘ v of index functions.

Main definitions #

Main results #

source
def Matrix.kroneckerPower {R : Type u_1} {m : Type u_3} {n : Type u_4} (κ : Type u_5) [CommMonoid R] [Fintype κ] (A : Matrix m n R) :
Matrix (κ → m) (κ → n) R

The Kronecker power of a matrix A : Matrix m n R: the matrix with rows indexed by κ → m and columns indexed by κ → n whose (v, u) entry is ∏ i, A (v i) (u i), the matrix of A acting in every factor of the κ-indexed tensor power.

Instances For
    source
    @[simp]
    theorem Matrix.kroneckerPower_apply {R : Type u_1} {m : Type u_3} {n : Type u_4} (κ : Type u_5) [CommMonoid R] [Fintype κ] (A : Matrix m n R) (v : κ → m) (u : κ → n) :
    kroneckerPower κ A v u = ∏ i : κ, A (v i) (u i)
    source
    @[simp]
    theorem Matrix.transpose_kroneckerPower {R : Type u_1} {m : Type u_3} {n : Type u_4} {κ : Type u_5} [CommMonoid R] [Fintype κ] (A : Matrix m n R) :
    (kroneckerPower κ A).transpose = kroneckerPower κ A.transpose

    The Kronecker power commutes with transposition.

    source
    @[simp]
    theorem Matrix.kroneckerPower_one {R : Type u_1} {n : Type u_4} {κ : Type u_5} [CommMonoidWithZero R] [DecidableEq n] [Fintype κ] :
    kroneckerPower κ 1 = 1

    The Kronecker power of the identity matrix is the identity matrix.

    source
    theorem Matrix.kroneckerPower_mul {R : Type u_1} {l : Type u_2} {m : Type u_3} {n : Type u_4} {κ : Type u_5} [CommSemiring R] [Fintype m] [Fintype κ] [DecidableEq κ] (A : Matrix l m R) (B : Matrix m n R) :
    kroneckerPower κ (A * B) = kroneckerPower κ A * kroneckerPower κ B

    The Kronecker power is multiplicative: the (v, u) entry of A^{⊗κ} * B^{⊗κ} expands, by distributing the product over the sums, into the product of the entries of A * B.

    source
    theorem Matrix.transpose_kroneckerPower_mul_self {R : Type u_1} {n : Type u_4} {κ : Type u_5} [CommSemiring R] [Fintype n] [DecidableEq n] [Fintype κ] [DecidableEq κ] {A : Matrix n n R} (hA : A.transpose * A = 1) :
    (kroneckerPower κ A).transpose * kroneckerPower κ A = 1

    The Kronecker power of a matrix A with Aᵀ * A = 1 satisfies the same identity.

    source
    theorem Matrix.toMatrix_piTensorProductMap_mulVecLin {R : Type u_1} {m : Type u_3} {κ : Type u_5} [CommSemiring R] [Fintype m] [DecidableEq m] [Fintype κ] [DecidableEq κ] (A : Matrix m m R) :
    (LinearMap.toMatrix (Basis.piTensorProduct fun (x : κ) => Pi.basisFun R m) (Basis.piTensorProduct fun (x : κ) => Pi.basisFun R m)) (PiTensorProduct.map fun (x : κ) => A.mulVecLin) = kroneckerPower κ A

    The Kronecker power is the matrix of the tensor power. The matrix of A acting in every factor of the κ-indexed tensor power of m → R, in the monomial basis built from the standard bases, is the Kronecker power of A.

    source
    theorem Matrix.apply_comp_mul_prod_of_commute_kroneckerPower {R : Type u_1} {m : Type u_3} {κ : Type u_5} [CommSemiring R] [Fintype m] [DecidableEq m] [Fintype κ] [DecidableEq κ] {M : Matrix (κ → m) (κ → m) R} (π : Equiv.Perm m) (d : m → R) (hM : Commute M (kroneckerPower κ (of fun (x y : m) => if x = π y then d y else 0))) (v u : κ → m) :
    M (⇑π ∘ v) (⇑π ∘ u) * ∏ i : κ, d (u i) = (∏ i : κ, d (v i)) * M v u

    Commuting with the Kronecker power of a monomial matrix. Let A be the monomial matrix sending the y-th basis vector to d y times the π y-th one, so A x y = d y when x = π y and 0 otherwise. If M commutes with the Kronecker power of A, then relabelling both indices of an entry of M by π satisfies the cross-multiplied identity M (π ∘ v) (π ∘ u) * ∏ i, d (u i) = (∏ i, d (v i)) * M v u, with the column weight ∏ i, d (u i) on the left and the row weight ∏ i, d (v i) on the right. When the column weight is invertible, the relabelled entry is therefore the original entry multiplied by the row weight and divided by the column weight.

    source
    @[simp]
    theorem Matrix.kroneckerPower_diagonal {R : Type u_1} {n : Type u_4} {κ : Type u_5} [CommMonoidWithZero R] [DecidableEq n] [Fintype κ] (d : n → R) :
    kroneckerPower κ (diagonal d) = diagonal fun (v : κ → n) => ∏ i : κ, d (v i)

    The Kronecker power of a diagonal matrix is the diagonal matrix with entry ∏ i, d (v i) at the index function v.

    source
    @[simp]
    theorem Matrix.kroneckerPower_toMatrix_toPEquiv {R : Type u_1} {m : Type u_3} {n : Type u_4} {κ : Type u_5} [CommMonoidWithZero R] [DecidableEq n] [Fintype κ] (f : m ≃ n) :
    kroneckerPower κ f.toPEquiv.toMatrix = (Equiv.piCongrRight fun (x : κ) => f).toPEquiv.toMatrix

    The Kronecker power of the matrix of an equivalence f : m ≃ n is the matrix of the equivalence v ↦ f ∘ v it induces on the index functions.