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.

def «termWithMatrixInner[_]_» : Lean.ParserDescr

Elaborate a term using the inner product induced by a matrix functional.

Equations

• One or more equations did not get rendered due to their size.

def «termWithPiInner[_]_» : Lean.ParserDescr

Elaborate a term using the inner product induced by a pi-family of functionals.

Equations

• One or more equations did not get rendered due to their size.

def tacticMat_inner_instances_ : Lean.ParserDescr

Register the inner-product instances induced by a matrix functional φ.

Equations

• One or more equations did not get rendered due to their size.

def tacticPi_inner_instances_ : Lean.ParserDescr

Register the inner-product instances induced by a pi-family of functionals ψ.

Equations

• One or more equations did not get rendered due to their size.

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 y 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 y 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) → 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) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [∀ (i : k), (ψ i).IsFaithfulPosMap] (x 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)] (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) → Dual ℂ (Matrix (s i) (s i) ℂ)} {i : k} : 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 → ℂ

Include a component vector into a dependent sigma-indexed vector.

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 → ℂ

Restrict a dependent sigma-indexed vector to one component.

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) : (pi ψ) x = (Matrix.blockDiagonal' (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) → Dual ℂ (Matrix (s i) (s i) ℂ)) (x : PiMat ℂ k s) (h : ∀ (a : PiMat ℂ k s), (pi ψ) a = (Matrix.blockDiagonal' x * Matrix.blockDiagonal' a).trace) : x = matrixBlock ψ

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

Section single_block

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

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

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

The density matrix of a faithful positive functional is positive definite.

noncomputable def sig {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (z : ℝ) : Matrix n n ℂ ≃ₐ[ℂ] Matrix n n ℂ

Modular automorphism associated to a faithful positive functional on matrices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem sig_apply {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (z : ℝ) (a : Matrix n n ℂ) : (sig hφ z) a = ⋯.rpow (-z) * a * ⋯.rpow z

@[simp]

theorem sig_symm_apply {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (z : ℝ) (a : Matrix n n ℂ) : (sig hφ z).symm a = ⋯.rpow z * a * ⋯.rpow (-z)

@[reducible]

noncomputable def Module.Dual.IsFaithfulPosMap.sig {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (z : ℝ) : Matrix n n ℂ ≃ₐ[ℂ] Matrix n n ℂ

The modular automorphism associated to a faithful positive matrix functional.

Equations

• hφ.sig z = sig hφ z

theorem Module.Dual.IsFaithfulPosMap.sig_apply {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (z : ℝ) (a : Matrix n n ℂ) : (hφ.sig z) a = ⋯.rpow (-z) * a * ⋯.rpow z

theorem Module.Dual.IsFaithfulPosMap.sig_symm_apply {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (z : ℝ) (a : Matrix n n ℂ) : (hφ.sig z).symm a = ⋯.rpow z * a * ⋯.rpow (-z)

theorem Module.Dual.IsFaithfulPosMap.sig_symm_eq {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (z : ℝ) : (hφ.sig z).symm = hφ.sig (-z)

theorem Module.Dual.IsFaithfulPosMap.sig_apply_sig {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (t r : ℝ) (a : Matrix n n ℂ) : (hφ.sig t) ((hφ.sig r) a) = (hφ.sig (t + r)) a

theorem Module.Dual.IsFaithfulPosMap.sig_conjTranspose {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (r : ℝ) (a : Matrix n n ℂ) : ((hφ.sig r) a).conjTranspose = (hφ.sig (-r)) a.conjTranspose

theorem Module.Dual.IsFaithfulPosMap.sig_adjoint {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {t : ℝ} : LinearMap.adjoint (hφ.sig t).toLinearMap = (hφ.sig t).toLinearMap

theorem Module.Dual.IsFaithfulPosMap.hMul_right {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (x y 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} [Fintype n] {φ : Dual ℂ (Matrix n n ℂ)} [φ.IsFaithfulPosMap] (x y z : Matrix n n ℂ) : inner ℂ (x * y) z = inner ℂ y (x.conjTranspose * z)

theorem Module.Dual.IsFaithfulPosMap.inner_right_hMul {n : Type u_2} [Fintype n] {φ : Dual ℂ (Matrix n n ℂ)} [φ.IsFaithfulPosMap] (x y 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] {φ : Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (x y 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] {φ : Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (x y 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] {φ : Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (x y 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] {φ : 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] {φ : 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] {φ : Dual ℂ (Matrix n n ℂ)} [φ.IsFaithfulPosMap] (f : Matrix n n ℂ ≃⋆ₐ[ℂ] Matrix n n ℂ) : Commute φ.matrix ↑f.ofMatrixUnitary ↔ f φ.matrix = φ.matrix

theorem Module.Dual.IsFaithfulPosMap.starAlgEquiv_is_isometry_tFAE {n : Type u_2} [DecidableEq n] [Fintype n] {φ : 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.ofMatrixUnitary].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] {φ : Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) : Basis (n × n) ℂ (Matrix n n ℂ)

The matrix-unit basis normalized by the square root of the density matrix.

Equations

• hφ.basis = Module.Basis.mk ⋯ ⋯

theorem Module.Dual.IsFaithfulPosMap.basis_apply {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (ij : n × n) : hφ.basis ij = Matrix.single 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₂] {φ : Dual ℂ (Matrix n n ℂ)} {ψ : Dual ℂ (Matrix n₂ n₂ ℂ)} (hφ : φ.IsFaithfulPosMap) (hψ : ψ.IsFaithfulPosMap) : (Matrix n n ℂ →ₗ[ℂ] Matrix n₂ n₂ ℂ) ≃ₗ[ℂ] Matrix (n₂ × n₂) (n × n) ℂ

Matrix representation of linear maps between two faithful matrix inner products.

Equations

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

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

Matrix representation of endomorphisms for a faithful matrix inner product.

Equations

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

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

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

The normalized matrix basis as an orthonormal basis.

Equations

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

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

theorem Module.Dual.IsFaithfulPosMap.inner_coord {n : Type u_2} [DecidableEq n] [Fintype n] {φ : 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.inner_coord' {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (ij : n × n) (y : Matrix n n ℂ) : inner ℂ (hφ.basis 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] {φ : 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₂] {φ : Dual ℂ (Matrix n n ℂ)} {ψ : 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)))

theorem Module.Dual.IsFaithfulPosMap.toMatrix_symm_apply {n : Type u_2} [DecidableEq n] [Fintype n] {φ : 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₂] {φ : Dual ℂ (Matrix n n ℂ)} {ψ : 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 : ι, single R φ i ∘ₗ proj i = 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, single ℂ (fun (r : k₂) => Mat ℂ (s₂ r)) r ∘ₗ proj r ∘ₗ f ∘ₗ single ℂ (fun (j : k) => Mat ℂ (s j)) p ∘ₗ 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) → Dual ℂ (Matrix (s i) (s i) ℂ)} [∀ (i : k), (ψ i).IsFaithfulPosMap] (x y : PiMat ℂ k s) : inner ℂ x y = (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) → Dual ℂ (Matrix (s i) (s i) ℂ)} [∀ (i : k), (ψ i).IsFaithfulPosMap] (x 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) → Dual ℂ (Matrix (s i) (s i) ℂ)} [∀ (i : k), (ψ i).IsFaithfulPosMap] (x y 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) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (x y z : PiMat ℂ k s) : (pi ψ) (star x * (y * z)) = (pi ψ) (star (x * (matrixBlock ψ * star z * (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) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (x y z : PiMat ℂ k s) : inner ℂ x (y * z) = inner ℂ (x * (matrixBlock ψ * star z * (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) → Dual ℂ (Matrix (s i) (s i) ℂ)} [∀ (i : k), (ψ i).IsFaithfulPosMap] (x y 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) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] : LinearMap.adjoint (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) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : Basis ((i : k) × s i × s i) ℂ (PiMat ℂ k s)

The dependent pi basis obtained from the normalized bases of each block.

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) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (ijk : (i : k) × s i × s i) : (IsFaithfulPosMap.basis hψ) ijk = Matrix.includeBlock (Matrix.single 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) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (i : k) (j l : s i) : (IsFaithfulPosMap.basis hψ) ⟨i, (j, l)⟩ = Matrix.includeBlock (Matrix.single 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) → 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) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] {i : k} {x 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) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] {i 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) → 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) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] {i 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) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) {i 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] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] : Orthonormal ℂ ⇑(IsFaithfulPosMap.basis hψ)

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

The dependent pi basis as an orthonormal basis.

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) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) {ijk : (i : k) × s i × s i} : (IsFaithfulPosMap.orthonormalBasis hψ) ijk = Matrix.includeBlock (Matrix.single 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) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) {i : k} {j l : s i} : (IsFaithfulPosMap.orthonormalBasis hψ) ⟨i, (j, l)⟩ = Matrix.includeBlock (Matrix.single j l 1 * ⋯.rpow (-(1 / 2)))

theorem Module.Dual.pi.IsFaithfulPosMap.inner_coord {k : Type u_3} [Fintype k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (ijk : (i : k) × s i × s i) (y : PiMat ℂ k s) : inner ℂ ((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) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (x : PiMat ℂ k s) (ijk : (i : k) × s i × s i) : ((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) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : IsSelfAdjoint (matrixBlock ψ)

@[reducible]

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) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : Invertible (matrixBlock ψ)

Invertibility of the block diagonal density matrix.

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) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] : (matrixBlock ψ)⁻¹ * 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) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : matrixBlock ψ * (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) → Dual ℂ (Matrix (s i) (s i) ℂ)} {φ : (i : k₂) → 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) ℂ

Matrix representation of maps between two faithful pi inner products.

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) → 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) ℂ

