mathlib3 documentation

monlib / linear_algebra.my_ips.nontracial

Some results on the Hilbert space on finite-dimensional C*-algebras #

This file contains some results on the Hilbert space on finite-dimensional C*-algebras (so just a direct sum of matrix algebras over ℂ).

Section single_block #

source
theorem inner_std_basis_matrix_left {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (i j : n) (x : matrix n n ℂ) :
has_inner.inner (matrix.std_basis_matrix i j 1) x = x.mul φ.matrix i j
source
theorem inner_std_basis_matrix_std_basis_matrix {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (i j k l : n) :
has_inner.inner (matrix.std_basis_matrix i j 1) (matrix.std_basis_matrix k l 1) = ite (i = k) (φ.matrix l j) 0
source
theorem linear_map.mul'_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 ℂ) :
⇑(⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))) x = finset.univ.sum (λ (i : n), finset.univ.sum (λ (j : n), finset.univ.sum (λ (k : n), finset.univ.sum (λ (l : n), (x i l * (φ.matrix)⁻¹ k j) • matrix.std_basis_matrix i j 1 ⊗ₜ[ℂ] matrix.std_basis_matrix k l 1))))

we can expres the nontracial adjoint of linear_map.mul' by $$m^*(x) = \sum_{i,j,k,l} x_{il}Q^{-1}_{kj}(e_{ij} \otimes_t e_{kl})$$

