Mathlib.Data.Matrix.Kronecker

Matrix.kroneckerMap definition

(f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β) : Matrix (l × n) (m × p) γ

Full source

/-- Produce a matrix with `f` applied to every pair of elements from `A` and `B`. -/
def kroneckerMap (f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β) : Matrix (l × n) (m × p) γ :=
  of fun (i : l × n) (j : m × p) => f (A i.1 j.1) (B i.2 j.2)

Kronecker Map of Matrices

Informal description

Given a function $ f : \alpha \to \beta \to \gamma $ and matrices $ A $ of size $ l \times m $ with entries in $ \alpha $ and $ B $ of size $ n \times p $ with entries in $ \beta $, the Kronecker map $ \text{kroneckerMap}\, f\, A\, B $ is the matrix of size $ (l \times n) \times (m \times p) $ with entries in $ \gamma $ defined by \[ (\text{kroneckerMap}\, f\, A\, B)_{(i_1, i_2), (j_1, j_2)} = f (A_{i_1 j_1}) (B_{i_2 j_2}). \]

Matrix.kroneckerMap_apply theorem

 (f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β) (i j) : kroneckerMap f A B i j = f (A i.1 j.1) (B i.2 j.2)

Full source

@[simp]
theorem kroneckerMap_apply (f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β) (i j) :
    kroneckerMap f A B i j = f (A i.1 j.1) (B i.2 j.2) :=
  rfl

Entry Formula for Kronecker Map of Matrices

Informal description

For any function $f : \alpha \to \beta \to \gamma$ and matrices $A \in M_{l \times m}(\alpha)$, $B \in M_{n \times p}(\beta)$, the $(i,j)$-th entry of the Kronecker map $\text{kroneckerMap}\, f\, A\, B$ is given by \[ (\text{kroneckerMap}\, f\, A\, B)_{i,j} = f (A_{i_1 j_1}) (B_{i_2 j_2}), \] where $i = (i_1, i_2)$ and $j = (j_1, j_2)$ are pairs of indices.

Matrix.kroneckerMap_transpose theorem

(f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β) : kroneckerMap f Aᵀ Bᵀ = (kroneckerMap f A B)ᵀ

Full source

theorem kroneckerMap_transpose (f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β) :
    kroneckerMap f Aᵀ Bᵀ = (kroneckerMap f A B)ᵀ :=
  ext fun _ _ => rfl

Transpose of Kronecker Map Equals Kronecker Map of Transposes

Informal description

For any function $ f : \alpha \to \beta \to \gamma $ and matrices $ A $ of size $ l \times m $ with entries in $ \alpha $ and $ B $ of size $ n \times p $ with entries in $ \beta $, the Kronecker map of the transposed matrices $ A^\top $ and $ B^\top $ is equal to the transpose of the Kronecker map of $ A $ and $ B $. That is, \[ \text{kroneckerMap}\, f\, A^\top\, B^\top = (\text{kroneckerMap}\, f\, A\, B)^\top. \]

Matrix.kroneckerMap_map_left theorem

 (f : α' → β → γ) (g : α → α') (A : Matrix l m α) (B : Matrix n p β) :
  kroneckerMap f (A.map g) B = kroneckerMap (fun a b => f (g a) b) A B

Full source

theorem kroneckerMap_map_left (f : α' → β → γ) (g : α → α') (A : Matrix l m α) (B : Matrix n p β) :
    kroneckerMap f (A.map g) B = kroneckerMap (fun a b => f (g a) b) A B :=
  ext fun _ _ => rfl

Kronecker Map Preserves Left Matrix Mapping

Informal description

For any function $f \colon \alpha' \to \beta \to \gamma$, a mapping $g \colon \alpha \to \alpha'$, a matrix $A$ of size $l \times m$ with entries in $\alpha$, and a matrix $B$ of size $n \times p$ with entries in $\beta$, the following equality holds: \[ \text{kroneckerMap}\, f\, (A.\text{map}\, g)\, B = \text{kroneckerMap}\, (\lambda a\, b, f (g a) b)\, A\, B. \]

Matrix.kroneckerMap_map_right theorem

 (f : α → β' → γ) (g : β → β') (A : Matrix l m α) (B : Matrix n p β) :
  kroneckerMap f A (B.map g) = kroneckerMap (fun a b => f a (g b)) A B

Full source

theorem kroneckerMap_map_right (f : α → β' → γ) (g : β → β') (A : Matrix l m α) (B : Matrix n p β) :
    kroneckerMap f A (B.map g) = kroneckerMap (fun a b => f a (g b)) A B :=
  ext fun _ _ => rfl

Kronecker Map Preserves Right Matrix Mapping

Informal description

For any function $f : \alpha \to \beta' \to \gamma$, a mapping $g : \beta \to \beta'$, a matrix $A$ of size $l \times m$ with entries in $\alpha$, and a matrix $B$ of size $n \times p$ with entries in $\beta$, the Kronecker map of $A$ and the mapped matrix $B.map\, g$ satisfies \[ \text{kroneckerMap}\, f\, A\, (B.map\, g) = \text{kroneckerMap}\, (\lambda a\, b, f\, a\, (g\, b))\, A\, B. \]