Matrix representation of endomorphisms for a faithful pi inner product.

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) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : toMatrixLinEquiv hψ hψ = ↑(toMatrix hψ)

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) → 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 }

Basis for block diagonal matrices induced by the faithful pi basis.

Equations

• Module.Dual.pi.IsFaithfulPosMap.isBlockDiagonalBasis hψ = { repr := (↑Matrix.isBlockDiagonalPiAlgEquiv).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) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : (isBlockDiagonalBasis hψ).repr = (↑Matrix.isBlockDiagonalPiAlgEquiv).trans (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) → Dual ℂ (Matrix (s i) (s i) ℂ)} {φ : (i : k₂) → 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) : (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) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (f : PiMat ℂ k s →ₗ[ℂ] PiMat ℂ k s) (r l : (r : k) × s r × s r) : (toMatrix ⋯) f r l = (f (Matrix.includeBlock (⋯.basis l.snd)) r.fst * ⋯.rpow (1 / 2)) r.snd.1 r.snd.2

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

theorem inner_single_single {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (i j k l : n) : inner ℂ (Matrix.single i j 1) (Matrix.single 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 ℂ) : (adjoint (mul' ℂ (Matrix n n ℂ))) x = ∑ i : n, ∑ j : n, ∑ k : n, ∑ l : n, (x i l * φ.matrix⁻¹ k j) • Matrix.single i j 1 ⊗ₜ[ℂ] Matrix.single k l 1

m^*(x) = ∑_{i,j,k,l} x_{il} Q⁻¹_{kj} (e_{ij} ⊗ₜ e_{kl}).

theorem Matrix.linearMap_ext_iff_inner_map {n : Type u_2} [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {x 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] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {x 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 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 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 x : Matrix n n ℂ) : inner ℂ a x = inner ℂ (x.conjTranspose * a) 1

theorem oneInner {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] {φ : 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 LinearMap.mulLeft_toMatrix {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (x : Matrix n n ℂ) : hφ.toMatrix (mulLeft ℂ x) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) x 1

theorem LinearMap.mulRight_toMatrix {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : Matrix n n ℂ) : hφ.toMatrix (mulRight ℂ x) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 ((hφ.sig (1 / 2)) x).transpose

theorem includeBlock_adjoint {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (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_single_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 l : s i) (x : PiMat ℂ k s) : inner ℂ (Matrix.single ⟨i, j⟩ ⟨i, l⟩ 1).blockDiag' x = (x i * (ψ i).matrix) j l

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

theorem pi_inner_single_single {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 j : k} (a b : s i) (c d : s j) : inner ℂ (Matrix.single ⟨i, a⟩ ⟨i, b⟩ 1).blockDiag' (Matrix.single ⟨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_single_single_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 b c d : s i) : inner ℂ (Matrix.single ⟨i, a⟩ ⟨i, b⟩ 1).blockDiag' (Matrix.single ⟨i, c⟩ ⟨i, d⟩ 1).blockDiag' = if a = c then (ψ i).matrix d b else 0

theorem pi_inner_single_single_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 j : k} (h : i ≠ j) (a b : s i) (c d : s j) : inner ℂ (Matrix.single ⟨i, a⟩ ⟨i, b⟩ 1).blockDiag' (Matrix.single ⟨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) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] {i : k} (x : Matrix (s i) (s i) ℂ) : (adjoint (mul' ℂ (PiMat ℂ k s))) (Matrix.includeBlock x) = (TensorProduct.map Matrix.includeBlock Matrix.includeBlock) ((adjoint (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) : (adjoint (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.single ⟨r, a⟩ ⟨r, b⟩ 1).blockDiag' ⊗ₜ[ℂ] (Matrix.single ⟨r, c⟩ ⟨r, d⟩ 1).blockDiag'

theorem LinearMap.pi_mul'_apply_includeBlock {k : Type u_3} [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] {i : k} (x : TensorProduct ℂ (Matrix (s i) (s i) ℂ) (Matrix (s i) (s i) ℂ)) : (mul' ℂ (PiMat ℂ k s)) ((TensorProduct.map Matrix.includeBlock Matrix.includeBlock) x) = Matrix.includeBlock ((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) : (mul' ℂ (PiMat ℂ k s)) ((adjoint (mul' ℂ (PiMat ℂ k s))) x) = ∑ i : k, (ψ i).matrix⁻¹.trace • Matrix.includeBlock (x i)

theorem Matrix.smul_inj_mul_one {n : Type u_2} [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] {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)] (α : ℂ) : mul' ℂ (PiMat ℂ k s) ∘ₗ adjoint (mul' ℂ (PiMat ℂ k s)) = α • 1 ↔ ∀ (i : k), (ψ i).matrix⁻¹.trace = α