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

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

Section single_block

theorem Module.Dual.IsFaithfulPosMap.basis_apply' {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (i j : n) : hφ.basis (i, j) = Matrix.single i j 1 * ⋯.rpow (-(1 / 2))

theorem sig_apply_pos_def_matrix {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (t s : ℝ) : (hφ.sig t) (⋯.rpow s) = ⋯.rpow s

theorem sig_apply_pos_def_matrix' {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (t : ℝ) : (hφ.sig t) φ.matrix = φ.matrix

theorem Nontracial.inner_symm {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x y : Matrix n n ℂ) : inner ℂ x y = inner ℂ ((hφ.sig (-1)) y.conjTranspose) x.conjTranspose

Section direct_sum

theorem Module.Dual.pi.IsFaithfulPosMap.inner_coord' {k : Type u_2} [Fintype k] {s : k → Type u_1} [(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} (ij : s i × s i) (x : PiMat ℂ k s) : inner ℂ ((IsFaithfulPosMap.basis ⋯) ⟨i, ij⟩) x = (x * fun (j : k) => ⋯.rpow (1 / 2)) i ij.1 ij.2

theorem Module.Dual.pi.IsFaithfulPosMap.map_star {k : Type u_2} [Fintype k] {s : k → Type u_1} [(i : k) → Fintype (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (x : PiMat ℂ k s) : (pi ψ) (star x) = star ((pi ψ) x)

theorem Nontracial.Pi.unit_adjoint_eq {k : Type u_2} [Fintype k] {s : k → Type u_1} [(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 (Algebra.linearMap ℂ (PiMat ℂ k s)) = Module.Dual.pi ψ

theorem Module.Dual.pi.IsFaithfulPosMap.matrixIsPosDef {k : Type u_1} {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) : (ψ i).matrix.PosDef

The positive-definite matrices associated to a faithful positive functional on each block.

noncomputable def Pi.PosDef.rpow {k : Type u_1} {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {a : PiMat ℂ k s} (ha : ∀ (i : k), Matrix.PosDef (a i)) (r : ℝ) (i : k) : Matrix (s i) (s i) ℂ

Pointwise real powers of a positive-definite element of PiMat.

Equations

• Pi.PosDef.rpow ha r i = ⋯.rpow r

theorem Pi.PosDef.rpow_hMul_rpow {k : Type u_1} {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {a : PiMat ℂ k s} (ha : ∀ (i : k), Matrix.PosDef (a i)) (r₁ r₂ : ℝ) : rpow ha r₁ * rpow ha r₂ = rpow ha (r₁ + r₂)

theorem Pi.PosDef.rpow_zero {k : Type u_1} {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {a : PiMat ℂ k s} (ha : ∀ (i : k), Matrix.PosDef (a i)) : rpow ha 0 = 1

theorem basis_repr_apply' {k : Type u_2} [Fintype k] {s : k → Type u_1} [(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) : have hQ := ⋯; ((Module.Dual.pi.IsFaithfulPosMap.basis hψ).repr x) ijk = (x * Pi.PosDef.rpow hQ (1 / 2)) ijk.fst ijk.snd.1 ijk.snd.2

theorem Module.Dual.pi.IsFaithfulPosMap.includeBlock_right_inner {k : Type u_1} [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} (y : (j : k) → Matrix (s j) (s j) ℂ) (x : Matrix (s i) (s i) ℂ) : inner ℂ y (Matrix.includeBlock x) = inner ℂ (y i) x

theorem pi_includeBlock_right_rankOne {k : Type u_4} [Fintype k] [DecidableEq k] {s : k → Type u_1} [(i : k) → Fintype (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} {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) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] [hψ₂ : ∀ (i : k₂), (ψ₂ i).IsFaithfulPosMap] (a : PiMat ℂ k₂ s₂) {i : k} (b : Matrix (s i) (s i) ℂ) (c : PiMat ℂ k s) (j : k₂) : (((rankOne ℂ) a) (Matrix.includeBlock b)) c j = inner ℂ b (c i) • a j

theorem pi_includeBlock_left_rankOne {k : Type u_3} [Fintype k] {s : k → Type u_1} [(i : k) → Fintype (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} {k₂ : Type u_4} [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] [hψ₂ : ∀ (i : k₂), (ψ₂ i).IsFaithfulPosMap] (b : PiMat ℂ k s) {i : k₂} (a : Matrix (s₂ i) (s₂ i) ℂ) (c : PiMat ℂ k s) (j : k₂) : (((rankOne ℂ) (Matrix.includeBlock a)) b) c j = inner ℂ b c • if h : i = j then ⋯.mpr a else 0

noncomputable def Module.Dual.pi.IsFaithfulPosMap.sig {k : Type u_1} {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) (z : ℝ) : PiMat ℂ k s ≃ₐ[ℂ] PiMat ℂ k s

The modular automorphism on a direct product of matrix blocks.

Equations

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

@[simp]

theorem Module.Dual.pi.IsFaithfulPosMap.sig_apply {k : Type u_2} {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (z : ℝ) (x : PiMat ℂ k s) : (sig hψ z) x = Pi.PosDef.rpow ⋯ (-z) * x * Pi.PosDef.rpow ⋯ z

@[simp]

theorem Module.Dual.pi.IsFaithfulPosMap.sig_symm_apply {k : Type u_2} {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (z : ℝ) (x : PiMat ℂ k s) : (sig hψ z).symm x = Pi.PosDef.rpow ⋯ z * x * Pi.PosDef.rpow ⋯ (-z)

@[simp]

theorem Module.Dual.pi.IsFaithfulPosMap.sig_symm_eq {k : Type u_2} {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (z : ℝ) : (sig hψ z).symm = sig hψ (-z)

theorem Module.Dual.pi.IsFaithfulPosMap.sig_apply_single_block {k : Type u_2} [DecidableEq k] {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (z : ℝ) {i : k} (x : Matrix (s i) (s i) ℂ) : (sig hψ z) (Matrix.includeBlock x) = Matrix.includeBlock ((⋯.sig z) x)

theorem Module.Dual.pi.IsFaithfulPosMap.sig_eq_pi_blocks {k : Type u_2} {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (z : ℝ) (x : PiMat ℂ k s) {i : k} : (sig hψ z) x i = (⋯.sig z) (x i)

theorem Pi.PosDef.rpow.isPosDef {k : Type u_1} {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {a : PiMat ℂ k s} (ha : ∀ (i : k), Matrix.PosDef (a i)) (r : ℝ) (i : k) : (rpow ha r i).PosDef

theorem Pi.PosDef.rpow.is_self_adjoint {k : Type u_1} {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {a : PiMat ℂ k s} (ha : ∀ (i : k), Matrix.PosDef (a i)) (r : ℝ) : star (rpow ha r) = rpow ha r

theorem Module.Dual.pi.IsFaithfulPosMap.sig_star {k : Type u_2} {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (z : ℝ) (x : PiMat ℂ k s) : star ((sig hψ z) x) = (sig hψ (-z)) (star x)

theorem Module.Dual.pi.IsFaithfulPosMap.sig_apply_sig {k : Type u_2} {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (t r : ℝ) (x : PiMat ℂ k s) : (sig hψ t) ((sig hψ r) x) = (sig hψ (t + r)) x

theorem Module.Dual.pi.IsFaithfulPosMap.sig_zero {k : Type u_2} {s : k → Type u_1} [(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) : (sig hψ 0) x = x

theorem Module.Dual.pi.IsFaithfulPosMap.toMatrixLinEquiv_apply'' {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} {k₂ : Type u_4} [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] [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)) * Pi.PosDef.rpow ⋯ (1 / 2)) r.fst r.snd.1 r.snd.2

theorem Module.Dual.pi.IsFaithfulPosMap.toMatrix_apply'' {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_1} [(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 hψ) f r l = (f (Matrix.includeBlock (⋯.basis l.snd)) * Pi.PosDef.rpow ⋯ (1 / 2)) r.fst r.snd.1 r.snd.2

theorem Module.Dual.pi.IsFaithfulPosMap.toMatrixLinEquiv_symm_apply' {k : Type u_4} [Fintype k] [DecidableEq k] {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} {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] [hψ₂ : ∀ (i : k₂), (ψ₂ i).IsFaithfulPosMap] (x : Matrix ((i : k₂) × s₂ i × s₂ i) ((i : k) × s i × s i) ℂ) : (toMatrixLinEquiv hψ hψ₂).symm x = ∑ a : k₂, ∑ i : s₂ a, ∑ j : s₂ a, ∑ b : k, ∑ c : s b, ∑ d : s b, x ⟨a, (i, j)⟩ ⟨b, (c, d)⟩ • ↑(((rankOne ℂ) ((IsFaithfulPosMap.basis hψ₂) ⟨a, (i, j)⟩)) ((IsFaithfulPosMap.basis hψ) ⟨b, (c, d)⟩))

theorem Module.Dual.pi.IsFaithfulPosMap.toMatrix_symm_apply' {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (x : Matrix ((i : k) × s i × s i) ((i : k) × s i × s i) ℂ) : (toMatrix hψ).symm x = ∑ a : k, ∑ i : s a, ∑ j : s a, ∑ b : k, ∑ c : s b, ∑ d : s b, x ⟨a, (i, j)⟩ ⟨b, (c, d)⟩ • ↑(((rankOne ℂ) ((IsFaithfulPosMap.basis hψ) ⟨a, (i, j)⟩)) ((IsFaithfulPosMap.basis hψ) ⟨b, (c, d)⟩))

theorem Module.Dual.pi.IsFaithfulPosMap.toMatrix_eq_orthonormalBasis_toMatrix {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_1} [(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 →ₗ[ℂ] PiMat ℂ k s) : (toMatrix ⋯) x = (IsFaithfulPosMap.orthonormalBasis hψ).toMatrix x

theorem Matrix.toLin_apply_rankOne {𝕜 : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₁] [InnerProductSpace 𝕜 H₂] {ι₁ : Type u_4} {ι₂ : Type u_5} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 H₁) (b₂ : OrthonormalBasis ι₂ 𝕜 H₂) (x : Matrix ι₂ ι₁ 𝕜) : (toLin b₁.toBasis b₂.toBasis) x = ∑ i : ι₂, ∑ j : ι₁, x i j • ↑(((rankOne 𝕜) (b₂ i)) (b₁ j))

@[simp]

theorem Module.Dual.pi.IsFaithfulPosMap.orthonormalBasis_eq_toBasis {k : Type u_2} [Fintype k] {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) : (IsFaithfulPosMap.orthonormalBasis hψ).toBasis = IsFaithfulPosMap.basis hψ

theorem Module.Dual.pi.IsFaithfulPosMap.linearMap_eq {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} {k₂ : Type u_4} [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] [hψ₂ : ∀ (i : k₂), (ψ₂ i).IsFaithfulPosMap] (x : PiMat ℂ k s →ₗ[ℂ] PiMat ℂ k₂ s₂) : x = ∑ a : (i : k₂) × s₂ i × s₂ i, ∑ b : (i : k) × s i × s i, (toMatrixLinEquiv hψ hψ₂) x a b • ↑(((rankOne ℂ) ((IsFaithfulPosMap.basis hψ₂) a)) ((IsFaithfulPosMap.basis hψ) b))

noncomputable def Module.Dual.pi.IsFaithfulPosMap.psiToFun' {k : Type u_1} [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) ℂ)} {k₂ : Type u_3} [Fintype k₂] {s₂ : k₂ → Type u_4} [(i : k₂) → Fintype (s₂ i)] [(i : k₂) → DecidableEq (s₂ i)] {ψ₂ : (i : k₂) → Dual ℂ (Matrix (s₂ i) (s₂ i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (hψ₂ : ∀ (i : k₂), (ψ₂ i).IsFaithfulPosMap) (t r : ℝ) : (PiMat ℂ k s →ₗ[ℂ] PiMat ℂ k₂ s₂) →ₗ[ℂ] TensorProduct ℂ (PiMat ℂ k₂ s₂) (PiMat ℂ k s)ᵐᵒᵖ

Forward map underlying psi for faithful positive functionals on matrix-block products.

Equations

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

theorem Module.Dual.pi.IsFaithfulPosMap.toMatrixLinEquiv_rankOne_apply {k : Type u_4} [Fintype k] [DecidableEq k] {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} {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] [hψ₂ : ∀ (i : k₂), (ψ₂ i).IsFaithfulPosMap] (x : PiMat ℂ k₂ s₂) (y : PiMat ℂ k s) : (toMatrixLinEquiv hψ hψ₂) ↑(((rankOne ℂ) x) y) = fun (i : (i : k₂) × s₂ i × s₂ i) (j : (i : k) × s i × s i) => (Matrix.replicateCol (Fin 1) (Matrix.reshape (x i.fst * ⋯.rpow (1 / 2))) * (Matrix.replicateCol (Fin 1) (Matrix.reshape (y j.fst * ⋯.rpow (1 / 2)))).conjTranspose) i.snd j.snd

theorem Pi.IsFaithfulPosMap.ToMatrix.rankOne_apply {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_1} [(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 y : PiMat ℂ k s) : (Module.Dual.pi.IsFaithfulPosMap.toMatrix hψ) ↑(((rankOne ℂ) x) y) = fun (i j : (i : k) × s i × s i) => (Matrix.replicateCol (Fin 1) (Matrix.reshape (x i.fst * ⋯.rpow (1 / 2))) * (Matrix.replicateCol (Fin 1) (Matrix.reshape (y j.fst * ⋯.rpow (1 / 2)))).conjTranspose) i.snd j.snd

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

theorem Module.Dual.pi.IsFaithfulPosMap.psiToFun'_apply {k : Type u_3} [Fintype k] [DecidableEq k] {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} {k₂ : Type u_4} [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] [hψ₂ : ∀ (i : k₂), (ψ₂ i).IsFaithfulPosMap] (t r : ℝ) (b : PiMat ℂ k s) (a : PiMat ℂ k₂ s₂) : (psiToFun' hψ hψ₂ t r) ↑(((rankOne ℂ) a) b) = (sig hψ₂ t) a ⊗ₜ[ℂ] ↑(op ℂ) (star ((sig hψ r) b))

def Pi.transposeAlgEquiv (p : Type u_1) (n : p → Type u_2) [(i : p) → Fintype (n i)] [(i : p) → DecidableEq (n i)] : PiMat ℂ p n ≃ₐ[ℂ] (PiMat ℂ p n)ᵐᵒᵖ

Transpose each matrix block of a product as an algebra equivalence to the opposite algebra.

Equations

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

@[simp]

theorem Pi.transposeAlgEquiv_symm_apply (p : Type u_1) (n : p → Type u_2) [(i : p) → Fintype (n i)] [(i : p) → DecidableEq (n i)] (A : (PiMat ℂ p n)ᵐᵒᵖ) (i : p) : (transposeAlgEquiv p n).symm A i = Matrix.transpose (MulOpposite.unop A i)

@[simp]

theorem Pi.transposeAlgEquiv_apply (p : Type u_1) (n : p → Type u_2) [(i : p) → Fintype (n i)] [(i : p) → DecidableEq (n i)] (A : PiMat ℂ p n) : (transposeAlgEquiv p n) A = MulOpposite.op fun (i : p) => Matrix.transpose (A i)

theorem Pi.transposeAlgEquiv_symm_op_apply {k : Type u_1} {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (A : PiMat ℂ k s) : (transposeAlgEquiv k s).symm (MulOpposite.op A) = fun (i : k) => Matrix.transpose (A i)

noncomputable def tensorProductMulOpEquiv {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] : TensorProduct ℂ (PiMat ℂ k s) (PiMat ℂ k s)ᵐᵒᵖ ≃ₐ[ℂ] (i : k × k) → Matrix (s i.1 × s i.2) (s i.1 × s i.2) ℂ

The tensor-product equivalence used to pass from block products to block-diagonal matrices.

Equations

• tensorProductMulOpEquiv = (AlgEquiv.TensorProduct.map 1 (Pi.transposeAlgEquiv k s).symm).trans (f₂_equiv✝.trans f₃_equiv✝)

noncomputable def Module.Dual.pi.IsFaithfulPosMap.psiInvFun' {k : Type u_1} [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) ℂ)} {k₂ : Type u_3} [Fintype k₂] {s₂ : k₂ → Type u_4} [(i : k₂) → Fintype (s₂ i)] [(i : k₂) → DecidableEq (s₂ i)] {ψ₂ : (i : k₂) → Dual ℂ (Matrix (s₂ i) (s₂ i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (hψ₂ : ∀ (i : k₂), (ψ₂ i).IsFaithfulPosMap) (t r : ℝ) : TensorProduct ℂ (PiMat ℂ k s) (PiMat ℂ k₂ s₂)ᵐᵒᵖ →ₗ[ℂ] PiMat ℂ k₂ s₂ →ₗ[ℂ] PiMat ℂ k s

Inverse map underlying psi for faithful positive functionals on matrix-block products.

Equations

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

theorem Module.Dual.pi.IsFaithfulPosMap.psiInvFun'_apply {k : Type u_3} [Fintype k] {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} {k₂ : Type u_4} [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] [hψ₂ : ∀ (i : k₂), (ψ₂ i).IsFaithfulPosMap] (t r : ℝ) (x : PiMat ℂ k s) (y : (PiMat ℂ k₂ s₂)ᵐᵒᵖ) : (psiInvFun' hψ hψ₂ t r) (x ⊗ₜ[ℂ] y) = ↑(((rankOne ℂ) ((sig hψ (-t)) x)) ((sig hψ₂ (-r)) (star (MulOpposite.unop y))))

theorem Module.Dual.pi.IsFaithfulPosMap.Psi_left_inv {k : Type u_3} [Fintype k] {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} {k₂ : Type u_4} [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] [hψ₂ : ∀ (i : k₂), (ψ₂ i).IsFaithfulPosMap] (t r : ℝ) (x : PiMat ℂ k s) (y : PiMat ℂ k₂ s₂) : (psiInvFun' hψ hψ₂ t r) ((psiToFun' hψ₂ hψ t r) ↑(((rankOne ℂ) x) y)) = ↑(((rankOne ℂ) x) y)

theorem Module.Dual.pi.IsFaithfulPosMap.Psi_right_inv {k : Type u_3} [Fintype k] {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} {k₂ : Type u_4} [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] [hψ₂ : ∀ (i : k₂), (ψ₂ i).IsFaithfulPosMap] (t r : ℝ) (x : PiMat ℂ k s) (y : (PiMat ℂ k₂ s₂)ᵐᵒᵖ) : (psiToFun' hψ₂ hψ t r) ((psiInvFun' hψ hψ₂ t r) (x ⊗ₜ[ℂ] y)) = x ⊗ₜ[ℂ] y

noncomputable def Module.Dual.pi.IsFaithfulPosMap.psi {k : Type u_1} [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) ℂ)} {k₂ : Type u_3} [Fintype k₂] {s₂ : k₂ → Type u_4} [(i : k₂) → Fintype (s₂ i)] [(i : k₂) → DecidableEq (s₂ i)] {ψ₂ : (i : k₂) → Dual ℂ (Matrix (s₂ i) (s₂ i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (hψ₂ : ∀ (i : k₂), (ψ₂ i).IsFaithfulPosMap) (t r : ℝ) : (PiMat ℂ k s →ₗ[ℂ] PiMat ℂ k₂ s₂) ≃ₗ[ℂ] TensorProduct ℂ (PiMat ℂ k₂ s₂) (PiMat ℂ k s)ᵐᵒᵖ

Linear equivalence between linear maps and tensor products for faithful positive block functionals.

Equations

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

@[simp]

theorem Module.Dual.pi.IsFaithfulPosMap.psi_symm_apply {k : Type u_1} [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) ℂ)} {k₂ : Type u_3} [Fintype k₂] {s₂ : k₂ → Type u_4} [(i : k₂) → Fintype (s₂ i)] [(i : k₂) → DecidableEq (s₂ i)] {ψ₂ : (i : k₂) → Dual ℂ (Matrix (s₂ i) (s₂ i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (hψ₂ : ∀ (i : k₂), (ψ₂ i).IsFaithfulPosMap) (t r : ℝ) (x : TensorProduct ℂ (PiMat ℂ k₂ s₂) (PiMat ℂ k s)ᵐᵒᵖ) : (psi hψ hψ₂ t r).symm x = (psiInvFun' hψ₂ hψ t r) x

@[simp]

theorem Module.Dual.pi.IsFaithfulPosMap.psi_apply {k : Type u_1} [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) ℂ)} {k₂ : Type u_3} [Fintype k₂] {s₂ : k₂ → Type u_4} [(i : k₂) → Fintype (s₂ i)] [(i : k₂) → DecidableEq (s₂ i)] {ψ₂ : (i : k₂) → Dual ℂ (Matrix (s₂ i) (s₂ i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap) (hψ₂ : ∀ (i : k₂), (ψ₂ i).IsFaithfulPosMap) (t r : ℝ) (x : PiMat ℂ k s →ₗ[ℂ] PiMat ℂ k₂ s₂) : (psi hψ hψ₂ t r) x = (psiToFun' hψ hψ₂ t r) x

theorem Pi.inner_symm {k : Type u_2} [Fintype k] {s : k → Type u_1} [(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 y : PiMat ℂ k s) : inner ℂ x y = inner ℂ ((Module.Dual.pi.IsFaithfulPosMap.sig hψ (-1)) (star y)) (star x)

theorem Module.Dual.pi.IsFaithfulPosMap.sig_adjoint {k : Type u_2} [Fintype k] {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] {t : ℝ} : LinearMap.adjoint (sig hψ t).toLinearMap = (sig hψ t).toLinearMap

theorem Module.Dual.IsFaithfulPosMap.norm_eq {n : Type u_1} [Fintype n] {ψ : Dual ℂ (Matrix n n ℂ)} [hψ : ψ.IsFaithfulPosMap] (x : Matrix n n ℂ) : ‖x‖ = √(RCLike.re (ψ (x.conjTranspose * x)))

theorem Module.Dual.pi.IsFaithfulPosMap.norm_eq {k : Type u_2} [Fintype k] {s : k → Type u_1} [(i : k) → Fintype (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (x : (i : k) → Matrix (s i) (s i) ℂ) : ‖x‖ = √(RCLike.re ((pi ψ) (star x * x)))

theorem Pi.rankOneLm_real_apply {k : Type u_4} [Fintype k] {s : k → Type u_3} [(i : k) → Fintype (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} {k₂ : Type u_1} [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] [hφ : ∀ (i : k₂), (φ i).IsFaithfulPosMap] (x : PiMat ℂ k s) (y : PiMat ℂ k₂ s₂) : (↑(((rankOne ℂ) x) y)).real = ↑(((rankOne ℂ) (star x)) ((Module.Dual.pi.IsFaithfulPosMap.sig hφ (-1)) (star y)))

theorem Pi.PosDef.rpow_one_eq_self {k : Type u_1} {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {Q : PiMat ℂ k s} (hQ : ∀ (i : k), Matrix.PosDef (Q i)) : rpow hQ 1 = Q

theorem Pi.PosDef.rpow_neg_one_eq_inv_self {k : Type u_1} {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {Q : PiMat ℂ k s} (hQ : ∀ (i : k), Matrix.PosDef (Q i)) : rpow hQ (-1) = Q⁻¹

theorem Module.Dual.pi.IsFaithfulPosMap.inner_left_conj' {k : Type u_2} [Fintype k] {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (a b c : PiMat ℂ k s) : inner ℂ a (b * c) = inner ℂ (a * (sig hψ (-1)) (star c)) b

theorem Module.Dual.pi.IsFaithfulPosMap.inner_right_conj' {k : Type u_2} [Fintype k] {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (a b c : PiMat ℂ k s) : inner ℂ (a * c) b = inner ℂ a (b * (sig hψ (-1)) (star c))

theorem Moudle.Dual.Pi.IsFaithfulPosMap.sig_trans_sig {k : Type u_2} {s : k → Type u_1} [(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 y : ℝ) : (Module.Dual.pi.IsFaithfulPosMap.sig hψ y).trans (Module.Dual.pi.IsFaithfulPosMap.sig hψ x) = Module.Dual.pi.IsFaithfulPosMap.sig hψ (x + y)

theorem Module.Dual.pi.IsFaithfulPosMap.sig_comp_sig {k : Type u_2} {s : k → Type u_1} [(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 : ℝ) : (sig hψ x).toLinearMap ∘ₗ (sig hψ y).toLinearMap = (sig hψ (x + y)).toLinearMap

theorem Module.Dual.pi.IsFaithfulPosMap.sig_zero' {k : Type u_2} {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] : sig hψ 0 = 1

theorem Pi.comp_sig_eq_iff {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) ℂ)} {A : Type u_1} [AddCommMonoid A] [Module ℂ A] [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (t : ℝ) (f g : PiMat ℂ k s →ₗ[ℂ] A) : f ∘ₗ (Module.Dual.pi.IsFaithfulPosMap.sig hψ t).toLinearMap = g ↔ f = g ∘ₗ (Module.Dual.pi.IsFaithfulPosMap.sig hψ (-t)).toLinearMap

theorem Pi.sig_comp_eq_iff {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) ℂ)} {A : Type u_1} [AddCommMonoid A] [Module ℂ A] [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (t : ℝ) (f g : A →ₗ[ℂ] PiMat ℂ k s) : (Module.Dual.pi.IsFaithfulPosMap.sig hψ t).toLinearMap ∘ₗ f = g ↔ f = (Module.Dual.pi.IsFaithfulPosMap.sig hψ (-t)).toLinearMap ∘ₗ g

theorem LinearMap.pi.adjoint_real_eq {k : Type u_4} [Fintype k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {k₂ : Type u_1} [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) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] [hφ : ∀ (i : k₂), (φ i).IsFaithfulPosMap] (f : PiMat ℂ k s →ₗ[ℂ] PiMat ℂ k₂ s₂) : (adjoint f).real = (Module.Dual.pi.IsFaithfulPosMap.sig hψ 1).toLinearMap ∘ₗ adjoint f.real ∘ₗ (Module.Dual.pi.IsFaithfulPosMap.sig hφ (-1)).toLinearMap

theorem Module.Dual.pi.IsFaithfulPosMap.basis.apply_cast_eq_mp {k : Type u_2} {s : k → Type u_1} [(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} (h : i = j) (p : s i × s i) : ⋯.mp (⋯.basis p) = ⋯.basis (⋯.mpr p)

theorem Matrix.includeBlock_apply' {k : Type u_1} [DecidableEq k] {s : k → Type u_2} (x : PiMat ℂ k s) (i j : k) : includeBlock (x i) j = if i = j then x j else 0

theorem pi_lmul_toMatrix {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_1} [(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) : (Module.Dual.pi.IsFaithfulPosMap.toMatrix hψ) (lmul x) = Matrix.blockDiagonal' fun (i : k) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (x i) 1

theorem pi_rmul_toMatrix {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_1} [(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) : (Module.Dual.pi.IsFaithfulPosMap.toMatrix hψ) (rmul x) = Matrix.blockDiagonal' fun (i : k) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 ((⋯.sig (1 / 2)) (x i)).transpose

theorem unitary.coe_pi {k : Type u_2} {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (U : (i : k) → ↥(Matrix.unitaryGroup (s i) ℂ)) : ↑(pi U) = fun (i : k) => ↑(U i)

theorem unitary.coe_pi_apply {k : Type u_2} {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (U : (i : k) → ↥(Matrix.unitaryGroup (s i) ℂ)) (i : k) : (fun (i : k) => ↑(U i)) i = ↑(U i)

theorem pi_inner_aut_toMatrix {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_1} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap] (U : (i : k) → ↥(Matrix.unitaryGroup (s i) ℂ)) : (Module.Dual.pi.IsFaithfulPosMap.toMatrix hψ) (unitary.innerAutStarAlg ℂ (unitary.pi U)).toLinearMap = Matrix.blockDiagonal' fun (i : k) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (↑(U i)) ((⋯.sig (-(1 / 2))) ↑(U i)).conj