PhyslibAlpha.AlgebraicFramework.CStarAlgebra.OrderUnit

The self-adjoint part of a C⋆-algebra is an order-unit space

`selfAdjoint A`, for a unital C⋆-algebra `A`, is the physically meaningful home for the whole `OrderUnit`/`Effect`/`Weight`/`Channel`/`Measurement` framework built on top of it: the algebra `A` itself is *not* an order-unit space in that sense, since `x ≤ n • 1` forces `x` self-adjoint (`StarOrderedRing.le_iff`), so only the self-adjoint elements can ever be compared to `1` at all.

`1` bounds every self-adjoint element by `IsSelfAdjoint.le_algebraMap_norm_self`, giving `IsOrderUnit`. Archimedeanity is the one genuinely analytic fact: if `x ≤ ε • 1` for every `ε > 0`, then `x` is a limit of `ε • 1` as `ε → 0`, and `≤` is a closed relation (`OrderClosedTopology`, itself from the norm-closedness of the nonnegative cone, `isClosed_nonneg`), so the limit inequality `x ≤ 0` survives.

Main definitions

`selfAdjoint.instIsOrderUnit`, `selfAdjoint.instIsArchimedeanOrderUnit`

3 declarations

instance

Scalar multiplication by $r \ge 0$ is monotone on $\text{selfAdjoint}(A)$

#instPosSMulMono

In a unital $C^*$ -algebra $A$ , scalar multiplication by non-negative real numbers preserves the partial order on the set of self-adjoint elements $\text{selfAdjoint}(A)$ . Specifically, for any $r \in \mathbb{R}$ with $r \ge 0$ and any self-adjoint elements $x, y \in A$ , if $x \le y$ in the standard Loewner order, then $r \cdot x \le r \cdot y$ .

instance

The self-adjoint part of a unital $C^*$ -algebra is an order-unit space

#instIsOrderUnit

Let $A$ be a unital $C^*$ -algebra. The space of self-adjoint elements of $A$ , denoted by $\text{selfAdjoint } A$ , is an order-unit space. This means the identity element $1$ of the algebra acts as an order unit, such that for every self-adjoint element $x \in \text{selfAdjoint } A$ , there exists a natural number $n$ such that $x \leq n \cdot 1$ .

instance

`selfAdjoint A` is an Archimedean order-unit space

#instIsArchimedeanOrderUnit

Let $A$ be a unital $C^*$ -algebra. The space of self-adjoint elements of $A$ , denoted by `selfAdjoint A`, is an Archimedean order-unit space.

PhyslibAlpha.AlgebraicFramework.CStarAlgebra.OrderUnit

The self-adjoint part of a C⋆-algebra is an order-unit space

Main definitions

Scalar multiplication by r≥0r \ge 0r≥0 is monotone on selfAdjoint(A)\text{selfAdjoint}(A)selfAdjoint(A)

The self-adjoint part of a unital C∗C^*C∗-algebra is an order-unit space

`selfAdjoint A` is an Archimedean order-unit space

Scalar multiplication by $r \ge 0$ is monotone on $\text{selfAdjoint}(A)$

The self-adjoint part of a unital $C^*$ -algebra is an order-unit space