# mathlibdocumentation

data.matrix.kronecker

# Kronecker product of matrices #

This defines the Kronecker product.

## Main definitions #

• matrix.kronecker_map: A generalization of the Kronecker product: given a map f : α → β → γ and matrices A and B with coefficients in α and β, respectively, it is defined as the matrix with coefficients in γ such that kronecker_map f A B (i₁, i₂) (j₁, j₂) = f (A i₁ j₁) (B i₁ j₂).
• matrix.kronecker_map_bilinear: when f is bilinear, so is kronecker_map f.

## Specializations #

• matrix.kronecker: An alias of kronecker_map (*). Prefer using the notation.

• matrix.kronecker_bilinear: matrix.kronecker is bilinear

• matrix.kronecker_tmul: An alias of kronecker_map (⊗ₜ). Prefer using the notation.

• matrix.kronecker_tmul_bilinear: matrix.tmul_kronecker is bilinear

## Notations #

These require open_locale kronecker:

• A ⊗ₖ B for kronecker_map (*) A B. Lemmas about this notation use the token kronecker.
• A ⊗ₖₜ B and A ⊗ₖₜ[R] B for kronecker_map (⊗ₜ) A B. Lemmas about this notation use the token kronecker_tmul.
@[simp]
def matrix.kronecker_map {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (f : α → β → γ) (A : m α) (B : p β) :
matrix (l × n) (m × p) γ

Produce a matrix with f applied to every pair of elements from A and B.

Equations
theorem matrix.kronecker_map_transpose {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (f : α → β → γ) (A : m α) (B : p β) :
= B)
theorem matrix.kronecker_map_map_left {α : Type u_2} {α' : Type u_3} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (f : α' → β → γ) (g : α → α') (A : m α) (B : p β) :
(A.map g) B = matrix.kronecker_map (λ (a : α) (b : β), f (g a) b) A B
theorem matrix.kronecker_map_map_right {α : Type u_2} {β : Type u_4} {β' : Type u_5} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (f : α → β' → γ) (g : β → β') (A : m α) (B : p β) :
(B.map g) = matrix.kronecker_map (λ (a : α) (b : β), f a (g b)) A B
theorem matrix.kronecker_map_map {α : Type u_2} {β : Type u_4} {γ : Type u_6} {γ' : Type u_7} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (f : α → β → γ) (g : γ → γ') (A : m α) (B : p β) :
B).map g = matrix.kronecker_map (λ (a : α) (b : β), g (f a b)) A B
@[simp]
theorem matrix.kronecker_map_zero_left {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [has_zero α] [has_zero γ] (f : α → β → γ) (hf : ∀ (b : β), f 0 b = 0) (B : p β) :
B = 0
@[simp]
theorem matrix.kronecker_map_zero_right {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [has_zero β] [has_zero γ] (f : α → β → γ) (hf : ∀ (a : α), f a 0 = 0) (A : m α) :
0 = 0
theorem matrix.kronecker_map_add_left {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [has_add α] [has_add γ] (f : α → β → γ) (hf : ∀ (a₁ a₂ : α) (b : β), f (a₁ + a₂) b = f a₁ b + f a₂ b) (A₁ A₂ : m α) (B : p β) :
(A₁ + A₂) B = B + B
theorem matrix.kronecker_map_add_right {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [has_add β] [has_add γ] (f : α → β → γ) (hf : ∀ (a : α) (b₁ b₂ : β), f a (b₁ + b₂) = f a b₁ + f a b₂) (A : m α) (B₁ B₂ : p β) :
(B₁ + B₂) = B₁ + B₂
theorem matrix.kronecker_map_smul_left {R : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [ α] [ γ] (f : α → β → γ) (r : R) (hf : ∀ (a : α) (b : β), f (r a) b = r f a b) (A : m α) (B : p β) :
(r A) B = r B
theorem matrix.kronecker_map_smul_right {R : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [ β] [ γ] (f : α → β → γ) (r : R) (hf : ∀ (a : α) (b : β), f a (r b) = r f a b) (A : m α) (B : p β) :
(r B) = r B
theorem matrix.kronecker_map_diagonal_diagonal {α : Type u_2} {β : Type u_4} {γ : Type u_6} {m : Type u_9} {n : Type u_10} [has_zero α] [has_zero β] [has_zero γ] [decidable_eq m] [decidable_eq n] (f : α → β → γ) (hf₁ : ∀ (b : β), f 0 b = 0) (hf₂ : ∀ (a : α), f a 0 = 0) (a : m → α) (b : n → β) :
= matrix.diagonal (λ (mn : m × n), f (a mn.fst) (b mn.snd))
@[simp]
theorem matrix.kronecker_map_one_one {α : Type u_2} {β : Type u_4} {γ : Type u_6} {m : Type u_9} {n : Type u_10} [has_zero α] [has_zero β] [has_zero γ] [has_one α] [has_one β] [has_one γ] [decidable_eq m] [decidable_eq n] (f : α → β → γ) (hf₁ : ∀ (b : β), f 0 b = 0) (hf₂ : ∀ (a : α), f a 0 = 0) (hf₃ : f 1 1 = 1) :
1 = 1
theorem matrix.kronecker_map_reindex {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} {l' : Type u_14} {m' : Type u_15} {n' : Type u_16} {p' : Type u_17} (f : α → β → γ) (el : l l') (em : m m') (en : n n') (ep : p p') (M : m α) (N : p β) :
( em) M) ( ep) N) = (matrix.reindex (el.prod_congr en) (em.prod_congr ep)) N)
theorem matrix.kronecker_map_reindex_left {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {l' : Type u_14} {m' : Type u_15} {n' : Type u_16} (f : α → β → γ) (el : l l') (em : m m') (M : m α) (N : n' β) :
( em) M) N = (matrix.reindex (el.prod_congr (equiv.refl n)) (em.prod_congr (equiv.refl n'))) N)
theorem matrix.kronecker_map_reindex_right {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {l' : Type u_14} {m' : Type u_15} {n' : Type u_16} (f : α → β → γ) (em : m m') (en : n n') (M : l' α) (N : n β) :
theorem matrix.kronecker_map_assoc {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} {q : Type u_12} {r : Type u_13} {δ : Type u_1} {ξ : Type u_3} {ω : Type u_5} {ω' : Type u_7} (f : α → β → γ) (g : γ → δ → «ω») (f' : α → ξ → ω') (g' : β → δ → ξ) (A : m α) (B : p β) (D : r δ) (φ : «ω» ω') (hφ : ∀ (a : α) (b : β) (d : δ), φ (g (f a b) d) = f' a (g' b d)) :
((matrix.reindex n q) p r)).trans φ.map_matrix) B) D) = B D)
theorem matrix.kronecker_map_assoc₁ {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} {q : Type u_12} {r : Type u_13} {δ : Type u_1} {ξ : Type u_3} {ω : Type u_5} (f : α → β → γ) (g : γ → δ → «ω») (f' : α → ξ → «ω») (g' : β → δ → ξ) (A : m α) (B : p β) (D : r δ) (h : ∀ (a : α) (b : β) (d : δ), g (f a b) d = f' a (g' b d)) :
(matrix.reindex n q) p r)) B) D) = B D)
def matrix.kronecker_map_bilinear {R : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [ α] [ β] [ γ] (f : α →ₗ[R] β →ₗ[R] γ) :
m α →ₗ[R] p β →ₗ[R] matrix (l × n) (m × p) γ

When f is bilinear then matrix.kronecker_map f is also bilinear.

Equations
@[simp]
theorem matrix.kronecker_map_bilinear_apply_apply {R : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [ α] [ β] [ γ] (f : α →ₗ[R] β →ₗ[R] γ) (m_1 : m α) (B : p β) :
m_1) B = matrix.kronecker_map (λ (r : α), (f r)) m_1 B
theorem matrix.kronecker_map_bilinear_mul_mul {R : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {l' : Type u_14} {m' : Type u_15} {n' : Type u_16} [fintype m] [fintype m'] [ α] [ β] [ γ] (f : α →ₗ[R] β →ₗ[R] γ) (h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = ((f a) a') * (f b) b') (A : m α) (B : n α) (A' : matrix l' m' β) (B' : matrix m' n' β) :
(A B)) (A' B') = A' B'

matrix.kronecker_map_bilinear commutes with ⬝ if f commutes with *.

This is primarily used with R = ℕ to prove matrix.mul_kronecker_mul.

### Specialization to matrix.kronecker_map (*)#

@[simp]
def matrix.kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [has_mul α] :
m α p αmatrix (l × n) (m × p) α

The Kronecker product. This is just a shorthand for kronecker_map (*). Prefer the notation ⊗ₖ rather than this definition.

Equations
@[simp]
theorem matrix.kronecker_apply {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [has_mul α] (A : m α) (B : p α) (i₁ : l) (i₂ : n) (j₁ : m) (j₂ : p) :
(A ⊗ₖ B) (i₁, i₂) (j₁, j₂) = (A i₁ j₁) * B i₂ j₂
def matrix.kronecker_bilinear (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [semiring α] [ α] :
m α →ₗ[R] p α →ₗ[R] matrix (l × n) (m × p) α

matrix.kronecker as a bilinear map.

Equations

What follows is a copy, in order, of every matrix.kronecker_map lemma above that has hypotheses which can be filled by properties of *.

@[simp]
theorem matrix.zero_kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (B : p α) :
0 ⊗ₖ B = 0
@[simp]
theorem matrix.kronecker_zero {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (A : m α) :
A ⊗ₖ 0 = 0
theorem matrix.add_kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [distrib α] (A₁ A₂ : m α) (B : p α) :
(A₁ + A₂) ⊗ₖ B = A₁ ⊗ₖ B + A₂ ⊗ₖ B
theorem matrix.kronecker_add {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [distrib α] (A : m α) (B₁ B₂ : p α) :
A ⊗ₖ (B₁ + B₂) = A ⊗ₖ B₁ + A ⊗ₖ B₂
theorem matrix.smul_kronecker (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [monoid R] [monoid α] [ α] [ α] (r : R) (A : m α) (B : p α) :
(r A) ⊗ₖ B = r A ⊗ₖ B
theorem matrix.kronecker_smul (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [monoid R] [monoid α] [ α] [ α] (r : R) (A : m α) (B : p α) :
A ⊗ₖ (r B) = r A ⊗ₖ B
theorem matrix.diagonal_kronecker_diagonal {α : Type u_2} {m : Type u_9} {n : Type u_10} [decidable_eq m] [decidable_eq n] (a : m → α) (b : n → α) :
= matrix.diagonal (λ (mn : m × n), (a mn.fst) * b mn.snd)
@[simp]
theorem matrix.one_kronecker_one {α : Type u_2} {m : Type u_9} {n : Type u_10} [decidable_eq m] [decidable_eq n] :
1 ⊗ₖ 1 = 1
theorem matrix.mul_kronecker_mul {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {l' : Type u_14} {m' : Type u_15} {n' : Type u_16} [fintype m] [fintype m'] (A : m α) (B : n α) (A' : matrix l' m' α) (B' : matrix m' n' α) :
(A B) ⊗ₖ (A' B') = A ⊗ₖ A' B ⊗ₖ B'
@[simp]
theorem matrix.kronecker_assoc {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} {q : Type u_12} {r : Type u_13} [semigroup α] (A : m α) (B : p α) (C : r α) :
(matrix.reindex n q) p r)) (A ⊗ₖ B ⊗ₖ C) = A ⊗ₖ (B ⊗ₖ C)

### Specialization to matrix.kronecker_map (⊗ₜ)#

@[simp]
def matrix.kronecker_tmul (R : Type u_1) {α : Type u_2} {β : Type u_4} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [ α] [ β] :
m α p βmatrix (l × n) (m × p) β)

The Kronecker tensor product. This is just a shorthand for kronecker_map (⊗ₜ). Prefer the notation ⊗ₖₜ rather than this definition.

Equations
@[simp]
theorem matrix.kronecker_tmul_apply (R : Type u_1) {α : Type u_2} {β : Type u_4} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [ α] [ β] (A : m α) (B : p β) (i₁ : l) (i₂ : n) (j₁ : m) (j₂ : p) :
matrix.kronecker_map (λ (_x : α) (_y : β), _x ⊗ₜ[R] _y) A B (i₁, i₂) (j₁, j₂) = A i₁ j₁ ⊗ₜ[R] B i₂ j₂
def matrix.kronecker_tmul_bilinear (R : Type u_1) {α : Type u_2} {β : Type u_4} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [ α] [ β] :
m α →ₗ[R] p β →ₗ[R] matrix (l × n) (m × p) β)

matrix.kronecker as a bilinear map.

Equations

What follows is a copy, in order, of every matrix.kronecker_map lemma above that has hypotheses which can be filled by properties of ⊗ₜ.

@[simp]
theorem matrix.zero_kronecker_tmul (R : Type u_1) {α : Type u_2} {β : Type u_4} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [ α] [ β] (B : p β) :
0 ⊗ₖₜ[R] B = 0
@[simp]
theorem matrix.kronecker_tmul_zero (R : Type u_1) {α : Type u_2} {β : Type u_4} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [ α] [ β] (A : m α) :
A ⊗ₖₜ[R] 0 = 0
theorem matrix.add_kronecker_tmul (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [ α] (A₁ A₂ : m α) (B : p α) :
(A₁ + A₂) ⊗ₖₜ[R] B = matrix.kronecker_map (λ (_x _y : α), _x ⊗ₜ[R] _y) A₁ B + matrix.kronecker_map (λ (_x _y : α), _x ⊗ₜ[R] _y) A₂ B
theorem matrix.kronecker_tmul_add (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [ α] (A : m α) (B₁ B₂ : p α) :
A ⊗ₖₜ[R] (B₁ + B₂) = matrix.kronecker_map (λ (_x _y : α), _x ⊗ₜ[R] _y) A B₁ + matrix.kronecker_map (λ (_x _y : α), _x ⊗ₜ[R] _y) A B₂
theorem matrix.smul_kronecker_tmul (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [ α] (r : R) (A : m α) (B : p α) :
(r A) ⊗ₖₜ[R] B = r matrix.kronecker_map (λ (_x _y : α), _x ⊗ₜ[R] _y) A B
theorem matrix.kronecker_tmul_smul (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [ α] (r : R) (A : m α) (B : p α) :
A ⊗ₖₜ[R] (r B) = r matrix.kronecker_map (λ (_x _y : α), _x ⊗ₜ[R] _y) A B
theorem matrix.diagonal_kronecker_tmul_diagonal (R : Type u_1) {α : Type u_2} {m : Type u_9} {n : Type u_10} [ α] [decidable_eq m] [decidable_eq n] (a : m → α) (b : n → α) :
= matrix.diagonal (λ (mn : m × n), a mn.fst ⊗ₜ[R] b mn.snd)
@[simp]
theorem matrix.kronecker_tmul_assoc (R : Type u_1) {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} {q : Type u_12} {r : Type u_13} [ α] [ β] [ γ] (A : m α) (B : p β) (C : r γ) :
(matrix.reindex n q) p r)) ((A ⊗ₖₜ[R] B ⊗ₖₜ[R] C).map β γ)) = A ⊗ₖₜ[R] (B ⊗ₖₜ[R] C)
@[simp]
theorem matrix.one_kronecker_tmul_one (R : Type u_1) {α : Type u_2} {m : Type u_9} {n : Type u_10} [semiring α] [ α] [decidable_eq m] [decidable_eq n] :
1 ⊗ₖₜ[R] 1 = 1
theorem matrix.mul_kronecker_tmul_mul (R : Type u_1) {α : Type u_2} {β : Type u_4} {l : Type u_8} {m : Type u_9} {n : Type u_10} {l' : Type u_14} {m' : Type u_15} {n' : Type u_16} [semiring α] [semiring β] [ α] [ β] [fintype m] [fintype m'] (A : m α) (B : n α) (A' : matrix l' m' β) (B' : matrix m' n' β) :
(A B) ⊗ₖₜ[R] (A' B') = matrix.kronecker_map (λ (_x : α) (_y : β), _x ⊗ₜ[R] _y) A A' matrix.kronecker_map (λ (_x : α) (_y : β), _x ⊗ₜ[R] _y) B B'