Matrix.kroneckerMap_map theorem

 (f : α → β → γ) (g : γ → γ') (A : Matrix l m α) (B : Matrix n p β) :
  (kroneckerMap f A B).map g = kroneckerMap (fun a b => g (f a b)) A B

Full source

theorem kroneckerMap_map (f : α → β → γ) (g : γ → γ') (A : Matrix l m α) (B : Matrix n p β) :
    (kroneckerMap f A B).map g = kroneckerMap (fun a b => g (f a b)) A B :=
  ext fun _ _ => rfl

Composition of Mapping with Kronecker Map

Informal description

For any functions $ f : \alpha \to \beta \to \gamma $ and $ g : \gamma \to \gamma' $, and matrices $ A $ of size $ l \times m $ with entries in $ \alpha $ and $ B $ of size $ n \times p $ with entries in $ \beta $, the following equality holds: \[ \text{map}\, g\, (\text{kroneckerMap}\, f\, A\, B) = \text{kroneckerMap}\, (\lambda a\, b, g (f a b))\, A\, B. \]

Matrix.kroneckerMap_zero_left theorem

 [Zero α] [Zero γ] (f : α → β → γ) (hf : ∀ b, f 0 b = 0) (B : Matrix n p β) : kroneckerMap f (0 : Matrix l m α) B = 0

Full source

@[simp]
theorem kroneckerMap_zero_left [Zero α] [Zero γ] (f : α → β → γ) (hf : ∀ b, f 0 b = 0)
    (B : Matrix n p β) : kroneckerMap f (0 : Matrix l m α) B = 0 :=
  ext fun _ _ => hf _

Kronecker Map with Zero Matrix on the Left Yields Zero Matrix

Informal description

Let $\alpha$ and $\gamma$ be types equipped with zero elements $0_\alpha$ and $0_\gamma$ respectively. Given a function $f : \alpha \to \beta \to \gamma$ such that $f(0_\alpha, b) = 0_\gamma$ for all $b \in \beta$, and a matrix $B$ of size $n \times p$ with entries in $\beta$, the Kronecker map of the zero matrix (of size $l \times m$ with entries in $\alpha$) with $B$ satisfies \[ \text{kroneckerMap}\, f\, 0\, B = 0. \]

Matrix.kroneckerMap_zero_right theorem

 [Zero β] [Zero γ] (f : α → β → γ) (hf : ∀ a, f a 0 = 0) (A : Matrix l m α) : kroneckerMap f A (0 : Matrix n p β) = 0

Full source

@[simp]
theorem kroneckerMap_zero_right [Zero β] [Zero γ] (f : α → β → γ) (hf : ∀ a, f a 0 = 0)
    (A : Matrix l m α) : kroneckerMap f A (0 : Matrix n p β) = 0 :=
  ext fun _ _ => hf _

Kronecker Map with Zero Matrix on the Right Yields Zero Matrix

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types equipped with zero elements $0_\beta$ and $0_\gamma$ respectively. Given a function $f : \alpha \to \beta \to \gamma$ such that $f(a, 0_\beta) = 0_\gamma$ for all $a \in \alpha$, and a matrix $A$ of size $l \times m$ with entries in $\alpha$, the Kronecker map of $A$ with the zero matrix (of size $n \times p$ with entries in $\beta$) satisfies \[ \text{kroneckerMap}\, f\, A\, 0 = 0. \]

Matrix.kroneckerMap_add_left theorem

 [Add α] [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 β) : kroneckerMap f (A₁ + A₂) B = kroneckerMap f A₁ B + kroneckerMap f A₂ B

Full source

theorem kroneckerMap_add_left [Add α] [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 β) :
    kroneckerMap f (A₁ + A₂) B = kroneckerMap f A₁ B + kroneckerMap f A₂ B :=
  ext fun _ _ => hf _ _ _

Additivity of Kronecker Map in the Left Argument

Informal description

Let $\alpha$ and $\gamma$ be types equipped with addition operations, and let $f : \alpha \to \beta \to \gamma$ be a function such that for all $a_1, a_2 \in \alpha$ and $b \in \beta$, we have $f(a_1 + a_2, b) = f(a_1, b) + f(a_2, b)$. Then for any matrices $A_1, A_2$ of size $l \times m$ with entries in $\alpha$ and matrix $B$ of size $n \times p$ with entries in $\beta$, the Kronecker map satisfies: \[ \text{kroneckerMap}\, f\, (A_1 + A_2)\, B = \text{kroneckerMap}\, f\, A_1\, B + \text{kroneckerMap}\, f\, A_2\, B. \]

Matrix.kroneckerMap_add_right theorem

 [Add β] [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 β) : kroneckerMap f A (B₁ + B₂) = kroneckerMap f A B₁ + kroneckerMap f A B₂

Full source

theorem kroneckerMap_add_right [Add β] [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 β) :
    kroneckerMap f A (B₁ + B₂) = kroneckerMap f A B₁ + kroneckerMap f A B₂ :=
  ext fun _ _ => hf _ _ _

Additivity of Kronecker Map in the Right Argument

Informal description

Let $\beta$ and $\gamma$ be types equipped with addition operations, and let $f : \alpha \to \beta \to \gamma$ be a function such that for all $a \in \alpha$ and $b_1, b_2 \in \beta$, we have $f(a, b_1 + b_2) = f(a, b_1) + f(a, b_2)$. Then for any matrix $A$ of size $l \times m$ with entries in $\alpha$ and matrices $B_1, B_2$ of size $n \times p$ with entries in $\beta$, the Kronecker map satisfies: \[ \text{kroneckerMap}\, f\, A\, (B_1 + B_2) = \text{kroneckerMap}\, f\, A\, B_1 + \text{kroneckerMap}\, f\, A\, B_2. \]

Matrix.kroneckerMap_smul_left theorem

 [SMul R α] [SMul R γ] (f : α → β → γ) (r : R) (hf : ∀ a b, f (r • a) b = r • f a b) (A : Matrix l m α)
  (B : Matrix n p β) : kroneckerMap f (r • A) B = r • kroneckerMap f A B

Full source

theorem kroneckerMap_smul_left [SMul R α] [SMul R γ] (f : α → β → γ) (r : R)
    (hf : ∀ a b, f (r • a) b = r • f a b) (A : Matrix l m α) (B : Matrix n p β) :
    kroneckerMap f (r • A) B = r • kroneckerMap f A B :=
  ext fun _ _ => hf _ _

Left Scalar Multiplication Commutes with Kronecker Map

Informal description

Let $R$ be a type with a scalar multiplication operation on types $\alpha$ and $\gamma$, and let $f : \alpha \to \beta \to \gamma$ be a function such that for all $a \in \alpha$ and $b \in \beta$, $f (r \cdot a) b = r \cdot f a b$. Then for any scalar $r \in R$, matrix $A$ of size $l \times m$ with entries in $\alpha$, and matrix $B$ of size $n \times p$ with entries in $\beta$, the Kronecker map satisfies: \[ \text{kroneckerMap}\, f\, (r \cdot A)\, B = r \cdot \text{kroneckerMap}\, f\, A\, B. \]

Matrix.kroneckerMap_smul_right theorem

 [SMul R β] [SMul R γ] (f : α → β → γ) (r : R) (hf : ∀ a b, f a (r • b) = r • f a b) (A : Matrix l m α)
  (B : Matrix n p β) : kroneckerMap f A (r • B) = r • kroneckerMap f A B

Full source

theorem kroneckerMap_smul_right [SMul R β] [SMul R γ] (f : α → β → γ) (r : R)
    (hf : ∀ a b, f a (r • b) = r • f a b) (A : Matrix l m α) (B : Matrix n p β) :
    kroneckerMap f A (r • B) = r • kroneckerMap f A B :=
  ext fun _ _ => hf _ _

Right Scalar Multiplication Commutes with Kronecker Map

Informal description

Let $R$ be a type with a scalar multiplication operation on types $\beta$ and $\gamma$, and let $f : \alpha \to \beta \to \gamma$ be a function such that for all $a \in \alpha$ and $b \in \beta$, $f(a, r \cdot b) = r \cdot f(a, b)$. Then for any scalar $r \in R$, matrix $A$ of size $l \times m$ with entries in $\alpha$, and matrix $B$ of size $n \times p$ with entries in $\beta$, the Kronecker map satisfies: \[ \text{kroneckerMap}\, f\, A\, (r \cdot B) = r \cdot \text{kroneckerMap}\, f\, A\, B. \]

Matrix.kroneckerMap_stdBasisMatrix_stdBasisMatrix theorem

 [Zero α] [Zero β] [Zero γ] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (i₁ : l) (j₁ : m) (i₂ : n)
  (j₂ : p) (f : α → β → γ) (hf₁ : ∀ b, f 0 b = 0) (hf₂ : ∀ a, f a 0 = 0) (a : α) (b : β) :
  kroneckerMap f (stdBasisMatrix i₁ j₁ a) (stdBasisMatrix i₂ j₂ b) = stdBasisMatrix (i₁, i₂) (j₁, j₂) (f a b)

Full source

theorem kroneckerMap_stdBasisMatrix_stdBasisMatrix
    [Zero α] [Zero β] [Zero γ] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p]
    (i₁ : l) (j₁ : m) (i₂ : n) (j₂ : p)
    (f : α → β → γ) (hf₁ : ∀ b, f 0 b = 0) (hf₂ : ∀ a, f a 0 = 0) (a : α) (b : β) :
    kroneckerMap f (stdBasisMatrix i₁ j₁ a) (stdBasisMatrix i₂ j₂ b) =
      stdBasisMatrix (i₁, i₂) (j₁, j₂) (f a b) := by
  ext ⟨i₁', i₂'⟩ ⟨j₁', j₂'⟩
  dsimp [stdBasisMatrix]
  aesop

Kronecker Map of Standard Basis Matrices is Standard Basis Matrix of Function Application

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types with zero elements, and let $l$, $m$, $n$, and $p$ be types with decidable equality. Given indices $i_1 \in l$, $j_1 \in m$, $i_2 \in n$, $j_2 \in p$, a function $f : \alpha \to \beta \to \gamma$ such that $f(0, b) = 0$ for all $b \in \beta$ and $f(a, 0) = 0$ for all $a \in \alpha$, and elements $a \in \alpha$ and $b \in \beta$, the Kronecker map of the standard basis matrices satisfies: \[ \text{kroneckerMap}\, f\, (\text{stdBasisMatrix}\, i_1\, j_1\, a)\, (\text{stdBasisMatrix}\, i_2\, j_2\, b) = \text{stdBasisMatrix}\, (i_1, i_2)\, (j_1, j_2)\, (f\, a\, b). \]

Matrix.kroneckerMap_diagonal_diagonal theorem

 [Zero α] [Zero β] [Zero γ] [DecidableEq m] [DecidableEq n] (f : α → β → γ) (hf₁ : ∀ b, f 0 b = 0)
  (hf₂ : ∀ a, f a 0 = 0) (a : m → α) (b : n → β) :
  kroneckerMap f (diagonal a) (diagonal b) = diagonal fun mn => f (a mn.1) (b mn.2)

Full source

theorem kroneckerMap_diagonal_diagonal [Zero α] [Zero β] [Zero γ] [DecidableEq m] [DecidableEq n]
    (f : α → β → γ) (hf₁ : ∀ b, f 0 b = 0) (hf₂ : ∀ a, f a 0 = 0) (a : m → α) (b : n → β) :
    kroneckerMap f (diagonal a) (diagonal b) = diagonal fun mn => f (a mn.1) (b mn.2) := by
  ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
  simp [diagonal, apply_ite f, ite_and, ite_apply, apply_ite (f (a i₁)), hf₁, hf₂]

Kronecker Map of Diagonal Matrices is Diagonal

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a function such that $f(0, b) = 0$ for all $b \in \beta$ and $f(a, 0) = 0$ for all $a \in \alpha$. Let $A = \text{diagonal}(a)$ be an $m \times m$ diagonal matrix with entries $a_i$ and $B = \text{diagonal}(b)$ be an $n \times n$ diagonal matrix with entries $b_j$. Then the Kronecker map of $A$ and $B$ is the $(m \times n) \times (m \times n)$ diagonal matrix given by \[ \text{kroneckerMap}\, f\, A\, B = \text{diagonal}\big(f(a_{i}, b_{j})\big)_{(i,j) \in m \times n}. \]

Matrix.kroneckerMap_diagonal_right theorem

 [Zero β] [Zero γ] [DecidableEq n] (f : α → β → γ) (hf : ∀ a, f a 0 = 0) (A : Matrix l m α) (b : n → β) :
  kroneckerMap f A (diagonal b) = blockDiagonal fun i => A.map fun a => f a (b i)

Full source

theorem kroneckerMap_diagonal_right [Zero β] [Zero γ] [DecidableEq n] (f : α → β → γ)
    (hf : ∀ a, f a 0 = 0) (A : Matrix l m α) (b : n → β) :
    kroneckerMap f A (diagonal b) = blockDiagonal fun i => A.map fun a => f a (b i) := by
  ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
  simp [diagonal, blockDiagonal, apply_ite (f (A i₁ j₁)), hf]

Kronecker Map with Right Diagonal Matrix Yields Block Diagonal Matrix

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a function such that $f(a, 0) = 0$ for all $a \in \alpha$, where $\beta$ and $\gamma$ have zero elements. Let $A$ be an $l \times m$ matrix with entries in $\alpha$, and let $B = \text{diagonal}(b)$ be an $n \times n$ diagonal matrix with entries $b_j \in \beta$ (where $n$ has decidable equality). Then the Kronecker map of $A$ and $B$ is equal to the block diagonal matrix whose $i$-th block is the matrix $A$ with entries mapped by $f(\cdot, b_i)$. In symbols: \[ \text{kroneckerMap}\, f\, A\, (\text{diagonal}\, b) = \text{blockDiagonal}\, \left(\lambda i, A.\text{map}\, (\lambda a, f\, a\, b_i)\right). \]

Matrix.kroneckerMap_diagonal_left theorem

 [Zero α] [Zero γ] [DecidableEq l] (f : α → β → γ) (hf : ∀ b, f 0 b = 0) (a : l → α) (B : Matrix m n β) :
  kroneckerMap f (diagonal a) B =
    Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal fun i => B.map fun b => f (a i) b)

Full source

theorem kroneckerMap_diagonal_left [Zero α] [Zero γ] [DecidableEq l] (f : α → β → γ)
    (hf : ∀ b, f 0 b = 0) (a : l → α) (B : Matrix m n β) :
    kroneckerMap f (diagonal a) B =
      Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _)
        (blockDiagonal fun i => B.map fun b => f (a i) b) := by
  ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
  simp [diagonal, blockDiagonal, apply_ite f, ite_apply, hf]

Kronecker Map of Diagonal Matrix with General Matrix via Reindexing

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a function such that $f(0, b) = 0$ for all $b \in \beta$, and let $A = \text{diagonal}(a)$ be an $l \times l$ diagonal matrix with entries $a_i \in \alpha$, and $B$ be an $m \times n$ matrix with entries in $\beta$. Then the Kronecker map of $A$ and $B$ is equal to the reindexing (via product commutativity) of the block diagonal matrix whose blocks are $B$ mapped under $f(a_i, \cdot)$ for each $i \in l$. More precisely: \[ \text{kroneckerMap}\, f\, (\text{diagonal}\, a)\, B = \text{reindex}\, (\text{prodComm}\, l\, m)\, (\text{prodComm}\, l\, n)\, \left(\text{blockDiagonal}\, \left(\lambda i, B.\text{map}\, (\lambda b, f (a i) b)\right)\right). \]

Matrix.kroneckerMap_one_one theorem

 [Zero α] [Zero β] [Zero γ] [One α] [One β] [One γ] [DecidableEq m] [DecidableEq n] (f : α → β → γ)
  (hf₁ : ∀ b, f 0 b = 0) (hf₂ : ∀ a, f a 0 = 0) (hf₃ : f 1 1 = 1) :
  kroneckerMap f (1 : Matrix m m α) (1 : Matrix n n β) = 1

Full source

@[simp]
theorem kroneckerMap_one_one [Zero α] [Zero β] [Zero γ] [One α] [One β] [One γ] [DecidableEq m]
    [DecidableEq n] (f : α → β → γ) (hf₁ : ∀ b, f 0 b = 0) (hf₂ : ∀ a, f a 0 = 0)
    (hf₃ : f 1 1 = 1) : kroneckerMap f (1 : Matrix m m α) (1 : Matrix n n β) = 1 :=
  (kroneckerMap_diagonal_diagonal _ hf₁ hf₂ _ _).trans <| by simp only [hf₃, diagonal_one]

Kronecker Map of Identity Matrices Yields Identity Matrix

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types with zero and one elements, and let $f : \alpha \to \beta \to \gamma$ be a function such that: 1. $f(0, b) = 0$ for all $b \in \beta$, 2. $f(a, 0) = 0$ for all $a \in \alpha$, 3. $f(1, 1) = 1$. Let $I_m$ be the $m \times m$ identity matrix over $\alpha$ and $I_n$ be the $n \times n$ identity matrix over $\beta$ (where $m$ and $n$ have decidable equality). Then the Kronecker map of $I_m$ and $I_n$ is the $(m \times n) \times (m \times n)$ identity matrix over $\gamma$, i.e., \[ \text{kroneckerMap}\, f\, I_m\, I_n = I_{m \times n}. \]

Matrix.kroneckerMap_reindex theorem

 (f : α → β → γ) (el : l ≃ l') (em : m ≃ m') (en : n ≃ n') (ep : p ≃ p') (M : Matrix l m α) (N : Matrix n p β) :
  kroneckerMap f (reindex el em M) (reindex en ep N) = reindex (el.prodCongr en) (em.prodCongr ep) (kroneckerMap f M N)

Full source

theorem kroneckerMap_reindex (f : α → β → γ) (el : l ≃ l') (em : m ≃ m') (en : n ≃ n') (ep : p ≃ p')
    (M : Matrix l m α) (N : Matrix n p β) :
    kroneckerMap f (reindex el em M) (reindex en ep N) =
      reindex (el.prodCongr en) (em.prodCongr ep) (kroneckerMap f M N) := by
  ext ⟨i, i'⟩ ⟨j, j'⟩
  rfl

Reindexing Commutes with Kronecker Map of Matrices

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a function, and let $M$ be an $l \times m$ matrix with entries in $\alpha$ and $N$ be an $n \times p$ matrix with entries in $\beta$. Given equivalences (bijections with inverses) $el : l \simeq l'$, $em : m \simeq m'$, $en : n \simeq n'$, and $ep : p \simeq p'$, the Kronecker map of the reindexed matrices satisfies: \[ \text{kroneckerMap}\, f\, (M_{\text{reindex}\, el\, em})\, (N_{\text{reindex}\, en\, ep}) = (\text{kroneckerMap}\, f\, M\, N)_{\text{reindex}\, (el \times en)\, (em \times ep)} \] where $M_{\text{reindex}\, el\, em}$ denotes the matrix $M$ with rows and columns reindexed by $el$ and $em$ respectively, and similarly for $N$.

