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_hMul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [StarMul A] {φ : A →ₗ[R] R} (x : A) (y : A) (z : A) : φ (star (x * y) * z) = φ (star y * (star x * z))

A lemma that states the right multiplication property of a linear functional.

theorem linear_functional_left_hMul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [StarMul A] {φ : A →ₗ[R] R} (x : A) (y : A) (z : A) : φ (star x * (y * z)) = φ (star (star y * x) * z)

A lemma that states the left multiplication property of a linear functional.

noncomputable def Module.Dual.pi.matrixBlock {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)) (i : k) : Matrix (s i) (s i) ℂ

A function that returns the direct sum of matrices for each index of type 'i'.

Equations

• Module.Dual.pi.matrixBlock ψ = ∑ i : k, Matrix.includeBlock (ψ i).matrix

theorem inner_pi_eq_sum {k : Type u_3} [Fintype k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [∀ (i : k), (ψ i).IsFaithfulPosMap] (x : PiMat ℂ k s) (y : PiMat ℂ k s) : inner x y = ∑ i : k, 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 blockDiagonal'_includeBlock_trace' {R : Type u_2} {k : Type u_3} [CommSemiring R] [Fintype k] [DecidableEq k] {s : k → Type u_4} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (j : k) (x : Matrix (s j) (s j) R) : (Matrix.blockDiagonal' (Matrix.includeBlock x)).trace = x.trace

theorem Module.Dual.pi.matrixBlock_apply {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} {i : k} : Module.Dual.pi.matrixBlock ψ i = (ψ i).matrix

def inclPi {k : Type u_2} [DecidableEq k] {s : k → Type u_3} {i : k} (x : s i → ℂ) : (j : k) × s j → ℂ

Equations

• inclPi x j = if h : i = j.fst then x (⋯.mpr j.snd) else 0

def exclPi {k : Type u_2} {s : k → Type u_3} (x : (j : k) × s j → ℂ) (i : k) : s i → ℂ

Equations

• exclPi x i j = x ⟨i, j⟩

theorem Module.Dual.pi.apply'' {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (ψ : (i : k) → Matrix (s i) (s i) ℂ →ₗ[ℂ] ℂ) (x : PiMat ℂ k s) : (Module.Dual.pi ψ) x = (Matrix.blockDiagonal' (Module.Dual.pi.matrixBlock ψ) * Matrix.blockDiagonal' x).trace

theorem Module.Dual.pi.apply_eq_of {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)) (x : PiMat ℂ k s) (h : ∀ (a : PiMat ℂ k s), (Module.Dual.pi ψ) a = (Matrix.blockDiagonal' x * Matrix.blockDiagonal' a).trace) : x = Module.Dual.pi.matrixBlock ψ

theorem unitary.inj_hMul {A : Type u_2} [Monoid A] [StarMul A] (U : ↥(unitary A)) (x : A) (y : A) : x = y ↔ x * ↑U = y * ↑U

Section single_block

theorem Module.Dual.IsFaithfulPosMap.inner_eq {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [φ.IsFaithfulPosMap] (x : Matrix n n ℂ) (y : Matrix n n ℂ) : inner x y = φ (x.conjTranspose * y)

theorem Module.Dual.IsFaithfulPosMap.inner_eq' {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (x : Matrix n n ℂ) (y : Matrix n n ℂ) : inner x y = (φ.matrix * x.conjTranspose * y).trace

def Module.Dual.IsFaithfulPosMap.matrixIsPosDef {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) : φ.matrix.PosDef

Equations

• ⋯ = ⋯

theorem Module.Dual.IsFaithfulPosMap.hMul_right {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (x : Matrix n n ℂ) (y : Matrix n n ℂ) (z : Matrix n n ℂ) : φ (x.conjTranspose * (y * z)) = φ ((x * (φ.matrix * z.conjTranspose * φ.matrix⁻¹)).conjTranspose * y)

theorem Module.Dual.IsFaithfulPosMap.inner_left_hMul {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [φ.IsFaithfulPosMap] (x : Matrix n n ℂ) (y : Matrix n n ℂ) (z : Matrix n n ℂ) : inner (x * y) z = inner y (x.conjTranspose * z)

theorem Module.Dual.IsFaithfulPosMap.inner_right_hMul {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [φ.IsFaithfulPosMap] (x : Matrix n n ℂ) (y : Matrix n n ℂ) (z : Matrix n n ℂ) : inner x (y * z) = inner (y.conjTranspose * x) z

theorem Module.Dual.IsFaithfulPosMap.inner_left_conj {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (x : Matrix n n ℂ) (y : Matrix n n ℂ) (z : Matrix n n ℂ) : inner x (y * z) = inner (x * (φ.matrix * z.conjTranspose * φ.matrix⁻¹)) y

theorem Module.Dual.IsFaithfulPosMap.hMul_left {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (x : Matrix n n ℂ) (y : Matrix n n ℂ) (z : Matrix n n ℂ) : φ ((x * y).conjTranspose * z) = φ (x.conjTranspose * (z * (φ.matrix * y.conjTranspose * φ.matrix⁻¹)))

theorem Module.Dual.IsFaithfulPosMap.inner_right_conj {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (x : Matrix n n ℂ) (y : Matrix n n ℂ) (z : Matrix n n ℂ) : inner (x * y) z = inner x (z * (φ.matrix * y.conjTranspose * φ.matrix⁻¹))

theorem Module.Dual.IsFaithfulPosMap.adjoint_eq {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) : LinearMap.adjoint φ = Algebra.linearMap ℂ (Matrix n n ℂ)

theorem Module.Dual.IsFaithfulPosMap.starAlgEquiv_adjoint_eq {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (f : Matrix n n ℂ ≃⋆ₐ[ℂ] Matrix n n ℂ) (x : Matrix n n ℂ) : (LinearMap.adjoint f.toLinearMap) x = f.symm (x * φ.matrix) * φ.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.IsFaithfulPosMap.starAlgEquiv_unitary_commute_iff {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [φ.IsFaithfulPosMap] (f : Matrix n n ℂ ≃⋆ₐ[ℂ] Matrix n n ℂ) : Commute φ.matrix ↑f.of_matrix_unitary ↔ f φ.matrix = φ.matrix

theorem Module.Dual.IsFaithfulPosMap.starAlgEquiv_is_isometry_tFAE {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] (f : Matrix n n ℂ ≃⋆ₐ[ℂ] Matrix n n ℂ) : [f φ.matrix = φ.matrix, LinearMap.adjoint f.toLinearMap = f.symm.toLinearMap, φ ∘ₗ f.toLinearMap = φ, ∀ (x y : Matrix n n ℂ), inner (f x) (f y) = inner x y, ∀ (x : Matrix n n ℂ), ‖f x‖ = ‖x‖, Commute φ.matrix ↑f.of_matrix_unitary].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‖,
• φ.matrix commutes with f.unitary.

noncomputable def Module.Dual.IsFaithfulPosMap.basis {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) : Basis (n × n) ℂ (Matrix n n ℂ)

Equations

• hφ.basis = Basis.mk ⋯ ⋯

theorem Module.Dual.IsFaithfulPosMap.basis_apply {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (ij : n × n) : hφ.basis ij = Matrix.stdBasisMatrix ij.1 ij.2 1 * ⋯.rpow (-(1 / 2))

noncomputable def Module.Dual.IsFaithfulPosMap.toMatrixLinEquiv {n : Type u_2} {n₂ : Type u_3} [DecidableEq n] [DecidableEq n₂] [Fintype n] [Fintype n₂] {φ : Module.Dual ℂ (Matrix n n ℂ)} {ψ : Module.Dual ℂ (Matrix n₂ n₂ ℂ)} (hφ : φ.IsFaithfulPosMap) (hψ : ψ.IsFaithfulPosMap) : (Matrix n n ℂ →ₗ[ℂ] Matrix n₂ n₂ ℂ) ≃ₗ[ℂ] Matrix (n₂ × n₂) (n × n) ℂ

Equations

• hφ.toMatrixLinEquiv hψ = LinearMap.toMatrix hφ.basis hψ.basis

noncomputable def Module.Dual.IsFaithfulPosMap.toMatrix {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) : (Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) ≃ₐ[ℂ] Matrix (n × n) (n × n) ℂ

Equations

• hφ.toMatrix = LinearMap.toMatrixAlgEquiv hφ.basis

theorem Module.Dual.IsFaithfulPosMap.basis_is_orthonormal {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) : Orthonormal ℂ ⇑hφ.basis

noncomputable def Module.Dual.IsFaithfulPosMap.orthonormalBasis {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) : OrthonormalBasis (n × n) ℂ (Matrix n n ℂ)

Equations

• hφ.orthonormalBasis = hφ.basis.toOrthonormalBasis ⋯

theorem Module.Dual.IsFaithfulPosMap.orthonormalBasis_apply {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (ij : n × n) : hφ.orthonormalBasis ij = Matrix.stdBasisMatrix ij.1 ij.2 1 * ⋯.rpow (-(1 / 2))

theorem Module.Dual.IsFaithfulPosMap.inner_coord {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (ij : n × n) (y : Matrix n n ℂ) : inner (hφ.orthonormalBasis ij) y = (y * ⋯.rpow (1 / 2)) ij.1 ij.2

theorem Module.Dual.IsFaithfulPosMap.basis_repr_apply {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (x : Matrix n n ℂ) (ij : n × n) : (hφ.basis.repr x) ij = inner (hφ.basis ij) x

theorem Module.Dual.IsFaithfulPosMap.toMatrixLinEquiv_symm_apply {n : Type u_2} {n₂ : Type u_3} [DecidableEq n] [DecidableEq n₂] [Fintype n] [Fintype n₂] {φ : Module.Dual ℂ (Matrix n n ℂ)} {ψ : Module.Dual ℂ (Matrix n₂ n₂ ℂ)} (hφ : φ.IsFaithfulPosMap) (hψ : ψ.IsFaithfulPosMap) (x : Matrix (n₂ × n₂) (n × n) ℂ) : (hφ.toMatrixLinEquiv hψ).symm x = ↑(∑ i : n₂, ∑ j : n₂, ∑ k : n, ∑ l : n, x (i, j) (k, l) • ((rankOne ℂ) (hψ.basis (i, j))) (hφ.basis (k, l)))

@[simp]

theorem AlgEquiv.toLinearEquiv_coe {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [Semiring M₁] [Algebra R M₁] [Semiring M₂] [Algebra R M₂] (φ : M₁ ≃ₐ[R] M₂) : φ.toLinearEquiv = ↑φ

theorem Module.Dual.IsFaithfulPosMap.toMatrix_symm_apply {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (x : Matrix (n × n) (n × n) ℂ) : hφ.toMatrix.symm x = ↑(∑ i : n, ∑ j : n, ∑ k : n, ∑ l : n, x (i, j) (k, l) • ((rankOne ℂ) (hφ.basis (i, j))) (hφ.basis (k, l)))

theorem Module.Dual.eq_rankOne_of_faithful_pos_map {n : Type u_2} {n₂ : Type u_3} [DecidableEq n] [DecidableEq n₂] [Fintype n] [Fintype n₂] {φ : Module.Dual ℂ (Matrix n n ℂ)} {ψ : Module.Dual ℂ (Matrix n₂ n₂ ℂ)} (hφ : φ.IsFaithfulPosMap) (hψ : ψ.IsFaithfulPosMap) (x : Matrix n n ℂ →ₗ[ℂ] Matrix n₂ n₂ ℂ) : x = ↑(∑ i : n₂, ∑ j : n₂, ∑ k : n, ∑ l : n, (hφ.toMatrixLinEquiv hψ) x (i, j) (k, l) • ((rankOne ℂ) (hψ.basis (i, j))) (hφ.basis (k, l)))

Section direct_sum

theorem LinearMap.sum_single_comp_proj {R : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Semiring R] {φ : ι → Type u_4} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] : ∑ i : ι, LinearMap.single R φ i ∘ₗ LinearMap.proj i = LinearMap.id

theorem LinearMap.lrsum_eq_single_proj_lrcomp {k : Type u_3} {k₂ : Type u_4} [Fintype k] [Fintype k₂] [DecidableEq k] [DecidableEq k₂] {s : k → Type u_2} {s₂ : k₂ → Type u_1} (f : PiMat ℂ k s →ₗ[ℂ] PiMat ℂ k₂ s₂) : ∑ r : k₂, ∑ p : k, LinearMap.single ℂ (fun (r : k₂) => Mat ℂ (s₂ r)) r ∘ₗ LinearMap.proj r ∘ₗ f ∘ₗ LinearMap.single ℂ (fun (j : k) => Mat ℂ (s j)) p ∘ₗ LinearMap.proj p = f

theorem Module.Dual.pi.IsFaithfulPosMap.inner_eq {k : Type u_3} [Fintype k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [∀ (i : k), (ψ i).IsFaithfulPosMap] (x : PiMat ℂ k s) (y : PiMat ℂ k s) : inner x y = (Module.Dual.pi ψ) (star x * y)

theorem Module.Dual.pi.IsFaithfulPosMap.inner_eq' {k : Type u_3} [Fintype k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [∀ (i : k), (ψ i).IsFaithfulPosMap] (x : PiMat ℂ k s) (y : PiMat ℂ k s) : inner x y = ∑ i : k, ((ψ i).matrix * Matrix.conjTranspose (x i) * y i).trace

theorem Module.Dual.pi.IsFaithfulPosMap.inner_left_hMul {k : Type u_3} [Fintype k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [∀ (i : k), (ψ i).IsFaithfulPosMap] (x : PiMat ℂ k s) (y : PiMat ℂ k s) (z : PiMat ℂ k s) : inner (x * y) z = inner y (star x * z)

theorem Module.Dual.pi.IsFaithfulPosMap.hMul_right {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (x : PiMat ℂ k s) (y : PiMat ℂ k s) (z : PiMat ℂ k s) : (Module.Dual.pi ψ) (star x * (y * z)) = (Module.Dual.pi ψ) (star (x * (Module.Dual.pi.matrixBlock ψ * star z * (Module.Dual.pi.matrixBlock ψ)⁻¹)) * y)

theorem Module.Dual.pi.IsFaithfulPosMap.inner_left_conj {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (x : PiMat ℂ k s) (y : PiMat ℂ k s) (z : PiMat ℂ k s) : inner x (y * z) = inner (x * (Module.Dual.pi.matrixBlock ψ * star z * (Module.Dual.pi.matrixBlock ψ)⁻¹)) y

theorem Module.Dual.pi.IsFaithfulPosMap.inner_right_hMul {k : Type u_3} [Fintype k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [∀ (i : k), (ψ i).IsFaithfulPosMap] (x : PiMat ℂ k s) (y : PiMat ℂ k s) (z : PiMat ℂ k s) : inner x (y * z) = inner (star y * x) z

theorem Module.Dual.pi.IsFaithfulPosMap.adjoint_eq {k : Type u_3} [Fintype k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] : LinearMap.adjoint (Module.Dual.pi ψ) = Algebra.linearMap ℂ (PiMat ℂ k s)

noncomputable def Module.Dual.pi.IsFaithfulPosMap.basis {k : Type u_2} [Fintype k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : Basis ((i : k) × s i × s i) ℂ (PiMat ℂ k s)

Equations

• Module.Dual.pi.IsFaithfulPosMap.basis hψ = Pi.basis fun (i : k) => ⋯.basis

theorem Module.Dual.pi.IsFaithfulPosMap.basis_apply {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (ijk : (i : k) × s i × s i) : (Module.Dual.pi.IsFaithfulPosMap.basis hψ) ijk = Matrix.includeBlock (Matrix.stdBasisMatrix ijk.snd.1 ijk.snd.2 1 * ⋯.rpow (-(1 / 2)))

theorem Module.Dual.pi.IsFaithfulPosMap.basis_apply' {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (i : k) (j : s i) (l : s i) : (Module.Dual.pi.IsFaithfulPosMap.basis hψ) ⟨i, (j, l)⟩ = Matrix.includeBlock (Matrix.stdBasisMatrix j l 1 * ⋯.rpow (-(1 / 2)))

theorem Module.Dual.pi.IsFaithfulPosMap.includeBlock_left_inner {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) {i : k} (x : Matrix (s i) (s i) ℂ) (y : PiMat ℂ k s) : inner (Matrix.includeBlock x) y = inner x (y i)

theorem Module.Dual.pi.IsFaithfulPosMap.includeBlock_inner_same {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] {i : k} {x : Matrix (s i) (s i) ℂ} {y : Matrix (s i) (s i) ℂ} : inner (Matrix.includeBlock x) (Matrix.includeBlock y) = inner x y

theorem Module.Dual.pi.IsFaithfulPosMap.includeBlock_inner_same' {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] {i : k} {j : k} {x : Matrix (s i) (s i) ℂ} {y : Matrix (s j) (s j) ℂ} (h : i = j) : inner (Matrix.includeBlock x) (Matrix.includeBlock y) = inner x (⋯.mpr y)

theorem Module.Dual.pi.IsFaithfulPosMap.includeBlock_inner_block_left {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] {j : k} {x : PiMat ℂ k s} {y : Matrix (s j) (s j) ℂ} {i : k} : inner (Matrix.includeBlock (x i)) (Matrix.includeBlock y) = if i = j then inner (x j) y else 0

theorem Module.Dual.pi.IsFaithfulPosMap.includeBlock_inner_ne_same {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] {i : k} {j : k} {x : Matrix (s i) (s i) ℂ} {y : Matrix (s j) (s j) ℂ} (h : i ≠ j) : inner (Matrix.includeBlock x) (Matrix.includeBlock y) = 0

theorem Module.Dual.pi.IsFaithfulPosMap.basis.apply_cast_eq_mpr {k : Type u_3} {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) {i : k} {j : k} {a : s j × s j} (h : i = j) : ⋯.basis (⋯.mpr a) = ⋯.mpr (⋯.basis a)

theorem Module.Dual.pi.IsFaithfulPosMap.basis_is_orthonormal {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] : Orthonormal ℂ ⇑(Module.Dual.pi.IsFaithfulPosMap.basis hψ)

noncomputable def Module.Dual.pi.IsFaithfulPosMap.orthonormalBasis {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : OrthonormalBasis ((i : k) × s i × s i) ℂ (PiMat ℂ k s)

Equations

• Module.Dual.pi.IsFaithfulPosMap.orthonormalBasis hψ = (Module.Dual.pi.IsFaithfulPosMap.basis hψ).toOrthonormalBasis ⋯

theorem Module.Dual.pi.IsFaithfulPosMap.orthonormalBasis_apply {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) {ijk : (i : k) × s i × s i} : (Module.Dual.pi.IsFaithfulPosMap.orthonormalBasis hψ) ijk = Matrix.includeBlock (Matrix.stdBasisMatrix ijk.snd.1 ijk.snd.2 1 * ⋯.rpow (-(1 / 2)))

theorem Module.Dual.pi.IsFaithfulPosMap.orthonormalBasis_apply' {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) {i : k} {j : s i} {l : s i} : (Module.Dual.pi.IsFaithfulPosMap.orthonormalBasis hψ) ⟨i, (j, l)⟩ = Matrix.includeBlock (Matrix.stdBasisMatrix j l 1 * ⋯.rpow (-(1 / 2)))

theorem Module.Dual.pi.IsFaithfulPosMap.inner_coord {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (ijk : (i : k) × s i × s i) (y : PiMat ℂ k s) : inner ((Module.Dual.pi.IsFaithfulPosMap.basis hψ) ijk) y = (y ijk.fst * ⋯.rpow (1 / 2)) ijk.snd.1 ijk.snd.2

theorem Module.Dual.pi.IsFaithfulPosMap.basis_repr_apply {k : Type u_3} [Fintype k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (x : PiMat ℂ k s) (ijk : (i : k) × s i × s i) : ((Module.Dual.pi.IsFaithfulPosMap.basis hψ).repr x) ijk = inner (⋯.basis ijk.snd) (x ijk.fst)

theorem Module.Dual.pi.IsFaithfulPosMap.MatrixBlock.isSelfAdjoint {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : IsSelfAdjoint (Module.Dual.pi.matrixBlock ψ)

noncomputable def Module.Dual.pi.IsFaithfulPosMap.matrixBlockInvertible {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : Invertible (Module.Dual.pi.matrixBlock ψ)

Equations

• Module.Dual.pi.IsFaithfulPosMap.matrixBlockInvertible hψ = { invOf := (Module.Dual.pi.matrixBlock ψ)⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

theorem Module.Dual.pi.IsFaithfulPosMap.matrixBlock_inv_hMul_self {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] : (Module.Dual.pi.matrixBlock ψ)⁻¹ * Module.Dual.pi.matrixBlock ψ = 1

theorem Module.Dual.pi.IsFaithfulPosMap.matrixBlock_self_hMul_inv {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : Module.Dual.pi.matrixBlock ψ * (Module.Dual.pi.matrixBlock ψ)⁻¹ = 1

noncomputable def Module.Dual.pi.IsFaithfulPosMap.toMatrixLinEquiv {k : Type u_2} {k₂ : Type u_3} [Fintype k] [Fintype k₂] [DecidableEq k] {s : k → Type u_4} {s₂ : k₂ → Type u_1} [(i : k) → Fintype (s i)] [(i : k₂) → Fintype (s₂ i)] [(i : k) → DecidableEq (s i)] [(i : k₂) → DecidableEq (s₂ i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} {φ : (i : k₂) → Module.Dual ℂ (Matrix (s₂ i) (s₂ i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (hφ : ∀ (i : k₂), (φ i).IsFaithfulPosMap) : (PiMat ℂ k s →ₗ[ℂ] PiMat ℂ k₂ s₂) ≃ₗ[ℂ] Matrix ((i : k₂) × s₂ i × s₂ i) ((i : k) × s i × s i) ℂ

Equations

• Module.Dual.pi.IsFaithfulPosMap.toMatrixLinEquiv hψ hφ = LinearMap.toMatrix (Module.Dual.pi.IsFaithfulPosMap.basis hψ) (Module.Dual.pi.IsFaithfulPosMap.basis hφ)

noncomputable def Module.Dual.pi.IsFaithfulPosMap.toMatrix {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : (PiMat ℂ k s →ₗ[ℂ] PiMat ℂ k s) ≃ₐ[ℂ] Matrix ((i : k) × s i × s i) ((i : k) × s i × s i) ℂ

Equations

• Module.Dual.pi.IsFaithfulPosMap.toMatrix hψ = LinearMap.toMatrixAlgEquiv (Module.Dual.pi.IsFaithfulPosMap.basis hψ)

theorem Module.Dual.pi.IsFaithfulPosMap.toMatrixLinEquiv_eq_toMatrix {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : Module.Dual.pi.IsFaithfulPosMap.toMatrixLinEquiv hψ hψ = (Module.Dual.pi.IsFaithfulPosMap.toMatrix hψ).toLinearEquiv

noncomputable def Module.Dual.pi.IsFaithfulPosMap.isBlockDiagonalBasis {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : Basis ((i : k) × s i × s i) ℂ { x : Matrix ((i : k) × s i) ((i : k) × s i) ℂ // x.IsBlockDiagonal }

Equations

• Module.Dual.pi.IsFaithfulPosMap.isBlockDiagonalBasis hψ = { repr := Matrix.isBlockDiagonalPiAlgEquiv.toLinearEquiv.trans (Module.Dual.pi.IsFaithfulPosMap.basis hψ).repr }

@[simp]

theorem Module.Dual.pi.IsFaithfulPosMap.isBlockDiagonalBasis_repr {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : (Module.Dual.pi.IsFaithfulPosMap.isBlockDiagonalBasis hψ).repr = Matrix.isBlockDiagonalPiAlgEquiv.toLinearEquiv.trans (Module.Dual.pi.IsFaithfulPosMap.basis hψ).repr

theorem Module.Dual.pi.IsFaithfulPosMap.toMatrixLinEquiv_apply' {k : Type u_3} {k₂ : Type u_4} [Fintype k] [Fintype k₂] [DecidableEq k] {s : k → Type u_2} {s₂ : k₂ → Type u_1} [(i : k) → Fintype (s i)] [(i : k₂) → Fintype (s₂ i)] [(i : k) → DecidableEq (s i)] [(i : k₂) → DecidableEq (s₂ i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} {φ : (i : k₂) → Module.Dual ℂ (Matrix (s₂ i) (s₂ i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] [hφ : ∀ (i : k₂), (φ i).IsFaithfulPosMap] (f : PiMat ℂ k s →ₗ[ℂ] PiMat ℂ k₂ s₂) (r : (r : k₂) × s₂ r × s₂ r) (l : (r : k) × s r × s r) : (Module.Dual.pi.IsFaithfulPosMap.toMatrixLinEquiv hψ hφ) f r l = (f (Matrix.includeBlock (⋯.basis l.snd)) r.fst * ⋯.rpow (1 / 2)) r.snd.1 r.snd.2

theorem Module.Dual.pi.IsFaithfulPosMap.toMatrix_apply' {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (f : PiMat ℂ k s →ₗ[ℂ] PiMat ℂ k s) (r : (r : k) × s r × s r) (l : (r : k) × s r × s r) : (Module.Dual.pi.IsFaithfulPosMap.toMatrix ⋯) f r l = (f (Matrix.includeBlock (⋯.basis l.snd)) r.fst * ⋯.rpow (1 / 2)) r.snd.1 r.snd.2

theorem inner_stdBasisMatrix_left {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (i : n) (j : n) (x : Matrix n n ℂ) : inner (Matrix.stdBasisMatrix i j 1) x = (x * φ.matrix) i j

theorem inner_stdBasisMatrix_stdBasisMatrix {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (i : n) (j : n) (k : n) (l : n) : inner (Matrix.stdBasisMatrix i j 1) (Matrix.stdBasisMatrix k l 1) = if i = k then φ.matrix l j else 0

theorem LinearMap.mul'_adjoint {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : Matrix n n ℂ) : (LinearMap.adjoint (LinearMap.mul' ℂ (Matrix n n ℂ))) x = ∑ i : n, ∑ j : n, ∑ k : n, ∑ l : n, (x i l * φ.matrix⁻¹ k j) • Matrix.stdBasisMatrix i j 1 ⊗ₜ[ℂ] Matrix.stdBasisMatrix k l 1

theorem Matrix.linearMap_ext_iff_inner_map {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {x : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} {y : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} : x = y ↔ ∀ (u v : Matrix n n ℂ), inner (x u) v = inner (y u) v

theorem Matrix.linearMap_ext_iff_map_inner {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {x : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} {y : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} : x = y ↔ ∀ (u v : Matrix n n ℂ), inner v (x u) = inner v (y u)

theorem Matrix.inner_conj_Q {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (a : Matrix n n ℂ) (x : Matrix n n ℂ) : inner x (φ.matrix * a * φ.matrix⁻¹) = inner (x * a.conjTranspose) 1

theorem Matrix.inner_star_right {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (b : Matrix n n ℂ) (y : Matrix n n ℂ) : inner b y = inner 1 (b.conjTranspose * y)

theorem Matrix.inner_star_left {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (a : Matrix n n ℂ) (x : Matrix n n ℂ) : inner a x = inner (x.conjTranspose * a) 1

theorem one_inner {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (a : Matrix n n ℂ) : inner 1 a = (φ.matrix * a).trace

theorem Module.Dual.IsFaithfulPosMap.map_star {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (x : Matrix n n ℂ) : φ (star x) = star (φ x)

theorem Nontracial.unit_adjoint_eq {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : LinearMap.adjoint (Algebra.linearMap ℂ (Matrix n n ℂ)) = φ

theorem Qam.Nontracial.mul_comp_mul_adjoint {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : LinearMap.mul' ℂ (Matrix n n ℂ) ∘ₗ LinearMap.adjoint (LinearMap.mul' ℂ (Matrix n n ℂ)) = φ.matrix⁻¹.trace • 1

theorem includeBlock_adjoint {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] {i : k} (x : PiMat ℂ k s) : (LinearMap.adjoint Matrix.includeBlock) x = x i

theorem pi_inner_stdBasisMatrix_left {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (i : k) (j : s i) (l : s i) (x : PiMat ℂ k s) : inner (Matrix.stdBasisMatrix ⟨i, j⟩ ⟨i, l⟩ 1).blockDiag' x = (x i * (ψ i).matrix) j l

theorem eq_mpr_stdBasisMatrix {k : Type u_2} {s : k → Type u_3} [(i : k) → DecidableEq (s i)] {i : k} {j : k} {b : s j} {c : s j} (h₁ : i = j) : ⋯.mpr (Matrix.stdBasisMatrix b c 1) = Matrix.stdBasisMatrix (⋯.mpr b) (⋯.mpr c) 1

theorem pi_inner_stdBasisMatrix_stdBasisMatrix {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] {i : k} {j : k} (a : s i) (b : s i) (c : s j) (d : s j) : inner (Matrix.stdBasisMatrix ⟨i, a⟩ ⟨i, b⟩ 1).blockDiag' (Matrix.stdBasisMatrix ⟨j, c⟩ ⟨j, d⟩ 1).blockDiag' = if h : i = j then if a = ⋯.mpr c then (ψ i).matrix (⋯.mpr d) b else 0 else 0

theorem pi_inner_stdBasisMatrix_stdBasisMatrix_same {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] {i : k} (a : s i) (b : s i) (c : s i) (d : s i) : inner (Matrix.stdBasisMatrix ⟨i, a⟩ ⟨i, b⟩ 1).blockDiag' (Matrix.stdBasisMatrix ⟨i, c⟩ ⟨i, d⟩ 1).blockDiag' = if a = c then (ψ i).matrix d b else 0

theorem pi_inner_stdBasisMatrix_stdBasisMatrix_ne {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] {i : k} {j : k} (h : i ≠ j) (a : s i) (b : s i) (c : s j) (d : s j) : inner (Matrix.stdBasisMatrix ⟨i, a⟩ ⟨i, b⟩ 1).blockDiag' (Matrix.stdBasisMatrix ⟨j, c⟩ ⟨j, d⟩ 1).blockDiag' = 0

theorem LinearMap.pi_mul'_adjoint_single_block {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] {i : k} (x : Matrix (s i) (s i) ℂ) : (LinearMap.adjoint (LinearMap.mul' ℂ (PiMat ℂ k s))) (Matrix.includeBlock x) = (TensorProduct.map Matrix.includeBlock Matrix.includeBlock) ((LinearMap.adjoint (LinearMap.mul' ℂ (Matrix (s i) (s i) ℂ))) x)

theorem LinearMap.pi_mul'_adjoint {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (x : PiMat ℂ k s) : (LinearMap.adjoint (LinearMap.mul' ℂ (PiMat ℂ k s))) x = ∑ r : k, ∑ a : s r, ∑ b : s r, ∑ c : s r, ∑ d : s r, (x r a d * (Module.Dual.pi.matrixBlock ψ r)⁻¹ c b) • (Matrix.stdBasisMatrix ⟨r, a⟩ ⟨r, b⟩ 1).blockDiag' ⊗ₜ[ℂ] (Matrix.stdBasisMatrix ⟨r, c⟩ ⟨r, d⟩ 1).blockDiag'

theorem LinearMap.pi_mul'_apply_includeBlock {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {i : k} (x : TensorProduct ℂ (Matrix (s i) (s i) ℂ) (Matrix (s i) (s i) ℂ)) : (LinearMap.mul' ℂ (PiMat ℂ k s)) ((TensorProduct.map Matrix.includeBlock Matrix.includeBlock) x) = Matrix.includeBlock ((LinearMap.mul' ℂ (Matrix (s i) (s i) ℂ)) x)

theorem LinearMap.pi_mul'_comp_mul'_adjoint {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (x : PiMat ℂ k s) : (LinearMap.mul' ℂ (PiMat ℂ k s)) ((LinearMap.adjoint (LinearMap.mul' ℂ (PiMat ℂ k s))) x) = ∑ i : k, (ψ i).matrix⁻¹.trace • Matrix.includeBlock (x i)

theorem Matrix.smul_inj_mul_one {n : Type u_2} [Fintype n] [DecidableEq n] [Nonempty n] (x : ℂ) (y : ℂ) : x • 1 = y • 1 ↔ x = y

theorem LinearMap.pi_mul'_comp_mul'_adjoint_eq_smul_id_iff {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] [∀ (i : k), Nontrivial (s i)] (α : ℂ) : LinearMap.mul' ℂ (PiMat ℂ k s) ∘ₗ LinearMap.adjoint (LinearMap.mul' ℂ (PiMat ℂ k s)) = α • 1 ↔ ∀ (i : k), (ψ i).matrix⁻¹.trace = α