PhyslibAlpha.AlgebraicFramework.StarAlgebra.SelfAdjoint

Let $R$ be an additive group with a star-additive monoid structure. For any element $x \in R$, $x$ belongs to the set of self-adjoint elements $\text{selfAdjoint } R$ if and only if $x$ is self-adjoint (satisfies the predicate `IsSelfAdjoint x`).

Let $A$ be a star-algebra over a commutative ring $R$. For any element $x \in A$, $x$ belongs to the $R$-submodule of self-adjoint elements if and only if $x$ is a self-adjoint element of $A$ (i.e., $x \in \text{selfAdjoint } A$).

Given a star-algebra $A$ and a commutative ring $R$, let $\text{selfAdjoint } A = \{x \in A \mid x^* = x\}$ denote the set of self-adjoint elements. This definition provides the $R$-linear equivalence (isomorphism of $R$-modules) between the $R$-submodule structure of self-adjoint elements and the collection of self-adjoint elements viewed as a basic additive group. The map identifies an element $x$ in the submodule with itself in the set of self-adjoint elements.

Let $A$ be a star-algebra over a commutative ring $R$. The map $\text{submodulePLM} : \text{submodule } R A \to \text{selfAdjoint } A$ is a positive linear map from the $R$-submodule of self-adjoint elements of $A$ to the type of self-adjoint elements. It identifies an element $x$ in the submodule with itself in the set of self-adjoint elements $\text{selfAdjoint } A = \{x \in A \mid x^* = x\}$, preserving the $R$-linear structure and the property of monotonicity.

Given a star-algebra $A$ over a commutative ring $R$, this map is the inverse of the positive linear map `submodulePLM`. It identifies a self-adjoint element $x \in \text{selfAdjoint } A$ with its corresponding element in the $R$-submodule of self-adjoint elements. The map is constructed from the inverse of the $R$-linear equivalence `submoduleEquiv` and is shown to be monotone (order-preserving).

Let $A$ be an algebra over a ring $R$ equipped with an involution. The identity element $1$ of the algebra $A$ is a self-adjoint element. This definition provides the multiplicative identity instance for the $R$-submodule of self-adjoint elements in $A$, where the identity $1$ of the submodule corresponds to the identity $1$ of the underlying algebra.

Let $A$ be an algebra over a ring $R$ equipped with an involution. The identity element $1$ of the $R$-submodule of self-adjoint elements, when viewed as an element of the algebra $A$, is equal to the identity element $1$ of the algebra $A$.

Let $A$ be a star-algebra over a commutative ring $R$. Let $\text{submoduleEquiv}$ be the $R$-linear equivalence between the $R$-submodule of self-adjoint elements and the type of self-adjoint elements in $A$. The image of the identity element $1$ of the submodule under this equivalence is equal to the identity element $1$ of the algebra $A$.

Let $R$ be a commutative ring and $A$ a star-algebra. Let $\phi: \text{selfAdjoint.submodule } R \ A \simeq_R \text{selfAdjoint } A$ be the $R$-linear equivalence between the $R$-submodule of self-adjoint elements and the type of self-adjoint elements. Then, the image of the identity element $1 \in \text{selfAdjoint } A$ under the inverse equivalence $\phi^{-1}$, when viewed as an element of the algebra $A$, is equal to $1$.

Let $A$ be a star-algebra over a ring $R$. This definition is the $R$-linear isomorphism between the $R$-submodule of self-adjoint elements in $A$ and the type $\text{selfAdjoint } A$ of self-adjoint elements, considered as a unital positive linear map. It maps the identity element $1$ to $1$ and is monotone with respect to the partial order on self-adjoint elements.

Let $A$ be a star-algebra over a commutative ring $R$. The function `submoduleUPLMSymm` is the unital positive $R$-linear map from the set of self-adjoint elements $\text{selfAdjoint } A = \{x \in A \mid x^* = x\}$ to the $R$-submodule of self-adjoint elements $\text{submodule } R \ A$. It is defined as the inverse of the map `submoduleUPLM`. As a unital positive linear map, it preserves the identity element $1$ and is monotone (positive) with respect to the natural ordering of self-adjoint elements.

The unital positive $\mathbb{R}$-linear map from the subspace of self-adjoint complex numbers $\text{selfAdjoint}(\mathbb{C}) = \{z \in \mathbb{C} \mid \bar{z} = z\}$ to the real numbers $\mathbb{R}$. This map identifies each self-adjoint complex number with its corresponding real value.