mathlib3 documentation

monlib / quantum_graph.mess

Some messy stuff #

This file contains some messy stuff that I don't want to put in the main file.

Will organise this later.

source
noncomputable def ι_map {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) :
(matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) →ₗ[ℂ] tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ)
Equations
source
theorem sig_neg_one {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (a : matrix n n ℂ) :
⇑(_.sig (-1)) a = (φ.matrix.mul a).mul (φ.matrix)⁻¹
source
theorem sig_one {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (a : matrix n n ℂ) :
⇑(_.sig 1) a = ((φ.matrix)⁻¹.mul a).mul φ.matrix
source
theorem ι_map_apply_rank_one {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (a b : matrix n n ℂ) :
⇑(ι_map _) ↑(rank_one a b) = ⇑(_.sig (-1)) b.conj_transpose ⊗ₜ[ℂ] a
source
theorem ι_map_eq_Psi {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
ι_map _ = (tensor_product.map 1 unop).comp (ten_swap.comp (_.Psi 0 1).to_linear_map)
source
theorem ι_map_comp_inv {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
(ι_map _).comp ((_.Psi 0 1).symm.to_linear_map.comp (ten_swap.comp (tensor_product.map 1 op))) = 1
source
theorem ι_inv_comp_ι_map {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
((_.Psi 0 1).symm.to_linear_map.comp (ten_swap.comp (tensor_product.map 1 op))).comp (ι_map _) = 1
source
noncomputable def ι_inv_map {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) :
tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ) →ₗ[ℂ] matrix n n ℂ →ₗ[ℂ] matrix n n ℂ
Equations
source
noncomputable def ι_linear_equiv {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) :
(matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) ≃ₗ[ℂ] tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ)
Equations
source
noncomputable def phi_map {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) :
(matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) →ₗ[ℂ] tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ) →ₗ[ℂ] tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ)
Equations
source
theorem module.dual.is_faithful_pos_map.sig_is_symmetric {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {t : ℝ} :
(_.sig t).to_linear_map.is_symmetric
source
theorem ι_inv_map_mul_adjoint_eq_rmul {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
(ι_inv_map _).comp (⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))) = rmul
source
theorem Psi_inv_0_0_mul_adjoint_eq_lmul {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
↑((_.Psi 0 0).symm).comp ((tensor_product.map 1 op).comp (⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ)))) = lmul
source
theorem ten_swap_Psi_eq_Psi_real {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {t s : ℝ} :
ten_swap.comp ↑(_.Psi t s) = ↑(_.Psi s t).real
source
theorem rank_one_map_rank_one_eq {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x y z w : matrix n n ℂ) :
tensor_product.map ↑(rank_one x y) ↑(rank_one z w) = ↑(rank_one (x ⊗ₜ[ℂ] z) (y ⊗ₜ[ℂ] w))
source
theorem phi_map_eq {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
phi_map _ = rmul_map_lmul.comp (ι_map _)
source
noncomputable def grad {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) :
(matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) →+ matrix n n ℂ →ₗ[ℂ] tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ)
Equations
source
noncomputable def one_tensor_map {n : Type u_1} [fintype n] [decidable_eq n] :
matrix n n ℂ →ₗ[ℂ] tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ)
Equations
source
noncomputable def tensor_one_map {n : Type u_1} [fintype n] [decidable_eq n] :
matrix n n ℂ →ₗ[ℂ] tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ)
Equations
source
theorem one_tensor_map_apply {n : Type u_1} [fintype n] [decidable_eq n] (x : matrix n n ℂ) :
⇑one_tensor_map x = x ⊗ₜ[ℂ] 1
source
theorem tensor_one_map_apply {n : Type u_1} [fintype n] [decidable_eq n] (x : matrix n n ℂ) :
⇑tensor_one_map x = 1 ⊗ₜ[ℂ] x
source
theorem grad_apply {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑(grad _) x = (⇑(phi_map _) x.real).comp tensor_one_map - (⇑(phi_map _) x).comp one_tensor_map
source
theorem one_tensor_map_adjoint {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
⇑linear_map.adjoint one_tensor_map = ↑(tensor_product.lid ℂ (matrix n n ℂ)).comp (↑(tensor_product.comm ℂ (matrix n n ℂ) ℂ).comp (tensor_product.map 1 (⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ)))))
source
theorem one_tensor_map_adjoint_apply {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x y : matrix n n ℂ) :
⇑(⇑linear_map.adjoint one_tensor_map) (x ⊗ₜ[ℂ] y) = ⇑φ y • x
source
theorem tensor_one_map_adjoint {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
⇑linear_map.adjoint tensor_one_map = ↑(tensor_product.lid ℂ (matrix n n ℂ)).comp (tensor_product.map (⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ))) 1)
source
theorem tensor_one_map_adjoint_apply {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x y : matrix n n ℂ) :
⇑(⇑linear_map.adjoint tensor_one_map) (x ⊗ₜ[ℂ] y) = ⇑φ x • y
source
theorem phi_map_adjoint {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑linear_map.adjoint (⇑(phi_map _) x) = ⇑(phi_map _) x.real
source
theorem grad_adjoint {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑linear_map.adjoint (⇑(grad _) x) = ↑(tensor_product.lid ℂ (matrix n n ℂ)).comp ((tensor_product.map (⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ))) 1).comp (⇑(phi_map _) x)) - ↑(tensor_product.lid ℂ (matrix n n ℂ)).comp (↑(tensor_product.comm ℂ (matrix n n ℂ) ℂ).comp ((tensor_product.map 1 (⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ)))).comp (⇑(phi_map _) x.real)))
source
theorem sig_map_mul {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (t : ℝ) (x y : matrix n n ℂ) :
⇑(_.sig t) (x.mul y) = (⇑(_.sig t) x).mul (⇑(_.sig t) y)
source
theorem phi_map_mul {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (A B : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑(phi_map _) (⇑(⇑(qam.refl_idempotent _) A) B) = (⇑(phi_map _) A).comp (⇑(phi_map _) B)
source
theorem phi_map_of_real_Schur_idempotent {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ} (hx1 : x.is_real) (hx2 : ⇑(⇑(qam.refl_idempotent _) x) x = x) :
⇑linear_map.adjoint (⇑(phi_map _) x) = ⇑(phi_map _) x ∧ is_idempotent_elem (⇑(phi_map _) x)
source
def phi_map_of_real_Schur_idempotent_orthogonal_projection {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ} (hx1 : x.is_real) (hx2 : ⇑(⇑(qam.refl_idempotent _) x) x = x) :
∃ (U : submodule ℂ (tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ))), ↑(orthogonal_projection' U) = ⇑(phi_map _) x
source
noncomputable def phi_map_of_real_Schur_idempotent.submodule {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ} (hx1 : x.is_real) (hx2 : ⇑(⇑(qam.refl_idempotent phi_map_of_real_Schur_idempotent.submodule._proof_1) x) x = x) :
submodule ℂ (tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ))
Equations
source
def phi_map_of_real_Schur_idempotent.orthogonal_projection_eq {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ} (hx1 : x.is_real) (hx2 : ⇑(⇑(qam.refl_idempotent _) x) x = x) :
↑(orthogonal_projection' (phi_map_of_real_Schur_idempotent.submodule hx1 hx2)) = ⇑(phi_map _) x
source
theorem grad_apply_of_real_Schur_idempotent {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ} (hx1 : x.is_real) (hx2 : ⇑(⇑(qam.refl_idempotent _) x) x = x) :
(⇑(phi_map _) x).comp (⇑(grad _) x) = ⇑(grad _) x
source
theorem grad_of_real_Schur_idempotent_range {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ} (hx1 : x.is_real) (hx2 : ⇑(⇑(qam.refl_idempotent _) x) x = x) :
linear_map.range (⇑(grad _) x) ≤ phi_map_of_real_Schur_idempotent.submodule hx1 hx2
source
noncomputable def D_in {n : Type u_1} [fintype n] [decidable_eq n] :
(matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) →ₗ[ℂ] matrix n n ℂ →ₗ[ℂ] matrix n n ℂ
Equations
source
noncomputable def D_out {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) :
(matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) →+ matrix n n ℂ →ₗ[ℂ] matrix n n ℂ
Equations
source
theorem D_in_apply {n : Type u_1} [fintype n] [decidable_eq n] (x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑D_in x = ⇑lmul (⇑x 1)
source
theorem D_out_apply {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑(D_out _) x = ⇑rmul (⇑(⇑linear_map.adjoint x) 1)
source
theorem tensor_one_map_adjoint_comp_phi_map_comp_one_tensor_map_rank_one {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x y : matrix n n ℂ) :
↑(tensor_product.lid ℂ (matrix n n ℂ)).comp ((tensor_product.map (⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ))) 1).comp ((⇑(phi_map _) ↑(rank_one x y)).comp ((tensor_product.map 1 (algebra.linear_map ℂ (matrix n n ℂ))).comp (↑((tensor_product.comm ℂ (matrix n n ℂ) ℂ).symm).comp ↑((tensor_product.lid ℂ (matrix n n ℂ)).symm))))) = ↑(rank_one x y)
source
theorem tensor_one_map_adjoint_comp_phi_map_comp_one_tensor_map {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
↑(tensor_product.lid ℂ (matrix n n ℂ)).comp ((tensor_product.map (⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ))) 1).comp ((⇑(phi_map _) x).comp ((tensor_product.map 1 (algebra.linear_map ℂ (matrix n n ℂ))).comp (↑((tensor_product.comm ℂ (matrix n n ℂ) ℂ).symm).comp ↑((tensor_product.lid ℂ (matrix n n ℂ)).symm))))) = x
source
theorem tensor_one_map_adjoint_comp_phi_map_comp_tensor_one_map {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
↑(tensor_product.lid ℂ (matrix n n ℂ)).comp ((tensor_product.map (⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ))) 1).comp ((⇑(phi_map _) x).comp ((tensor_product.map (algebra.linear_map ℂ (matrix n n ℂ)) 1).comp ↑((tensor_product.lid ℂ (matrix n n ℂ)).symm)))) = ⇑D_in x
source
theorem one_tensor_map_adjoint_comp_phi_map_comp_tensor_one_map {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
↑(tensor_product.lid ℂ (matrix n n ℂ)).comp (↑(tensor_product.comm ℂ (matrix n n ℂ) ℂ).comp ((tensor_product.map 1 (⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ)))).comp ((⇑(phi_map _) x).comp ((tensor_product.map (algebra.linear_map ℂ (matrix n n ℂ)) 1).comp ↑((tensor_product.lid ℂ (matrix n n ℂ)).symm))))) = ⇑linear_map.adjoint x.real
source
theorem one_tensor_map_adjoint_comp_phi_map_comp_one_tensor_map {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
↑(tensor_product.lid ℂ (matrix n n ℂ)).comp (↑(tensor_product.comm ℂ (matrix n n ℂ) ℂ).comp ((tensor_product.map 1 (⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ)))).comp ((⇑(phi_map _) x).comp ((tensor_product.map 1 (algebra.linear_map ℂ (matrix n n ℂ))).comp (↑((tensor_product.comm ℂ (matrix n n ℂ) ℂ).symm).comp ↑((tensor_product.lid ℂ (matrix n n ℂ)).symm)))))) = ⇑(D_out _) x.real
source
theorem qam.refl_idempotent_real {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (a b : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
(⇑(⇑(qam.refl_idempotent _) a) b).real = ⇑(⇑(qam.refl_idempotent _) b.real) a.real
source
theorem qam.refl_idempotent_adjoint {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (a b : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑linear_map.adjoint (⇑(⇑(qam.refl_idempotent _) a) b) = ⇑(⇑(qam.refl_idempotent _) (⇑linear_map.adjoint a)) (⇑linear_map.adjoint b)
source
theorem D_in_Schur_product_eq_ir_refl {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (A B : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑D_in (⇑(⇑(qam.refl_idempotent _) A) B) = ⇑(⇑(qam.refl_idempotent _) (A.comp (⇑linear_map.adjoint B.real))) 1
source
theorem D_out_Schur_product_eq_ir_refl' {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (A B : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑(D_out _) (⇑(⇑(qam.refl_idempotent _) A) B) = ⇑(⇑(qam.refl_idempotent _) 1) ((⇑linear_map.adjoint B).comp A.real)
source
theorem grad_adjoint_grad {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
(⇑linear_map.adjoint (⇑(grad _) x)).comp (⇑(grad _) x) = ⇑D_in (⇑(⇑(qam.refl_idempotent _) x) x.real) - ⇑(⇑(qam.refl_idempotent _) x) x - ⇑(⇑(qam.refl_idempotent _) (⇑linear_map.adjoint x)) (⇑linear_map.adjoint x) + ⇑(D_out _) (⇑(⇑(qam.refl_idempotent _) x.real) x)
source
theorem ι_inv_grad_apply_rank_one {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (a b x : matrix n n ℂ) :
⇑(ι_inv_map _) (⇑(⇑(grad _) ↑(rank_one a b)) x) = (⇑rmul x).comp ↑(rank_one a b).real - ↑(rank_one a b).comp (⇑rmul x)
source
theorem ι_inv_map_apply {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x y : matrix n n ℂ) :
⇑(ι_inv_map _) (x ⊗ₜ[ℂ] y) = ↑(rank_one y (⇑(_.sig (-1)) x.conj_transpose))
source
theorem phi_map_eq' {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑(phi_map _) x = (ι_map _).comp ((⇑(qam.refl_idempotent _) x).comp (ι_inv_map _))
source
theorem phi_map_maps_to_bimodule_maps {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {A : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ} :
(⇑(phi_map _) A).is_bimodule_map
source
theorem phi_map_range {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
linear_map.range (phi_map _) ≤ is_bimodule_map.submodule
source
theorem orthonormal_basis_tensor_product_sum_repr {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (a b : matrix n n ℂ) :
finset.univ.sum (λ (x_3 : n × n), finset.univ.sum (λ (x_4 : n × n), has_inner.inner (⇑(_.basis.tensor_product _.basis) (x_3, x_4)) (a ⊗ₜ[ℂ] b) • ⇑(_.basis.tensor_product _.basis) (x_3, x_4))) = a ⊗ₜ[ℂ] b
source
theorem linear_map.tensor_matrix_eq_rank_one {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ) →ₗ[ℂ] tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ)) :
x = finset.univ.sum (λ (i : n × n), finset.univ.sum (λ (j : n × n), finset.univ.sum (λ (k : n × n), finset.univ.sum (λ (l : n × n), has_inner.inner (⇑(_.basis.tensor_product _.basis) (i, j)) (⇑x (⇑(_.basis.tensor_product _.basis) (k, l))) • ↑(rank_one (⇑(_.basis.tensor_product _.basis) (i, j)) (⇑(_.basis.tensor_product _.basis) (k, l)))))))
source
noncomputable def phi_inv_map {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) :
↥is_bimodule_map.submodule →ₗ[ℂ] matrix n n ℂ →ₗ[ℂ] matrix n n ℂ
Equations
source
noncomputable def phi_inv'_map {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) :
(tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ) →ₗ[ℂ] tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ)) →ₗ[ℂ] matrix n n ℂ →ₗ[ℂ] matrix n n ℂ
Equations
source
noncomputable def phi_inv'_map_coe {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) :
↥is_bimodule_map.submodule →ₗ[ℂ] matrix n n ℂ →ₗ[ℂ] matrix n n ℂ
Equations
source
theorem phi_inv'_map_apply {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x y : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑(phi_inv'_map _) (tensor_product.map x y) = y.comp (↑(rank_one 1 1).comp x)
source
theorem ι_linear_equiv_apply_eq {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑(ι_linear_equiv _) x = ⇑(ι_map _) x
source
theorem ι_linear_equiv_symm_apply_eq {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ)) :
⇑((ι_linear_equiv _).symm) x = ⇑(ι_inv_map _) x
source
noncomputable def phi_map_coe {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) :
(matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) →ₗ[ℂ] ↥is_bimodule_map.submodule
Equations
source
theorem phi_map_left_inverse {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
(phi_inv_map _).comp (phi_map_coe _) = 1
source
theorem phi_inv'_map_phi_map {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
(phi_inv'_map_coe _).comp (phi_map_coe _) = 1
source
theorem phi_map_right_inverse {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : {x // x.is_bimodule_map}) :
⇑(phi_map_coe _) (⇑(phi_inv_map _) x) = x
source
noncomputable def phi_linear_equiv {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) :
(matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) ≃ₗ[ℂ] {x // x.is_bimodule_map}
Equations
source
theorem linear_equiv.comp_inj {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [semiring R] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M₁] [module R M₂] [module R M₃] (f : M₁ ≃ₗ[R] M₂) {x y : M₂ →ₗ[R] M₃} :
x = y ↔ x.comp ↑f = y.comp ↑f
source
theorem phi_inv'_map_eq_phi_inv'_map {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
phi_inv_map _ = phi_inv'_map_coe _
source
theorem sig_apply_sig_inv {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {t : ℝ} {x : matrix n n ℂ} :
⇑(_.sig t) (⇑(_.sig (-t)) x) = x
source
theorem sig_inv_apply_sig {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {t : ℝ} {x : matrix n n ℂ} :
⇑(_.sig (-t)) (⇑(_.sig t) x) = x
source
theorem rsmul_module_map_of_real_lsmul_module_map {n : Type u_1} [fintype n] {f : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ} (hf : ∀ (a x : matrix n n ℂ), ⇑f (a.mul x) = a.mul (⇑f x)) (a x : matrix n n ℂ) :
⇑(f.real) (a.mul x) = (⇑(f.real) a).mul x
source
theorem lsmul_module_map_iff_symm_eq_rsmul_module_map {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {f : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ} :
f = ⇑rmul (⇑f 1) ↔ ⇑(linear_equiv.symm_map ℂ (matrix n n ℂ)) f = ⇑lmul (⇑f 1)
source
theorem linear_map.real_adjoint_eq {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (f : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑linear_map.adjoint f.real = (_.sig (-1)).to_linear_map.comp ((⇑linear_map.adjoint f).real.comp (_.sig 1).to_linear_map)
source
theorem left_hand_twist_eq_sig_one {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
↑(tensor_product.lid ℂ (matrix n n ℂ)).comp ((tensor_product.map ((⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ))).comp (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 ↑(tensor_product.comm ℂ (matrix n n ℂ) (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).comp tensor_one_map))))) = (_.sig 1).to_linear_map
source
theorem right_hand_twist_eq_sig_neg_one {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
↑(tensor_product.lid ℂ (matrix n n ℂ)).comp (↑(tensor_product.comm ℂ (matrix n n ℂ) ℂ).comp ((tensor_product.map 1 ((⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ))).comp (linear_map.mul' ℂ (matrix n n ℂ)))).comp (↑(tensor_product.assoc ℂ (matrix n n ℂ) (matrix n n ℂ) (matrix n n ℂ)).comp ((tensor_product.map ↑(tensor_product.comm ℂ (matrix n n ℂ) (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 one_tensor_map)))))) = (_.sig (-1)).to_linear_map
source
theorem balance_symm_1 {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
(⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ))).comp ((linear_map.mul' ℂ (matrix n n ℂ)).comp (tensor_product.map (_.sig 1).to_linear_map 1)) = (⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ))).comp ((linear_map.mul' ℂ (matrix n n ℂ)).comp (tensor_product.map 1 (_.sig (-1)).to_linear_map))
source
theorem balance_symm_2 {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
(⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ))).comp ((linear_map.mul' ℂ (matrix n n ℂ)).comp (tensor_product.map 1 (_.sig (-1)).to_linear_map)) = (⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ))).comp ((linear_map.mul' ℂ (matrix n n ℂ)).comp ↑(tensor_product.comm ℂ (matrix n n ℂ) (matrix n n ℂ)))