mathlib3 documentation

monlib / linear_algebra.my_ips.frob

Frobenius equations #

This file contains the proof of the Frobenius equations.

source
noncomputable def module.dual.tensor_mul {n : Type u_1} {p : Type u_2} (φ₁ : module.dual ℂ (matrix n n ℂ)) (φ₂ : module.dual ℂ (matrix p p ℂ)) :
module.dual ℂ (tensor_product ℂ (matrix n n ℂ) (matrix p p ℂ))
Equations
source
theorem module.dual.tensor_mul_apply {n : Type u_1} {p : Type u_2} [fintype n] [fintype p] [decidable_eq n] [decidable_eq p] (φ₁ : module.dual ℂ (matrix n n ℂ)) (φ₂ : module.dual ℂ (matrix p p ℂ)) (x : matrix n n ℂ) (y : matrix p p ℂ) :
⇑(φ₁.tensor_mul φ₂) (x ⊗ₜ[ℂ] y) = ⇑φ₁ x * ⇑φ₂ y
source
theorem module.dual.tensor_mul_apply' {n : Type u_1} {p : Type u_2} [fintype n] [fintype p] [decidable_eq n] [decidable_eq p] (φ₁ : module.dual ℂ (matrix n n ℂ)) (φ₂ : module.dual ℂ (matrix p p ℂ)) (x : tensor_product ℂ (matrix n n ℂ) (matrix p p ℂ)) :
⇑(φ₁.tensor_mul φ₂) x = finset.univ.sum (λ (i : n), finset.univ.sum (λ (j : n), finset.univ.sum (λ (k : p), finset.univ.sum (λ (l : p), ⇑tensor_product.to_kronecker x (i, k) (j, l) * (⇑φ₁ (matrix.std_basis_matrix i j 1) * ⇑φ₂ (matrix.std_basis_matrix k l 1))))))
source
theorem module.dual.tensor_mul_apply'' {n : Type u_1} {p : Type u_2} [fintype n] [fintype p] [decidable_eq n] [decidable_eq p] (φ₁ : module.dual ℂ (matrix n n ℂ)) (φ₂ : module.dual ℂ (matrix p p ℂ)) (a : matrix (n × p) (n × p) ℂ) :
⇑(linear_map.comp (φ₁.tensor_mul φ₂) matrix.kronecker_to_tensor_product) a = ((matrix.kronecker_map has_mul.mul φ₁.matrix φ₂.matrix).mul a).trace
source
theorem module.dual.tensor_mul_matrix {n : Type u_1} {p : Type u_2} [fintype n] [fintype p] [decidable_eq n] [decidable_eq p] (φ₁ : module.dual ℂ (matrix n n ℂ)) (φ₂ : module.dual ℂ (matrix p p ℂ)) :
module.dual.matrix (linear_map.comp (φ₁.tensor_mul φ₂) matrix.kronecker_to_tensor_product) = matrix.kronecker_map has_mul.mul φ₁.matrix φ₂.matrix
source
@[instance]
def module.dual.is_faithful_pos_map.tensor_mul {n : Type u_1} {p : Type u_2} [fintype n] [fintype p] [decidable_eq n] [decidable_eq p] {φ₁ : module.dual ℂ (matrix n n ℂ)} {φ₂ : module.dual ℂ (matrix p p ℂ)} [hφ₁ : fact φ₁.is_faithful_pos_map] [hφ₂ : fact φ₂.is_faithful_pos_map] :
fact (module.dual.is_faithful_pos_map (linear_map.comp (φ₁.tensor_mul φ₂) matrix.kronecker_to_tensor_product))
source
theorem matrix.kronecker_to_tensor_product_adjoint {n : Type u_1} {p : Type u_2} [fintype n] [fintype p] [decidable_eq n] [decidable_eq p] {φ : module.dual ℂ (matrix n n ℂ)} {ψ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] [hψ : fact ψ.is_faithful_pos_map] :
tensor_product.to_kronecker = ⇑linear_map.adjoint matrix.kronecker_to_tensor_product
source
theorem tensor_product.to_kronecker_adjoint {n : Type u_1} {p : Type u_2} [fintype n] [fintype p] [decidable_eq n] [decidable_eq p] {φ : module.dual ℂ (matrix n n ℂ)} {ψ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] [hψ : fact ψ.is_faithful_pos_map] :
matrix.kronecker_to_tensor_product = ⇑linear_map.adjoint tensor_product.to_kronecker
source
theorem matrix.kronecker_to_tensor_product_comp_to_kronecker {n : Type u_1} {p : Type u_2} [fintype n] [fintype p] [decidable_eq n] [decidable_eq p] :
matrix.kronecker_to_tensor_product.comp tensor_product.to_kronecker = 1
source
theorem frobenius_equation {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
(tensor_product.map (linear_map.mul' ℂ (matrix n n ℂ)) 1).comp (↑((tensor_product.assoc ℂ (matrix n n ℂ) (matrix n n ℂ) (matrix n n ℂ)).symm).comp (tensor_product.map 1 (⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))))) = (⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))).comp (linear_map.mul' ℂ (matrix n n ℂ))
source
noncomputable def matrix_direct_sum_from_to {k : Type u_3} [fintype k] [decidable_eq k] {s : k → Type u_4} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] (i j : k) :
matrix (s i) (s i) ℂ →ₗ[ℂ] matrix (s j) (s j) ℂ
Equations
source
theorem matrix_direct_sum_from_to_same {k : Type u_3} [fintype k] [decidable_eq k] {s : k → Type u_4} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] (i : k) :
matrix_direct_sum_from_to i i = 1
source
theorem linear_map.pi_mul'_apply_include_block' {k : Type u_3} [fintype k] [decidable_eq k] {s : k → Type u_4} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] {i j : k} :
(linear_map.mul' ℂ (Π (i : k), matrix (s i) (s i) ℂ)).comp (tensor_product.map matrix.include_block matrix.include_block) = ite (i = j) (matrix.include_block.comp ((linear_map.mul' ℂ (matrix (s j) (s j) ℂ)).comp (tensor_product.map (matrix_direct_sum_from_to i j) 1))) 0
source
noncomputable def direct_sum_tensor_matrix {k : Type u_3} [fintype k] [decidable_eq k] {s : k → Type u_4} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] :
tensor_product ℂ (Π (i : k), matrix (s i) (s i) ℂ) (Π (i : k), matrix (s i) (s i) ℂ) ≃ₗ[ℂ] Π (i : k × k), tensor_product ℂ (matrix (s i.fst) (s i.fst) ℂ) (matrix (s i.snd) (s i.snd) ℂ)
Equations
source
noncomputable def direct_sum_tensor_to_kronecker {k : Type u_3} [fintype k] [decidable_eq k] {s : k → Type u_4} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] :
tensor_product ℂ (Π (i : k), matrix (s i) (s i) ℂ) (Π (i : k), matrix (s i) (s i) ℂ) ≃ₗ[ℂ] Π (i : k × k), matrix (s i.fst × s i.snd) (s i.fst × s i.snd) ℂ
Equations
source
theorem frobenius_equation_direct_sum_aux {k : Type u_3} [fintype k] [decidable_eq k] {s : k → Type u_4} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] {θ : Π (i : k), module.dual ℂ (matrix (s i) (s i) ℂ)} [hθ : ∀ (i : k), fact (θ i).is_faithful_pos_map] (x y : Π (i : k), matrix (s i) (s i) ℂ) (i j : k) :
⇑((tensor_product.map (linear_map.mul' ℂ (Π (i : k), matrix (s i) (s i) ℂ)) 1).comp (↑((tensor_product.assoc ℂ (Π (i : k), matrix (s i) (s i) ℂ) (Π (i : k), matrix (s i) (s i) ℂ) (Π (i : k), matrix (s i) (s i) ℂ)).symm).comp (tensor_product.map 1 (⇑linear_map.adjoint (linear_map.mul' ℂ (Π (i : k), matrix (s i) (s i) ℂ)))))) (⇑matrix.include_block (x i) ⊗ₜ[ℂ] ⇑matrix.include_block (y j)) = ite (i = j) (⇑((tensor_product.map matrix.include_block matrix.include_block).comp ((⇑linear_map.adjoint (linear_map.mul' ℂ (matrix (s j) (s j) ℂ))).comp (linear_map.mul' ℂ (matrix (s j) (s j) ℂ)))) (x j ⊗ₜ[ℂ] y j)) 0
source
theorem direct_sum_tensor_to_kronecker_apply {k : Type u_3} [fintype k] [decidable_eq k] {s : k → Type u_4} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] (x y : Π (i : k), matrix (s i) (s i) ℂ) (r : k × k) (a b : s r.fst × s r.snd) :
⇑direct_sum_tensor_to_kronecker (x ⊗ₜ[ℂ] y) r a b = x r.fst a.fst b.fst * y r.snd a.snd b.snd
source
theorem frobenius_equation' {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
(tensor_product.map 1 (linear_map.mul' ℂ (matrix n n ℂ))).comp (↑(tensor_product.assoc ℂ (matrix n n ℂ) (matrix n n ℂ) (matrix n n ℂ)).comp (tensor_product.map (⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))) 1)) = (⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))).comp (linear_map.mul' ℂ (matrix n n ℂ))
source
theorem linear_map.mul'_assoc {n : Type u_1} [fintype n] [decidable_eq n] :
(linear_map.mul' ℂ (matrix n n ℂ)).comp (tensor_product.map (linear_map.mul' ℂ (matrix n n ℂ)) 1) = (linear_map.mul' ℂ (matrix n n ℂ)).comp ((tensor_product.map 1 (linear_map.mul' ℂ (matrix n n ℂ))).comp ↑(tensor_product.assoc ℂ (matrix n n ℂ) (matrix n n ℂ) (matrix n n ℂ)))
source
theorem linear_map.mul'_coassoc {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
(tensor_product.map (⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))) 1).comp (⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))) = ↑((tensor_product.assoc ℂ (matrix n n ℂ) (matrix n n ℂ) (matrix n n ℂ)).symm).comp ((tensor_product.map 1 (⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ)))).comp (⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))))
source
theorem linear_map.mul'_comp_unit_map_id_eq_lid {n : Type u_1} [fintype n] [decidable_eq n] :
(linear_map.mul' ℂ (matrix n n ℂ)).comp (tensor_product.map (algebra.linear_map ℂ (matrix n n ℂ)) 1) = ↑(tensor_product.lid ℂ (matrix n n ℂ))
source
theorem linear_map.mul'_comp_id_map_unit_assoc_eq_lid {n : Type u_1} [fintype n] [decidable_eq n] :
(linear_map.mul' ℂ (matrix n n ℂ)).comp ((tensor_product.map 1 (algebra.linear_map ℂ (matrix n n ℂ))).comp ↑((tensor_product.comm ℂ (matrix n n ℂ) ℂ).symm)) = ↑(tensor_product.lid ℂ (matrix n n ℂ))
source
theorem linear_map.mul'_adjoint_eq' {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
(tensor_product.map (linear_map.mul' ℂ (matrix n n ℂ)) 1).comp (↑((tensor_product.assoc ℂ (matrix n n ℂ) (matrix n n ℂ) (matrix n n ℂ)).symm).comp ((tensor_product.map 1 ((⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))).comp (algebra.linear_map ℂ (matrix n n ℂ)))).comp (↑((tensor_product.comm ℂ (matrix n n ℂ) ℂ).symm).comp ↑((tensor_product.lid ℂ (matrix n n ℂ)).symm)))) = ⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))
source
theorem linear_map.mul'_adjoint_eq'' {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
(tensor_product.map 1 (linear_map.mul' ℂ (matrix n n ℂ))).comp (↑(tensor_product.assoc ℂ (matrix n n ℂ) (matrix n n ℂ) (matrix n n ℂ)).comp ((tensor_product.map ((⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))).comp (algebra.linear_map ℂ (matrix n n ℂ))) 1).comp ↑((tensor_product.lid ℂ (matrix n n ℂ)).symm))) = ⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))