PhyslibAlpha.AlgebraicFramework.CStarAlgebra.Projection

For a $C^*$-algebra $A$, a **projection** is an effect $p$ in the self-adjoint part of $A$ that is idempotent, satisfying the condition $p^2 = p$. An effect is defined as a self-adjoint element $p$ such that $0 \le p \le 1$. Thus, a projection is a self-adjoint element $p \in A$ that satisfies $p^2 = p$ (which implies $0 \le p \le 1$ in a $C^*$-algebra).

For a $C^*$-algebra $A$, this is the canonical coercion (inclusion) that maps a projection $p \in \text{Projection}(A)$ to its underlying element in the set of effects $\text{Effect}(\text{selfAdjoint } A)$, effectively forgetting the idempotence condition $p^2 = p$.

Let $A$ be a $C^*$-algebra. For any two projections $p, q \in \text{Projection}(A)$, if they are equal when viewed as effects (i.e., as elements of the self-adjoint part of $A$ satisfying $0 \le p, q \le 1$), then $p = q$ as projections.

Let $A$ be a $C^*$-algebra. Every projection $p \in A$ is a sharp effect, meaning it cannot be expressed as a non-trivial mixture (convex combination) of two distinct effects. That is, if $p = \lambda q + (1 - \lambda) r$ for some effects $q, r$ and $0 < \lambda < 1$, then $q = r = p$.

For a projection $p$ in a $C^*$-algebra $A$, its complementary projection is defined as $1 - p$.

For any projection $p$ in a $C^*$-algebra $A$, taking the complement of its complement returns the original projection $p$.

Let $A$ be a $C^*$-algebra and $p \in A$ be a projection (a self-adjoint element satisfying $p^2 = p$). The spectrum of $p$ over the real numbers, denoted $\sigma(p)$, is a subset of $\{0, 1\}$. That is, $\sigma(p) \subseteq \{0, 1\}$.