Matrix.kroneckerMap_reindex_left theorem

 (f : α → β → γ) (el : l ≃ l') (em : m ≃ m') (M : Matrix l m α) (N : Matrix n n' β) :
  kroneckerMap f (Matrix.reindex el em M) N =
    reindex (el.prodCongr (Equiv.refl _)) (em.prodCongr (Equiv.refl _)) (kroneckerMap f M N)

Full source

theorem kroneckerMap_reindex_left (f : α → β → γ) (el : l ≃ l') (em : m ≃ m') (M : Matrix l m α)
    (N : Matrix n n' β) :
    kroneckerMap f (Matrix.reindex el em M) N =
      reindex (el.prodCongr (Equiv.refl _)) (em.prodCongr (Equiv.refl _)) (kroneckerMap f M N) :=
  kroneckerMap_reindex _ _ _ (Equiv.refl _) (Equiv.refl _) _ _

Left Reindexing Commutes with Kronecker Map of Matrices

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a function, and let $M$ be an $l \times m$ matrix with entries in $\alpha$ and $N$ be an $n \times n'$ matrix with entries in $\beta$. Given equivalences (bijections with inverses) $el : l \simeq l'$ and $em : m \simeq m'$, the Kronecker map of the reindexed matrix $M$ and $N$ satisfies: \[ \text{kroneckerMap}\, f\, (M_{\text{reindex}\, el\, em})\, N = (\text{kroneckerMap}\, f\, M\, N)_{\text{reindex}\, (el \times \text{id})\, (em \times \text{id})} \] where $M_{\text{reindex}\, el\, em}$ denotes the matrix $M$ with rows and columns reindexed by $el$ and $em$ respectively, and $\text{id}$ is the identity equivalence on the appropriate index sets.

Matrix.kroneckerMap_reindex_right theorem

 (f : α → β → γ) (em : m ≃ m') (en : n ≃ n') (M : Matrix l l' α) (N : Matrix m n β) :
  kroneckerMap f M (reindex em en N) =
    reindex ((Equiv.refl _).prodCongr em) ((Equiv.refl _).prodCongr en) (kroneckerMap f M N)

Full source

theorem kroneckerMap_reindex_right (f : α → β → γ) (em : m ≃ m') (en : n ≃ n') (M : Matrix l l' α)
    (N : Matrix m n β) :
    kroneckerMap f M (reindex em en N) =
      reindex ((Equiv.refl _).prodCongr em) ((Equiv.refl _).prodCongr en) (kroneckerMap f M N) :=
  kroneckerMap_reindex _ (Equiv.refl _) (Equiv.refl _) _ _ _ _

Right Reindexing Commutes with Kronecker Map of Matrices

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a function, $M$ be an $l \times l'$ matrix with entries in $\alpha$, and $N$ be an $m \times n$ matrix with entries in $\beta$. Given equivalences (bijections with inverses) $em : m \simeq m'$ and $en : n \simeq n'$, the Kronecker map of $M$ and the reindexed matrix $N$ satisfies: \[ \text{kroneckerMap}\, f\, M\, (N_{\text{reindex}\, em\, en}) = (\text{kroneckerMap}\, f\, M\, N)_{\text{reindex}\, (\text{id} \times em)\, (\text{id} \times en)} \] where $N_{\text{reindex}\, em\, en}$ denotes the matrix $N$ with rows and columns reindexed by $em$ and $en$ respectively, and $\text{id}$ is the identity equivalence on the appropriate index sets.

Matrix.kroneckerMap_assoc theorem

 {δ ξ ω ω' : Type*} (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)) :
  (reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)).trans (Equiv.mapMatrix φ)
      (kroneckerMap g (kroneckerMap f A B) D) =
    kroneckerMap f' A (kroneckerMap g' B D)

Full source

theorem kroneckerMap_assoc {δ ξ ω ω' : Type*} (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)) :
    (reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)).trans (Equiv.mapMatrix φ)
        (kroneckerMap g (kroneckerMap f A B) D) =
      kroneckerMap f' A (kroneckerMap g' B D) :=
  ext fun _ _ => hφ _ _ _

Associativity of Kronecker Map under Equivalence and Compatibility Condition

Informal description

Let $\alpha, \beta, \gamma, \delta, \xi, \omega, \omega'$ be types, and let $f : \alpha \to \beta \to \gamma$, $g : \gamma \to \delta \to \omega$, $f' : \alpha \to \xi \to \omega'$, and $g' : \beta \to \delta \to \xi$ be functions. For matrices $A \in \text{Matrix}\, l\, m\, \alpha$, $B \in \text{Matrix}\, n\, p\, \beta$, and $D \in \text{Matrix}\, q\, r\, \delta$, and an equivalence $\varphi : \omega \simeq \omega'$ satisfying the compatibility condition: \[ \forall a \in \alpha, b \in \beta, d \in \delta, \quad \varphi (g (f a b) d) = f' a (g' b d), \] the following equality holds: \[ \text{reindex}\, (\text{Equiv.prodAssoc}\, l\, n\, q)\, (\text{Equiv.prodAssoc}\, m\, p\, r) \circ \text{Equiv.mapMatrix}\, \varphi \circ \text{kroneckerMap}\, g\, (\text{kroneckerMap}\, f\, A\, B)\, D = \text{kroneckerMap}\, f'\, A\, (\text{kroneckerMap}\, g'\, B\, D). \] Here, $\text{reindex}$ applies the associativity equivalence on product indices, $\text{Equiv.mapMatrix}\, \varphi$ applies $\varphi$ entrywise to the matrix, and $\text{kroneckerMap}$ constructs a new matrix by applying the given function to corresponding entries of the input matrices.

Matrix.kroneckerMap_assoc₁ theorem

 {δ ξ ω : Type*} (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)) :
  reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r) (kroneckerMap g (kroneckerMap f A B) D) =
    kroneckerMap f' A (kroneckerMap g' B D)

Full source

theorem kroneckerMap_assoc₁ {δ ξ ω : Type*} (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)) :
    reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)
        (kroneckerMap g (kroneckerMap f A B) D) =
      kroneckerMap f' A (kroneckerMap g' B D) :=
  ext fun _ _ => h _ _ _

Associativity of Kronecker Map under Compatibility Condition

Informal description

Let $\alpha, \beta, \gamma, \delta, \xi, \omega$ be types, and let $f : \alpha \to \beta \to \gamma$, $g : \gamma \to \delta \to \omega$, $f' : \alpha \to \xi \to \omega$, and $g' : \beta \to \delta \to \xi$ be functions. For matrices $A \in \text{Matrix}\, l\, m\, \alpha$, $B \in \text{Matrix}\, n\, p\, \beta$, and $D \in \text{Matrix}\, q\, r\, \delta$, if the functions satisfy the compatibility condition: \[ \forall a \in \alpha, b \in \beta, d \in \delta, \quad g (f a b) d = f' a (g' b d), \] then the following equality holds: \[ \text{reindex}\, (\text{Equiv.prodAssoc}\, l\, n\, q)\, (\text{Equiv.prodAssoc}\, m\, p\, r)\, (\text{kroneckerMap}\, g\, (\text{kroneckerMap}\, f\, A\, B)\, D) = \text{kroneckerMap}\, f'\, A\, (\text{kroneckerMap}\, g'\, B\, D). \] Here, $\text{reindex}$ applies the associativity equivalence on product indices, and $\text{kroneckerMap}$ constructs a new matrix by applying the given function to corresponding entries of the input matrices.

Matrix.kroneckerMapBilinear definition

 [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ]
  (f : α →ₗ[R] β →ₗ[R] γ) : Matrix l m α →ₗ[R] Matrix n p β →ₗ[R] Matrix (l × n) (m × p) γ

Full source

/-- When `f` is bilinear then `Matrix.kroneckerMap f` is also bilinear. -/
@[simps!]
def kroneckerMapBilinear [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ]
    [Module R α] [Module R β] [Module R γ] (f : α →ₗ[R] β →ₗ[R] γ) :
    MatrixMatrix l m α →ₗ[R] Matrix n p β →ₗ[R] Matrix (l × n) (m × p) γ :=
  LinearMap.mk₂ R (kroneckerMap fun r s => f r s) (kroneckerMap_add_left _ <| f.map_add₂)
    (fun _ => kroneckerMap_smul_left _ _ <| f.map_smul₂ _)
    (kroneckerMap_add_right _ fun a => (f a).map_add) fun r =>
    kroneckerMap_smul_right _ _ fun a => (f a).map_smul r

Bilinear Kronecker product of matrices

Informal description

Given a commutative semiring $R$ and modules $\alpha$, $\beta$, $\gamma$ over $R$, the function `Matrix.kroneckerMapBilinear` takes a bilinear map $f : \alpha \to_{R} \beta \to_{R} \gamma$ and returns a bilinear map from matrices over $\alpha$ to matrices over $\beta$ to matrices over $\gamma$. Specifically, for matrices $A$ of size $l \times m$ and $B$ of size $n \times p$, the result is a matrix of size $(l \times n) \times (m \times p)$ where each entry is obtained by applying $f$ to the corresponding entries of $A$ and $B$.

