Small facts about partial isometries and projections

theorem Orthogonalization.MvN.star_mul_self_mul_star {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {v : H →L[ℂ] H} (h : IsStarProjection (star v * v)) : star v * (v * star v) = star v

Adjoint form of mul_star_mul_self_eq_self: if v* v is a projection then v* (v v*) = v*.

theorem Orthogonalization.MvN.mul_eq_self_of_star_mul_self_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {v p : H →L[ℂ] H} (hp : IsStarProjection p) (h : star v * v = p) : v * p = v

If v* v = p is a projection then v p = v.

theorem Orthogonalization.MvN.proj_mul_star_eq_self_of_star_mul_self_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {v p : H →L[ℂ] H} (hp : IsStarProjection p) (h : star v * v = p) : p * star v = star v

If v* v = p is a projection then p v* = v*.

theorem Orthogonalization.MvN.isStarProjection_sub_of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {e z : H →L[ℂ] H} (hz : IsStarProjection z) (he : IsStarProjection e) (hez : e * z = e) (hze : z * e = e) : IsStarProjection (z - e)

z − e is a projection when e ≤ z are projections.

theorem Orthogonalization.MvN.proj_mul_sub_eq_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {e z : H →L[ℂ] H} (he : IsStarProjection e) (hez : e * z = e) : e * (z - e) = 0

A projection e ≤ z is orthogonal to z − e.

theorem Orthogonalization.MvN.central_mul_eq_self_of_star_mul_self_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {z u : H →L[ℂ] H} (hz : Blocks.IsCentralProj M z) (huM : u ∈ M) (h : star u * u = z) : z * u = u

An element u ∈ M with u* u = z, z a central projection, satisfies z u = u (from u z = u and centrality).

Comparison from an inclusion into an equivalent projection

theorem Orthogonalization.MvN.exists_partial_isometry_of_le_of_equiv {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {P P' Q : H →L[ℂ] H} (hP : IsStarProjection P) (hPM : P ∈ M) (hPP' : P * P' = P) (h : MvNEquiv M P' Q) : ∃ w ∈ M, star w * w = P ∧ IsStarProjection (w * star w) ∧ w * star w * Q = w * star w

If P ≤ P' and P' ∼ Q then P is equivalent to a subprojection of Q: w := v P for the partial isometry v of P' ∼ Q satisfies w* w = P, w w* ≤ Q. (P' need not be assumed to be a projection: it is v* v.)

Isometries with orthogonal ranges summing to z, from halving

theorem Orthogonalization.MvN.exists_isometries_of_halving {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) {z : H →L[ℂ] H} (hz : Blocks.IsCentralProj M z) (hz0 : z ≠ 0) (hH4 : ∀ (q : H →L[ℂ] H), IsStarProjection q → q ∈ M → q * z = q → q ≠ 0 → ∃ (e : H →L[ℂ] H), IsStarProjection e ∧ e ∈ M ∧ e * q = e ∧ MvNEquiv M e (q - e) ∧ MvNEquiv M e q) (n : ℕ) (hn : 0 < n) : ∃ (u : Fin n → H →L[ℂ] H), (∀ (i : Fin n), u i ∈ M) ∧ (∀ (i : Fin n), star (u i) * u i = z) ∧ (∀ (i j : Fin n), i ≠ j → star (u i) * u j = 0) ∧ ∑ i : Fin n, u i * star (u i) = z

Under a nonzero central projection z with the halving property (field H4 of the interface at z), for every n ≥ 1 there are u_1, …, u_n ∈ M with u_i* u_i = z, u_i* u_j = 0 for i ≠ j, and ∑ u_i u_i* = z. Proof: halve z = e + (z − e) with e ∼ z − e ∼ z, take partial isometries v_e : z → e, v_f : z → z − e, and iterate: u := (v_e, v_f u'_1, …, v_f u'_n) for u' a family of length n.