source
theorem matrix.linear_map_ext_iff_inner_map {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 ℂ} :
x = y ↔ ∀ (u v : matrix n n ℂ), has_inner.inner (⇑x u) v = has_inner.inner (⇑y u) v
source
theorem matrix.linear_map_ext_iff_map_inner {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 ℂ} :
x = y ↔ ∀ (u v : matrix n n ℂ), has_inner.inner v (⇑x u) = has_inner.inner v (⇑y u)
source
theorem matrix.inner_conj_Q {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (a x : matrix n n ℂ) :
has_inner.inner x ((φ.matrix.mul a).mul (φ.matrix)⁻¹) = has_inner.inner (x.mul a.conj_transpose) 1
source
theorem matrix.inner_star_right {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (b y : matrix n n ℂ) :
has_inner.inner b y = has_inner.inner 1 (b.conj_transpose.mul y)
source
theorem matrix.inner_star_left {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (a x : matrix n n ℂ) :
has_inner.inner a x = has_inner.inner (x.conj_transpose.mul a) 1
source
theorem one_inner {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (a : matrix n n ℂ) :
has_inner.inner 1 a = (φ.matrix.mul a).trace
source
theorem module.dual.is_faithful_pos_map.map_star {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (x : matrix n n ℂ) :
⇑φ (has_star.star x) = has_star.star (⇑φ x)
source
theorem nontracial.unit_adjoint_eq {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 ℂ)) = φ
source
theorem qam.nontracial.mul_comp_mul_adjoint {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] :
(linear_map.mul' ℂ (matrix n n ℂ)).comp (⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))) = (φ.matrix)⁻¹.trace • 1
source
theorem module.dual.is_faithful_pos_map.inner_coord' {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (ij : n × n) (x : matrix n n ℂ) :
has_inner.inner (⇑(_.basis) ij) x = x.mul (_.rpow (1 / 2)) ij.fst ij.snd
source
theorem rank_one_to_matrix {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 ℂ) :
⇑(_.to_matrix) ↑(rank_one a b) = (matrix.col (⇑matrix.reshape (a.mul (_.rpow (1 / 2))))).mul (matrix.col (⇑matrix.reshape (b.mul (_.rpow (1 / 2))))).conj_transpose
source
noncomputable def module.dual.is_faithful_pos_map.sig {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (z : ℝ) :
matrix n n ℂ ≃ₐ[ℂ] matrix n n ℂ
Equations
source
theorem module.dual.is_faithful_pos_map.sig_apply {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (z : ℝ) (x : matrix n n ℂ) :
⇑(hφ.sig z) x = ((_.rpow (-z)).mul x).mul (_.rpow z)
source
theorem module.dual.is_faithful_pos_map.sig_symm_apply {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (z : ℝ) (x : matrix n n ℂ) :
⇑((hφ.sig z).symm) x = ((_.rpow z).mul x).mul (_.rpow (-z))
source
theorem module.dual.is_faithful_pos_map.sig_symm_eq {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (z : ℝ) :
(hφ.sig z).symm = hφ.sig (-z)
source
noncomputable def module.dual.is_faithful_pos_map.Psi_to_fun' {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (t s : ℝ) :
(matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) →ₗ[ℂ] tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ)ᵐᵒᵖ
Equations
source
theorem module.dual.is_faithful_pos_map.sig_conj_transpose {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (t : ℝ) (x : matrix n n ℂ) :
(⇑(hφ.sig t) x).conj_transpose = ⇑(hφ.sig (-t)) x.conj_transpose
source
theorem module.dual.is_faithful_pos_map.Psi_to_fun'_apply {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (t s : ℝ) (x y : matrix n n ℂ) :
⇑(_.Psi_to_fun' t s) ↑(rank_one x y) = ⇑(_.sig t) x ⊗ₜ[ℂ] ⇑op (⇑(_.sig s) y).conj_transpose
source
noncomputable def module.dual.is_faithful_pos_map.Psi_inv_fun' {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (t s : ℝ) :
tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ)ᵐᵒᵖ →ₗ[ℂ] matrix n n ℂ →ₗ[ℂ] matrix n n ℂ
Equations
source
theorem module.dual.is_faithful_pos_map.basis_op_repr_apply {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (x : (matrix n n ℂ)ᵐᵒᵖ) (ij : n × n) :
⇑(⇑(hφ.basis.mul_opposite.repr) x) ij = (⇑unop x).mul (_.rpow (1 / 2)) ij.fst ij.snd
source
theorem module.dual.is_faithful_pos_map.Psi_inv_fun'_apply {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (t s : ℝ) (x : matrix n n ℂ) (y : (matrix n n ℂ)ᵐᵒᵖ) :
⇑(_.Psi_inv_fun' t s) (x ⊗ₜ[ℂ] y) = ↑(rank_one (⇑(_.sig (-t)) x) (⇑(_.sig (-s)) (⇑unop y).conj_transpose))
source
theorem module.dual.is_faithful_pos_map.sig_apply_sig {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (t s : ℝ) (x : matrix n n ℂ) :
⇑(hφ.sig t) (⇑(hφ.sig s) x) = ⇑(hφ.sig (t + s)) x
source
theorem module.dual.is_faithful_pos_map.sig_zero {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (x : matrix n n ℂ) :
⇑(hφ.sig 0) x = x
source
theorem module.dual.is_faithful_pos_map.Psi_left_inv' {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (t s : ℝ) (A : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑(hφ.Psi_inv_fun' t s) (⇑(hφ.Psi_to_fun' t s) A) = A
source
theorem module.dual.is_faithful_pos_map.Psi_right_inv' {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (t s : ℝ) (x : matrix n n ℂ) (y : (matrix n n ℂ)ᵐᵒᵖ) :
⇑(hφ.Psi_to_fun' t s) (⇑(hφ.Psi_inv_fun' t s) (x ⊗ₜ[ℂ] y)) = x ⊗ₜ[ℂ] y
source
@[simp]
theorem module.dual.is_faithful_pos_map.Psi_apply {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (t s : ℝ) (x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑(hφ.Psi t s) x = ⇑(hφ.Psi_to_fun' t s) x
source
noncomputable def module.dual.is_faithful_pos_map.Psi {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (t s : ℝ) :
(matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) ≃ₗ[ℂ] tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ)ᵐᵒᵖ

this defines the linear equivalence from linear maps on $M_n$ to $M_n\otimes M_n^\textnormal{op}$, i.e., $$\Psi_{t,s}\colon \mathcal{L}(M_n) \cong_{\texttt{l}} M_n \otimes M_n^\textnormal{op}$$

Equations
source
@[simp]
theorem module.dual.is_faithful_pos_map.Psi_symm_apply {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (t s : ℝ) (x : tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ)ᵐᵒᵖ) :
⇑((hφ.Psi t s).symm) x = ⇑(hφ.Psi_inv_fun' t s) x
source
theorem module.dual.is_faithful_pos_map.Psi_0_0_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 ℂ) :
⇑(_.Psi 0 0) x = ⇑(tensor_product.map x op) (⇑(⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))) 1)
source
theorem module.dual.is_faithful_pos_map.Psi_eq {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (t s : ℝ) (x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑(_.Psi t s) x = ⇑(tensor_product.map (_.sig t).to_linear_map (op.comp ((_.sig (-s)).to_linear_map.comp unop))) (⇑(tensor_product.map x op) (⇑(⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))) 1))
source
theorem linear_map.mul_left_to_matrix {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (hφ : φ.is_faithful_pos_map) (x : matrix n n ℂ) :
⇑(hφ.to_matrix) (linear_map.mul_left ℂ x) = matrix.kronecker_map has_mul.mul x 1
source
theorem linear_map.mul_right_to_matrix {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : matrix n n ℂ) :
⇑(_.to_matrix) (linear_map.mul_right ℂ x) = matrix.kronecker_map has_mul.mul 1 (⇑(_.sig (1 / 2)) x).transpose
source
theorem nontracial.inner_symm {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 ℂ) :
has_inner.inner x y = has_inner.inner (⇑(_.sig (-1)) y.conj_transpose) x.conj_transpose
source
theorem module.dual.is_faithful_pos_map.sig_adjoint {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {t : ℝ} :
⇑linear_map.adjoint (_.sig t).to_linear_map = (_.sig t).to_linear_map
source
theorem nontracial.inner_symm' {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 ℂ) :
has_inner.inner x y = has_inner.inner (⇑(_.sig (-(1 / 2))) y.conj_transpose) (⇑(_.sig (-(1 / 2))) x.conj_transpose)
source
theorem module.dual.is_faithful_pos_map.basis_apply' {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (i j : n) :
⇑(_.basis) (i, j) = (matrix.std_basis_matrix i j 1).mul (_.rpow (-(1 / 2)))
source
theorem sig_apply_pos_def_matrix {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (t s : ℝ) :
⇑(_.sig t) (_.rpow s) = _.rpow s
source
theorem sig_apply_pos_def_matrix' {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (t : ℝ) :
⇑(_.sig t) φ.matrix = φ.matrix
source
theorem linear_functional_comp_sig {n : Type u_1} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (t : ℝ) :
linear_map.comp φ (_.sig t).to_linear_map = φ
source
theorem linear_functional_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) x) = ⇑φ x

Section direct_sum #

source
theorem include_block_adjoint {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] {i : k} (x : Π (j : k), matrix (s j) (s j) ℂ) :
⇑(⇑linear_map.adjoint matrix.include_block) x = x i
source
@[protected, instance]
def pi.tensor_product_finite_dimensional {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] :
finite_dimensional ℂ (tensor_product ℂ (Π (i : k), matrix (s i) (s i) ℂ) (Π (i : k), matrix (s i) (s i) ℂ))
source
theorem pi_inner_std_basis_matrix_left {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (i : k) (j l : s i) (x : Π (i : k), matrix (s i) (s i) ℂ) :
has_inner.inner (matrix.std_basis_matrix ⟨i, j⟩ ⟨i, l⟩ 1).block_diag' x = (x i * (ψ i).matrix) j l
source
theorem eq_mpr_std_basis_matrix {k : Type u_1} {s : k → Type u_2} [Π (i : k), decidable_eq (s i)] {i j : k} {b c : s j} (h₁ : i = j) :
_.mpr (matrix.std_basis_matrix b c 1) = matrix.std_basis_matrix (_.mpr b) (_.mpr c) 1
source
theorem pi_inner_std_basis_matrix_std_basis_matrix {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] {i j : k} (a b : s i) (c d : s j) :
has_inner.inner (matrix.std_basis_matrix ⟨i, a⟩ ⟨i, b⟩ 1).block_diag' (matrix.std_basis_matrix ⟨j, c⟩ ⟨j, d⟩ 1).block_diag' = dite (i = j) (λ (h : i = j), ite (a = _.mpr c) ((ψ i).matrix (_.mpr d) b) 0) (λ (h : ¬i = j), 0)
source
theorem pi_inner_std_basis_matrix_std_basis_matrix_same {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] {i : k} (a b c d : s i) :
has_inner.inner (matrix.std_basis_matrix ⟨i, a⟩ ⟨i, b⟩ 1).block_diag' (matrix.std_basis_matrix ⟨i, c⟩ ⟨i, d⟩ 1).block_diag' = ite (a = c) ((ψ i).matrix d b) 0
source
theorem pi_inner_std_basis_matrix_std_basis_matrix_ne {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] {i j : k} (h : i ≠ j) (a b : s i) (c d : s j) :
has_inner.inner (matrix.std_basis_matrix ⟨i, a⟩ ⟨i, b⟩ 1).block_diag' (matrix.std_basis_matrix ⟨j, c⟩ ⟨j, d⟩ 1).block_diag' = 0
source
theorem linear_map.pi_mul'_adjoint_single_block {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] {i : k} (x : matrix (s i) (s i) ℂ) :
⇑(⇑linear_map.adjoint (linear_map.mul' ℂ (Π (i : k), matrix (s i) (s i) ℂ))) (⇑matrix.include_block x) = ⇑(tensor_product.map matrix.include_block matrix.include_block) (⇑(⇑linear_map.adjoint (linear_map.mul' ℂ (matrix (s i) (s i) ℂ))) x)
source
theorem linear_map.pi_mul'_adjoint {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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 : Π (i : k), matrix (s i) (s i) ℂ) :
⇑(⇑linear_map.adjoint (linear_map.mul' ℂ (Π (i : k), matrix (s i) (s i) ℂ))) x = finset.univ.sum (λ (r : k), finset.univ.sum (λ (a : s r), finset.univ.sum (λ (b : s r), finset.univ.sum (λ (c : s r), finset.univ.sum (λ (d : s r), (x r a d * (module.dual.pi.matrix_block ψ r)⁻¹ c b) • (matrix.std_basis_matrix ⟨r, a⟩ ⟨r, b⟩ 1).block_diag' ⊗ₜ[ℂ] (matrix.std_basis_matrix ⟨r, c⟩ ⟨r, d⟩ 1).block_diag')))))
source
theorem linear_map.pi_mul'_apply_include_block {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] {i : k} (x : tensor_product ℂ (matrix (s i) (s i) ℂ) (matrix (s i) (s i) ℂ)) :
⇑(linear_map.mul' ℂ (Π (i : k), matrix (s i) (s i) ℂ)) (⇑(tensor_product.map matrix.include_block matrix.include_block) x) = ⇑matrix.include_block (⇑(linear_map.mul' ℂ (matrix (s i) (s i) ℂ)) x)
source
theorem linear_map.pi_mul'_comp_mul'_adjoint {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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 : Π (i : k), matrix (s i) (s i) ℂ) :
⇑(linear_map.mul' ℂ (Π (i : k), matrix (s i) (s i) ℂ)) (⇑(⇑linear_map.adjoint (linear_map.mul' ℂ (Π (i : k), matrix (s i) (s i) ℂ))) x) = finset.univ.sum (λ (i : k), ((ψ i).matrix)⁻¹.trace • ⇑matrix.include_block (x i))
source
theorem linear_map.pi_mul'_comp_mul'_adjoint_eq_smul_id_iff {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] [∀ (i : k), nontrivial (s i)] (α : ℂ) :
(linear_map.mul' ℂ (Π (i : k), matrix (s i) (s i) ℂ)).comp (⇑linear_map.adjoint (linear_map.mul' ℂ (Π (i : k), matrix (s i) (s i) ℂ))) = α • 1 ↔ ∀ (i : k), ((ψ i).matrix)⁻¹.trace = α
source
theorem module.dual.pi.is_faithful_pos_map.inner_coord' {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] {i : k} (ij : s i × s i) (x : Π (i : k), matrix (s i) (s i) ℂ) :
has_inner.inner (⇑(module.dual.pi.is_faithful_pos_map.basis _) ⟨i, ij⟩) x = (x * λ (j : k), _.rpow (1 / 2)) i ij.fst ij.snd
source
theorem module.dual.pi.is_faithful_pos_map.map_star {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] {ψ : Π (i : k), module.dual ℂ (matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).is_faithful_pos_map) (x : Π (i : k), matrix (s i) (s i) ℂ) :
⇑(module.dual.pi ψ) (has_star.star x) = has_star.star (⇑(module.dual.pi ψ) x)
source
theorem nontracial.pi.unit_adjoint_eq {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] :
⇑linear_map.adjoint (algebra.linear_map ℂ (Π (i : k), matrix (s i) (s i) ℂ)) = module.dual.pi ψ
source
def module.dual.pi.is_faithful_pos_map.matrix_is_pos_def {k : Type u_1} {s : k → Type u_2} [Π (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) (i : k) :
(ψ i).matrix.pos_def
source
noncomputable def pi.pos_def.rpow {k : Type u_1} {s : k → Type u_2} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] {a : Π (i : k), matrix (s i) (s i) ℂ} (ha : ∀ (i : k), (a i).pos_def) (r : ℝ) (i : k) :
matrix (s i) (s i) ℂ
Equations
source
theorem pi.pos_def.rpow_mul_rpow {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] {a : Π (i : k), matrix (s i) (s i) ℂ} (ha : ∀ (i : k), (a i).pos_def) (r₁ r₂ : ℝ) :
pi.pos_def.rpow ha r₁ * pi.pos_def.rpow ha r₂ = pi.pos_def.rpow ha (r₁ + r₂)
source
theorem pi.pos_def.rpow_zero {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] {a : Π (i : k), matrix (s i) (s i) ℂ} (ha : ∀ (i : k), (a i).pos_def) :
pi.pos_def.rpow ha 0 = 1
source
theorem module.dual.pi.is_faithful_pos_map.include_block_right_inner {k : Type u_1} [fintype k] [decidable_eq k] {s : k → Type u_2} [Π (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] {i : k} (y : Π (j : k), matrix (s j) (s j) ℂ) (x : matrix (s i) (s i) ℂ) :
has_inner.inner y (⇑matrix.include_block x) = has_inner.inner (y i) x
source
theorem pi_include_block_right_rank_one {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (a : Π (i : k), matrix (s i) (s i) ℂ) {i : k} (b : matrix (s i) (s i) ℂ) (c : Π (i : k), matrix (s i) (s i) ℂ) (j : k) :
⇑(rank_one a (⇑matrix.include_block b)) c j = has_inner.inner b (c i) • a j
source
theorem pi_include_block_left_rank_one {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (b : Π (i : k), matrix (s i) (s i) ℂ) {i : k} (a : matrix (s i) (s i) ℂ) (c : Π (i : k), matrix (s i) (s i) ℂ) (j : k) :
⇑(rank_one (⇑matrix.include_block a) b) c j = has_inner.inner b c • dite (i = j) (λ (h : i = j), _.mpr a) (λ (h : ¬i = j), 0)
source
noncomputable def module.dual.pi.is_faithful_pos_map.sig {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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) (z : ℝ) :
(Π (i : k), matrix (s i) (s i) ℂ) ≃ₐ[ℂ] Π (i : k), matrix (s i) (s i) ℂ
Equations
source
theorem module.dual.pi.is_faithful_pos_map.sig_apply {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (z : ℝ) (x : Π (i : k), matrix (s i) (s i) ℂ) :
⇑(module.dual.pi.is_faithful_pos_map.sig hψ z) x = pi.pos_def.rpow _ (-z) * x * pi.pos_def.rpow _ z
source
theorem module.dual.pi.is_faithful_pos_map.sig_symm_apply {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (z : ℝ) (x : Π (i : k), matrix (s i) (s i) ℂ) :
⇑((module.dual.pi.is_faithful_pos_map.sig hψ z).symm) x = pi.pos_def.rpow _ z * x * pi.pos_def.rpow _ (-z)
source
theorem module.dual.pi.is_faithful_pos_map.sig_symm_eq {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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) (z : ℝ) :
(module.dual.pi.is_faithful_pos_map.sig hψ z).symm = module.dual.pi.is_faithful_pos_map.sig hψ (-z)
source
theorem module.dual.pi.is_faithful_pos_map.sig_apply_single_block {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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) (z : ℝ) {i : k} (x : matrix (s i) (s i) ℂ) :
⇑(module.dual.pi.is_faithful_pos_map.sig hψ z) (⇑matrix.include_block x) = ⇑matrix.include_block (⇑(_.sig z) x)
source
theorem module.dual.pi.is_faithful_pos_map.sig_eq_pi_blocks {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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) (z : ℝ) (x : Π (i : k), matrix (s i) (s i) ℂ) {i : k} :
⇑(module.dual.pi.is_faithful_pos_map.sig hψ z) x i = ⇑(_.sig z) (x i)
source
theorem pi.pos_def.rpow.is_pos_def {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] {a : Π (i : k), matrix (s i) (s i) ℂ} (ha : ∀ (i : k), (a i).pos_def) (r : ℝ) (i : k) :
(pi.pos_def.rpow ha r i).pos_def
source
theorem pi.pos_def.rpow.is_self_adjoint {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] {a : Π (i : k), matrix (s i) (s i) ℂ} (ha : ∀ (i : k), (a i).pos_def) (r : ℝ) :
has_star.star (pi.pos_def.rpow ha r) = pi.pos_def.rpow ha r
source
theorem module.dual.pi.is_faithful_pos_map.sig_star {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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) (z : ℝ) (x : Π (i : k), matrix (s i) (s i) ℂ) :
has_star.star (⇑(module.dual.pi.is_faithful_pos_map.sig hψ z) x) = ⇑(module.dual.pi.is_faithful_pos_map.sig hψ (-z)) (has_star.star x)
source
theorem module.dual.pi.is_faithful_pos_map.sig_apply_sig {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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) (t r : ℝ) (x : Π (i : k), matrix (s i) (s i) ℂ) :
⇑(module.dual.pi.is_faithful_pos_map.sig hψ t) (⇑(module.dual.pi.is_faithful_pos_map.sig hψ r) x) = ⇑(module.dual.pi.is_faithful_pos_map.sig hψ (t + r)) x
source
theorem module.dual.pi.is_faithful_pos_map.sig_zero {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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 : Π (i : k), matrix (s i) (s i) ℂ) :
⇑(module.dual.pi.is_faithful_pos_map.sig hψ 0) x = x
source
theorem module.dual.pi.is_faithful_pos_map.to_matrix_apply'' {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (f : (Π (i : k), matrix (s i) (s i) ℂ) →ₗ[ℂ] Π (i : k), matrix (s i) (s i) ℂ) (r l : Σ (r : k), s r × s r) :
⇑(module.dual.pi.is_faithful_pos_map.to_matrix _) f r l = (⇑f (⇑matrix.include_block (⇑(_.basis) l.snd)) * pi.pos_def.rpow _ (1 / 2)) r.fst r.snd.fst r.snd.snd
source
theorem finset.sum_product_univ {β : Type u_1} {α : Type u_2} {γ : Type u_3} [add_comm_monoid β] [fintype α] [fintype γ] {f : γ × α → β} :
finset.univ.sum (λ (x : γ × α), f x) = finset.univ.sum (λ (x : γ), finset.univ.sum (λ (y : α), f (x, y)))
source
theorem module.dual.pi.is_faithful_pos_map.to_matrix_symm_apply' {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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 : matrix (Σ (i : k), s i × s i) (Σ (i : k), s i × s i) ℂ) :
⇑((module.dual.pi.is_faithful_pos_map.to_matrix _).symm) x = finset.univ.sum (λ (a : k), finset.univ.sum (λ (i : s a), finset.univ.sum (λ (j : s a), finset.univ.sum (λ (b : k), finset.univ.sum (λ (c : s b), finset.univ.sum (λ (d : s b), x ⟨a, (i, j)⟩ ⟨b, (c, d)⟩ • ↑(rank_one (⇑(module.dual.pi.is_faithful_pos_map.basis _) ⟨a, (i, j)⟩) (⇑(module.dual.pi.is_faithful_pos_map.basis _) ⟨b, (c, d)⟩))))))))
source
theorem tensor_product.of_basis_eq_span {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group E] [module 𝕜 E] [add_comm_group F] [module 𝕜 F] (x : tensor_product 𝕜 E F) {ι₁ : Type u_4} {ι₂ : Type u_5} [fintype ι₁] [fintype ι₂] (b₁ : basis ι₁ 𝕜 E) (b₂ : basis ι₂ 𝕜 F) :
x = finset.univ.sum (λ (i : ι₁), finset.univ.sum (λ (j : ι₂), ⇑(⇑((b₁.tensor_product b₂).repr) x) (i, j) • ⇑b₁ i ⊗ₜ[𝕜] ⇑b₂ j))
source
theorem module.dual.pi.is_faithful_pos_map.to_matrix_eq_orthonormal_basis_to_matrix {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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 : (Π (i : k), matrix (s i) (s i) ℂ) →ₗ[ℂ] Π (i : k), matrix (s i) (s i) ℂ) :
⇑(module.dual.pi.is_faithful_pos_map.to_matrix _) x = ⇑(module.dual.pi.is_faithful_pos_map.orthonormal_basis.to_matrix) x
source
theorem module.dual.pi.is_faithful_pos_map.linear_map_eq {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (t r : ℝ) (x : (Π (i : k), matrix (s i) (s i) ℂ) →ₗ[ℂ] Π (i : k), matrix (s i) (s i) ℂ) :
x = finset.univ.sum (λ (a : Σ (i : k), (λ (i : k), s i) i × (λ (i : k), s i) i), finset.univ.sum (λ (b : Σ (i : k), (λ (i : k), s i) i × (λ (i : k), s i) i), ⇑(module.dual.pi.is_faithful_pos_map.to_matrix _) x a b • ↑(rank_one (⇑(module.dual.pi.is_faithful_pos_map.basis _) a) (⇑(module.dual.pi.is_faithful_pos_map.basis _) b))))
source
noncomputable def module.dual.pi.is_faithful_pos_map.Psi_to_fun' {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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) (t r : ℝ) :
((Π (i : k), matrix (s i) (s i) ℂ) →ₗ[ℂ] Π (i : k), matrix (s i) (s i) ℂ) →ₗ[ℂ] tensor_product ℂ (Π (i : k), matrix (s i) (s i) ℂ) (Π (i : k), matrix (s i) (s i) ℂ)ᵐᵒᵖ
Equations
source
theorem pi.is_faithful_pos_map.to_matrix.rank_one_apply {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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) ℂ) :
⇑(module.dual.pi.is_faithful_pos_map.to_matrix _) ↑(rank_one x y) = λ (i j : Σ (i : k), s i × s i), (matrix.col (⇑matrix.reshape ((x i.fst).mul (_.rpow (1 / 2))))).mul (matrix.col (⇑matrix.reshape ((y j.fst).mul (_.rpow (1 / 2))))).conj_transpose i.snd j.snd
source
theorem module.dual.pi.is_faithful_pos_map.basis_repr_apply_apply {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (a : Π (i : k), matrix (s i) (s i) ℂ) (x : Σ (i : k), s i × s i) :
⇑(⇑((module.dual.pi.is_faithful_pos_map.basis _).repr) a) x = ⇑(⇑(_.basis.repr) (a x.fst)) x.snd
source
theorem module.dual.pi.is_faithful_pos_map.Psi_to_fun'_apply {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (t r : ℝ) (a b : Π (i : k), matrix (s i) (s i) ℂ) :
⇑(module.dual.pi.is_faithful_pos_map.Psi_to_fun' hψ t r) ↑(rank_one a b) = ⇑(module.dual.pi.is_faithful_pos_map.sig hψ t) a ⊗ₜ[ℂ] ⇑op (has_star.star (⇑(module.dual.pi.is_faithful_pos_map.sig hψ r) b))
source
theorem algebra.tensor_product.map_apply_map_apply {R : Type u_1} [comm_semiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} {E : Type u_6} {F : Type u_7} [semiring A] [semiring B] [semiring C] [semiring D] [semiring E] [semiring F] [algebra R A] [algebra R B] [algebra R C] [algebra R D] [algebra R E] [algebra R F] (f : A →ₐ[R] B) (g : C →ₐ[R] D) (z : B →ₐ[R] E) (w : D →ₐ[R] F) (x : tensor_product R A C) :
⇑(algebra.tensor_product.map z w) (⇑(algebra.tensor_product.map f g) x) = ⇑(algebra.tensor_product.map (z.comp f) (w.comp g)) x
source
theorem tensor_product.map_apply_map_apply {R : Type u_1} [comm_semiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} {E : Type u_6} {F : Type u_7} [add_comm_monoid A] [add_comm_monoid B] [add_comm_monoid C] [add_comm_monoid D] [add_comm_monoid E] [add_comm_monoid F] [module R A] [module R B] [module R C] [module R D] [module R E] [module R F] (f : A →ₗ[R] B) (g : C →ₗ[R] D) (z : B →ₗ[R] E) (w : D →ₗ[R] F) (x : tensor_product R A C) :
⇑(tensor_product.map z w) (⇑(tensor_product.map f g) x) = ⇑(tensor_product.map (z.comp f) (w.comp g)) x
source
theorem algebra.tensor_product.map_id {R : Type u_1} [comm_semiring R] {A : Type u_2} {B : Type u_3} [semiring A] [semiring B] [algebra R A] [algebra R B] :
algebra.tensor_product.map (alg_hom.id R A) (alg_hom.id R B) = alg_hom.id R (tensor_product R A B)
source
def alg_equiv.tensor_product.map {R : Type u_1} [comm_semiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [semiring A] [semiring B] [semiring C] [semiring D] [algebra R A] [algebra R B] [algebra R C] [algebra R D] (f : A ≃ₐ[R] B) (g : C ≃ₐ[R] D) :
tensor_product R A C ≃ₐ[R] tensor_product R B D
Equations
source
def linear_equiv.tensor_product.map {R : Type u_1} [comm_semiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [add_comm_monoid A] [add_comm_monoid B] [add_comm_monoid C] [add_comm_monoid D] [module R A] [module R B] [module R C] [module R D] (f : A ≃ₗ[R] B) (g : C ≃ₗ[R] D) :
tensor_product R A C ≃ₗ[R] tensor_product R B D
Equations
source
@[simp]
theorem linear_equiv.tensor_product.map_apply {R : Type u_1} [comm_semiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [add_comm_monoid A] [add_comm_monoid B] [add_comm_monoid C] [add_comm_monoid D] [module R A] [module R B] [module R C] [module R D] (f : A ≃ₗ[R] B) (g : C ≃ₗ[R] D) (x : tensor_product R A C) :
⇑(linear_equiv.tensor_product.map f g) x = ⇑(tensor_product.map ↑f ↑g) x
source
@[simp]
theorem linear_equiv.tensor_product.map_symm_apply {R : Type u_1} [comm_semiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [add_comm_monoid A] [add_comm_monoid B] [add_comm_monoid C] [add_comm_monoid D] [module R A] [module R B] [module R C] [module R D] (f : A ≃ₗ[R] B) (g : C ≃ₗ[R] D) (x : tensor_product R B D) :
⇑((linear_equiv.tensor_product.map f g).symm) x = ⇑(tensor_product.map ↑(f.symm) ↑(g.symm)) x
source
@[simp]
theorem pi.transpose_alg_equiv_symm_apply (p : Type u_1) [fintype p] [decidable_eq p] (n : p → Type u_2) [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] (A : (Π (i : p), matrix (n i) (n i) ℂ)ᵐᵒᵖ) (i : p) :
⇑((pi.transpose_alg_equiv p n).symm) A i = (mul_opposite.unop A i).transpose
source
def pi.transpose_alg_equiv (p : Type u_1) [fintype p] [decidable_eq p] (n : p → Type u_2) [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] :
(Π (i : p), matrix (n i) (n i) ℂ) ≃ₐ[ℂ] (Π (i : p), matrix (n i) (n i) ℂ)ᵐᵒᵖ
Equations
source
@[simp]
theorem pi.transpose_alg_equiv_apply (p : Type u_1) [fintype p] [decidable_eq p] (n : p → Type u_2) [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] (A : Π (i : p), matrix (n i) (n i) ℂ) :
⇑(pi.transpose_alg_equiv p n) A = mul_opposite.op (λ (i : p), (A i).transpose)
source
theorem pi.transpose_alg_equiv_symm_op_apply {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] (A : Π (i : k), matrix (s i) (s i) ℂ) :
⇑((pi.transpose_alg_equiv k s).symm) (mul_opposite.op A) = λ (i : k), (A i).transpose
source
def tensor_product_mul_op_equiv {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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
noncomputable def module.dual.pi.is_faithful_pos_map.Psi_inv_fun' {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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) (t r : ℝ) :
tensor_product ℂ (Π (i : k), matrix (s i) (s i) ℂ) (Π (i : k), matrix (s i) (s i) ℂ)ᵐᵒᵖ →ₗ[ℂ] (Π (i : k), matrix (s i) (s i) ℂ) →ₗ[ℂ] Π (i : k), matrix (s i) (s i) ℂ
Equations
source
theorem rank_one_smul_smul {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (x y : E) (r₁ r₂ : 𝕜) :
rank_one (r₁ • x) (has_star.star r₂ • y) = (r₁ * r₂) • rank_one x y
source
theorem rank_one_lm_smul_smul {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (x y : E) (r₁ r₂ : 𝕜) :
↑(rank_one (r₁ • x) (has_star.star r₂ • y)) = (r₁ * r₂) • ↑(rank_one x y)
source
theorem rank_one_sum_sum {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι₁ : Type u_3} {ι₂ : Type u_4} [fintype ι₁] [fintype ι₂] (f : ι₁ → E) (g : ι₂ → E) :
rank_one (finset.univ.sum (λ (i : ι₁), f i)) (finset.univ.sum (λ (i : ι₂), g i)) = finset.univ.sum (λ (i : ι₁), finset.univ.sum (λ (j : ι₂), rank_one (f i) (g j)))
source
theorem rank_one_lm_sum_sum {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {ι₁ : Type u_3} {ι₂ : Type u_4} [fintype ι₁] [fintype ι₂] (f : ι₁ → E) (g : ι₂ → E) :
↑(rank_one (finset.univ.sum (λ (i : ι₁), f i)) (finset.univ.sum (λ (i : ι₂), g i))) = finset.univ.sum (λ (i : ι₁), finset.univ.sum (λ (j : ι₂), ↑(rank_one (f i) (g j))))
source
theorem module.dual.pi.is_faithful_pos_map.Psi_inv_fun'_apply {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (t r : ℝ) (x : Π (i : k), matrix (s i) (s i) ℂ) (y : (Π (i : k), matrix (s i) (s i) ℂ)ᵐᵒᵖ) :
⇑(module.dual.pi.is_faithful_pos_map.Psi_inv_fun' hψ t r) (x ⊗ₜ[ℂ] y) = ↑(rank_one (⇑(module.dual.pi.is_faithful_pos_map.sig hψ (-t)) x) (⇑(module.dual.pi.is_faithful_pos_map.sig hψ (-r)) (has_star.star (mul_opposite.unop y))))
source
theorem module.dual.pi.is_faithful_pos_map.Psi_left_inv {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (t r : ℝ) (x y : Π (i : k), matrix (s i) (s i) ℂ) :
⇑(module.dual.pi.is_faithful_pos_map.Psi_inv_fun' hψ t r) (⇑(module.dual.pi.is_faithful_pos_map.Psi_to_fun' hψ t r) ↑(rank_one x y)) = ↑(rank_one x y)
source
theorem module.dual.pi.is_faithful_pos_map.Psi_right_inv {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (t r : ℝ) (x : Π (i : k), matrix (s i) (s i) ℂ) (y : (Π (i : k), matrix (s i) (s i) ℂ)ᵐᵒᵖ) :
⇑(module.dual.pi.is_faithful_pos_map.Psi_to_fun' hψ t r) (⇑(module.dual.pi.is_faithful_pos_map.Psi_inv_fun' hψ t r) (x ⊗ₜ[ℂ] y)) = x ⊗ₜ[ℂ] y
source
noncomputable def module.dual.pi.is_faithful_pos_map.Psi {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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) (t r : ℝ) :
((Π (i : k), matrix (s i) (s i) ℂ) →ₗ[ℂ] Π (i : k), matrix (s i) (s i) ℂ) ≃ₗ[ℂ] tensor_product ℂ (Π (i : k), matrix (s i) (s i) ℂ) (Π (i : k), matrix (s i) (s i) ℂ)ᵐᵒᵖ
Equations
source
@[simp]
theorem module.dual.pi.is_faithful_pos_map.Psi_apply {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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) (t r : ℝ) (x : (Π (i : k), matrix (s i) (s i) ℂ) →ₗ[ℂ] Π (i : k), matrix (s i) (s i) ℂ) :
⇑(module.dual.pi.is_faithful_pos_map.Psi hψ t r) x = ⇑(module.dual.pi.is_faithful_pos_map.Psi_to_fun' hψ t r) x
source
@[simp]
theorem module.dual.pi.is_faithful_pos_map.Psi_symm_apply {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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) (t r : ℝ) (x : tensor_product ℂ (Π (i : k), matrix (s i) (s i) ℂ) (Π (i : k), matrix (s i) (s i) ℂ)ᵐᵒᵖ) :
⇑((module.dual.pi.is_faithful_pos_map.Psi hψ t r).symm) x = ⇑(module.dual.pi.is_faithful_pos_map.Psi_inv_fun' hψ t r) x
source
theorem pi.inner_symm {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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) ℂ) :
has_inner.inner x y = has_inner.inner (⇑(module.dual.pi.is_faithful_pos_map.sig hψ (-1)) (has_star.star y)) (has_star.star x)
source
theorem module.dual.pi.is_faithful_pos_map.sig_adjoint {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] {t : ℝ} :
⇑linear_map.adjoint (module.dual.pi.is_faithful_pos_map.sig hψ t).to_linear_map = (module.dual.pi.is_faithful_pos_map.sig hψ t).to_linear_map
source
theorem module.dual.is_faithful_pos_map.norm_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 ℂ) :
‖x‖ = real.sqrt (⇑is_R_or_C.re (⇑ψ (x.conj_transpose.mul x)))
source
theorem module.dual.pi.is_faithful_pos_map.norm_eq {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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 : Π (i : k), matrix (s i) (s i) ℂ) :
‖x‖ = real.sqrt (⇑is_R_or_C.re (⇑(module.dual.pi ψ) (has_star.star x * x)))
source
theorem norm_mul_norm_eq_norm_tmul {𝕜 : Type u_1} {B : Type u_2} {C : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group B] [normed_add_comm_group C] [inner_product_space 𝕜 B] [inner_product_space 𝕜 C] [finite_dimensional 𝕜 B] [finite_dimensional 𝕜 C] (x : B) (y : C) :
‖x‖ * ‖y‖ = ‖x ⊗ₜ[𝕜] y‖
source
@[protected, instance]
def matrix.is_fd {n : Type u_1} [fintype n] [decidable_eq n] :
finite_dimensional ℂ (matrix n n ℂ)
source
@[protected, instance]
def matrix.is_star_module {n : Type u_1} [fintype n] [decidable_eq n] :
star_module ℂ (matrix n n ℂ)
source
@[protected, instance]
def pi.matrix.is_fd {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] :
finite_dimensional ℂ (Π (i : k), matrix (s i) (s i) ℂ)
source
@[protected, instance]
def pi.matrix.is_star_module {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] :
star_module ℂ (Π (i : k), matrix (s i) (s i) ℂ)
source
@[protected, instance]
def pi.matrix.is_topological_add_group {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] :
topological_add_group (Π (i : k), matrix (s i) (s i) ℂ)
source
@[protected, instance]
def pi.matrix.has_continuous_smul {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] :
has_continuous_smul ℂ (Π (i : k), matrix (s i) (s i) ℂ)
source
theorem pi.rank_one_lm_real_apply {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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) ℂ) :
(rank_one_lm x y).real = rank_one_lm (has_star.star x) (⇑(module.dual.pi.is_faithful_pos_map.sig hψ (-1)) (has_star.star y))
source
theorem pi.pos_def.rpow_one_eq_self {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] {Q : Π (i : k), matrix (s i) (s i) ℂ} (hQ : ∀ (i : k), (Q i).pos_def) :
pi.pos_def.rpow hQ 1 = Q
source
theorem pi.pos_def.rpow_neg_one_eq_inv_self {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (i : k), fintype (s i)] [Π (i : k), decidable_eq (s i)] {Q : Π (i : k), matrix (s i) (s i) ℂ} (hQ : ∀ (i : k), (Q i).pos_def) :
pi.pos_def.rpow hQ (-1) = Q⁻¹
source
theorem module.dual.pi.is_faithful_pos_map.inner_left_conj' {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (a b c : Π (i : k), matrix (s i) (s i) ℂ) :
has_inner.inner a (b * c) = has_inner.inner (a * ⇑(module.dual.pi.is_faithful_pos_map.sig hψ (-1)) (has_star.star c)) b
source
theorem module.dual.pi.is_faithful_pos_map.inner_right_conj' {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (a b c : Π (i : k), matrix (s i) (s i) ℂ) :
has_inner.inner (a * c) b = has_inner.inner a (b * ⇑(module.dual.pi.is_faithful_pos_map.sig hψ (-1)) (has_star.star c))
source
theorem moudle.dual.pi.is_faithful_pos_map.sig_trans_sig {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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 : ℝ) :
(module.dual.pi.is_faithful_pos_map.sig hψ y).trans (module.dual.pi.is_faithful_pos_map.sig hψ x) = module.dual.pi.is_faithful_pos_map.sig hψ (x + y)
source
theorem module.dual.pi.is_faithful_pos_map.sig_comp_sig {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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 : ℝ) :
(module.dual.pi.is_faithful_pos_map.sig hψ x).to_linear_map.comp (module.dual.pi.is_faithful_pos_map.sig hψ y).to_linear_map = (module.dual.pi.is_faithful_pos_map.sig hψ (x + y)).to_linear_map
source
theorem module.dual.pi.is_faithful_pos_map.sig_zero' {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] :
module.dual.pi.is_faithful_pos_map.sig hψ 0 = 1
source
theorem pi.comp_sig_eq_iff {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (t : ℝ) (f g : (Π (i : k), matrix (s i) (s i) ℂ) →ₗ[ℂ] Π (i : k), matrix (s i) (s i) ℂ) :
f.comp (module.dual.pi.is_faithful_pos_map.sig hψ t).to_linear_map = g ↔ f = g.comp (module.dual.pi.is_faithful_pos_map.sig hψ (-t)).to_linear_map
source
theorem pi.sig_comp_eq_iff {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (t : ℝ) (f g : (Π (i : k), matrix (s i) (s i) ℂ) →ₗ[ℂ] Π (i : k), matrix (s i) (s i) ℂ) :
(module.dual.pi.is_faithful_pos_map.sig hψ t).to_linear_map.comp f = g ↔ f = (module.dual.pi.is_faithful_pos_map.sig hψ (-t)).to_linear_map.comp g
source
theorem rank_one_lm_eq_rank_one {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (x y : E) :
rank_one_lm x y = ↑(rank_one x y)
source
theorem linear_map.pi.adjoint_real_eq {k : Type u_2} [fintype k] [decidable_eq k] {s : k → Type u_3} [Π (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] (f : (Π (i : k), matrix (s i) (s i) ℂ) →ₗ[ℂ] Π (i : k), matrix (s i) (s i) ℂ) :
(⇑linear_map.adjoint f).real = (module.dual.pi.is_faithful_pos_map.sig hψ 1).to_linear_map.comp ((⇑linear_map.adjoint f.real).comp (module.dual.pi.is_faithful_pos_map.sig hψ (-1)).to_linear_map)