Matrix.kroneckerMapBilinear_mul_mul theorem

 [CommSemiring R] [Fintype m] [Fintype m'] [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β]
  [NonUnitalNonAssocSemiring γ] [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' β) :
  kroneckerMapBilinear f (A * B) (A' * B') = kroneckerMapBilinear f A A' * kroneckerMapBilinear f B B'

Full source

/-- `Matrix.kroneckerMapBilinear` commutes with `*` if `f` does.

This is primarily used with `R = ℕ` to prove `Matrix.mul_kronecker_mul`. -/
theorem kroneckerMapBilinear_mul_mul [CommSemiring R] [Fintype m] [Fintype m']
    [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ]
    [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' β) :
    kroneckerMapBilinear f (A * B) (A' * B') =
      kroneckerMapBilinear f A A' * kroneckerMapBilinear f B B' := by
  ext ⟨i, i'⟩ ⟨j, j'⟩
  simp only [kroneckerMapBilinear_apply_apply, mul_apply, ← Finset.univ_product_univ,
    Finset.sum_product, kroneckerMap_apply]
  simp_rw [map_sum f, LinearMap.sum_apply, map_sum, h_comm]

Bilinearity and Commutation of Kronecker Product with Matrix Multiplication

Informal description

Let $R$ be a commutative semiring, and let $\alpha, \beta, \gamma$ be non-unital non-associative semirings that are also $R$-modules. Given a bilinear map $f : \alpha \to_R \beta \to_R \gamma$ such that for all $a, b \in \alpha$ and $a', b' \in \beta$, the following commutation condition holds: \[ f(a * b)(a' * b') = f(a)(a') * f(b)(b'), \] then for any matrices $A \in \text{Matrix}\, l\, m\, \alpha$, $B \in \text{Matrix}\, m\, n\, \alpha$, $A' \in \text{Matrix}\, l'\, m'\, \beta$, and $B' \in \text{Matrix}\, m'\, n'\, \beta$, we have: \[ \text{kroneckerMapBilinear}\, f\, (A * B)\, (A' * B') = (\text{kroneckerMapBilinear}\, f\, A\, A') * (\text{kroneckerMapBilinear}\, f\, B\, B'). \]

Matrix.trace_kroneckerMapBilinear theorem

 [CommSemiring R] [Fintype m] [Fintype n] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α]
  [Module R β] [Module R γ] (f : α →ₗ[R] β →ₗ[R] γ) (A : Matrix m m α) (B : Matrix n n β) :
  trace (kroneckerMapBilinear f A B) = f (trace A) (trace B)

Full source

/-- `trace` distributes over `Matrix.kroneckerMapBilinear`.

This is primarily used with `R = ℕ` to prove `Matrix.trace_kronecker`. -/
theorem trace_kroneckerMapBilinear [CommSemiring R] [Fintype m] [Fintype n] [AddCommMonoid α]
    [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ]
    (f : α →ₗ[R] β →ₗ[R] γ) (A : Matrix m m α) (B : Matrix n n β) :
    trace (kroneckerMapBilinear f A B) = f (trace A) (trace B) := by
  simp_rw [Matrix.trace, Matrix.diag, kroneckerMapBilinear_apply_apply, LinearMap.map_sum₂,
    map_sum, ← Finset.univ_product_univ, Finset.sum_product, kroneckerMap_apply]

Trace of Bilinear Kronecker Product Equals Bilinear Map Applied to Traces

Informal description

Let $R$ be a commutative semiring, and let $\alpha$, $\beta$, $\gamma$ be $R$-modules. Given a bilinear map $f \colon \alpha \to_R \beta \to_R \gamma$ and square matrices $A$ of size $m \times m$ over $\alpha$ and $B$ of size $n \times n$ over $\beta$, the trace of the bilinear Kronecker product of $A$ and $B$ with respect to $f$ satisfies: \[ \operatorname{trace}(\text{kroneckerMapBilinear}\, f\, A\, B) = f (\operatorname{trace} A) (\operatorname{trace} B). \]

Matrix.det_kroneckerMapBilinear theorem

 [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [NonAssocSemiring α] [NonAssocSemiring β]
  [CommRing γ] [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 m m α) (B : Matrix n n β) :
  det (kroneckerMapBilinear f A B) =
    det (A.map fun a => f a 1) ^ Fintype.card n * det (B.map fun b => f 1 b) ^ Fintype.card m

Full source

/-- `determinant` of `Matrix.kroneckerMapBilinear`.

This is primarily used with `R = ℕ` to prove `Matrix.det_kronecker`. -/
theorem det_kroneckerMapBilinear [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m]
    [DecidableEq n] [NonAssocSemiring α] [NonAssocSemiring β] [CommRing γ] [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 m m α) (B : Matrix n n β) :
    det (kroneckerMapBilinear f A B) =
      det (A.map fun a => f a 1) ^ Fintype.card n * det (B.map fun b => f 1 b) ^ Fintype.card m :=
  calc
    det (kroneckerMapBilinear f A B) =
        det (kroneckerMapBilinear f A 1 * kroneckerMapBilinear f 1 B) := by
      rw [← kroneckerMapBilinear_mul_mul f h_comm, Matrix.mul_one, Matrix.one_mul]
    _ = det (blockDiagonal fun (_ : n) => A.map fun a => f a 1) *
        det (blockDiagonal fun (_ : m) => B.map fun b => f 1 b) := by
      rw [det_mul, ← diagonal_one, ← diagonal_one, kroneckerMapBilinear_apply_apply,
        kroneckerMap_diagonal_right _ fun _ => _, kroneckerMapBilinear_apply_apply,
        kroneckerMap_diagonal_left _ fun _ => _, det_reindex_self]
      · intro; exact LinearMap.map_zero₂ _ _
      · intro; exact map_zero _
    _ = _ := by simp_rw [det_blockDiagonal, Finset.prod_const, Finset.card_univ]

Determinant Formula for Bilinear Kronecker Product of Matrices

Informal description

Let $R$ be a commutative semiring, and let $\alpha$, $\beta$ be non-associative semirings and $\gamma$ a commutative ring, all of which are $R$-modules. Given a bilinear map $f \colon \alpha \to_R \beta \to_R \gamma$ satisfying the commutation condition: \[ f(a \cdot b)(a' \cdot b') = f(a)(a') \cdot f(b)(b') \quad \text{for all } a, b \in \alpha \text{ and } a', b' \in \beta, \] then for any square matrices $A \in \text{Matrix}(m, m, \alpha)$ and $B \in \text{Matrix}(n, n, \beta)$, the determinant of their bilinear Kronecker product is given by: \[ \det(\text{kroneckerMapBilinear}\, f\, A\, B) = \det(A')^n \cdot \det(B')^m, \] where $A'$ is the matrix $A$ with entries mapped by $f(\cdot, 1_\beta)$, $B'$ is the matrix $B$ with entries mapped by $f(1_\alpha, \cdot)$, and $m$, $n$ are the sizes of the index sets for $A$ and $B$ respectively.

Matrix.kronecker definition

[Mul α] : Matrix l m α → Matrix n p α → Matrix (l × n) (m × p) α

Full source

/-- The Kronecker product. This is just a shorthand for `kroneckerMap (*)`. Prefer the notation
`⊗ₖ` rather than this definition. -/
@[simp]
def kronecker [Mul α] : Matrix l m α → Matrix n p α → Matrix (l × n) (m × p) α :=
  kroneckerMap (· * ·)

Kronecker product of matrices

Informal description

The Kronecker product of two matrices $ A $ of size $ l \times m $ and $ B $ of size $ n \times p $ with entries in a type $ \alpha $ equipped with multiplication is the matrix of size $ (l \times n) \times (m \times p) $ defined by \[ (A \otimes B)_{(i_1, i_2), (j_1, j_2)} = A_{i_1 j_1} \cdot B_{i_2 j_2}. \] This is a specialization of the general Kronecker map to the case where the function $ f $ is multiplication.

Kronecker.term_⊗ₖ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc Matrix.kroneckerMap]
scoped[Kronecker] infixl:100 " ⊗ₖ " => Matrix.kroneckerMap (· * ·)

Kronecker product notation `⊗ₖ`

Informal description

The notation `A ⊗ₖ B` represents the Kronecker product of two matrices `A` and `B` with coefficients in a type `α` equipped with a multiplication operation. For matrices `A : Matrix l m α` and `B : Matrix n p α`, the Kronecker product `A ⊗ₖ B` is a matrix of type `Matrix (l × n) (m × p) α` defined by `(A ⊗ₖ B) (i₁, i₂) (j₁, j₂) = A i₁ j₁ * B i₂ j₂` for all indices `(i₁, i₂)` and `(j₁, j₂)`.

Matrix.kronecker_apply theorem

 [Mul α] (A : Matrix l m α) (B : Matrix n p α) (i₁ i₂ j₁ j₂) : (A ⊗ₖ B) (i₁, i₂) (j₁, j₂) = A i₁ j₁ * B i₂ j₂

Full source

@[simp]
theorem kronecker_apply [Mul α] (A : Matrix l m α) (B : Matrix n p α) (i₁ i₂ j₁ j₂) :
    (A ⊗ₖ B) (i₁, i₂) (j₁, j₂) = A i₁ j₁ * B i₂ j₂ :=
  rfl

Entrywise Formula for Kronecker Product of Matrices

Informal description

For any type $\alpha$ with a multiplication operation, and for matrices $A \in \text{Matrix}\, l\, m\, \alpha$ and $B \in \text{Matrix}\, n\, p\, \alpha$, the $(i_1, i_2)$-th entry of the Kronecker product $A \otimes_k B$ at position $(j_1, j_2)$ is given by the product of the corresponding entries of $A$ and $B$: \[ (A \otimes_k B)_{(i_1, i_2), (j_1, j_2)} = A_{i_1 j_1} \cdot B_{i_2 j_2}. \]

Matrix.kroneckerBilinear definition

 [CommSemiring R] [Semiring α] [Algebra R α] : Matrix l m α →ₗ[R] Matrix n p α →ₗ[R] Matrix (l × n) (m × p) α

Full source

/-- `Matrix.kronecker` as a bilinear map. -/
def kroneckerBilinear [CommSemiring R] [Semiring α] [Algebra R α] :
    MatrixMatrix l m α →ₗ[R] Matrix n p α →ₗ[R] Matrix (l × n) (m × p) α :=
  kroneckerMapBilinear (Algebra.lmul R α)

Bilinear Kronecker product of matrices over an $R$-algebra

Informal description

Given a commutative semiring $R$ and a semiring $\alpha$ that is an $R$-algebra, the function `Matrix.kroneckerBilinear` is a bilinear map that takes two matrices $A \in \text{Matrix}\, l\, m\, \alpha$ and $B \in \text{Matrix}\, n\, p\, \alpha$ and returns their Kronecker product $A \otimes_k B \in \text{Matrix}\, (l \times n)\, (m \times p)\, \alpha$, where the multiplication is performed using the $R$-algebra structure of $\alpha$.

Matrix.zero_kronecker theorem

[MulZeroClass α] (B : Matrix n p α) : (0 : Matrix l m α) ⊗ₖ B = 0

Full source

theorem zero_kronecker [MulZeroClass α] (B : Matrix n p α) : (0 : Matrix l m α) ⊗ₖ B = 0 :=
  kroneckerMap_zero_left _ zero_mul B

Kronecker Product with Zero Matrix Yields Zero Matrix

Informal description

Let $\alpha$ be a type equipped with a multiplication operation and a zero element $0_\alpha$ forming a `MulZeroClass`. For any matrix $B$ of size $n \times p$ with entries in $\alpha$, the Kronecker product of the zero matrix (of size $l \times m$) with $B$ satisfies \[ 0 \otimes_k B = 0. \]

Matrix.kronecker_zero theorem

[MulZeroClass α] (A : Matrix l m α) : A ⊗ₖ (0 : Matrix n p α) = 0

Full source

theorem kronecker_zero [MulZeroClass α] (A : Matrix l m α) : A ⊗ₖ (0 : Matrix n p α) = 0 :=
  kroneckerMap_zero_right _ mul_zero A

Kronecker Product with Zero Matrix Yields Zero Matrix

Informal description

Let $\alpha$ be a type equipped with a multiplication operation and a zero element $0$ satisfying the multiplicative zero property (i.e., $a \cdot 0 = 0 \cdot a = 0$ for all $a \in \alpha$). For any matrix $A$ of size $l \times m$ with entries in $\alpha$ and the zero matrix $0$ of size $n \times p$ with entries in $\alpha$, the Kronecker product $A \otimes_k 0$ equals the zero matrix.

Matrix.add_kronecker theorem

[Distrib α] (A₁ A₂ : Matrix l m α) (B : Matrix n p α) : (A₁ + A₂) ⊗ₖ B = A₁ ⊗ₖ B + A₂ ⊗ₖ B

Full source

theorem add_kronecker [Distrib α] (A₁ A₂ : Matrix l m α) (B : Matrix n p α) :
    (A₁ + A₂) ⊗ₖ B = A₁ ⊗ₖ B + A₂ ⊗ₖ B :=
  kroneckerMap_add_left _ add_mul _ _ _

Distributivity of Kronecker Product over Matrix Addition in First Argument

Informal description

Let $\alpha$ be a type equipped with addition and multiplication satisfying the distributive property. For any matrices $A_1, A_2$ of size $l \times m$ with entries in $\alpha$ and matrix $B$ of size $n \times p$ with entries in $\alpha$, the Kronecker product satisfies: \[ (A_1 + A_2) \otimes_k B = A_1 \otimes_k B + A_2 \otimes_k B. \]

Matrix.kronecker_add theorem

[Distrib α] (A : Matrix l m α) (B₁ B₂ : Matrix n p α) : A ⊗ₖ (B₁ + B₂) = A ⊗ₖ B₁ + A ⊗ₖ B₂

Full source

theorem kronecker_add [Distrib α] (A : Matrix l m α) (B₁ B₂ : Matrix n p α) :
    A ⊗ₖ (B₁ + B₂) = A ⊗ₖ B₁ + A ⊗ₖ B₂ :=
  kroneckerMap_add_right _ mul_add _ _ _

Distributivity of Kronecker Product over Matrix Addition in Second Argument

Informal description

Let $\alpha$ be a type equipped with addition and multiplication satisfying the distributive property. For any matrix $A$ of size $l \times m$ with entries in $\alpha$ and matrices $B_1, B_2$ of size $n \times p$ with entries in $\alpha$, the Kronecker product satisfies: \[ A \otimes_k (B_1 + B_2) = (A \otimes_k B_1) + (A \otimes_k B_2). \]

Matrix.smul_kronecker theorem

 [Mul α] [SMul R α] [IsScalarTower R α α] (r : R) (A : Matrix l m α) (B : Matrix n p α) : (r • A) ⊗ₖ B = r • A ⊗ₖ B

Full source

theorem smul_kronecker [Mul α] [SMul R α] [IsScalarTower R α α] (r : R)
    (A : Matrix l m α) (B : Matrix n p α) : (r • A) ⊗ₖ B = r • A ⊗ₖ B :=
  kroneckerMap_smul_left _ _ (fun _ _ => smul_mul_assoc _ _ _) _ _

Scalar Multiplication Commutes with Kronecker Product: $(r \cdot A) \otimes_k B = r \cdot (A \otimes_k B)$

Informal description

Let $R$ be a type with a scalar multiplication operation on $\alpha$, and assume that $\alpha$ is equipped with a multiplication operation and that $R$ acts compatibly with $\alpha$ (i.e., $[IsScalarTower\, R\, \alpha\, \alpha]$). For any scalar $r \in R$, matrix $A$ of size $l \times m$ with entries in $\alpha$, and matrix $B$ of size $n \times p$ with entries in $\alpha$, the Kronecker product satisfies: \[ (r \cdot A) \otimes_k B = r \cdot (A \otimes_k B). \]

Matrix.kronecker_smul theorem

 [Mul α] [SMul R α] [SMulCommClass R α α] (r : R) (A : Matrix l m α) (B : Matrix n p α) : A ⊗ₖ (r • B) = r • A ⊗ₖ B

Full source

theorem kronecker_smul [Mul α] [SMul R α] [SMulCommClass R α α] (r : R)
    (A : Matrix l m α) (B : Matrix n p α) : A ⊗ₖ (r • B) = r • A ⊗ₖ B :=
  kroneckerMap_smul_right _ _ (fun _ _ => mul_smul_comm _ _ _) _ _

Scalar Multiplication Commutes with Kronecker Product

Informal description

Let $R$ be a type with a scalar multiplication operation on $\alpha$, and suppose the multiplication and scalar multiplication on $\alpha$ satisfy the scalar commutativity condition `SMulCommClass R α α`. Then for any scalar $r \in R$, matrix $A$ of size $l \times m$ with entries in $\alpha$, and matrix $B$ of size $n \times p$ with entries in $\alpha$, the Kronecker product satisfies: \[ A \otimes_k (r \cdot B) = r \cdot (A \otimes_k B). \]

Matrix.stdBasisMatrix_kronecker_stdBasisMatrix theorem

 [MulZeroClass α] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (ia : l) (ja : m) (ib : n) (jb : p)
  (a b : α) : stdBasisMatrix ia ja a ⊗ₖ stdBasisMatrix ib jb b = stdBasisMatrix (ia, ib) (ja, jb) (a * b)

Full source

theorem stdBasisMatrix_kronecker_stdBasisMatrix
    [MulZeroClass α] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p]
    (ia : l) (ja : m) (ib : n) (jb : p) (a b : α) :
    stdBasisMatrixstdBasisMatrix ia ja a ⊗ₖ stdBasisMatrix ib jb b = stdBasisMatrix (ia, ib) (ja, jb) (a * b) :=
  kroneckerMap_stdBasisMatrix_stdBasisMatrix _ _ _ _ _ zero_mul mul_zero _ _

Kronecker Product of Standard Basis Matrices is Standard Basis Matrix of Product

Informal description

Let $\alpha$ be a type with a multiplication operation and a zero element, and let $l$, $m$, $n$, $p$ be types with decidable equality. For any indices $i_a \in l$, $j_a \in m$, $i_b \in n$, $j_b \in p$ and elements $a, b \in \alpha$, the Kronecker product of the standard basis matrices satisfies: \[ \text{stdBasisMatrix}\, i_a\, j_a\, a \otimes_k \text{stdBasisMatrix}\, i_b\, j_b\, b = \text{stdBasisMatrix}\, (i_a, i_b)\, (j_a, j_b)\, (a \cdot b). \]

Matrix.diagonal_kronecker_diagonal theorem

 [MulZeroClass α] [DecidableEq m] [DecidableEq n] (a : m → α) (b : n → α) :
  diagonal a ⊗ₖ diagonal b = diagonal fun mn => a mn.1 * b mn.2

Full source

theorem diagonal_kronecker_diagonal [MulZeroClass α] [DecidableEq m] [DecidableEq n] (a : m → α)
    (b : n → α) : diagonaldiagonal a ⊗ₖ diagonal b = diagonal fun mn => a mn.1 * b mn.2 :=
  kroneckerMap_diagonal_diagonal _ zero_mul mul_zero _ _

Kronecker Product of Diagonal Matrices is Diagonal with Pointwise Product

Informal description

Let $\alpha$ be a type with a multiplication operation and a zero element, and let $m$ and $n$ be types with decidable equality. For any vectors $a : m \to \alpha$ and $b : n \to \alpha$, the Kronecker product of the diagonal matrices $\text{diagonal}(a)$ and $\text{diagonal}(b)$ is equal to the diagonal matrix whose entries are given by the pointwise product of $a$ and $b$: \[ \text{diagonal}(a) \otimes_k \text{diagonal}(b) = \text{diagonal}\big( (i,j) \mapsto a(i) \cdot b(j) \big). \]

Matrix.kronecker_diagonal theorem

 [MulZeroClass α] [DecidableEq n] (A : Matrix l m α) (b : n → α) : A ⊗ₖ diagonal b = blockDiagonal fun i => A <• b i

Full source

theorem kronecker_diagonal [MulZeroClass α] [DecidableEq n] (A : Matrix l m α) (b : n → α) :
    A ⊗ₖ diagonal b = blockDiagonal fun i => A <• b i :=
  kroneckerMap_diagonal_right _ mul_zero _ _

Kronecker Product with Diagonal Matrix Yields Scaled Block Diagonal Matrix

Informal description

Let $A$ be an $l \times m$ matrix with entries in a type $\alpha$ that has a multiplicative zero element, and let $b : n \to \alpha$ be a vector defining a diagonal matrix $\text{diagonal}(b)$ of size $n \times n$ (where $n$ has decidable equality). Then the Kronecker product $A \otimes_k \text{diagonal}(b)$ is equal to the block diagonal matrix whose $i$-th block is the matrix $A$ with each entry multiplied by $b_i$. In symbols: \[ A \otimes_k \text{diagonal}(b) = \text{blockDiagonal}\, (\lambda i, b_i \cdot A). \]

Matrix.diagonal_kronecker theorem

 [MulZeroClass α] [DecidableEq l] (a : l → α) (B : Matrix m n α) :
  diagonal a ⊗ₖ B = Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal fun i => a i • B)

Full source

theorem diagonal_kronecker [MulZeroClass α] [DecidableEq l] (a : l → α) (B : Matrix m n α) :
    diagonaldiagonal a ⊗ₖ B =
      Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal fun i => a i • B) :=
  kroneckerMap_diagonal_left _ zero_mul _ _

