Two C⋆-algebraic steps of Lemma 3.2 #
theorem
Orthogonalization.MvN.mul_eq_zero_of_mul_sub_eq_self
{H : Type u_1}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
{v Q R S : H →L[ℂ] H}
(hS : IsSelfAdjoint S)
(hR : IsStarProjection R)
(hSR : S * R = S)
(hQR : Q * R = R)
(hvQR : v * (Q - R) = v)
:
If S = S* and S R = S for a projection R ≤ Q, then v (Q − R) = v forces v S = 0.
theorem
Orthogonalization.MvN.star_add_mul_add_eq_of_le
{H : Type u_1}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
{u₀ v Q R P L : H →L[ℂ] H}
(hR : IsStarProjection R)
(hL : IsStarProjection L)
(hQR : IsStarProjection (Q - R))
(hPL : IsStarProjection (P - L))
(hu₀R : star u₀ * u₀ = R)
(hu₀L : u₀ * star u₀ = L)
(hv1 : star v * v = Q - R)
(hv2 : v * star v = P - L)
(hRQ : R * Q = R)
(hLP : L * P = L)
:
The sum of two partial isometries u₀ : R → L and v : Q − R → P − L, for projections
R ≤ Q and L ≤ P, is a partial isometry Q → P: the cross terms u₀* v, u₀ v* vanish
because L (P − L) = 0 and R (Q − R) = 0.
Lemma 3.2 in M_n(M) #
theorem
Orthogonalization.MvN.exists_partial_isometry_of_supports
{H : Type u_1}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(M : VonNeumannAlgebra H)
{p : H →L[ℂ] H}
(hp : IsStarProjection p)
(E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H)
(hEtr : ∀ x ∈ M, p * x * p = x → ∀ y ∈ M, p * y * p = y → E (x * y) = E (y * x))
{n : ℕ}
(hcomp :
∀ (P Q : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)),
P ∈ matrixAlgebra M n →
IsStarProjection P →
P * amplify n p = P →
Q ∈ matrixAlgebra M n →
IsStarProjection Q →
Q * amplify n p = Q →
∑ i : Fin n, E (entry P i i) = ∑ i : Fin n, E (entry Q i i) → MvNEquiv (matrixAlgebra M n) P Q)
(hpolar :
∀ x ∈ matrixAlgebra M n,
∃ u ∈ matrixAlgebra M n, star u * u = rightSupport x ∧ u * star u = leftSupport x ∧ x = u * CFC.sqrt (star x * x))
{x Q P : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)}
(hxM : x ∈ matrixAlgebra M n)
(hQ : IsStarProjection Q)
(hQM : Q ∈ matrixAlgebra M n)
(hQamp : Q * amplify n p = Q)
(hP : IsStarProjection P)
(hPM : P ∈ matrixAlgebra M n)
(hPamp : P * amplify n p = P)
(hxQ : x * Q = x)
(hPx : P * x = x)
(hE : ∑ i : Fin n, E (entry Q i i) = ∑ i : Fin n, E (entry P i i))
:
Lemma 3.2 in M_n(M). For x ∈ M_n(M) and projections Q, P ≤ 1_n ⊗ p of M_n(M)
with x Q = x, P x = x and ∑ᵢ E(Qᵢᵢ) = ∑ᵢ E(Pᵢᵢ), there is a partial isometry
u ∈ M_n(M) with u* u = Q, u u* = P and x = u √(x* x): write x = u₀ √(x* x) with
u₀* u₀ = R ≤ Q, u₀ u₀* = L ≤ P the supports of x, compare Q − R ∼ P − L by a partial
isometry v, and take u = u₀ + v.
theorem
Orthogonalization.MvN.exists_pvm_of_partial_isometry
{H : Type u_1}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(M : VonNeumannAlgebra H)
{p : H →L[ℂ] H}
(hp : IsStarProjection p)
{n : ℕ}
[NeZero n]
{q : Fin n → H →L[ℂ] H}
(hq : ∀ (i : Fin n), IsStarProjection (q i))
(hqM : ∀ (i : Fin n), q i ∈ M)
{u : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)}
(huM : u ∈ matrixAlgebra M n)
(huu : star u * u = single 0 p)
(huu' : u * star u = FinDim.blockProj q)
{X : Fin n → H →L[ℂ] H}
{y : H →L[ℂ] H}
(hux : u * single 0 (CFC.sqrt y) = col 0 X)
:
From a partial isometry u ∈ M_n(M) with u* u = e_{00} ⊗ p, u u* = ⊕ᵢ qᵢ and
u (e_{00} ⊗ s) = ∑ᵢ e_{i0} ⊗ X i (s = √y): the operators p'ᵢ = (u* (e_{ii} ⊗ qᵢ) u)₀₀
form a PVM of the corner p M p with s p'ᵢ s = (X i)* qᵢ (X i).
theorem
Orthogonalization.MvN.exists_pvm_of_selection_of_neZero
{H : Type u_1}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(M : VonNeumannAlgebra H)
{p : H →L[ℂ] H}
(hp : IsStarProjection p)
(hpM : p ∈ M)
(E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H)
(hEp : E p = p)
(hEtr : ∀ x ∈ M, p * x * p = x → ∀ y ∈ M, p * y * p = y → E (x * y) = E (y * x))
{n : ℕ}
[NeZero n]
(hcomp :
∀ (P Q : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)),
P ∈ matrixAlgebra M n →
IsStarProjection P →
P * amplify n p = P →
Q ∈ matrixAlgebra M n →
IsStarProjection Q →
Q * amplify n p = Q →
∑ i : Fin n, E (entry P i i) = ∑ i : Fin n, E (entry Q i i) → MvNEquiv (matrixAlgebra M n) P Q)
(hpolar :
∀ x ∈ matrixAlgebra M n,
∃ u ∈ matrixAlgebra M n, star u * u = rightSupport x ∧ u * star u = leftSupport x ∧ x = u * CFC.sqrt (star x * x))
(a q : Fin n → H →L[ℂ] H)
(haM : ∀ (i : Fin n), a i ∈ M)
(ha0 : ∀ (i : Fin n), 0 ≤ a i)
(hap : ∑ i : Fin n, a i = p)
(hq : ∀ (i : Fin n), IsStarProjection (q i))
(hqM : ∀ (i : Fin n), q i ∈ M)
(hqp : ∀ (i : Fin n), q i * p = q i)
(hqa : ∀ (i : Fin n), Commute (q i) (a i))
(hqE : ∑ i : Fin n, E (q i) = p)
:
Lemma 3.2 in M_n(M) for n ≥ 1 (the index 0 : Fin n carries the column).
theorem
Orthogonalization.MvN.exists_pvm_of_selection
{H : Type u_1}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(M : VonNeumannAlgebra H)
{p : H →L[ℂ] H}
(hp : IsStarProjection p)
(hpM : p ∈ M)
(E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H)
(hEp : E p = p)
(hEtr : ∀ x ∈ M, p * x * p = x → ∀ y ∈ M, p * y * p = y → E (x * y) = E (y * x))
{n : ℕ}
(hcomp :
∀ (P Q : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)),
P ∈ matrixAlgebra M n →
IsStarProjection P →
P * amplify n p = P →
Q ∈ matrixAlgebra M n →
IsStarProjection Q →
Q * amplify n p = Q →
∑ i : Fin n, E (entry P i i) = ∑ i : Fin n, E (entry Q i i) → MvNEquiv (matrixAlgebra M n) P Q)
(hpolar :
∀ x ∈ matrixAlgebra M n,
∃ u ∈ matrixAlgebra M n, star u * u = rightSupport x ∧ u * star u = leftSupport x ∧ x = u * CFC.sqrt (star x * x))
(a q : Fin n → H →L[ℂ] H)
(haM : ∀ (i : Fin n), a i ∈ M)
(ha0 : ∀ (i : Fin n), 0 ≤ a i)
(hap : ∑ i : Fin n, a i = p)
(hq : ∀ (i : Fin n), IsStarProjection (q i))
(hqM : ∀ (i : Fin n), q i ∈ M)
(hqp : ∀ (i : Fin n), q i * p = q i)
(hqa : ∀ (i : Fin n), Commute (q i) (a i))
(hqE : ∑ i : Fin n, E (q i) = p)
:
Lemma 3.2 of the paper applied in M_n(M) (proof of Theorem 1.2, finite case, Section 3):
given the projections qᵢ ≤ p of Lemma 3.1 (qᵢ commuting with aᵢ, ∑ E(qᵢ) = p), there is a
PVM p'ᵢ of the corner p M p with √y p'ᵢ √y = qᵢ aᵢ, y = ∑ⱼ qⱼ aⱼ.