Compression: linearity, positivity, and the identity on an invariant subspace

noncomputable def Orthogonalization.Blocks.compressToₗ {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (K : Submodule ℂ H) [CompleteSpace ↥K] : (H →L[ℂ] H) →ₗ[ℂ] ↥K →L[ℂ] ↥K

Compression to K as a ℂ-linear map B(H) → B(K).

Equations

• Orthogonalization.Blocks.compressToₗ K = { toFun := CommutingRepetition.VN.compressTo K, map_add' := ⋯, map_smul' := ⋯ }

theorem Orthogonalization.Blocks.compressToₗ_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (K : Submodule ℂ H) [CompleteSpace ↥K] (T : H →L[ℂ] H) : (compressToₗ K) T = CommutingRepetition.VN.compressTo K T

theorem Orthogonalization.Blocks.compressTo_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (K : Submodule ℂ H) [CompleteSpace ↥K] (S T : H →L[ℂ] H) : CommutingRepetition.VN.compressTo K (S - T) = CommutingRepetition.VN.compressTo K S - CommutingRepetition.VN.compressTo K T

theorem Orthogonalization.Blocks.compressTo_sum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (K : Submodule ℂ H) [CompleteSpace ↥K] {ι : Type u_2} (s : Finset ι) (f : ι → H →L[ℂ] H) : CommutingRepetition.VN.compressTo K (∑ i ∈ s, f i) = ∑ i ∈ s, CommutingRepetition.VN.compressTo K (f i)

theorem Orthogonalization.Blocks.compressTo_eq_one_of_forall_apply_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (K : Submodule ℂ H) [CompleteSpace ↥K] {T : H →L[ℂ] H} (hT : ∀ v ∈ K, T v = v) : CommutingRepetition.VN.compressTo K T = 1

An operator acting as the identity on K compresses to 1.

theorem Orthogonalization.Blocks.compressTo_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (K : Submodule ℂ H) [CompleteSpace ↥K] {T : H →L[ℂ] H} (hT : 0 ≤ T) : 0 ≤ CommutingRepetition.VN.compressTo K T

Compression preserves positivity (T = √T * √T).

The inverse of a bijective compression

theorem Orthogonalization.Blocks.mul_eq_self_left {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} (hz : IsCentralProj M z) {x : H →L[ℂ] H} (hx : x ∈ M) (hxz : x * z = x) : z * x = x

An element of M supported in z on the right is supported in z on the left too (z is central).

noncomputable def Orthogonalization.Blocks.liftOp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (y : ↥L →L[ℂ] ↥L) : H →L[ℂ] H

The preimage in M z = {x ∈ M | x z = x} of an operator on L (chosen by hsurj).

Equations

• Orthogonalization.Blocks.liftOp hsurj y = ⋯.choose

theorem Orthogonalization.Blocks.liftOp_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (y : ↥L →L[ℂ] ↥L) : liftOp hsurj y ∈ M

theorem Orthogonalization.Blocks.liftOp_mul_z {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (y : ↥L →L[ℂ] ↥L) : liftOp hsurj y * z = liftOp hsurj y

theorem Orthogonalization.Blocks.compressTo_liftOp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (y : ↥L →L[ℂ] ↥L) : CommutingRepetition.VN.compressTo L (liftOp hsurj y) = y

theorem Orthogonalization.Blocks.liftOp_eq_of {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) {x : H →L[ℂ] H} {y : ↥L →L[ℂ] ↥L} (hx : x ∈ M) (hxz : x * z = x) (hxy : CommutingRepetition.VN.compressTo L x = y) : liftOp hsurj y = x

Uniqueness: an element of M z compressing to y is liftOp y.

theorem Orthogonalization.Blocks.liftOp_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) (y y' : ↥L →L[ℂ] ↥L) : liftOp hsurj (y + y') = liftOp hsurj y + liftOp hsurj y'

theorem Orthogonalization.Blocks.liftOp_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) (c : ℂ) (y : ↥L →L[ℂ] ↥L) : liftOp hsurj (c • y) = c • liftOp hsurj y

noncomputable def Orthogonalization.Blocks.liftOpₗ {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) : (↥L →L[ℂ] ↥L) →ₗ[ℂ] H →L[ℂ] H

The inverse of a bijective compression, as a ℂ-linear map B(L) → B(H).