Kronecker Product of Diagonal Matrix with General Matrix via Reindexing and Block Diagonal

Informal description

Let $\alpha$ be a type with a multiplication operation and a zero element (i.e., a `MulZeroClass`), and let $l$, $m$, $n$ be index types with $l$ having decidable equality. Given a diagonal matrix $A = \text{diagonal}(a)$ where $a : l \to \alpha$ defines the diagonal entries, and an arbitrary matrix $B$ of size $m \times n$ with entries in $\alpha$, the Kronecker product $A \otimes_k B$ is equal to the reindexing (via swapping the product order) of the block diagonal matrix whose blocks are scalar multiples $a_i \cdot B$ for each $i \in l$. More precisely: \[ \text{diagonal}(a) \otimes_k B = \text{reindex}(\text{swap}, \text{swap})\left(\text{blockDiagonal}(\lambda i, a_i \cdot B)\right), \] where $\text{swap}$ denotes the product commutativity equivalence between $l \times m$ and $m \times l$.

Matrix.natCast_kronecker_natCast theorem

 [NonAssocSemiring α] [DecidableEq m] [DecidableEq n] (a b : ℕ) : (a : Matrix m m α) ⊗ₖ (b : Matrix n n α) = ↑(a * b)

Full source

@[simp]
theorem natCast_kronecker_natCast [NonAssocSemiring α] [DecidableEq m] [DecidableEq n] (a b : ℕ) :
    (a : Matrix m m α) ⊗ₖ (b : Matrix n n α) = ↑(a * b) :=
  (diagonal_kronecker_diagonal _ _).trans <| by simp_rw [← Nat.cast_mul]; rfl

Kronecker Product of Scalar Matrices is Scalar Matrix of Product

Informal description

Let $\alpha$ be a non-associative semiring, and let $m$ and $n$ be types with decidable equality. For any natural numbers $a$ and $b$, the Kronecker product of the scalar matrices $a I_m$ and $b I_n$ (where $I_m$ and $I_n$ are identity matrices of sizes $m \times m$ and $n \times n$ respectively) is equal to the scalar matrix $(a \cdot b) I_{m \times n}$. In symbols: \[ a I_m \otimes_k b I_n = (a \cdot b) I_{m \times n}. \]

Matrix.kronecker_natCast theorem

 [NonAssocSemiring α] [DecidableEq n] (A : Matrix l m α) (b : ℕ) :
  A ⊗ₖ (b : Matrix n n α) = blockDiagonal fun _ => b • A

Full source

theorem kronecker_natCast [NonAssocSemiring α] [DecidableEq n] (A : Matrix l m α) (b : ℕ) :
    A ⊗ₖ (b : Matrix n n α) = blockDiagonal fun _ => b • A :=
  kronecker_diagonal _ _ |>.trans <| by
    congr! 2
    ext
    simp [(Nat.cast_commute b _).eq]

Kronecker Product with Scalar Matrix: $A \otimes_k bI = b \cdot \text{blockDiagonal}(A)$

Informal description

Let $\alpha$ be a non-associative semiring, $n$ a type with decidable equality, and $A$ an $l \times m$ matrix with entries in $\alpha$. For any natural number $b$, the Kronecker product $A \otimes_k (b : \text{Matrix}\,n\,n\,\alpha)$ is equal to the block diagonal matrix where each block is the scalar multiple $b \cdot A$. In symbols: \[ A \otimes_k (b : \text{Matrix}\,n\,n\,\alpha) = \text{blockDiagonal}\, (\lambda \_, b \cdot A). \]

Matrix.natCast_kronecker theorem

 [NonAssocSemiring α] [DecidableEq l] (a : ℕ) (B : Matrix m n α) :
  (a : Matrix l l α) ⊗ₖ B = Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal fun _ => a • B)

Full source

theorem natCast_kronecker [NonAssocSemiring α] [DecidableEq l] (a : ℕ) (B : Matrix m n α) :
    (a : Matrix l l α) ⊗ₖ B =
      Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal fun _ => a • B) :=
  diagonal_kronecker _ _ |>.trans <| by
    congr! 2
    ext
    simp [(Nat.cast_commute a _).eq]

Kronecker Product of Scalar Matrix with General Matrix via Reindexing and Block Diagonal

Informal description

Let $\alpha$ be a non-associative semiring, $l$ be a type with decidable equality, and $m, n$ be arbitrary types. For any natural number $a \in \mathbb{N}$ and any matrix $B$ of size $m \times n$ with entries in $\alpha$, the Kronecker product of the scalar matrix $a I_l$ (where $I_l$ is the identity matrix of size $l \times l$) with $B$ is equal to the reindexing (via swapping the product order) of the block diagonal matrix whose blocks are scalar multiples $a \cdot B$. More precisely: \[ a I_l \otimes_k B = \text{reindex}(\text{swap}, \text{swap})\left(\text{blockDiagonal}(\lambda \_, a \cdot B)\right), \] where $\text{swap}$ denotes the product commutativity equivalence between $l \times m$ and $m \times l$.

Matrix.kronecker_ofNat theorem

 [NonAssocSemiring α] [DecidableEq n] (A : Matrix l m α) (b : ℕ) [b.AtLeastTwo] :
  A ⊗ₖ (ofNat(b) : Matrix n n α) = blockDiagonal fun _ => A <• (ofNat(b) : α)

Full source

theorem kronecker_ofNat [NonAssocSemiring α] [DecidableEq n] (A : Matrix l m α) (b : ℕ)
    [b.AtLeastTwo] : A ⊗ₖ (ofNat(b) : Matrix n n α) =
      blockDiagonal fun _ => A <• (ofNat(b) : α) :=
  kronecker_diagonal _ _

Kronecker Product with Scalar Matrix of Natural Number $\geq 2$ Yields Scaled Block Diagonal Matrix

Informal description

