PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.Projection

For a $C^*$-algebra $A$ equipped with a partial order, a **projection** is an element $p$ in the self-adjoint part of $A$ that is an effect (satisfying $0 \le p \le 1$) and is idempotent, meaning it satisfies the condition $p^2 = p$.

This definition provides a canonical coercion from a projection $p$ in a $C^*$-algebra $A$ to an effect in the self-adjoint part of $A$. A projection is an element of the self-adjoint part that is both an effect (satisfying $0 \le p \le 1$) and idempotent ($p^2 = p$). This mapping allows a projection to be treated simply as an element of the interval $[0, 1]$ within the self-adjoint part of the algebra, effectively "forgetting" the idempotence property.

Let $A$ be a $C^*$-algebra. For any two projections $p, q$ in $A$, if they are equal when regarded as effects in the self-adjoint part of $A$, then $p = q$.

Let $A$ be a $C^*$-algebra. Every projection $p \in A$ is a sharp effect. Specifically, if $p$ is a self-adjoint element of $A$ such that $p^2 = p$ (which implies $0 \le p \le 1$), then $p$ is an extreme point of the effect interval $[0, 1]$ in the space of self-adjoint elements $\text{selfAdjoint } A$.

Given a projection $p$ in a unital $C^*$-algebra $A$, its complement is the projection defined as $1 - p$, where $1$ is the identity element of the algebra.

For any projection $p$ in a $C^*$-algebra $A$, taking the complement of its complement returns the original projection $p$. If the complement of $p$ is defined as $1 - p$, then $1 - (1 - p) = p$.

Let $A$ be a $C^*$-algebra. For any projection $p$ in $A$, the real spectrum of $p$, denoted as $\sigma_{\mathbb{R}}(p)$, is a subset of $\{0, 1\}$.