Matrix.kroneckerMap_diagonal_diagonal
theorem Matrix.kroneckerMap_diagonal_diagonal :
∀ {α : Type u_2} {β : Type u_4} {γ : Type u_6} {m : Type u_9} {n : Type u_10} [inst : Zero α] [inst_1 : Zero β]
[inst_2 : Zero γ] [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] (f : α → β → γ),
(∀ (b : β), f 0 b = 0) →
(∀ (a : α), f a 0 = 0) →
∀ (a : m → α) (b : n → β),
Matrix.kroneckerMap f (Matrix.diagonal a) (Matrix.diagonal b) =
Matrix.diagonal fun mn => f (a mn.1) (b mn.2)
This theorem states that for any types `α`, `β`, `γ`, `m`, and `n`, where `α`, `β`, and `γ` have a zero and `m` and `n` have decidable equality, and a function `f` from `α` and `β` to `γ` such that `f` of `0` and any `β` equals `0` and `f` of any `α` and `0` equals `0`, for any functions `a` from `m` to `α` and `b` from `n` to `β`, the Kronecker product (i.e., the operation that combines two matrices into a larger matrix) of the diagonal matrix defined by `a` and the diagonal matrix defined by `b` using the function `f` is equal to the diagonal matrix defined by the function from `m` and `n` to `f` of `a` of `m` and `b` of `n`. This essentially demonstrates a relationship between the Kronecker product and diagonal matrices.
More concisely: For types `α`, `β`, `γ`, `m`, and `n` with zeroes and decidable equality, and a function `f` from `α × β` to `γ` satisfying `f(0, _) = f(_, 0) = 0`, the Kronecker product of diagonal matrices defined by functions `m → α` `a` and `n → β` `b` using `f` equals the diagonal matrix defined by the function `m × n → γ` `x mapsto f(a(x), b(y))`.
|
Matrix.det_kroneckerMapBilinear
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} [inst : CommSemiring R]
[inst_1 : Fintype m] [inst_2 : Fintype n] [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] [inst_5 : CommRing α]
[inst_6 : CommRing β] [inst_7 : CommRing γ] [inst_8 : Module R α] [inst_9 : Module R β] [inst_10 : Module R γ]
(f : α →ₗ[R] β →ₗ[R] γ),
(∀ (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
The theorem `Matrix.det_kroneckerMapBilinear` states that for any commutative semiring `R`, any types `α`, `β`, `γ`, `m`, `n` where `m` and `n` are finite and have decidable equality, and any commutative rings `α`, `β`, `γ` that are modules over `R`, given a bilinear map `f` from `α` and `β` to `γ` that satisfies a certain property ((f(a * b))(a' * b') = (f(a))(a') * (f(b))(b') for all `a`, `b` in `α` and `a'`, `b'` in `β`), for any matrices `A` and `B` with entries in `α` and `β` respectively, the determinant of the matrix obtained by applying the Kronecker product bilinear map to `A` and `B` is equal to the product of the determinant of `A` mapped under `f` with its entries multiplied by 1 (raised to the power of the number of elements in `n`), and the determinant of `B` mapped under `f` with its entries multiplied by 1 (raised to the power of the number of elements in `m`).
More concisely: For any commutative semiring `R`, bilinear map `f` over `R` satisfying a certain property, and matrices `A` and `B` over commutative rings `α`, `β`, `γ` that are modules over `R`, the determinant of the Kronecker product of `A` and `B` mapped under `f` is the product of the determinant of `A` mapped under `f` raised to the power of `n`, and the determinant of `B` mapped under `f` raised to the power of `m`, where `n` is the number of columns of `A` and `m` is the number of rows of `B`.
|
Matrix.trace_kroneckerMapBilinear
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} [inst : CommSemiring R]
[inst_1 : Fintype m] [inst_2 : Fintype n] [inst_3 : AddCommMonoid α] [inst_4 : AddCommMonoid β]
[inst_5 : AddCommMonoid γ] [inst_6 : Module R α] [inst_7 : Module R β] [inst_8 : Module R γ]
(f : α →ₗ[R] β →ₗ[R] γ) (A : Matrix m m α) (B : Matrix n n β),
(((Matrix.kroneckerMapBilinear f) A) B).trace = (f A.trace) B.trace
The theorem `Matrix.trace_kroneckerMapBilinear` states that for any commutative semiring `R`, any types `α`, `β`, `γ`, `m`, and `n`, given that `m` and `n` are finite types, `α`, `β`, and `γ` are additive commutative monoids and `R`-modules, and given a bilinear map `f` from `α` and `β` to `γ`, and matrices `A` and `B` with entries in `α` and `β` respectively, the trace of the result of applying the Kronecker map (bilinear version) to these matrices equals the result of applying `f` to the trace of `A` and the trace of `B`. In simpler terms, the trace operation distributes over the Kronecker map operation for bilinear maps and matrices with entries in a commutative semiring. This is primarily used with `R` being the natural numbers to prove `Matrix.trace_kronecker`.
More concisely: For any commutative semiring `R`, any finite type `α`, and bilinear maps `f : α × α → γ`, `A : matrix α m n`, and `B : matrix α n m` with entries in `α`, the trace of the Kronecker product `A ⊗ B` is equal to the composition of the trace function with `f`, i.e., `trace(A) ⊤ ∘ trace(B) = trace(f(A, B))`.
|
Matrix.kroneckerMapBilinear_mul_mul
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} [inst : CommSemiring R] [inst_1 : Fintype m]
[inst_2 : Fintype m'] [inst_3 : NonUnitalNonAssocSemiring α] [inst_4 : NonUnitalNonAssocSemiring β]
[inst_5 : NonUnitalNonAssocSemiring γ] [inst_6 : Module R α] [inst_7 : Module R β] [inst_8 : Module R γ]
(f : α →ₗ[R] β →ₗ[R] γ),
(∀ (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'
The theorem `Matrix.kroneckerMapBilinear_mul_mul` states that for any commutative semiring `R`, types `α`, `β`, `γ`, and matrix types `l`, `m`, `n`, `l'`, `m'`, `n'`, if `α`, `β`, and `γ` are non-unital, non-associative semirings and are modules over `R`, and if we have a bilinear map `f` from `α` to `β` to `γ` which commutes with multiplication, then the operation `Matrix.kroneckerMapBilinear` applied to this map and matrices `A`, `B`, `A'`, `B'` also commutes with multiplication. More formally, if `(f (a * b)) (a' * b') = (f a) a' * (f b) b'` for all `a, b` in `α` and `a', b'` in `β`, then `((Matrix.kroneckerMapBilinear f) (A * B)) (A' * B') = ((Matrix.kroneckerMapBilinear f) A) A' * ((Matrix.kroneckerMapBilinear f) B) B'` for all matrices `A, B` of type `α` and `A', B'` of type `β`. This is primarily used with `R = ℕ` to prove `Matrix.mul_kronecker_mul`.
More concisely: For any commutative semiring `R`, bilinear map `f` from a non-unital, non-associative semiring `α` to `β` to `γ` that commutes with multiplication, and matrices `A, B, A', B'` over `α` and `β`, respectively: `(f (a * b)) (a' * b') = (f a) a' * (f b) b'` implies `((Matrix.kroneckerMapBilinear f) (A * B)) (A' * B') = ((Matrix.kroneckerMapBilinear f) A) A' * ((Matrix.kroneckerMapBilinear f) B) B'`.
|
Matrix.kroneckerMap_smul_right
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} [inst : SMul R β] [inst_1 : SMul R γ] (f : α → β → γ) (r : R),
(∀ (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
The theorem `Matrix.kroneckerMap_smul_right` states that for any types `R`, `α`, `β`, `γ`, `l`, `m`, `n`, and `p`, and given a scalar multiplication operation on `β` and `γ` (denoted `SMul R β` and `SMul R γ`), a function `f` from `α` and `β` to `γ`, a scalar `r` of type `R`, and a matrix `A` of type `Matrix l m α` and a matrix `B` of type `Matrix n p β`, if for all `a` of type `α` and `b` of type `β`, `f a (r • b)` equals to `r • f a b`, then the Kronecker map of `f` applied to `A` and `r` scaled `B` equals to `r` scaled Kronecker map of `f` applied to `A` and `B`. This theorem essentially states that the scalar multiplication can be distributed over the Kronecker map operation under certain conditions.
More concisely: If for all `a` in `α` and `b` in `β`, `f(a) (r * b) = r * (f(a) * b)`, then `(kroneckerMap f A) * (r * B) = r * (kroneckerMap f A * B)`.
|
Matrix.kroneckerMap_smul_left
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} [inst : SMul R α] [inst_1 : SMul R γ] (f : α → β → γ) (r : R),
(∀ (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
The given theorem, `Matrix.kroneckerMap_smul_left`, states that for all types `R`, `α`, `β`, `γ`, `l`, `m`, `n`, and `p`, where `R` is a scalar, `α` and `γ` are types involving scalar multiplication, if we have a function `f` from `α` and `β` to `γ` such that for any elements `a` in `α` and `b` in `β`, scalar multiplication of `r` to the product of `f(a, b)` is equal to the application of `f` to the scalar multiplication of `r` and `a` and `b` (i.e., `f(r * a, b) = r * f(a, b)`), then for any matrices `A` of type `α` and `B` of type `β`, applying `kroneckerMap` to the scalar multiplication of `r` and `A` and `B` is the same as scalar multiplication of `r` to the `kroneckerMap` of `f`, `A` and `B` (i.e., `kroneckerMap(f, r * A, B) = r * kroneckerMap(f, A, B)`). This theorem connects the concept of scalar multiplication and the Kronecker product operation in the context of matrices.
More concisely: For any function `f` between two types involving scalar multiplication such that `r * f(a, b) = f(r * a, b)` for all scalars `r` and elements `a` and `b`, the Kronecker product of `f` with the scalar multiplication of matrices `r * A` and `B` is equal to the scalar multiplication of `r` times the Kronecker product of `f` with matrices `A` and `B`.
|