Let $\alpha$ be a non-associative semiring, $n$ a type with decidable equality, and $A$ an $l \times m$ matrix with entries in $\alpha$. For any natural number $b \geq 2$, the Kronecker product of $A$ with the $n \times n$ scalar matrix $b$ (interpreted as a matrix via the `OfNat` instance) is equal to the block diagonal matrix where each block is the matrix $A$ with all entries multiplied by $b$. In symbols: \[ A \otimes_k b = \text{blockDiagonal}\, (\lambda \_, b \cdot A). \]

Matrix.ofNat_kronecker theorem

 [NonAssocSemiring α] [DecidableEq l] (a : ℕ) [a.AtLeastTwo] (B : Matrix m n α) :
  (ofNat(a) : Matrix l l α) ⊗ₖ B =
    Matrix.reindex (.prodComm _ _) (.prodComm _ _) (blockDiagonal fun _ => (ofNat(a) : α) • B)

Full source

theorem ofNat_kronecker [NonAssocSemiring α] [DecidableEq l] (a : ℕ) [a.AtLeastTwo]
    (B : Matrix m n α) : (ofNat(a) : Matrix l l α) ⊗ₖ B =
      Matrix.reindex (.prodComm _ _) (.prodComm _ _)
        (blockDiagonal fun _ => (ofNat(a) : α) • B) :=
  diagonal_kronecker _ _

Kronecker Product of Scalar Matrix with General Matrix via Reindexing and Block Diagonal

Informal description

Let $\alpha$ be a non-associative semiring, $l$ be a type with decidable equality, and $a \geq 2$ be a natural number. For any matrix $B$ of size $m \times n$ with entries in $\alpha$, the Kronecker product of the scalar matrix $\text{ofNat}(a) : \text{Matrix}\, l\, l\, \alpha$ (which has $a$ on the diagonal and zeros elsewhere) with $B$ is equal to the reindexing (via swapping the product order) of the block diagonal matrix whose blocks are scalar multiples $(a : \alpha) \cdot B$. More precisely: \[ \text{ofNat}(a) \otimes_k B = \text{reindex}(\text{swap}, \text{swap})\left(\text{blockDiagonal}(\lambda \_, a \cdot B)\right), \] where $\text{swap}$ denotes the product commutativity equivalence between $l \times m$ and $m \times l$.

Matrix.one_kronecker_one theorem

[MulZeroOneClass α] [DecidableEq m] [DecidableEq n] : (1 : Matrix m m α) ⊗ₖ (1 : Matrix n n α) = 1

Full source

theorem one_kronecker_one [MulZeroOneClass α] [DecidableEq m] [DecidableEq n] :
    (1 : Matrix m m α) ⊗ₖ (1 : Matrix n n α) = 1 :=
  kroneckerMap_one_one _ zero_mul mul_zero (one_mul _)

Kronecker Product of Identity Matrices Yields Identity Matrix

Informal description

Let $\alpha$ be a type with a multiplicative monoid structure and a zero element (i.e., a `MulZeroOneClass`). For any two square matrices $I_m$ of size $m \times m$ and $I_n$ of size $n \times n$ over $\alpha$ (where $m$ and $n$ have decidable equality), the Kronecker product of the identity matrices is the identity matrix, i.e., \[ I_m \otimes_k I_n = I_{m \times n}. \]

Matrix.kronecker_one theorem

[MulZeroOneClass α] [DecidableEq n] (A : Matrix l m α) : A ⊗ₖ (1 : Matrix n n α) = blockDiagonal fun _ => A

Full source

theorem kronecker_one [MulZeroOneClass α] [DecidableEq n] (A : Matrix l m α) :
    A ⊗ₖ (1 : Matrix n n α) = blockDiagonal fun _ => A :=
  (kronecker_diagonal _ _).trans <| congr_arg _ <| funext fun _ => Matrix.ext fun _ _ => mul_one _

Kronecker Product with Identity Matrix Yields Block Diagonal Matrix

Informal description

Let $\alpha$ be a type with multiplicative and zero elements forming a `MulZeroOneClass`, and let $n$ be a type with decidable equality. For any matrix $A$ of size $l \times m$ with entries in $\alpha$, the Kronecker product of $A$ with the identity matrix of size $n \times n$ is equal to the block diagonal matrix where each block is $A$. In symbols: \[ A \otimes_k I_n = \text{blockDiagonal}\, (\lambda \_, A), \] where $I_n$ denotes the identity matrix of size $n \times n$.

Matrix.one_kronecker theorem

 [MulZeroOneClass α] [DecidableEq l] (B : Matrix m n α) :
  (1 : Matrix l l α) ⊗ₖ B = Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal fun _ => B)

Full source

theorem one_kronecker [MulZeroOneClass α] [DecidableEq l] (B : Matrix m n α) :
    (1 : Matrix l l α) ⊗ₖ B =
      Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal fun _ => B) :=
  (diagonal_kronecker _ _).trans <|
    congr_arg _ <| congr_arg _ <| funext fun _ => Matrix.ext fun _ _ => one_mul _

Kronecker Product of Identity Matrix with General Matrix via Reindexing and Block Diagonal

Informal description

Let $\alpha$ be a type with a multiplication operation and a zero element (i.e., a `MulZeroOneClass`), and let $l$, $m$, $n$ be index types with $l$ having decidable equality. Given the identity matrix $1_l$ of size $l \times l$ over $\alpha$ and an arbitrary matrix $B$ of size $m \times n$ over $\alpha$, the Kronecker product $1_l \otimes_k B$ is equal to the reindexing (via swapping the product order) of the block diagonal matrix whose blocks are all equal to $B$. More precisely: \[ 1_l \otimes_k B = \text{reindex}(\text{swap}, \text{swap})\left(\text{blockDiagonal}(\lambda \_, B)\right), \] where $\text{swap}$ denotes the product commutativity equivalence between $l \times m$ and $m \times l$.

Matrix.mul_kronecker_mul theorem

 [Fintype m] [Fintype m'] [CommSemiring α] (A : Matrix l m α) (B : Matrix m n α) (A' : Matrix l' m' α)
  (B' : Matrix m' n' α) : (A * B) ⊗ₖ (A' * B') = A ⊗ₖ A' * B ⊗ₖ B'

Full source

theorem mul_kronecker_mul [Fintype m] [Fintype m'] [CommSemiring α] (A : Matrix l m α)
    (B : Matrix m n α) (A' : Matrix l' m' α) (B' : Matrix m' n' α) :
    (A * B) ⊗ₖ (A' * B') = A ⊗ₖ A' * B ⊗ₖ B' :=
  kroneckerMapBilinear_mul_mul (Algebra.lmul ℕ α).toLinearMap mul_mul_mul_comm A B A' B'

Kronecker Product Distributes over Matrix Multiplication: $(AB) \otimes_k (A'B') = (A \otimes_k A')(B \otimes_k B')$

Informal description

Let $\alpha$ be a commutative semiring, and let $m$, $m'$ be finite types. For any matrices $A \in \text{Matrix}\, l\, m\, \alpha$, $B \in \text{Matrix}\, m\, n\, \alpha$, $A' \in \text{Matrix}\, l'\, m'\, \alpha$, and $B' \in \text{Matrix}\, m'\, n'\, \alpha$, the Kronecker product of the matrix products $A * B$ and $A' * B'$ is equal to the product of the Kronecker products $A \otimes_k A'$ and $B \otimes_k B'$. In symbols: \[ (A * B) \otimes_k (A' * B') = (A \otimes_k A') * (B \otimes_k B'). \]

Matrix.kronecker_assoc theorem

 [Semigroup α] (A : Matrix l m α) (B : Matrix n p α) (C : Matrix q r α) :
  reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r) (A ⊗ₖ B ⊗ₖ C) = A ⊗ₖ (B ⊗ₖ C)

Full source

theorem kronecker_assoc [Semigroup α] (A : Matrix l m α) (B : Matrix n p α) (C : Matrix q r α) :
    reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r) (A ⊗ₖ BA ⊗ₖ B ⊗ₖ C) = A ⊗ₖ (B ⊗ₖ C) :=
  kroneckerMap_assoc₁ _ _ _ _ A B C mul_assoc

Associativity of the Kronecker Product of Matrices

Informal description

Let $\alpha$ be a semigroup, and let $A$, $B$, and $C$ be matrices with entries in $\alpha$ of sizes $l \times m$, $n \times p$, and $q \times r$ respectively. Then, the Kronecker product satisfies the associativity property: \[ \text{reindex}\, (\text{prodAssoc}\, l\, n\, q)\, (\text{prodAssoc}\, m\, p\, r)\, (A \otimes_k B \otimes_k C) = A \otimes_k (B \otimes_k C), \] where $\text{reindex}$ applies the associativity equivalence on product indices, and $\otimes_k$ denotes the Kronecker product of matrices.

Matrix.kronecker_assoc' theorem

 [Semigroup α] (A : Matrix l m α) (B : Matrix n p α) (C : Matrix q r α) :
  submatrix (A ⊗ₖ B ⊗ₖ C) (Equiv.prodAssoc l n q).symm (Equiv.prodAssoc m p r).symm = A ⊗ₖ (B ⊗ₖ C)

Full source

@[simp]
theorem kronecker_assoc' [Semigroup α] (A : Matrix l m α) (B : Matrix n p α) (C : Matrix q r α) :
    submatrix (A ⊗ₖ BA ⊗ₖ B ⊗ₖ C) (Equiv.prodAssoc l n q).symm (Equiv.prodAssoc m p r).symm =
    A ⊗ₖ (B ⊗ₖ C) :=
  kroneckerMap_assoc₁ _ _ _ _ A B C mul_assoc

Associativity of Kronecker Product via Submatrix and Equivalence

Informal description

Let $\alpha$ be a semigroup, and let $A \in \text{Matrix}\, l\, m\, \alpha$, $B \in \text{Matrix}\, n\, p\, \alpha$, and $C \in \text{Matrix}\, q\, r\, \alpha$ be matrices. Then the submatrix of the triple Kronecker product $A \otimes_k B \otimes_k C$, obtained by applying the inverse of the associativity equivalence on the row and column indices, is equal to the Kronecker product $A \otimes_k (B \otimes_k C)$. In other words, the following equality holds: \[ \text{submatrix}\, (A \otimes_k B \otimes_k C)\, (\text{Equiv.prodAssoc}\, l\, n\, q)^{-1}\, (\text{Equiv.prodAssoc}\, m\, p\, r)^{-1} = A \otimes_k (B \otimes_k C), \] where $\text{submatrix}$ restricts the matrix to the specified row and column indices, and $\otimes_k$ denotes the Kronecker product.

Matrix.trace_kronecker theorem

[Fintype m] [Fintype n] [Semiring α] (A : Matrix m m α) (B : Matrix n n α) : trace (A ⊗ₖ B) = trace A * trace B

Full source

theorem trace_kronecker [Fintype m] [Fintype n] [Semiring α] (A : Matrix m m α) (B : Matrix n n α) :
    trace (A ⊗ₖ B) = trace A * trace B :=
  trace_kroneckerMapBilinear (Algebra.lmul ℕ α).toLinearMap _ _

Trace of Kronecker Product Equals Product of Traces

Informal description

For any square matrices $A$ of size $m \times m$ and $B$ of size $n \times n$ over a semiring $\alpha$, the trace of their Kronecker product $A \otimes_k B$ equals the product of their traces: \[ \operatorname{trace}(A \otimes_k B) = \operatorname{trace}(A) \cdot \operatorname{trace}(B). \]

Matrix.det_kronecker theorem

 [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing R] (A : Matrix m m R) (B : Matrix n n R) :
  det (A ⊗ₖ B) = det A ^ Fintype.card n * det B ^ Fintype.card m

Full source

theorem det_kronecker [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing R]
    (A : Matrix m m R) (B : Matrix n n R) :
    det (A ⊗ₖ B) = det A ^ Fintype.card n * det B ^ Fintype.card m := by
  refine (det_kroneckerMapBilinear (Algebra.lmul ℕ R).toLinearMap mul_mul_mul_comm _ _).trans ?_
  congr 3
  · ext i j
    exact mul_one _
  · ext i j
    exact one_mul _

