4. Projection Lemmas🔗

Let \mathcal{A} be a unital C^*-algebra in this chapter. Here we collect relevant results about (self-adjoint) projections in \mathcal{A}. Recall that an element p in a C^*-algebra is a projection if p^2 = p^* = p. By the Spectral Mapping Theorem (or using the full Gelfand Duality), a self-adjoint element a \in \mathcal{A} is a projection if and only if the spectrum of a is contained in \{0, 1\}.

Lemma4.1

uses 1used by 1✓L∃∀N

Tagsmathlib

For all projections p \in \mathcal{A}, p \le 1.

Lean code for Lemma4.1●1 theorem

theoremdefined in Mathlib/Algebra/Order/Star/Basic.lean

complete

theorem IsStarProjection.le_one.{u_1} {R : Type u_1} [Ring R] [PartialOrder R]
  [StarRing R] [StarOrderedRing R] {p : R} (hp : IsStarProjection p) :
  p ≤ 1

theorem IsStarProjection.le_one.{u_1}
  {R : Type u_1} [Ring R] [PartialOrder R]
  [StarRing R] [StarOrderedRing R] {p : R}
  (hp : IsStarProjection p) : p ≤ 1

Proof for Lemma 4.1

uses 0

We can get this by Gelfand duality (cf. Sakai 1.2.3) and Lemma 3.3.

Lemma4.2

Statement uses 2

Statement dependency previews

Preview

Corollary 3.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 3

Reverse dependency previews

Preview

Corollary 4.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Let \mathcal{A} be a C^*-algebra and p, q \in \mathcal{A} be projections. Then p - q \ge 0 if and only if qp = pq = q.

Lean code for Lemma4.2●1 theorem

theoremdefined in Mathlib/Analysis/CStarAlgebra/Projection.lean

complete

theorem IsStarProjection.le_tfae.{u_1} {A : Type u_1} [NonUnitalCStarAlgebra A]
  [PartialOrder A] [StarOrderedRing A] {p q : A}
  (hp : IsStarProjection p) (hq : IsStarProjection q) :
  [p ≤ q, q * p = p, p * q = p, IsStarProjection (q - p),
      IsIdempotentElem (q - p)].TFAE

theorem IsStarProjection.le_tfae.{u_1}
  {A : Type u_1} [NonUnitalCStarAlgebra A]
  [PartialOrder A] [StarOrderedRing A]
  {p q : A} (hp : IsStarProjection p)
  (hq : IsStarProjection q) :
  [p ≤ q, q * p = p, p * q = p,
      IsStarProjection (q - p),
      IsIdempotentElem (q - p)].TFAE

Proof for Lemma 4.2

uses 0

By Corollary 3.2, if p - q \ge 0 then q(p - q)q = qpq - q^3 = qpq - q \ge 0. By Lemma 4.1, we have p \le 1, and employing Corollary 3.2 we obtain qpq \le q1q = q. Since qpq \ge q and qpq \le q we have qpq = q, which implies that q(p - q)q = 0. By the C^*-property of the norm, we have \|(p - q)^{1/2} q\|^2 = \|q(p - q)q\| = 0 and so (p - q)^{1/2} q = 0 and therefore (p - q)q = (p - q)^{1/2}(p - q)^{1/2} q = 0. It follows that pq = q, and taking adjoints, qp = q. Conversely, if qp = pq = q, one easily checks that p - q is a projection, and so its spectrum is contained in \{0, 1\} and it is positive.

Corollary4.3

uses 1

Used by 2

Reverse dependency previews

Preview

Lemma 7.2.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

For all projections p, q \in \mathcal{A} such that q \le p, p - q is a projection.

Lean code for Corollary4.3●1 theorem

theoremdefined in Mathlib/Analysis/CStarAlgebra/Projection.lean

complete

theorem IsStarProjection.le_tfae.{u_1} {A : Type u_1} [NonUnitalCStarAlgebra A]
  [PartialOrder A] [StarOrderedRing A] {p q : A}
  (hp : IsStarProjection p) (hq : IsStarProjection q) :
  [p ≤ q, q * p = p, p * q = p, IsStarProjection (q - p),
      IsIdempotentElem (q - p)].TFAE

theorem IsStarProjection.le_tfae.{u_1}
  {A : Type u_1} [NonUnitalCStarAlgebra A]
  [PartialOrder A] [StarOrderedRing A]
  {p q : A} (hp : IsStarProjection p)
  (hq : IsStarProjection q) :
  [p ≤ q, q * p = p, p * q = p,
      IsStarProjection (q - p),
      IsIdempotentElem (q - p)].TFAE

The next result is specific to W^*-algebras. Sakai obtains it from the fact that the projections of a W^*-algebra form a complete lattice (Proposition 8.2.4, via the correspondence between \sigma-closed one-sided ideals and projections in Proposition 8.2.3). The proof of Theorem 7.2.6 only needs suprema of directed sets, for which the following direct argument suffices.

Lemma4.4

Statement uses 3

Statement dependency previews

Preview

Lemma 2.2.6

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Lemma 7.2.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

In a W^*-algebra M, the supremum of a nonempty directed set of projections is a projection.

Lean code for Lemma4.4●1 theorem

theoremdefined in LeanOA/Ultraweak/Normal.lean

complete

theorem Ultraweak.isStarProjection_of_isLUB.{u_1, u_2} {M : Type u_1}
  {P : Type u_2} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M]
  [NormedAddCommGroup P] [NormedSpace ℂ P] [CompleteSpace P]
  [Predual ℂ M P] {d : Set M} (hne : d.Nonempty)
  (hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d)
  (hdp : ∀ q ∈ d, IsStarProjection q) {e : M} (he : IsLUB d e) :
  IsStarProjection e

theorem Ultraweak.isStarProjection_of_isLUB.{u_1,
    u_2}
  {M : Type u_1} {P : Type u_2}
  [CStarAlgebra M] [PartialOrder M]
  [StarOrderedRing M]
  [NormedAddCommGroup P] [NormedSpace ℂ P]
  [CompleteSpace P] [Predual ℂ M P]
  {d : Set M} (hne : d.Nonempty)
  (hd :
    DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d)
  (hdp : ∀ q ∈ d, IsStarProjection q)
  {e : M} (he : IsLUB d e) :
  IsStarProjection e

In a W⋆-algebra, the supremum of a nonempty directed set of projections is a projection.

Proof for Lemma 4.4

uses 0

Let e be the supremum of the directed set (q_\alpha) of projections; it is the \sigma-limit of the q_\alpha by Theorem 7.1.4, hence is self-adjoint by Lemma 5.2. Since q_\alpha \le e \le 1, we have 0 \le q_\alpha (1 - e) q_\alpha \le q_\alpha (1 - q_\alpha) q_\alpha = 0, and so (1 - e) q_\alpha = 0 by the C^*-identity, i.e., e q_\alpha = q_\alpha. Multiplication is separately \sigma-continuous (Lemma 2.2.6), so q_\alpha = e q_\alpha \to e^2, but also q_\alpha \to e. Hence e^2 = e.