Comparison of projections and the centre-valued trace of an algebra with a vector trace

Two projections with the same centre-valued trace are Murray–von Neumann equivalent, in a von Neumann algebra M with a faithful tracial vector functional and in the matrix algebras M_n(M) (the comparison clauses equiv_of_eq and equiv_of_eq_matrix of the vendored IsCenterValuedTrace). With MIPRE/Background/Orthonormalization/CenterTrace.lean this gives field H3 of the structure-theory interface at the projection 1 (exists_isCenterValuedTrace), for every such M, with no factor hypothesis.

• Generalized comparison (mvNEquiv_of_map_eq): for a von Neumann algebra N with a faithful positive functional, and a linear map Φ that is tracial on N, compatible with left multiplication by central projections and faithful on projections, projections with the same image under Φ are equivalent. The vendored proof for factors (MvN/Comparison.lean, mvNEquiv_of_trace_eq) builds a maximal partial isometry W from p into q by a greedy chain; its factor hypothesis enters only to show that the complements p - W* W and q - W W* cannot both be nonzero. Here maximality gives (q - W W*) y (p - W* W) = 0 for every y ∈ N (exists_maximal_isPartialBetween, through exists_extension_of_mul_ne_zero), so the central support c of p - W* W (exists_centralSupport) kills q - W W*, and applying Φ to c (p - W* W) = p - W* W and c (q - W W*) = 0 shows that both complements have Φ = 0. The three vendored blocks that use the factor hypothesis are copied without it; the rest of MvN/Comparison.lean (partial isometries, the greedy step, strong limits of chains) is reused.
• The instances: N = M with Φ = E, and N = M_n(M) with Φ X = ∑ᵢ E(Xᵢᵢ) and the diagonal trace of τ, whose central projections are amplifications of central projections of M (exists_eq_amplify_of_commute, the first half of the vendored matrixAlgebra_factor).

The three factor-dependent steps of the vendored comparison theorem, without a factor

theorem MIPRE.Orthonormalization.exists_centralSupport {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : VonNeumannAlgebra K) {f : K →L[ℂ] K} (hfN : f ∈ N) : ∃ (c : K →L[ℂ] K), IsStarProjection c ∧ c ∈ N ∧ (∀ y ∈ N, Commute c y) ∧ c * f = f ∧ ∀ (e : K →L[ℂ] K), (∀ y ∈ N, e * y * f = 0) → e * c = 0

The central support of a projection f ∈ N: the projection c onto the closed span of the vectors y (f ξ), y ∈ N, is a central projection of N with c f = f, and every operator e with e y f = 0 for all y ∈ N vanishes on its range. This is the vendored corner lemma exists_mul_mul_ne_zero_of_factor (MvN/Comparison.lean) without its factor step, which identifies c with 1 there; the construction of c is copied from it.

theorem MIPRE.Orthonormalization.exists_extension_of_mul_ne_zero {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : VonNeumannAlgebra K) (τ : (K →L[ℂ] K) →ₗ[ℂ] ℂ) (hτ0 : ∀ x ∈ N, 0 ≤ τ (star x * x)) (hτf : ∀ x ∈ N, τ (star x * x) = 0 → x = 0) {p q w y : K →L[ℂ] K} (hp : IsStarProjection p) (hpN : p ∈ N) (hq : IsStarProjection q) (hqN : q ∈ N) (hw : Orthogonalization.MvN.IsPartialBetween N p q w) (hyN : y ∈ N) (hx0 : (q - w * star w) * y * (p - star w * w) ≠ 0) : ∃ (u : K →L[ℂ] K), Orthogonalization.MvN.IsPartialBetween N (p - star w * w) (q - w * star w) u ∧ 0 < (τ (star u * u)).re

Extension from a nonzero corner: if (q - w w*) y (p - w* w) ≠ 0 for some y ∈ N, the partial isometry w extends by a partial isometry u between the complements p - w* w, q - w w*, whose initial projection has positive trace when τ is faithful. This is the vendored exists_extension_of_ne (MvN/Comparison.lean), copied with the nonzero corner as a hypothesis: there it comes from the factor hypothesis.

theorem MIPRE.Orthonormalization.exists_maximal_isPartialBetween {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : VonNeumannAlgebra K) (τ : (K →L[ℂ] K) →ₗ[ℂ] ℂ) (hτ0 : ∀ x ∈ N, 0 ≤ τ (star x * x)) (hτf : ∀ x ∈ N, τ (star x * x) = 0 → x = 0) {p q : K →L[ℂ] K} (hp : IsStarProjection p) (hpN : p ∈ N) (hq : IsStarProjection q) (hqN : q ∈ N) : ∃ (W : K →L[ℂ] K), Orthogonalization.MvN.IsPartialBetween N p q W ∧ ∀ y ∈ N, (q - W * star W) * y * (p - star W * W) = 0

A maximal partial isometry between two projections: in a von Neumann algebra N with a faithful positive functional τ, some partial isometry W ∈ N from below p to below q leaves complements with no corner between them, (q - W W*) y (p - W* W) = 0 for every y ∈ N. The greedy chain is that of the vendored mvNEquiv_of_trace_eq (MvN/Comparison.lean), copied because that theorem hard-codes its factor hypothesis, through which maximality makes one of the two complements vanish.