Determinant of Kronecker Product: $\det(A \otimes_k B) = (\det A)^n (\det B)^m$

Informal description

Let $R$ be a commutative ring, and let $A$ and $B$ be square matrices over $R$ of sizes $m \times m$ and $n \times n$ respectively. Then the determinant of their Kronecker product $A \otimes_k B$ is given by: \[ \det(A \otimes_k B) = (\det A)^n \cdot (\det B)^m. \]

Kronecker.term_⊗ₖₜ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc kroneckerTMul]
scoped[Kronecker] infixl:100 " ⊗ₖₜ " => Matrix.kroneckerMap (· ⊗ₜ ·)

Kronecker tensor product notation

Informal description

The notation `A ⊗ₖₜ B` represents the Kronecker tensor product of matrices `A` and `B`, defined as `Matrix.kroneckerMap (· ⊗ₜ ·) A B`. This operation applies the tensor product `⊗ₜ` element-wise to pairs of elements from matrices `A` and `B`.

Kronecker.term_⊗ₖₜ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc kroneckerTMul] scoped[Kronecker] notation:100 x " ⊗ₖₜ[" R "] " y:100 =>
  Matrix.kroneckerMap (TensorProduct.tmul R) x y

Kronecker tensor product notation

Informal description

The notation `A ⊗ₖₜ[R] B` represents the Kronecker product of matrices `A` and `B` using the tensor product `⊗ₜ` over the ring `R`, defined as `Matrix.kroneckerMap (TensorProduct.tmul R) A B`. This operation creates a new matrix where each element of `A` is multiplied (via tensor product) with each element of `B`.

Matrix.kroneckerTMul_apply theorem

 (A : Matrix l m α) (B : Matrix n p β) (i₁ i₂ j₁ j₂) : (A ⊗ₖₜ B) (i₁, i₂) (j₁, j₂) = A i₁ j₁ ⊗ₜ[R] B i₂ j₂

Full source

@[simp]
theorem kroneckerTMul_apply (A : Matrix l m α) (B : Matrix n p β) (i₁ i₂ j₁ j₂) :
    (A ⊗ₖₜ B) (i₁, i₂) (j₁, j₂) = A i₁ j₁ ⊗ₜ[R] B i₂ j₂ :=
  rfl

Entry Formula for Kronecker Tensor Product of Matrices

Informal description

For matrices $A$ of size $l \times m$ with entries in $\alpha$ and $B$ of size $n \times p$ with entries in $\beta$, the $(i_1,i_2),(j_1,j_2)$-entry of the Kronecker tensor product $A \otimes_{k,t} B$ (with respect to a tensor product operation $\otimes_t$ over a ring $R$) is given by: \[ (A \otimes_{k,t} B)_{(i_1,i_2),(j_1,j_2)} = A_{i_1 j_1} \otimes_t B_{i_2 j_2}. \]

Matrix.kroneckerTMulBilinear_apply theorem

(A : Matrix l m α) (B : Matrix n p β) : kroneckerTMulBilinear R A B = A ⊗ₖₜ B

Full source

@[simp]
theorem kroneckerTMulBilinear_apply (A : Matrix l m α) (B : Matrix n p β) :
    kroneckerTMulBilinear R A B = A ⊗ₖₜ B := rfl

Bilinear Kronecker Tensor Product Equals Kronecker Tensor Product

Informal description

For matrices $A$ of size $l \times m$ with entries in $\alpha$ and $B$ of size $n \times p$ with entries in $\beta$, the bilinear Kronecker tensor product map evaluated at $(A, B)$ equals the Kronecker tensor product $A \otimes_{k,t} B$ over the ring $R$, i.e., \[ \text{kroneckerTMulBilinear}_R\, A\, B = A \otimes_{k,t} B. \]

Matrix.zero_kroneckerTMul theorem

(B : Matrix n p β) : (0 : Matrix l m α) ⊗ₖₜ[R] B = 0

Full source

theorem zero_kroneckerTMul (B : Matrix n p β) : (0 : Matrix l m α) ⊗ₖₜ[R] B = 0 :=
  kroneckerMap_zero_left _ (zero_tmul α) B

Zero Matrix Kronecker Tensor Product Yields Zero Matrix

Informal description

For any matrix $B$ of size $n \times p$ with entries in $\beta$, the Kronecker tensor product of the zero matrix (of size $l \times m$ with entries in $\alpha$) with $B$ is equal to the zero matrix, i.e., \[ 0 \otimes_{k,t} B = 0. \]

Matrix.kroneckerTMul_zero theorem

(A : Matrix l m α) : A ⊗ₖₜ[R] (0 : Matrix n p β) = 0

Full source

theorem kroneckerTMul_zero (A : Matrix l m α) : A ⊗ₖₜ[R] (0 : Matrix n p β) = 0 :=
  kroneckerMap_zero_right _ (tmul_zero β) A

Kronecker Tensor Product with Zero Matrix Yields Zero Matrix

Informal description

For any matrix $A$ of size $l \times m$ with entries in $\alpha$, the Kronecker tensor product of $A$ with the zero matrix of size $n \times p$ with entries in $\beta$ is equal to the zero matrix, i.e., \[ A \otimes_{kₜ[R]} 0 = 0. \]

Matrix.add_kroneckerTMul theorem

(A₁ A₂ : Matrix l m α) (B : Matrix n p α) : (A₁ + A₂) ⊗ₖₜ[R] B = A₁ ⊗ₖₜ B + A₂ ⊗ₖₜ B

Full source

theorem add_kroneckerTMul (A₁ A₂ : Matrix l m α) (B : Matrix n p α) :
    (A₁ + A₂) ⊗ₖₜ[R] B = A₁ ⊗ₖₜ B + A₂ ⊗ₖₜ B :=
  kroneckerMap_add_left _ add_tmul _ _ _

Additivity of Kronecker Tensor Product in the Left Argument: $(A_1 + A_2) \otimesₖₜ B = A_1 \otimesₖₜ B + A_2 \otimesₖₜ B$

Informal description

For any matrices $A_1, A_2$ of size $l \times m$ and matrix $B$ of size $n \times p$ with entries in a type $\alpha$ equipped with a tensor product operation $\otimesₜ$ over a ring $R$, the Kronecker tensor product satisfies: \[ (A_1 + A_2) \otimesₖₜ[R] B = A_1 \otimesₖₜ B + A_2 \otimesₖₜ B. \]

Matrix.kroneckerTMul_add theorem

(A : Matrix l m α) (B₁ B₂ : Matrix n p α) : A ⊗ₖₜ[R] (B₁ + B₂) = A ⊗ₖₜ B₁ + A ⊗ₖₜ B₂

Full source

theorem kroneckerTMul_add (A : Matrix l m α) (B₁ B₂ : Matrix n p α) :
    A ⊗ₖₜ[R] (B₁ + B₂) = A ⊗ₖₜ B₁ + A ⊗ₖₜ B₂ :=
  kroneckerMap_add_right _ tmul_add _ _ _

Additivity of Kronecker Tensor Product in the Right Argument: $A \otimesₖₜ (B_1 + B_2) = A \otimesₖₜ B_1 + A \otimesₖₜ B_2$

Informal description

For any matrix $A$ of size $l \times m$ with entries in $\alpha$ and matrices $B_1, B_2$ of size $n \times p$ with entries in $\alpha$, the Kronecker tensor product satisfies: \[ A \otimes_{kₜ[R]} (B_1 + B_2) = A \otimes_{kₜ} B_1 + A \otimes_{kₜ} B_2. \]

Matrix.smul_kroneckerTMul theorem

(r : R) (A : Matrix l m α) (B : Matrix n p α) : (r • A) ⊗ₖₜ[R] B = r • A ⊗ₖₜ B

Full source

theorem smul_kroneckerTMul (r : R) (A : Matrix l m α) (B : Matrix n p α) :
    (r • A) ⊗ₖₜ[R] B = r • A ⊗ₖₜ B :=
  kroneckerMap_smul_left _ _ (fun _ _ => smul_tmul' _ _ _) _ _

Scalar Multiplication Commutes with Kronecker Tensor Product: $(r \cdot A) \otimes_{kₜ[R]} B = r \cdot (A \otimes_{kₜ} B)$

Informal description

Let $R$ be a scalar multiplication domain, and let $A$ be an $l \times m$ matrix and $B$ an $n \times p$ matrix with entries in $\alpha$. For any scalar $r \in R$, the Kronecker tensor product satisfies: \[ (r \cdot A) \otimes_{kₜ[R]} B = r \cdot (A \otimes_{kₜ} B). \]

Matrix.kroneckerTMul_smul theorem

(r : R) (A : Matrix l m α) (B : Matrix n p α) : A ⊗ₖₜ[R] (r • B) = r • A ⊗ₖₜ B

Full source

theorem kroneckerTMul_smul (r : R) (A : Matrix l m α) (B : Matrix n p α) :
    A ⊗ₖₜ[R] (r • B) = r • A ⊗ₖₜ B :=
  kroneckerMap_smul_right _ _ (fun _ _ => tmul_smul _ _ _) _ _

Scalar Multiplication Commutes with Kronecker Tensor Product: $A \otimes_{kₜ[R]} (r \cdot B) = r \cdot (A \otimes_{kₜ} B)$

Informal description

Let $R$ be a scalar multiplication domain, and let $A$ be an $l \times m$ matrix and $B$ an $n \times p$ matrix with entries in $\alpha$. For any scalar $r \in R$, the Kronecker tensor product satisfies: \[ A \otimes_{kₜ[R]} (r \cdot B) = r \cdot (A \otimes_{kₜ} B). \]

Matrix.stdBasisMatrix_kroneckerTMul_stdBasisMatrix theorem

 [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (i₁ : l) (j₁ : m) (i₂ : n) (j₂ : p) (a : α) (b : β) :
  stdBasisMatrix i₁ j₁ a ⊗ₖₜ[R] stdBasisMatrix i₂ j₂ b = stdBasisMatrix (i₁, i₂) (j₁, j₂) (a ⊗ₜ b)

Full source

theorem stdBasisMatrix_kroneckerTMul_stdBasisMatrix
    [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p]
    (i₁ : l) (j₁ : m) (i₂ : n) (j₂ : p) (a : α) (b : β) :
    stdBasisMatrixstdBasisMatrix i₁ j₁ a ⊗ₖₜ[R] stdBasisMatrix i₂ j₂ b =
      stdBasisMatrix (i₁, i₂) (j₁, j₂) (a ⊗ₜ b) :=
  kroneckerMap_stdBasisMatrix_stdBasisMatrix _ _ _ _ _ (zero_tmul _) (tmul_zero _) _ _

Kronecker Tensor Product of Standard Basis Matrices is Standard Basis Matrix of Tensor Product

Informal description

Let $l$, $m$, $n$, and $p$ be types with decidable equality. Given indices $i_1 \in l$, $j_1 \in m$, $i_2 \in n$, $j_2 \in p$, and elements $a \in \alpha$ and $b \in \beta$, the Kronecker tensor product of the standard basis matrices satisfies: \[ \text{stdBasisMatrix}\, i_1\, j_1\, a \otimes_{kₜ[R]} \text{stdBasisMatrix}\, i_2\, j_2\, b = \text{stdBasisMatrix}\, (i_1, i_2)\, (j_1, j_2)\, (a \otimes_{ₜ} b). \]

Matrix.diagonal_kroneckerTMul_diagonal theorem

 [DecidableEq m] [DecidableEq n] (a : m → α) (b : n → α) :
  diagonal a ⊗ₖₜ[R] diagonal b = diagonal fun mn => a mn.1 ⊗ₜ b mn.2

Full source

theorem diagonal_kroneckerTMul_diagonal [DecidableEq m] [DecidableEq n] (a : m → α) (b : n → α) :
    diagonaldiagonal a ⊗ₖₜ[R] diagonal b = diagonal fun mn => a mn.1 ⊗ₜ b mn.2 :=
  kroneckerMap_diagonal_diagonal _ (zero_tmul _) (tmul_zero _) _ _

Kronecker Tensor Product of Diagonal Matrices is Diagonal

Informal description

Let $R$ be a commutative ring, and let $\alpha$ be an $R$-module. For any finite types $m$ and $n$ with decidable equality, and for any vectors $a : m \to \alpha$ and $b : n \to \alpha$, the Kronecker tensor product of the diagonal matrices $\text{diagonal}(a)$ and $\text{diagonal}(b)$ is equal to the diagonal matrix whose entries are given by the tensor product of the corresponding entries of $a$ and $b$. Specifically, \[ \text{diagonal}(a) \otimes_{kₜ[R]} \text{diagonal}(b) = \text{diagonal}\big(\lambda (i,j), a_i \otimes_{R} b_j\big). \]

Matrix.kroneckerTMul_diagonal theorem

 [DecidableEq n] (A : Matrix l m α) (b : n → α) :
  A ⊗ₖₜ[R] diagonal b = blockDiagonal fun i => A.map fun a => a ⊗ₜ[R] b i

Full source

theorem kroneckerTMul_diagonal [DecidableEq n] (A : Matrix l m α) (b : n → α) :
    A ⊗ₖₜ[R] diagonal b = blockDiagonal fun i => A.map fun a => a ⊗ₜ[R] b i :=
  kroneckerMap_diagonal_right _ (tmul_zero _) _ _

Kronecker Tensor Product with Diagonal Matrix Yields Block Diagonal Matrix

Informal description

Let $R$ be a commutative ring, $\alpha$ a type with a module structure over $R$, and $n$ a type with decidable equality. Given an $l \times m$ matrix $A$ with entries in $\alpha$ and a diagonal $n \times n$ matrix $\text{diagonal}(b)$ with diagonal entries $b_i \in \alpha$, the Kronecker tensor product $A \otimes_{kₜ[R]} \text{diagonal}(b)$ is equal to the block diagonal matrix whose $i$-th block is the matrix $A$ with each entry $a$ replaced by $a \otimes_{R} b_i$. In symbols: \[ A \otimes_{kₜ[R]} \text{diagonal}(b) = \text{blockDiagonal} \left( \lambda i, A.\text{map} (\lambda a, a \otimes_{R} b_i) \right). \]

Matrix.diagonal_kroneckerTMul theorem

 [DecidableEq l] (a : l → α) (B : Matrix m n α) :
  diagonal a ⊗ₖₜ[R] B =
    Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal fun i => B.map fun b => a i ⊗ₜ[R] b)

Full source

theorem diagonal_kroneckerTMul [DecidableEq l] (a : l → α) (B : Matrix m n α) :
    diagonaldiagonal a ⊗ₖₜ[R] B =
      Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _)
        (blockDiagonal fun i => B.map fun b => a i ⊗ₜ[R] b) :=
  kroneckerMap_diagonal_left _ (zero_tmul _) _ _

