Matrix units e_{ij} ⊗ 1

noncomputable def Orthogonalization.MvN.matrixUnit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (i j : Fin n) : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)

The matrix unit e_{ij} ⊗ 1 on H^n.

Equations

• Orthogonalization.MvN.matrixUnit i j = Orthogonalization.FinDim.embed i ∘SL Orthogonalization.FinDim.proj j

theorem Orthogonalization.MvN.matrixUnit_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (i j : Fin n) (w : FinDim.BlockSpace H (Fin n)) : (matrixUnit i j) w = (FinDim.embed i) (w.ofLp j)

theorem Orthogonalization.MvN.entry_matrixUnit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (i j k l : Fin n) : entry (matrixUnit i j) k l = if k = i ∧ l = j then 1 else 0

theorem Orthogonalization.MvN.entry_mul_matrixUnit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) (i j k l : Fin n) : entry (X * matrixUnit i j) k l = if j = l then entry X k i else 0

(X e_{ij})_{kl} = δ_{jl} X_{ki}.

theorem Orthogonalization.MvN.entry_matrixUnit_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {n : ℕ} (i j : Fin n) (X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) (k l : Fin n) : entry (matrixUnit i j * X) k l = if k = i then entry X j l else 0

(e_{ij} X)_{kl} = δ_{ki} X_{jl}.

theorem Orthogonalization.MvN.matrixUnit_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {n : ℕ} (i j : Fin n) : matrixUnit i j ∈ matrixAlgebra M n

M_n(M) of a factor is a factor

theorem Orthogonalization.MvN.matrixAlgebra_factor {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (hfactor : ∀ z ∈ M, (∀ y ∈ M, Commute z y) → ∃ (c : ℂ), z = c • 1) (n : ℕ) (Z : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) : Z ∈ matrixAlgebra M n → (∀ Y ∈ matrixAlgebra M n, Commute Z Y) → ∃ (c : ℂ), Z = c • 1

M_n(M) of a factor is a factor: if every central element of M is a scalar, then every central element of M_n(M) is a scalar.

The diagonal trace X ↦ ∑ᵢ τ(Xᵢᵢ)

noncomputable def Orthogonalization.MvN.entryₗ {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (i j : Fin n) : (FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) →ₗ[ℂ] H →L[ℂ] H

The entry (i, j) as a linear map on B(H^n).

Equations

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

theorem Orthogonalization.MvN.entryₗ_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (i j : Fin n) (X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) : (entryₗ i j) X = entry X i j

noncomputable def Orthogonalization.MvN.diagTrace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (n : ℕ) : (FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) →ₗ[ℂ] ℂ

The diagonal trace X ↦ ∑ᵢ τ(Xᵢᵢ) on B(H^n) of a linear functional τ on B(H).

Equations

• Orthogonalization.MvN.diagTrace τ n = ∑ i : Fin n, τ ∘ₗ Orthogonalization.MvN.entryₗ i i

theorem Orthogonalization.MvN.diagTrace_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (n : ℕ) (X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) : (diagTrace τ n) X = ∑ i : Fin n, τ (entry X i i)

theorem Orthogonalization.MvN.diagTrace_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hτ0 : ∀ x ∈ M, 0 ≤ τ (star x * x)) (n : ℕ) (X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) : X ∈ matrixAlgebra M n → 0 ≤ (diagTrace τ n) (star X * X)

The diagonal trace of a positive functional is positive on M_n(M).

theorem Orthogonalization.MvN.diagTrace_trace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hτtr : ∀ x ∈ M, ∀ y ∈ M, τ (x * y) = τ (y * x)) (n : ℕ) (X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) : X ∈ matrixAlgebra M n → ∀ Y ∈ matrixAlgebra M n, (diagTrace τ n) (X * Y) = (diagTrace τ n) (Y * X)

The diagonal trace of a tracial functional is tracial on M_n(M).

theorem Orthogonalization.MvN.diagTrace_faithful {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hτ0 : ∀ x ∈ M, 0 ≤ τ (star x * x)) (hτf : ∀ x ∈ M, τ (star x * x) = 0 → x = 0) (n : ℕ) (X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) : X ∈ matrixAlgebra M n → (diagTrace τ n) (star X * X) = 0 → X = 0

The diagonal trace of a faithful positive functional is faithful on M_n(M).

theorem Orthogonalization.MvN.diagTrace_amplify {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (n : ℕ) (x : H →L[ℂ] H) : (diagTrace τ n) (amplify n x) = ↑n * τ x

The diagonal trace of x ⊕ ⋯ ⊕ x is n τ(x).

theorem Orthogonalization.MvN.diagTrace_smul_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (n : ℕ) (c : ℂ) : (diagTrace τ n) (c • 1) = ↑n * (c * τ 1)

The diagonal trace of the scalar c • 1 is n c τ(1).