Projections in C⋆-algebras

Here we collect results about projections specific to C⋆-algebras.

Main results

• isStarProjection_iff_isIdempotentElem_and_isStarNormal: star projections are precisely idempotent normal elements.
• IsStarProjection.le_tfae: for star projections p and q, the following are equivalent:
  • p ≤ q
  • q * p = p
  • p * q = p
  • q - p is a star projection
  • q - p is an idempotent element

theorem isStarProjection_iff_quasispectrum_subset_and_isSelfAdjoint {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {p : A} : IsStarProjection p ↔ quasispectrum ℝ p ⊆ {0, 1} ∧ IsSelfAdjoint p

theorem IsIdempotentElem.isSelfAdjoint_iff_isStarNormal {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {p : A} (hp : IsIdempotentElem p) : IsSelfAdjoint p ↔ IsStarNormal p

An idempotent element in a non-unital C⋆-algebra is self-adjoint iff it is normal.

theorem isStarProjection_iff_isIdempotentElem_and_isStarNormal {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {p : A} : IsStarProjection p ↔ IsIdempotentElem p ∧ IsStarNormal p

An element in a non-unital C⋆-algebra is a star projection if and only if it is idempotent and normal.

theorem isStarProjection_iff_quasispectrum_subset_and_isStarNormal {A : Type u_1} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {p : A} : IsStarProjection p ↔ quasispectrum ℂ p ⊆ {0, 1} ∧ IsStarNormal p

theorem isStarProjection_iff_spectrum_subset_and_isSelfAdjoint {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℝ A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {p : A} : IsStarProjection p ↔ spectrum ℝ p ⊆ {0, 1} ∧ IsSelfAdjoint p

theorem isStarProjection_iff_spectrum_subset_and_isStarNormal {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {p : A} : IsStarProjection p ↔ spectrum ℂ p ⊆ {0, 1} ∧ IsStarNormal p

theorem IsStarProjection.le_tfae {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_iff_mul_eq_right {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p q : A} (hp : IsStarProjection p) (hq : IsStarProjection q) : p ≤ q ↔ q * p = p

theorem IsStarProjection.le_iff_mul_eq_left {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p q : A} (hp : IsStarProjection p) (hq : IsStarProjection q) : p ≤ q ↔ p * q = p

theorem IsStarProjection.le_iff_sub {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p q : A} (hp : IsStarProjection p) (hq : IsStarProjection q) : p ≤ q ↔ IsStarProjection (q - p)

theorem IsStarProjection.le_iff_idempotent_sub {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p q : A} (hp : IsStarProjection p) (hq : IsStarProjection q) : p ≤ q ↔ IsIdempotentElem (q - p)

theorem IsStarProjection.commute_of_le {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p q : A} (hp : IsStarProjection p) (hq : IsStarProjection q) (h : p ≤ q) : Commute p q