Kronecker Tensor Product of Diagonal Matrix with General Matrix via Reindexing

Informal description

Let $R$ be a commutative ring, $l$, $m$, $n$ be types with decidable equality on $l$, $a : l \to \alpha$ be a vector, and $B$ be an $m \times n$ matrix with entries in $\alpha$. Then the Kronecker tensor product of the diagonal matrix $\text{diagonal}(a)$ with $B$ is equal to the reindexing (via swapping coordinates) of the block diagonal matrix whose blocks are $B$ with each entry multiplied by $a_i$ under the tensor product $\otimes_{R}$. More precisely: \[ \text{diagonal}(a) \otimes_{kₜ[R]} B = \text{reindex}_{\text{prodComm}(l,m), \text{prodComm}(l,n)} \left( \text{blockDiagonal} \left( \lambda i, B.\text{map} (\lambda b, a_i \otimes_{R} b) \right) \right) \]

Matrix.kroneckerTMul_assoc theorem

 (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ) :
  reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r) (((A ⊗ₖₜ[R] B) ⊗ₖₜ[R] C).map (TensorProduct.assoc R α β γ)) =
    A ⊗ₖₜ[R] B ⊗ₖₜ[R] C

Full source

theorem kroneckerTMul_assoc (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ) :
    reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)
        (((A ⊗ₖₜ[R] B) ⊗ₖₜ[R] C).map (TensorProduct.assoc R α β γ)) =
      A ⊗ₖₜ[R] B ⊗ₖₜ[R] C :=
  ext fun _ _ => assoc_tmul _ _ _

Associativity of Kronecker Tensor Product of Matrices over a Commutative Ring

Informal description

Let $A$ be an $l \times m$ matrix, $B$ an $n \times p$ matrix, and $C$ a $q \times r$ matrix, all with entries in appropriate types over a commutative ring $R$. Then the following equality holds after reindexing and applying the tensor product associativity map: \[ \text{reindex}_{\text{prodAssoc}(l,n,q), \text{prodAssoc}(m,p,r)} \left( ((A \otimes_{kₜ[R]} B) \otimes_{kₜ[R]} C) \circ \text{TensorProduct.assoc}_R \right) = A \otimes_{kₜ[R]} (B \otimes_{kₜ[R]} C), \] where $\text{reindex}$ adjusts the matrix indices according to the product associativity equivalence, and $\otimes_{kₜ[R]}$ denotes the Kronecker tensor product of matrices over $R$.

Matrix.kroneckerTMul_assoc' theorem

 (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ) :
  submatrix (((A ⊗ₖₜ[R] B) ⊗ₖₜ[R] C).map (TensorProduct.assoc R α β γ)) (Equiv.prodAssoc l n q).symm
      (Equiv.prodAssoc m p r).symm =
    A ⊗ₖₜ[R] B ⊗ₖₜ[R] C

Full source

@[simp]
theorem kroneckerTMul_assoc' (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ) :
    submatrix (((A ⊗ₖₜ[R] B) ⊗ₖₜ[R] C).map (TensorProduct.assoc R α β γ))
      (Equiv.prodAssoc l n q).symm (Equiv.prodAssoc m p r).symm = A ⊗ₖₜ[R] B ⊗ₖₜ[R] C :=
  ext fun _ _ => assoc_tmul _ _ _

Associativity of Kronecker Tensor Product of Matrices via Submatrix and Reindexing

Informal description

Let $A$ be an $l \times m$ matrix, $B$ an $n \times p$ matrix, and $C$ a $q \times r$ matrix, all with entries in appropriate types over a commutative ring $R$. Then the following equality holds after applying the tensor product associativity map and reindexing via the inverse of the product associativity equivalence: \[ \text{submatrix}\left( \left((A \otimes_{kₜ[R]} B) \otimes_{kₜ[R]} C\right) \circ \text{TensorProduct.assoc}_R, \text{prodAssoc}(l,n,q)^{-1}, \text{prodAssoc}(m,p,r)^{-1} \right) = A \otimes_{kₜ[R]} (B \otimes_{kₜ[R]} C), \] where $\otimes_{kₜ[R]}$ denotes the Kronecker tensor product of matrices over $R$, and $\text{submatrix}$ adjusts the matrix indices according to the given reindexing functions.

Matrix.trace_kroneckerTMul theorem

[Fintype m] [Fintype n] (A : Matrix m m α) (B : Matrix n n β) : trace (A ⊗ₖₜ[R] B) = trace A ⊗ₜ[R] trace B

Full source

theorem trace_kroneckerTMul [Fintype m] [Fintype n] (A : Matrix m m α) (B : Matrix n n β) :
    trace (A ⊗ₖₜ[R] B) = tracetrace A ⊗ₜ[R] trace B :=
  trace_kroneckerMapBilinear (TensorProduct.mk R α β) _ _

Trace of Kronecker Tensor Product Equals Tensor Product of Traces

Informal description

Let $A$ be an $m \times m$ matrix and $B$ be an $n \times n$ matrix over appropriate types. The trace of their Kronecker tensor product $A \otimes_{kₜ[R]} B$ is equal to the tensor product of their traces: \[ \operatorname{trace}(A \otimes_{kₜ[R]} B) = \operatorname{trace}(A) \otimes_{kₜ[R]} \operatorname{trace}(B). \]

Matrix.one_kroneckerTMul_one theorem

[DecidableEq m] [DecidableEq n] : (1 : Matrix m m α) ⊗ₖₜ[R] (1 : Matrix n n α) = 1

Full source

@[simp]
theorem one_kroneckerTMul_one [DecidableEq m] [DecidableEq n] :
    (1 : Matrix m m α) ⊗ₖₜ[R] (1 : Matrix n n α) = 1 :=
  kroneckerMap_one_one _ (zero_tmul _) (tmul_zero _) rfl

Kronecker Tensor Product of Identity Matrices Yields Identity Matrix

Informal description

Let $m$ and $n$ be types with decidable equality, and let $I_m$ and $I_n$ be the identity matrices of sizes $m \times m$ and $n \times n$ respectively over a type $\alpha$. Then the Kronecker tensor product of $I_m$ and $I_n$ is the identity matrix of size $(m \times n) \times (m \times n)$, i.e., \[ I_m \otimes_{kₜ[R]} I_n = I_{m \times n}. \]

Matrix.mul_kroneckerTMul_mul theorem

 [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') = A ⊗ₖₜ[R] A' * B ⊗ₖₜ[R] B'

Full source

theorem mul_kroneckerTMul_mul [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') = A ⊗ₖₜ[R] A' * B ⊗ₖₜ[R] B' :=
  kroneckerMapBilinear_mul_mul (TensorProduct.mk R α β) tmul_mul_tmul A B A' B'

Kronecker Tensor Product Distributes over Matrix Multiplication: $(AB) \otimes_{kₜ[R]} (A'B') = (A \otimes_{kₜ[R]} A') (B \otimes_{kₜ[R]} B')$

Informal description

Let $R$ be a commutative semiring, and let $\alpha$ and $\beta$ be types. For matrices $A \in \text{Matrix}\, l\, m\, \alpha$, $B \in \text{Matrix}\, m\, n\, \alpha$, $A' \in \text{Matrix}\, l'\, m'\, \beta$, and $B' \in \text{Matrix}\, m'\, n'\, \beta$, where $m$ and $m'$ are finite types, the Kronecker tensor product satisfies the following identity: \[ (A * B) \otimes_{kₜ[R]} (A' * B') = (A \otimes_{kₜ[R]} A') * (B \otimes_{kₜ[R]} B'). \] Here, $\otimes_{kₜ[R]}$ denotes the Kronecker tensor product over $R$, and $*$ denotes matrix multiplication.

Matrix.det_kroneckerTMul theorem

 [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m m α) (B : Matrix n n β) :
  det (A ⊗ₖₜ[R] B) = (det A ^ Fintype.card n) ⊗ₜ[R] (det B ^ Fintype.card m)

Full source

theorem det_kroneckerTMul [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
    (A : Matrix m m α) (B : Matrix n n β) :
    det (A ⊗ₖₜ[R] B) = (det A ^ Fintype.card n) ⊗ₜ[R] (det B ^ Fintype.card m) := by
  refine (det_kroneckerMapBilinear (TensorProduct.mk R α β) tmul_mul_tmul _ _).trans ?_
  simp (config := { eta := false }) only [mk_apply, ← includeLeft_apply (S := R),
    ← includeRight_apply]
  simp only [← AlgHom.mapMatrix_apply, ← AlgHom.map_det]
  simp only [includeLeft_apply, includeRight_apply, tmul_pow, tmul_mul_tmul, one_pow,
    _root_.mul_one, _root_.one_mul]

Determinant of Kronecker Tensor Product: $\det(A \otimes_{kₜ[R]} B) = (\det A)^n \otimesₜ[R] (\det B)^m$

Informal description

Let $R$ be a commutative semiring, and let $\alpha$ and $\beta$ be types. For square matrices $A \in \text{Matrix}(m, m, \alpha)$ and $B \in \text{Matrix}(n, n, \beta)$, where $m$ and $n$ are finite types with decidable equality, the determinant of their Kronecker tensor product is given by: \[ \det(A \otimes_{kₜ[R]} B) = (\det A)^n \otimesₜ[R] (\det B)^m. \] Here, $\otimes_{kₜ[R]}$ denotes the Kronecker tensor product over $R$, and $\otimesₜ[R]$ denotes the tensor product in the module structure over $R$.

Mathlib.Data.Matrix.Kronecker

Main definitions

Specializations

Notations