The inner product space on finite dimensional C*-algebras #
This file contains some basic results on the inner product space on finite dimensional C*-algebras.
theorem
linear_functional_right_mul
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[algebra R A]
[star_semigroup A]
{φ : A →ₗ[R] R}
(x y z : A) :
⇑φ (has_star.star (x * y) * z) = ⇑φ (has_star.star y * (has_star.star x * z))
A lemma that states the right multiplication property of a linear functional.
theorem
linear_functional_left_mul
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[algebra R A]
[star_semigroup A]
{φ : A →ₗ[R] R}
(x y z : A) :
⇑φ (has_star.star x * (y * z)) = ⇑φ (has_star.star (has_star.star y * x) * z)
A lemma that states the left multiplication property of a linear functional.
def
module.dual.pi.matrix_block
{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) ℂ))
(i : k) :
A function that returns the direct sum of matrices for each index of type 'i'.
Equations
- module.dual.pi.matrix_block ψ = finset.univ.sum (λ (i : k), ⇑matrix.include_block (ψ i).matrix)
theorem
inner_pi_eq_sum
{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]
(x y : Π (i : k), matrix (s i) (s i) ℂ) :
has_inner.inner x y = finset.univ.sum (λ (i : k), has_inner.inner (x i) (y i))
A lemma that states the inner product of two direct sum matrices is the sum of the inner products of their components.
theorem
module.dual.pi.matrix_block_apply
{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) ℂ)}
{i : k} :
module.dual.pi.matrix_block ψ i = (ψ i).matrix
def
star_alg_equiv.pi
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{k : Type u_1}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(f : Π (i : k), matrix (s i) (s i) 𝕜 ≃⋆ₐ[𝕜] matrix (s i) (s i) 𝕜) :
A function that returns a star algebra equivalence for each index of type 'i'.
theorem
star_alg_equiv.pi_apply
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{k : Type u_1}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(f : Π (i : k), matrix (s i) (s i) 𝕜 ≃⋆ₐ[𝕜] matrix (s i) (s i) 𝕜)
(x : Π (i : k), matrix (s i) (s i) 𝕜)
(i : k) :
⇑(star_alg_equiv.pi f) x i = ⇑(f i) (x i)
noncomputable
def
star_alg_equiv.pi.unitary
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{k : Type u_1}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(f : Π (i : k), matrix (s i) (s i) 𝕜 ≃⋆ₐ[𝕜] matrix (s i) (s i) 𝕜)
(i : k) :
↥(matrix.unitary_group (s i) 𝕜)
the unitary element from the star algebraic equivalence
Equations
- star_alg_equiv.pi.unitary f = λ (i : k), matrix.star_alg_equiv.unitary (f i)
theorem
star_alg_equiv.of_pi_is_inner
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{k : Type u_1}
[fintype k]
[decidable_eq k]
{s : k → Type u_3}
[Π (i : k), fintype (s i)]
[Π (i : k), decidable_eq (s i)]
(f : Π (i : k), matrix (s i) (s i) 𝕜 ≃⋆ₐ[𝕜] matrix (s i) (s i) 𝕜) :
any $^*$-isomorphism on $\bigoplus_i M_{n_i}$ is an inner automorphism
theorem
star_alg_equiv.pi_symm_apply_apply
{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)]
(f : Π (i : k), matrix (s i) (s i) ℂ ≃⋆ₐ[ℂ] matrix (s i) (s i) ℂ)
(x : Π (i : k), matrix (s i) (s i) ℂ) :
⇑(star_alg_equiv.pi (λ (i : k), (f i).symm)) (⇑(star_alg_equiv.pi f) x) = x
theorem
module.dual.pi.apply_eq_of
{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) ℂ))
(x : Π (i : k), matrix (s i) (s i) ℂ)
(h : ∀ (a : Π (i : k), matrix ((λ (i : k), s i) i) ((λ (i : k), s i) i) ℂ), ⇑(module.dual.pi ψ) a = (matrix.block_diagonal' x * matrix.block_diagonal' a).trace) :
theorem
star_alg_equiv.pi_symm_apply_eq
{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)]
(f : Π (i : k), matrix (s i) (s i) ℂ ≃⋆ₐ[ℂ] matrix (s i) (s i) ℂ)
(x y : Π (i : k), matrix (s i) (s i) ℂ) :
⇑(star_alg_equiv.pi (λ (i : k), (f i).symm)) x = y ↔ x = ⇑(star_alg_equiv.pi f) y
Section single_block #
theorem
module.dual.is_faithful_pos_map.inner_eq
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x y : matrix n n ℂ) :
has_inner.inner x y = ⇑φ (x.conj_transpose.mul y)
theorem
module.dual.is_faithful_pos_map.inner_eq'
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x y : matrix n n ℂ) :
has_inner.inner x y = ((φ.matrix.mul x.conj_transpose).mul y).trace
def
module.dual.is_faithful_pos_map.matrix_is_pos_def
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
(hφ : φ.is_faithful_pos_map) :
theorem
module.dual.is_faithful_pos_map.mul_right
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
(hφ : φ.is_faithful_pos_map)
(x y z : matrix n n ℂ) :
⇑φ (x.conj_transpose.mul (y.mul z)) = ⇑φ ((x.mul ((φ.matrix.mul z.conj_transpose).mul (φ.matrix)⁻¹)).conj_transpose.mul y)
theorem
module.dual.is_faithful_pos_map.inner_left_mul
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x y z : matrix n n ℂ) :
has_inner.inner (x.mul y) z = has_inner.inner y (x.conj_transpose.mul z)
theorem
module.dual.is_faithful_pos_map.inner_right_mul
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x y z : matrix n n ℂ) :
has_inner.inner x (y.mul z) = has_inner.inner (y.conj_transpose.mul x) z
theorem
module.dual.is_faithful_pos_map.inner_left_conj
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x y z : matrix n n ℂ) :
has_inner.inner x (y.mul z) = has_inner.inner (x.mul ((φ.matrix.mul z.conj_transpose).mul (φ.matrix)⁻¹)) y
theorem
module.dual.is_faithful_pos_map.mul_left
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
(hφ : φ.is_faithful_pos_map)
(x y z : matrix n n ℂ) :
⇑φ ((x.mul y).conj_transpose.mul z) = ⇑φ (x.conj_transpose.mul (z.mul ((φ.matrix.mul y.conj_transpose).mul (φ.matrix)⁻¹)))
theorem
module.dual.is_faithful_pos_map.inner_right_conj
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x y z : matrix n n ℂ) :
has_inner.inner (x.mul y) z = has_inner.inner x (z.mul ((φ.matrix.mul y.conj_transpose).mul (φ.matrix)⁻¹))
theorem
module.dual.is_faithful_pos_map.adjoint_eq
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map] :
⇑linear_map.adjoint φ = algebra.linear_map ℂ (matrix n n ℂ)
theorem
module.dual.is_faithful_pos_map.star_alg_equiv_adjoint_eq
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(f : matrix n n ℂ ≃⋆ₐ[ℂ] matrix n n ℂ)
(x : matrix n n ℂ) :
⇑(⇑linear_map.adjoint f.to_alg_equiv.to_linear_map) x = (⇑(f.symm) (x.mul φ.matrix)).mul (φ.matrix)⁻¹
The adjoint of a star-algebraic equivalence $f$ on matrix algebras is given by
$$f^*\colon x \mapsto f^{-1}(x Q) Q^{-1},$$
where $Q$ is hφ.matrix.
theorem
module.dual.is_faithful_pos_map.star_alg_equiv_unitary_commute_iff
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(f : matrix n n ℂ ≃⋆ₐ[ℂ] matrix n n ℂ) :
theorem
module.dual.is_faithful_pos_map.star_alg_equiv_is_isometry_tfae
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
[nontrivial n]
(f : matrix n n ℂ ≃⋆ₐ[ℂ] matrix n n ℂ) :
[⇑f φ.matrix = φ.matrix, ⇑linear_map.adjoint f.to_alg_equiv.to_linear_map = f.symm.to_alg_equiv.to_linear_map, linear_map.comp φ f.to_alg_equiv.to_linear_map = φ, ∀ (x y : matrix n n ℂ), has_inner.inner (⇑f x) (⇑f y) = has_inner.inner x y, ∀ (x : matrix n n ℂ), ‖⇑f x‖ = ‖x‖, commute φ.matrix ⇑(matrix.star_alg_equiv.unitary f)].tfae
Let f be a star-algebraic equivalence on matrix algebras. Then tfae:
f φ.matrix = φ.matrix,f.adjoint = f⁻¹,φ ∘ f = φ,∀ x y, ⟪f x, f y⟫_ℂ = ⟪x, y⟫_ℂ,∀ x, ‖f x‖ = ‖x‖,φ.matrixcommutes withf.unitary.
@[protected]
noncomputable
def
module.dual.is_faithful_pos_map.basis
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
(hφ : φ.is_faithful_pos_map) :
@[protected]
theorem
module.dual.is_faithful_pos_map.basis_apply
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
(hφ : φ.is_faithful_pos_map)
(ij : n × n) :
@[protected]
noncomputable
def
module.dual.is_faithful_pos_map.to_matrix
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
(hφ : φ.is_faithful_pos_map) :
Equations
theorem
module.dual.is_faithful_pos_map.basis_is_orthonormal
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map] :
orthonormal ℂ ⇑(_.basis)
@[protected]
noncomputable
def
module.dual.is_faithful_pos_map.orthonormal_basis
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map] :
orthonormal_basis (n × n) ℂ (matrix n n ℂ)
Equations
- module.dual.is_faithful_pos_map.orthonormal_basis = module.dual.is_faithful_pos_map.orthonormal_basis._proof_1.basis.to_orthonormal_basis module.dual.is_faithful_pos_map.orthonormal_basis._proof_2
@[protected]
theorem
module.dual.is_faithful_pos_map.orthonormal_basis_apply
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(ij : n × n) :
⇑module.dual.is_faithful_pos_map.orthonormal_basis ij = (matrix.std_basis_matrix ij.fst ij.snd 1).mul (_.rpow (-(1 / 2)))
theorem
module.dual.is_faithful_pos_map.inner_coord
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(ij : n × n)
(y : matrix n n ℂ) :
has_inner.inner (⇑module.dual.is_faithful_pos_map.orthonormal_basis ij) y = y.mul (_.rpow (1 / 2)) ij.fst ij.snd
@[protected]
theorem
module.dual.is_faithful_pos_map.basis_repr_apply
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : matrix n n ℂ)
(ij : n × n) :
@[protected]
theorem
module.dual.is_faithful_pos_map.to_matrix_symm_apply
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : matrix (n × n) (n × n) ℂ) :
⇑(_.to_matrix.symm) x = finset.univ.sum (λ (i : n), finset.univ.sum (λ (j : n), finset.univ.sum (λ (k : n), finset.univ.sum (λ (l : n), x (i, j) (k, l) • ↑(rank_one (⇑(_.basis) (i, j)) (⇑(_.basis) (k, l)))))))
theorem
module.dual.eq_rank_one_of_faithful_pos_map
{n : Type u_3}
[decidable_eq n]
[fintype n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
x = finset.univ.sum (λ (i : n), finset.univ.sum (λ (j : n), finset.univ.sum (λ (k : n), finset.univ.sum (λ (l : n), ⇑(_.to_matrix) x (i, j) (k, l) • ↑(rank_one (⇑(_.basis) (i, j)) (⇑(_.basis) (k, l)))))))
Section direct_sum #
theorem
linear_map.sum_single_comp_proj
{R : Type u_1}
{ι : Type u_2}
[fintype ι]
[decidable_eq ι]
[semiring R]
{φ : ι → Type u_3}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)] :
finset.univ.sum (λ (i : ι), (linear_map.single i).comp (linear_map.proj i)) = linear_map.id
theorem
linear_map.lrsum_eq_single_proj_lrcomp
{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)]
(f : (Π (i : k), matrix (s i) (s i) ℂ) →ₗ[ℂ] Π (i : k), matrix (s i) (s i) ℂ) :
finset.univ.sum (λ (r : k), finset.univ.sum (λ (p : k), (linear_map.single r).comp ((linear_map.proj r).comp (f.comp ((linear_map.single p).comp (linear_map.proj p)))))) = f
theorem
module.dual.pi.is_faithful_pos_map.inner_eq
{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]
(x y : Π (i : k), matrix (s i) (s i) ℂ) :
has_inner.inner x y = ⇑(module.dual.pi ψ) (has_star.star x * y)
theorem
module.dual.pi.is_faithful_pos_map.inner_eq'
{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]
(x y : Π (i : k), matrix (s i) (s i) ℂ) :
has_inner.inner x y = finset.univ.sum (λ (i : k), (((ψ i).matrix.mul (x i).conj_transpose).mul (y i)).trace)
theorem
module.dual.pi.is_faithful_pos_map.inner_left_mul
{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]
(x y z : Π (i : k), matrix (s i) (s i) ℂ) :
has_inner.inner (x * y) z = has_inner.inner y (has_star.star x * z)
theorem
module.dual.pi.is_faithful_pos_map.mul_right
{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), (ψ i).is_faithful_pos_map)
(x y z : Π (i : k), matrix (s i) (s i) ℂ) :
⇑(module.dual.pi ψ) (has_star.star x * (y * z)) = ⇑(module.dual.pi ψ) (has_star.star (x * (module.dual.pi.matrix_block ψ * has_star.star z * (module.dual.pi.matrix_block ψ)⁻¹)) * y)
theorem
module.dual.pi.is_faithful_pos_map.inner_left_conj
{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]
(x y z : Π (i : k), matrix (s i) (s i) ℂ) :
has_inner.inner x (y * z) = has_inner.inner (x * (module.dual.pi.matrix_block ψ * has_star.star z * (module.dual.pi.matrix_block ψ)⁻¹)) y
theorem
module.dual.pi.is_faithful_pos_map.inner_right_mul
{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]
(x y z : Π (i : k), matrix (s i) (s i) ℂ) :
has_inner.inner x (y * z) = has_inner.inner (has_star.star y * x) z
theorem
module.dual.pi.is_faithful_pos_map.adjoint_eq
{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] :
⇑linear_map.adjoint (module.dual.pi ψ) = algebra.linear_map ℂ (Π (i : k), matrix (s i) (s i) ℂ)
@[protected]
noncomputable
def
module.dual.pi.is_faithful_pos_map.basis
{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), (ψ i).is_faithful_pos_map) :
Equations
- module.dual.pi.is_faithful_pos_map.basis hψ = pi.basis (λ (i : k), _.basis)
@[protected]
theorem
module.dual.pi.is_faithful_pos_map.basis_apply
{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), (ψ i).is_faithful_pos_map)
(ijk : Σ (i : k), s i × s i) :
⇑(module.dual.pi.is_faithful_pos_map.basis hψ) ijk = ⇑matrix.include_block ((matrix.std_basis_matrix ijk.snd.fst ijk.snd.snd 1).mul (_.rpow (-(1 / 2))))
@[protected]
theorem
module.dual.pi.is_faithful_pos_map.basis_apply'
{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), (ψ i).is_faithful_pos_map)
(i : k)
(j l : s i) :
⇑(module.dual.pi.is_faithful_pos_map.basis hψ) ⟨i, (j, l)⟩ = ⇑matrix.include_block ((matrix.std_basis_matrix j l 1).mul (_.rpow (-(1 / 2))))
theorem
module.dual.pi.is_faithful_pos_map.include_block_left_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}
(x : matrix (s i) (s i) ℂ)
(y : Π (j : k), matrix (s j) (s j) ℂ) :
has_inner.inner (⇑matrix.include_block x) y = has_inner.inner x (y i)
theorem
module.dual.pi.is_faithful_pos_map.include_block_inner_same
{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}
{x y : matrix (s i) (s i) ℂ} :
theorem
module.dual.pi.is_faithful_pos_map.include_block_inner_same'
{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 j : k}
{x : matrix (s i) (s i) ℂ}
{y : matrix (s j) (s j) ℂ}
(h : i = j) :
has_inner.inner (⇑matrix.include_block x) (⇑matrix.include_block y) = has_inner.inner x (_.mpr y)
theorem
module.dual.pi.is_faithful_pos_map.include_block_inner_ne_same
{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 j : k}
{x : matrix (s i) (s i) ℂ}
{y : matrix (s j) (s j) ℂ}
(h : i ≠ j) :
@[protected]
theorem
module.dual.pi.is_faithful_pos_map.basis.apply_cast_eq_mpr
{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), (ψ i).is_faithful_pos_map)
{i j : k}
{a : s j × s j}
(h : i = j) :
@[protected]
theorem
module.dual.pi.is_faithful_pos_map.basis_is_orthonormal
{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] :
@[protected]
noncomputable
def
module.dual.pi.is_faithful_pos_map.orthonormal_basis
{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] :
Equations
- module.dual.pi.is_faithful_pos_map.orthonormal_basis = (module.dual.pi.is_faithful_pos_map.basis module.dual.pi.is_faithful_pos_map.orthonormal_basis._proof_5).to_orthonormal_basis module.dual.pi.is_faithful_pos_map.orthonormal_basis._proof_6
@[protected]
theorem
module.dual.pi.is_faithful_pos_map.orthonormal_basis_apply
{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]
{ijk : Σ (i : k), s i × s i} :
⇑module.dual.pi.is_faithful_pos_map.orthonormal_basis ijk = ⇑matrix.include_block ((matrix.std_basis_matrix ijk.snd.fst ijk.snd.snd 1).mul (_.rpow (-(1 / 2))))
@[protected]
theorem
module.dual.pi.is_faithful_pos_map.orthonormal_basis_apply'
{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}
{j l : s i} :
⇑module.dual.pi.is_faithful_pos_map.orthonormal_basis ⟨i, (j, l)⟩ = ⇑matrix.include_block ((matrix.std_basis_matrix j l 1).mul (_.rpow (-(1 / 2))))
@[protected]
theorem
module.dual.pi.is_faithful_pos_map.inner_coord
{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]
(ijk : Σ (i : k), s i × s i)
(y : Π (i : k), matrix (s i) (s i) ℂ) :
@[protected]
theorem
module.dual.pi.is_faithful_pos_map.basis_repr_apply
{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]
(x : Π (i : k), matrix (s i) (s i) ℂ)
(ijk : Σ (i : k), s i × s i) :
⇑(⇑((module.dual.pi.is_faithful_pos_map.basis _).repr) x) ijk = has_inner.inner (⇑(_.basis) ijk.snd) (x ijk.fst)
theorem
module.dual.pi.is_faithful_pos_map.matrix_block.is_self_adjoint
{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] :
noncomputable
def
module.dual.pi.is_faithful_pos_map.matrix_block_invertible
{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] :
Equations
theorem
module.dual.pi.is_faithful_pos_map.matrix_block_inv_mul_self
{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] :
theorem
module.dual.pi.is_faithful_pos_map.matrix_block_self_mul_inv
{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] :
noncomputable
def
module.dual.pi.is_faithful_pos_map.to_matrix
{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), (ψ i).is_faithful_pos_map) :
noncomputable
def
module.dual.pi.is_faithful_pos_map.is_block_diagonal_basis
{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), (ψ i).is_faithful_pos_map) :
@[simp]
theorem
module.dual.pi.is_faithful_pos_map.is_block_diagonal_basis_repr
{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), (ψ i).is_faithful_pos_map) :
theorem
module.dual.pi.is_faithful_pos_map.to_matrix_apply'
{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]
(f : (Π (i : k), matrix (s i) (s i) ℂ) →ₗ[ℂ] Π (i : k), matrix (s i) (s i) ℂ)
(r l : Σ (r : k), s r × s r) :
theorem
module.dual.pi.is_faithful_pos_map.star_alg_equiv_adjoint_eq
{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]
(f : Π (i : k), matrix (s i) (s i) ℂ ≃⋆ₐ[ℂ] matrix (s i) (s i) ℂ)
(x : Π (i : k), matrix (s i) (s i) ℂ) :
theorem
module.dual.pi.is_faithful_pos_map.star_alg_equiv_commute_iff
{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]
(f : Π (i : k), matrix (s i) (s i) ℂ ≃⋆ₐ[ℂ] matrix (s i) (s i) ℂ) :
commute (module.dual.pi.matrix_block ψ) (λ (i : k), ⇑(star_alg_equiv.pi.unitary f i)) ↔ ⇑(star_alg_equiv.pi f) (module.dual.pi.matrix_block ψ) = module.dual.pi.matrix_block ψ
theorem
module.dual.pi.is_faithful_pos_map.star_alg_equiv_is_isometry_tfae
{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), nontrivial (s i)]
(f : Π (i : k), matrix (s i) (s i) ℂ ≃⋆ₐ[ℂ] matrix (s i) (s i) ℂ) :
[⇑(star_alg_equiv.pi f) (module.dual.pi.matrix_block ψ) = module.dual.pi.matrix_block ψ, ⇑linear_map.adjoint (star_alg_equiv.pi f).to_alg_equiv.to_linear_map = (star_alg_equiv.pi f).symm.to_alg_equiv.to_linear_map, linear_map.comp (module.dual.pi ψ) (star_alg_equiv.pi f).to_alg_equiv.to_linear_map = module.dual.pi ψ, ∀ (x y : Π (i : k), matrix ((λ (i : k), s i) i) ((λ (i : k), s i) i) ℂ), has_inner.inner (⇑(star_alg_equiv.pi f) x) (⇑(star_alg_equiv.pi f) y) = has_inner.inner x y, ∀ (x : Π (i : k), matrix (s i) (s i) ℂ), ‖⇑(star_alg_equiv.pi f) x‖ = ‖x‖, commute (module.dual.pi.matrix_block ψ) (λ (i : k), ⇑(star_alg_equiv.pi.unitary f i))].tfae