mathlib documentation

data.matrix.kronecker

Kronecker product of matrices #

This defines the Kronecker product.

Main definitions #

Specializations #

Notations #

These require open_locale kronecker:

@[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 : matrix l m α) (B : matrix n 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 : matrix l m α) (B : matrix n p β) :
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 : matrix l m α) (B : matrix n p β) :
matrix.kronecker_map f (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 : matrix l m α) (B : matrix n p β) :
matrix.kronecker_map f A (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 : matrix l m α) (B : matrix n p β) :
(matrix.kronecker_map f A 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 : matrix n p β) :
@[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 : matrix l m α) :
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₂ : matrix l m α) (B : matrix n p β) :
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 : matrix l m α) (B₁ B₂ : matrix n p β) :
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} [has_scalar R α] [has_scalar R γ] (f : α → β → γ) (r : R) (hf : ∀ (a : α) (b : β), f (r a) b = r f a b) (A : matrix l m α) (B : matrix n p β) :
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} [has_scalar R β] [has_scalar R γ] (f : α → β → γ) (r : R) (hf : ∀ (a : α) (b : β), f a (r b) = r f a b) (A : matrix l m α) (B : matrix n p β) :
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.kronecker_map f (matrix.diagonal a) (matrix.diagonal b) = 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) :
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 : matrix l m α) (N : matrix n p β) :
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 : matrix l m α) (N : matrix 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 : matrix l l' α) (N : matrix m 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 : matrix l m α) (B : matrix n p β) (D : matrix q r δ) (φ : «ω» ω') (hφ : ∀ (a : α) (b : β) (d : δ), φ (g (f a b) d) = f' a (g' 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 : matrix l m α) (B : matrix n p β) (D : matrix q r δ) (h : ∀ (a : α) (b : β) (d : δ), g (f a b) d = f' a (g' 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} [comm_semiring R] [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] [module R α] [module R β] [module R γ] (f : α →ₗ[R] β →ₗ[R] γ) :
matrix l m α →ₗ[R] matrix n 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} [comm_semiring R] [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] [module R α] [module R β] [module R γ] (f : α →ₗ[R] β →ₗ[R] γ) (m_1 : matrix l m α) (B : matrix n p β) :
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} [comm_semiring R] [fintype m] [fintype m'] [non_unital_non_assoc_semiring α] [non_unital_non_assoc_semiring β] [non_unital_non_assoc_semiring γ] [module R α] [module R β] [module R γ] (f : α →ₗ[R] β →ₗ[R] γ) (h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = ((f a) a') * (f b) b') (A : matrix l m α) (B : matrix m n α) (A' : matrix l' m' β) (B' : matrix m' n' β) :

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 α] :
matrix l m αmatrix n 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 : matrix l m α) (B : matrix n 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} [comm_semiring R] [semiring α] [algebra R α] :
matrix l m α →ₗ[R] matrix n 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} [mul_zero_class α] (B : matrix n 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} [mul_zero_class α] (A : matrix l 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₂ : matrix l m α) (B : matrix n 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 : matrix l m α) (B₁ B₂ : matrix n 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 α] [mul_action R α] [is_scalar_tower R α α] (r : R) (A : matrix l m α) (B : matrix n 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 α] [mul_action R α] [smul_comm_class R α α] (r : R) (A : matrix l m α) (B : matrix n p α) :
A ⊗ₖ (r B) = r A ⊗ₖ B
theorem matrix.diagonal_kronecker_diagonal {α : Type u_2} {m : Type u_9} {n : Type u_10} [mul_zero_class α] [decidable_eq m] [decidable_eq n] (a : m → α) (b : n → α) :
matrix.diagonal a ⊗ₖ matrix.diagonal b = 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} [mul_zero_one_class α] [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'] [comm_semiring α] (A : matrix l m α) (B : matrix m 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 : matrix l m α) (B : matrix n p α) (C : matrix q r α) :

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} [comm_semiring R] [add_comm_monoid α] [add_comm_monoid β] [module R α] [module R β] :
matrix l m αmatrix n 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} [comm_semiring R] [add_comm_monoid α] [add_comm_monoid β] [module R α] [module R β] (A : matrix l m α) (B : matrix n 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} [comm_semiring R] [add_comm_monoid α] [add_comm_monoid β] [module R α] [module R β] :
matrix l m α →ₗ[R] matrix n 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} [comm_semiring R] [add_comm_monoid α] [add_comm_monoid β] [module R α] [module R β] (B : matrix n 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} [comm_semiring R] [add_comm_monoid α] [add_comm_monoid β] [module R α] [module R β] (A : matrix l 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} [comm_semiring R] [add_comm_monoid α] [module R α] (A₁ A₂ : matrix l m α) (B : matrix n 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} [comm_semiring R] [add_comm_monoid α] [module R α] (A : matrix l m α) (B₁ B₂ : matrix n 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} [comm_semiring R] [add_comm_monoid α] [module R α] (r : R) (A : matrix l m α) (B : matrix n 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} [comm_semiring R] [add_comm_monoid α] [module R α] (r : R) (A : matrix l m α) (B : matrix n 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} [comm_semiring R] [add_comm_monoid α] [module R α] [decidable_eq m] [decidable_eq n] (a : m → α) (b : n → α) :
@[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} [comm_semiring R] [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] [module R α] [module R β] [module R γ] (A : matrix l m α) (B : matrix n p β) (C : matrix q r γ) :
@[simp]
theorem matrix.one_kronecker_tmul_one (R : Type u_1) {α : Type u_2} {m : Type u_9} {n : Type u_10} [comm_semiring R] [semiring α] [algebra R α] [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} [comm_semiring R] [semiring α] [semiring β] [algebra R α] [algebra R β] [fintype m] [fintype m'] (A : matrix l m α) (B : matrix m 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'