Kronecker product of matrices #
This defines the Kronecker product.
Main definitions #
Matrix.kroneckerMap: A generalization of the Kronecker product: given a mapf : α → β → γand matricesAandBwith coefficients inαandβ, respectively, it is defined as the matrix with coefficients inγsuch thatkroneckerMap f A B (i₁, i₂) (j₁, j₂) = f (A i₁ j₁) (B i₁ j₂).Matrix.kroneckerMapBilinear: whenfis bilinear, so iskroneckerMap f.
Specializations #
Matrix.kronecker: An alias ofkroneckerMap (*). Prefer using the notation.Matrix.kroneckerBilinear:Matrix.kroneckeris bilinearMatrix.kroneckerTMul: An alias ofkroneckerMap (⊗ₜ). Prefer using the notation.Matrix.kroneckerTMulBilinear:Matrix.kroneckerTMulis bilinear
Notations #
These require open Kronecker:
A ⊗ₖ BforkroneckerMap (*) A B. Lemmas about this notation use the tokenkronecker.A ⊗ₖₜ BandA ⊗ₖₜ[R] BforkroneckerMap (⊗ₜ) A B. Lemmas about this notation use the tokenkroneckerTMul.
def
Matrix.kroneckerMap
{α : 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 β)
:
Produce a matrix with f applied to every pair of elements from A and B.
Equations
- Matrix.kroneckerMap f A B = Matrix.of fun (i : l × n) (j : m × p) => f (A i.1 j.1) (B i.2 j.2)
Instances For
theorem
Matrix.kroneckerMap_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 β)
:
Matrix.kroneckerMap f A.transpose B.transpose = (Matrix.kroneckerMap f A B).transpose
theorem
Matrix.kroneckerMap_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.kroneckerMap f (A.map g) B = Matrix.kroneckerMap (fun (a : α) (b : β) => f (g a) b) A B
theorem
Matrix.kroneckerMap_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.kroneckerMap f A (B.map g) = Matrix.kroneckerMap (fun (a : α) (b : β) => f a (g b)) A B
theorem
Matrix.kroneckerMap_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.kroneckerMap f A B).map g = Matrix.kroneckerMap (fun (a : α) (b : β) => g (f a b)) A B
theorem
Matrix.kroneckerMap_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}
[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 β)
:
Matrix.kroneckerMap f (A₁ + A₂) B = Matrix.kroneckerMap f A₁ B + Matrix.kroneckerMap f A₂ B
theorem
Matrix.kroneckerMap_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}
[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 β)
:
Matrix.kroneckerMap f A (B₁ + B₂) = Matrix.kroneckerMap f A B₁ + Matrix.kroneckerMap f A B₂
theorem
Matrix.kroneckerMap_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}
[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 β)
:
Matrix.kroneckerMap f (r • A) B = r • Matrix.kroneckerMap f A B
theorem
Matrix.kroneckerMap_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}
[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 β)
:
Matrix.kroneckerMap f A (r • B) = r • Matrix.kroneckerMap f A B
theorem
Matrix.kroneckerMap_diagonal_diagonal
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{m : Type u_9}
{n : Type u_10}
[Zero α]
[Zero β]
[Zero γ]
[DecidableEq m]
[DecidableEq n]
(f : α → β → γ)
(hf₁ : ∀ (b : β), f 0 b = 0)
(hf₂ : ∀ (a : α), f a 0 = 0)
(a : m → α)
(b : n → β)
:
Matrix.kroneckerMap f (Matrix.diagonal a) (Matrix.diagonal b) = Matrix.diagonal fun (mn : m × n) => f (a mn.1) (b mn.2)
theorem
Matrix.kroneckerMap_diagonal_right
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[Zero β]
[Zero γ]
[DecidableEq n]
(f : α → β → γ)
(hf : ∀ (a : α), f a 0 = 0)
(A : Matrix l m α)
(b : n → β)
:
Matrix.kroneckerMap f A (Matrix.diagonal b) = Matrix.blockDiagonal fun (i : n) => A.map fun (a : α) => f a (b i)
theorem
Matrix.kroneckerMap_diagonal_left
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[Zero α]
[Zero γ]
[DecidableEq l]
(f : α → β → γ)
(hf : ∀ (b : β), f 0 b = 0)
(a : l → α)
(B : Matrix m n β)
:
Matrix.kroneckerMap f (Matrix.diagonal a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l))
(Matrix.blockDiagonal fun (i : l) => B.map fun (b : β) => f (a i) b)
@[simp]
theorem
Matrix.kroneckerMap_one_one
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{m : Type u_9}
{n : Type u_10}
[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)
:
Matrix.kroneckerMap f 1 1 = 1
theorem
Matrix.kroneckerMap_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 β)
:
Matrix.kroneckerMap f ((Matrix.reindex el em) M) ((Matrix.reindex en ep) N) = (Matrix.reindex (el.prodCongr en) (em.prodCongr ep)) (Matrix.kroneckerMap f M N)
theorem
Matrix.kroneckerMap_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' β)
:
Matrix.kroneckerMap f ((Matrix.reindex el em) M) N = (Matrix.reindex (el.prodCongr (Equiv.refl n)) (em.prodCongr (Equiv.refl n'))) (Matrix.kroneckerMap f M N)
theorem
Matrix.kroneckerMap_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 β)
:
Matrix.kroneckerMap f M ((Matrix.reindex em en) N) = (Matrix.reindex ((Equiv.refl l).prodCongr em) ((Equiv.refl l').prodCongr en)) (Matrix.kroneckerMap f M N)
theorem
Matrix.kroneckerMap_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_18}
{ξ : Type u_19}
{ω : Type u_20}
{ω' : Type u_21}
(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))
:
((Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)).trans φ.mapMatrix)
(Matrix.kroneckerMap g (Matrix.kroneckerMap f A B) D) = Matrix.kroneckerMap f' A (Matrix.kroneckerMap g' B D)
theorem
Matrix.kroneckerMap_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_18}
{ξ : Type u_19}
{ω : Type u_20}
(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))
:
(Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)) (Matrix.kroneckerMap g (Matrix.kroneckerMap f A B) D) = Matrix.kroneckerMap f' A (Matrix.kroneckerMap g' B D)
def
Matrix.kroneckerMapBilinear
{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}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[AddCommMonoid γ]
[Module R α]
[Module R β]
[Module R γ]
(f : α →ₗ[R] β →ₗ[R] γ)
:
When f is bilinear then Matrix.kroneckerMap f is also bilinear.
Equations
- Matrix.kroneckerMapBilinear f = LinearMap.mk₂ R (Matrix.kroneckerMap fun (r : α) (s : β) => (f r) s) ⋯ ⋯ ⋯ ⋯
Instances For
@[simp]
theorem
Matrix.kroneckerMapBilinear_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}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[AddCommMonoid γ]
[Module R α]
[Module R β]
[Module R γ]
(f : α →ₗ[R] β →ₗ[R] γ)
(m✝ : Matrix l m α)
(B : Matrix n p β)
:
((Matrix.kroneckerMapBilinear f) m✝) B = Matrix.kroneckerMap (fun (r : α) (s : β) => (f r) s) m✝ B
theorem
Matrix.kroneckerMapBilinear_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}
[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' β)
:
((Matrix.kroneckerMapBilinear f) (A * B)) (A' * B') = ((Matrix.kroneckerMapBilinear f) A) A' * ((Matrix.kroneckerMapBilinear f) B) B'
Matrix.kroneckerMapBilinear commutes with * if f does.
This is primarily used with R = ℕ to prove Matrix.mul_kronecker_mul.
theorem
Matrix.trace_kroneckerMapBilinear
{R : Type u_1}
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{m : Type u_9}
{n : Type u_10}
[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 β)
:
(((Matrix.kroneckerMapBilinear f) A) B).trace = (f A.trace) B.trace
trace distributes over Matrix.kroneckerMapBilinear.
This is primarily used with R = ℕ to prove Matrix.trace_kronecker.
theorem
Matrix.det_kroneckerMapBilinear
{R : Type u_1}
{α : Type u_2}
{β : Type u_4}
{γ : Type u_6}
{m : Type u_9}
{n : Type u_10}
[CommSemiring R]
[Fintype m]
[Fintype n]
[DecidableEq m]
[DecidableEq n]
[CommRing α]
[CommRing β]
[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 β)
:
(((Matrix.kroneckerMapBilinear f) A) B).det = (A.map fun (a : α) => (f a) 1).det ^ Fintype.card n * (B.map fun (b : β) => (f 1) b).det ^ Fintype.card m
determinant of Matrix.kroneckerMapBilinear.
This is primarily used with R = ℕ to prove Matrix.det_kronecker.
Specialization to Matrix.kroneckerMap (*) #
def
Matrix.kronecker
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[Mul α]
:
The Kronecker product. This is just a shorthand for kroneckerMap (*). Prefer the notation
⊗ₖ rather than this definition.
Equations
- Matrix.kronecker = Matrix.kroneckerMap fun (x1 x2 : α) => x1 * x2
Instances For
Equations
- Kronecker.«term_⊗ₖ_» = Lean.ParserDescr.trailingNode `Kronecker.«term_⊗ₖ_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ₖ ") (Lean.ParserDescr.cat `term 101))
Instances For
def
Matrix.kroneckerBilinear
{R : Type u_1}
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[CommSemiring R]
[Semiring α]
[Algebra R α]
:
Matrix.kronecker as a bilinear map.
Equations
- Matrix.kroneckerBilinear = Matrix.kroneckerMapBilinear ↑(Algebra.lmul R α)
Instances For
What follows is a copy, in order, of every Matrix.kroneckerMap lemma above that has
hypotheses which can be filled by properties of *.
theorem
Matrix.zero_kronecker
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[MulZeroClass α]
(B : Matrix n p α)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) 0 B = 0
theorem
Matrix.kronecker_zero
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[MulZeroClass α]
(A : Matrix l m α)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) 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 α)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (A₁ + A₂) B = Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A₁ B + Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) 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 α)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (B₁ + B₂) = Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B₁ + Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) 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 α]
[MulAction R α]
[IsScalarTower R α α]
(r : R)
(A : Matrix l m α)
(B : Matrix n p α)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (r • A) B = r • Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) 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 α]
[MulAction R α]
[SMulCommClass R α α]
(r : R)
(A : Matrix l m α)
(B : Matrix n p α)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (r • B) = r • Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B
theorem
Matrix.diagonal_kronecker_diagonal
{α : Type u_2}
{m : Type u_9}
{n : Type u_10}
[MulZeroClass α]
[DecidableEq m]
[DecidableEq n]
(a : m → α)
(b : n → α)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (Matrix.diagonal a) (Matrix.diagonal b) = Matrix.diagonal fun (mn : m × n) => a mn.1 * b mn.2
theorem
Matrix.kronecker_diagonal
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[MulZeroClass α]
[DecidableEq n]
(A : Matrix l m α)
(b : n → α)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (Matrix.diagonal b) = Matrix.blockDiagonal fun (i : n) => MulOpposite.op (b i) • A
theorem
Matrix.diagonal_kronecker
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[MulZeroClass α]
[DecidableEq l]
(a : l → α)
(B : Matrix m n α)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (Matrix.diagonal a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun (i : l) => a i • B)
@[simp]
theorem
Matrix.natCast_kronecker_natCast
{α : Type u_2}
{m : Type u_9}
{n : Type u_10}
[NonAssocSemiring α]
[DecidableEq m]
[DecidableEq n]
(a b : ℕ)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) ↑a ↑b = ↑(a * b)
theorem
Matrix.kronecker_natCast
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[NonAssocSemiring α]
[DecidableEq n]
(A : Matrix l m α)
(b : ℕ)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A ↑b = Matrix.blockDiagonal fun (x : n) => b • A
theorem
Matrix.natCast_kronecker
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[NonAssocSemiring α]
[DecidableEq l]
(a : ℕ)
(B : Matrix m n α)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (↑a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun (x : l) => a • B)
theorem
Matrix.kronecker_ofNat
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[Semiring α]
[DecidableEq n]
(A : Matrix l m α)
(b : ℕ)
[b.AtLeastTwo]
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (OfNat.ofNat b) = Matrix.blockDiagonal fun (x : n) => MulOpposite.op (OfNat.ofNat b) • A
theorem
Matrix.ofNat_kronecker
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[Semiring α]
[DecidableEq l]
(a : ℕ)
[a.AtLeastTwo]
(B : Matrix m n α)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (OfNat.ofNat a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun (x : l) => OfNat.ofNat a • B)
theorem
Matrix.one_kronecker_one
{α : Type u_2}
{m : Type u_9}
{n : Type u_10}
[MulZeroOneClass α]
[DecidableEq m]
[DecidableEq n]
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) 1 1 = 1
theorem
Matrix.kronecker_one
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[MulZeroOneClass α]
[DecidableEq n]
(A : Matrix l m α)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A 1 = Matrix.blockDiagonal fun (x : n) => A
theorem
Matrix.one_kronecker
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[MulZeroOneClass α]
[DecidableEq l]
(B : Matrix m n α)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) 1 B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun (x : l) => B)
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']
[CommSemiring α]
(A : Matrix l m α)
(B : Matrix m n α)
(A' : Matrix l' m' α)
(B' : Matrix m' n' α)
:
Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (A * B) (A' * B') = Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A A' * Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) B B'
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 α)
:
(Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r))
(Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B) C) = Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) B C)
@[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 α)
:
(Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B) C).submatrix
⇑(Equiv.prodAssoc l n q).symm ⇑(Equiv.prodAssoc m p r).symm = Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) B C)
theorem
Matrix.det_kronecker
{R : Type u_1}
{m : Type u_9}
{n : Type u_10}
[Fintype m]
[Fintype n]
[DecidableEq m]
[DecidableEq n]
[CommRing R]
(A : Matrix m m R)
(B : Matrix n n R)
:
(Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B).det = A.det ^ Fintype.card n * B.det ^ Fintype.card m
theorem
Matrix.inv_kronecker
{R : Type u_1}
{m : Type u_9}
{n : Type u_10}
[Fintype m]
[Fintype n]
[DecidableEq m]
[DecidableEq n]
[CommRing R]
(A : Matrix m m R)
(B : Matrix n n R)
:
(Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B)⁻¹ = Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) A⁻¹ B⁻¹
Specialization to Matrix.kroneckerMap (⊗ₜ) #
noncomputable def
Matrix.kroneckerTMul
(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}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
:
The Kronecker tensor product. This is just a shorthand for kroneckerMap (⊗ₜ).
Prefer the notation ⊗ₖₜ rather than this definition.
Equations
- Matrix.kroneckerTMul R = Matrix.kroneckerMap fun (x1 : α) (x2 : β) => x1 ⊗ₜ[R] x2
Instances For
Equations
- Kronecker.«term_⊗ₖₜ_» = Lean.ParserDescr.trailingNode `Kronecker.«term_⊗ₖₜ_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ₖₜ ") (Lean.ParserDescr.cat `term 101))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Matrix.kroneckerTMul_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}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
(A : Matrix l m α)
(B : Matrix n p β)
(i₁ : l)
(i₂ : n)
(j₁ : m)
(j₂ : p)
:
noncomputable def
Matrix.kroneckerTMulBilinear
(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}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
:
Matrix.kronecker as a bilinear map.
Equations
Instances For
What follows is a copy, in order, of every Matrix.kroneckerMap lemma above that has
hypotheses which can be filled by properties of ⊗ₜ.
theorem
Matrix.zero_kroneckerTMul
(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}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
(B : Matrix n p β)
:
Matrix.kroneckerMap (TensorProduct.tmul R) 0 B = 0
theorem
Matrix.kroneckerTMul_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}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
(A : Matrix l m α)
:
Matrix.kroneckerMap (TensorProduct.tmul R) A 0 = 0
theorem
Matrix.add_kroneckerTMul
(R : Type u_1)
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[CommSemiring R]
[AddCommMonoid α]
[Module R α]
(A₁ A₂ : Matrix l m α)
(B : Matrix n p α)
:
Matrix.kroneckerMap (TensorProduct.tmul R) (A₁ + A₂) B = Matrix.kroneckerMap (fun (x1 x2 : α) => x1 ⊗ₜ[R] x2) A₁ B + Matrix.kroneckerMap (fun (x1 x2 : α) => x1 ⊗ₜ[R] x2) A₂ B
theorem
Matrix.kroneckerTMul_add
(R : Type u_1)
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[CommSemiring R]
[AddCommMonoid α]
[Module R α]
(A : Matrix l m α)
(B₁ B₂ : Matrix n p α)
:
Matrix.kroneckerMap (TensorProduct.tmul R) A (B₁ + B₂) = Matrix.kroneckerMap (fun (x1 x2 : α) => x1 ⊗ₜ[R] x2) A B₁ + Matrix.kroneckerMap (fun (x1 x2 : α) => x1 ⊗ₜ[R] x2) A B₂
theorem
Matrix.smul_kroneckerTMul
(R : Type u_1)
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[CommSemiring R]
[AddCommMonoid α]
[Module R α]
(r : R)
(A : Matrix l m α)
(B : Matrix n p α)
:
Matrix.kroneckerMap (TensorProduct.tmul R) (r • A) B = r • Matrix.kroneckerMap (fun (x1 x2 : α) => x1 ⊗ₜ[R] x2) A B
theorem
Matrix.kroneckerTMul_smul
(R : Type u_1)
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
{p : Type u_11}
[CommSemiring R]
[AddCommMonoid α]
[Module R α]
(r : R)
(A : Matrix l m α)
(B : Matrix n p α)
:
Matrix.kroneckerMap (TensorProduct.tmul R) A (r • B) = r • Matrix.kroneckerMap (fun (x1 x2 : α) => x1 ⊗ₜ[R] x2) A B
theorem
Matrix.diagonal_kroneckerTMul_diagonal
(R : Type u_1)
{α : Type u_2}
{m : Type u_9}
{n : Type u_10}
[CommSemiring R]
[AddCommMonoid α]
[Module R α]
[DecidableEq m]
[DecidableEq n]
(a : m → α)
(b : n → α)
:
Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.diagonal a) (Matrix.diagonal b) = Matrix.diagonal fun (mn : m × n) => a mn.1 ⊗ₜ[R] b mn.2
theorem
Matrix.kroneckerTMul_diagonal
(R : Type u_1)
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[CommSemiring R]
[AddCommMonoid α]
[Module R α]
[DecidableEq n]
(A : Matrix l m α)
(b : n → α)
:
Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.diagonal b) = Matrix.blockDiagonal fun (i : n) => A.map fun (a : α) => a ⊗ₜ[R] b i
theorem
Matrix.diagonal_kroneckerTMul
(R : Type u_1)
{α : Type u_2}
{l : Type u_8}
{m : Type u_9}
{n : Type u_10}
[CommSemiring R]
[AddCommMonoid α]
[Module R α]
[DecidableEq l]
(a : l → α)
(B : Matrix m n α)
:
Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.diagonal a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l))
(Matrix.blockDiagonal fun (i : l) => B.map fun (b : α) => a i ⊗ₜ[R] b)
theorem
Matrix.kroneckerTMul_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}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[AddCommMonoid γ]
[Module R α]
[Module R β]
[Module R γ]
(A : Matrix l m α)
(B : Matrix n p β)
(C : Matrix q r γ)
:
(Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r))
((Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.kroneckerMap (TensorProduct.tmul R) A B) C).map
⇑(TensorProduct.assoc R α β γ)) = Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.kroneckerMap (TensorProduct.tmul R) B C)
@[simp]
theorem
Matrix.kroneckerTMul_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}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[AddCommMonoid γ]
[Module R α]
[Module R β]
[Module R γ]
(A : Matrix l m α)
(B : Matrix n p β)
(C : Matrix q r γ)
:
((Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.kroneckerMap (TensorProduct.tmul R) A B) C).map
⇑(TensorProduct.assoc R α β γ)).submatrix
⇑(Equiv.prodAssoc l n q).symm ⇑(Equiv.prodAssoc m p r).symm = Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.kroneckerMap (TensorProduct.tmul R) B C)
theorem
Matrix.trace_kroneckerTMul
(R : Type u_1)
{α : Type u_2}
{β : Type u_4}
{m : Type u_9}
{n : Type u_10}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
[Fintype m]
[Fintype n]
(A : Matrix m m α)
(B : Matrix n n β)
:
(Matrix.kroneckerMap (TensorProduct.tmul R) A B).trace = A.trace ⊗ₜ[R] B.trace
@[simp]
theorem
Matrix.one_kroneckerTMul_one
(R : Type u_1)
{α : Type u_2}
{m : Type u_9}
{n : Type u_10}
[CommSemiring R]
[Semiring α]
[Algebra R α]
[DecidableEq m]
[DecidableEq n]
:
Matrix.kroneckerMap (TensorProduct.tmul R) 1 1 = 1
theorem
Matrix.mul_kroneckerTMul_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}
[CommSemiring 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' β)
:
Matrix.kroneckerMap (TensorProduct.tmul R) (A * B) (A' * B') = Matrix.kroneckerMap (TensorProduct.tmul R) A A' * Matrix.kroneckerMap (TensorProduct.tmul R) B B'
theorem
Matrix.det_kroneckerTMul
(R : Type u_1)
{α : Type u_2}
{β : Type u_4}
{m : Type u_9}
{n : Type u_10}
[CommRing R]
[CommRing α]
[CommRing β]
[Algebra R α]
[Algebra R β]
[Fintype m]
[Fintype n]
[DecidableEq m]
[DecidableEq n]
(A : Matrix m m α)
(B : Matrix n n β)
:
(Matrix.kroneckerMap (TensorProduct.tmul R) A B).det = (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)