theorem MIPRE.Orthonormalization.mvNEquiv_of_map_eq {K : Type u} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : VonNeumannAlgebra K) (τ : (K →L[ℂ] K) →ₗ[ℂ] ℂ) (hτ0 : ∀ x ∈ N, 0 ≤ τ (star x * x)) (hτf : ∀ x ∈ N, τ (star x * x) = 0 → x = 0) {V : Type u_1} [AddCommGroup V] [Module ℂ V] (Φ : (K →L[ℂ] K) →ₗ[ℂ] V) (hΦtr : ∀ x ∈ N, ∀ y ∈ N, Φ (x * y) = Φ (y * x)) (hΦc : ∀ (c : K →L[ℂ] K), IsStarProjection c → c ∈ N → (∀ y ∈ N, Commute c y) → ∃ (L : V → V), ∀ x ∈ N, Φ (c * x) = L (Φ x)) (hΦf : ∀ (e : K →L[ℂ] K), IsStarProjection e → e ∈ N → Φ e = 0 → e = 0) {p q : K →L[ℂ] K} (hp : IsStarProjection p) (hpN : p ∈ N) (hq : IsStarProjection q) (hqN : q ∈ N) (hpq : Φ p = Φ q) : Orthogonalization.MvN.MvNEquiv N p q

Generalized comparison of projections: in a von Neumann algebra N with a faithful positive functional τ, two projections with the same image under a linear map Φ that is tracial on N, compatible with left multiplication by central projections, and faithful on projections, are Murray–von Neumann equivalent. Unlike the vendored mvNEquiv_of_trace_eq, τ need not be tracial: the traciality of Φ takes its place in the endgame.

theorem MIPRE.Orthonormalization.exists_eq_amplify_of_commute {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {n : ℕ} {X : Orthogonalization.FinDim.BlockSpace H (Fin n) →L[ℂ] Orthogonalization.FinDim.BlockSpace H (Fin n)} (hX : X ∈ Orthogonalization.MvN.matrixAlgebra M n) (hXc : ∀ Y ∈ Orthogonalization.MvN.matrixAlgebra M n, Commute X Y) : ∃ (c : H →L[ℂ] H), Orthogonalization.MvN.IsCentralIn M 1 c ∧ X = Orthogonalization.MvN.amplify n c

The centre of M_n(M) is the amplified centre of M: an element of M_n(M) commuting with M_n(M) is the amplification of a central element of M.

theorem MIPRE.Orthonormalization.IsCenterExpectation.equiv_of_eq {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {d : ℕ} {g : Fin d → H} {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} (hE : IsCenterExpectation M g E) (htr : ∀ x ∈ M, ∀ y ∈ M, (vecFunctional g) (x * y) = (vecFunctional g) (y * x)) (hsep : ∀ x ∈ M, (∀ (k : Fin d), x (g k) = 0) → x = 0) (q q' : H →L[ℂ] H) : IsStarProjection q → q ∈ M → IsStarProjection q' → q' ∈ M → E q = E q' → Orthogonalization.MvN.MvNEquiv M q q'

Comparison in M: projections with the same centre-valued trace are equivalent.

theorem MIPRE.Orthonormalization.IsCenterExpectation.equiv_of_eq_matrix {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {d : ℕ} {g : Fin d → H} {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} (hE : IsCenterExpectation M g E) (htr : ∀ x ∈ M, ∀ y ∈ M, (vecFunctional g) (x * y) = (vecFunctional g) (y * x)) (hsep : ∀ x ∈ M, (∀ (k : Fin d), x (g k) = 0) → x = 0) (n : ℕ) (P Q : Orthogonalization.FinDim.BlockSpace H (Fin n) →L[ℂ] Orthogonalization.FinDim.BlockSpace H (Fin n)) : P ∈ Orthogonalization.MvN.matrixAlgebra M n → IsStarProjection P → Q ∈ Orthogonalization.MvN.matrixAlgebra M n → IsStarProjection Q → ∑ i : Fin n, E (Orthogonalization.MvN.entry P i i) = ∑ i : Fin n, E (Orthogonalization.MvN.entry Q i i) → Orthogonalization.MvN.MvNEquiv (Orthogonalization.MvN.matrixAlgebra M n) P Q

Comparison in M_n(M): projections with the same diagonal centre-valued trace ∑ᵢ E(Xᵢᵢ) are equivalent.

theorem MIPRE.Orthonormalization.IsCenterExpectation.isCenterValuedTrace {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {d : ℕ} {g : Fin d → H} {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} (hE : IsCenterExpectation M g E) (htr : ∀ x ∈ M, ∀ y ∈ M, (vecFunctional g) (x * y) = (vecFunctional g) (y * x)) (hsep : ∀ x ∈ M, (∀ (k : Fin d), x (g k) = 0) → x = 0) : Orthogonalization.MvN.IsCenterValuedTrace M 1 E

A centre-valued expectation is a centre-valued trace (field H3 at the projection 1).

theorem MIPRE.Orthonormalization.exists_isCenterValuedTrace {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {d : ℕ} (g : Fin d → H) (htr : ∀ x ∈ M, ∀ y ∈ M, (vecFunctional g) (x * y) = (vecFunctional g) (y * x)) (hsep : ∀ x ∈ M, (∀ (k : Fin d), x (g k) = 0) → x = 0) : ∃ (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H), Orthogonalization.MvN.IsCenterValuedTrace M 1 E

Field H3 at the projection 1 for a von Neumann algebra with a faithful tracial vector functional: it has a centre-valued trace. No factor, type or separability hypothesis.