English
If U1 and U2 are unitary matrices of sizes n×n and m×m over a ring with involution, then their Kronecker product U1 ⊗ U2 is unitary of size (n×m) by (n×m).
Русский
Пусть U1 и U2 — унитарные матрицы размерности n×n и m×m над кольцом с инволюцией, тогда их кронекеровское произведение U1 ⊗ U2 является унитарной матрицей размером (n×m)×(n×m).
LaTeX
$$$U_1 \in \\mathrm{U}(n,R) \\land U_2 \\in \\mathrm{U}(m,R) \\Rightarrow U_1 \\otimes U_2 \\in \\mathrm{U}(nm,R).$$$
Lean4
/-- The kronecker product of two unitary matrices is unitary.
This is stated for `unitary` instead of `unitaryGroup` as it holds even for
non-commutative coefficients. -/
theorem kronecker_mem_unitary {R m : Type*} [Semiring R] [StarRing R] [Fintype m] [DecidableEq m] {U₁ : Matrix n n R}
{U₂ : Matrix m m R} (hU₁ : U₁ ∈ unitary (Matrix n n R)) (hU₂ : U₂ ∈ unitary (Matrix m m R)) :
U₁ ⊗ₖ U₂ ∈ unitary (Matrix (n × m) (n × m) R) :=
by
simp_rw [unitary.mem_iff, star_eq_conjTranspose, conjTranspose_kronecker']
constructor <;> ext <;>
simp only [mul_apply, submatrix_apply, kroneckerMap_apply, Prod.fst_swap, conjTranspose_apply, ← star_apply,
Prod.snd_swap, ← mul_assoc]
· simp_rw [mul_assoc _ (star U₁ _ _), ← Finset.univ_product_univ, Finset.sum_product]
rw [Finset.sum_comm]
simp_rw [← Finset.sum_mul, ← Finset.mul_sum, ← Matrix.mul_apply, hU₁.1, Matrix.one_apply, mul_boole, ite_mul,
zero_mul, Finset.sum_ite_irrel, ← Matrix.mul_apply, hU₂.1, Matrix.one_apply, Finset.sum_const_zero, ← ite_and,
Prod.eq_iff_fst_eq_snd_eq]
·
simp_rw [mul_assoc _ _ (star U₂ _ _), ← Finset.univ_product_univ, Finset.sum_product, ← Finset.sum_mul, ←
Finset.mul_sum, ← Matrix.mul_apply, hU₂.2, Matrix.one_apply, mul_boole, ite_mul, zero_mul, Finset.sum_ite_irrel, ←
Matrix.mul_apply, hU₁.2, Matrix.one_apply, Finset.sum_const_zero, ← ite_and, and_comm, Prod.eq_iff_fst_eq_snd_eq]