Equations

• Orthogonalization.Blocks.liftOpₗ hsurj hinj = { toFun := Orthogonalization.Blocks.liftOp hsurj, map_add' := ⋯, map_smul' := ⋯ }

theorem Orthogonalization.Blocks.liftOpₗ_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) (y : ↥L →L[ℂ] ↥L) : (liftOpₗ hsurj hinj) y = liftOp hsurj y

theorem Orthogonalization.Blocks.liftOp_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) (y y' : ↥L →L[ℂ] ↥L) : liftOp hsurj (y - y') = liftOp hsurj y - liftOp hsurj y'

theorem Orthogonalization.Blocks.liftOp_sum {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) {ι : Type u_2} (s : Finset ι) (f : ι → ↥L →L[ℂ] ↥L) : liftOp hsurj (∑ i ∈ s, f i) = ∑ i ∈ s, liftOp hsurj (f i)

theorem Orthogonalization.Blocks.liftOp_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) (hLM : ∀ x ∈ M, ∀ v ∈ L, x v ∈ L) (y y' : ↥L →L[ℂ] ↥L) : liftOp hsurj (y * y') = liftOp hsurj y * liftOp hsurj y'

theorem Orthogonalization.Blocks.liftOp_star {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) (hz : IsCentralProj M z) (y : ↥L →L[ℂ] ↥L) : liftOp hsurj (star y) = star (liftOp hsurj y)

theorem Orthogonalization.Blocks.liftOp_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) (hz : IsCentralProj M z) (hLz : ∀ v ∈ L, z v = v) : liftOp hsurj 1 = z

theorem Orthogonalization.Blocks.isStarProjection_liftOp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) (hz : IsCentralProj M z) (hLM : ∀ x ∈ M, ∀ v ∈ L, x v ∈ L) {y : ↥L →L[ℂ] ↥L} (hy : IsStarProjection y) : IsStarProjection (liftOp hsurj y)

Projections of B(L) lift to projections of M.

noncomputable def Orthogonalization.Blocks.liftFunctional {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) : (↥L →L[ℂ] ↥L) →ₗ[ℂ] ℂ

The transported functional φ ∘ liftOp on B(L).

Equations

• Orthogonalization.Blocks.liftFunctional hsurj hinj φ = φ ∘ₗ Orthogonalization.Blocks.liftOpₗ hsurj hinj

theorem Orthogonalization.Blocks.liftFunctional_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (y : ↥L →L[ℂ] ↥L) : (liftFunctional hsurj hinj φ) y = φ (liftOp hsurj y)

theorem Orthogonalization.Blocks.liftFunctional_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) (hz : IsCentralProj M z) (hLM : ∀ x ∈ M, ∀ v ∈ L, x v ∈ L) {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ x ∈ M, 0 ≤ φ (star x * x)) (y : ↥L →L[ℂ] ↥L) : 0 ≤ (liftFunctional hsurj hinj φ) (star y * y)

A functional positive on M transports to a functional positive on all of B(L).

theorem Orthogonalization.Blocks.liftFunctional_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z : H →L[ℂ] H} {L : Submodule ℂ H} (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) (hz : IsCentralProj M z) (hLz : ∀ v ∈ L, z v = v) {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφz : φ z = 1) : (liftFunctional hsurj hinj φ) 1 = 1

The transport theorem

theorem Orthogonalization.Blocks.orthAt_of_compress_bijective {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (M : VonNeumannAlgebra H) {z : H →L[ℂ] H} (hz : IsCentralProj M z) (L : Submodule ℂ H) (hLz : ∀ v ∈ L, z v = v) (hLM : ∀ x ∈ M, ∀ v ∈ L, x v ∈ L) (hinj : ∀ x ∈ M, x * z = x → CommutingRepetition.VN.compressTo L x = 0 → x = 0) (hsurj : ∀ (y : ↥L →L[ℂ] ↥L), ∃ x ∈ M, x * z = x ∧ CommutingRepetition.VN.compressTo L x = y) (ι : Type u_2) [Fintype ι] : OrthAt M z ι

Transport of Theorem 1.2 through a bijective compression. If z is a central projection of M, L ≤ range z is an M-invariant subspace, and compression to L maps {x ∈ M | x z = x} bijectively onto B(L), then Theorem 1.2 holds at z.