PhyslibAlpha.AlgebraicFramework.StarAlgebra.Restrict

Given a positive linear map $f : E_1 \to E_2$ and submodules $F_1 \subseteq E_1$ and $F_2 \subseteq E_2$ over a ring $S$, such that $f$ maps $F_1$ into $F_2$ (i.e., $\forall x \in F_1, f(x) \in F_2$), this definition constructs the restriction $f|_{F_1} : F_1 \to F_2$ as a positive linear map.

Given a unital positive linear map $f : E_1 \to E_2$ over a ring $R$, and submodules $F_1 \subseteq E_1$ and $F_2 \subseteq E_2$ over a ring $S$, this definition constructs the restriction $f|_{F_1} : F_1 \to F_2$ as a unital positive linear map. This construction requires that $F_1$ and $F_2$ possess multiplicative identities $1_{F_1}$ and $1_{F_2}$ that coincide with the identities of the parent spaces (i.e., $1_{F_1} = 1_{E_1}$ and $1_{F_2} = 1_{E_2}$), and that $f$ maps elements of $F_1$ into $F_2$ ($\forall x \in F_1, f(x) \in F_2$).

Given a complex-linear positive map $f : A_1 \to A_2$ between two algebras, this definition constructs the induced real-linear positive map $f|_{sa} : \text{selfAdjoint } A_1 \to \text{selfAdjoint } A_2$. This map restricts the domain and codomain of $f$ to the respective submodules of self-adjoint elements, utilizing the property that positive linear maps preserve self-adjointness.

Let $A_1$ and $A_2$ be complex algebras, and let $f: A_1 \to A_2$ be a complex-linear positive map. Let $f|_{sa}: \text{selfAdjoint } A_1 \to \text{selfAdjoint } A_2$ be the restriction of $f$ to the submodules of self-adjoint elements. For any self-adjoint element $x \in \text{selfAdjoint } A_1$, the application of the restricted map $f|_{sa}$ to $x$ is equal to the application of the original map $f$ to $x$, i.e., $f|_{sa}(x) = f(x)$.

Given a positive complex-linear functional $f : A_1 \to \mathbb{C}$ on a $*$-algebra $A_1$, this definition constructs the induced positive real-linear functional $f|_{sa} : \text{selfAdjoint } A_1 \to \mathbb{R}$. The map restricts the domain of $f$ to the submodule of self-adjoint elements and identifies the codomain with $\mathbb{R}$, utilizing the property that a positive map sends self-adjoint elements to self-adjoint elements (which, in the case of $\mathbb{C}$, are the real numbers).

Let $A_1$ be a complex $*$-algebra and $f: A_1 \to \mathbb{C}$ be a positive complex-linear functional. Let $f|_{sa} : \text{selfAdjoint } A_1 \to \mathbb{R}$ be the restriction of $f$ to the submodule of self-adjoint elements of $A_1$. For any $x \in \text{selfAdjoint } A_1$, the value of the restricted functional $f|_{sa}(x)$, when considered as a complex number, is equal to $f(x)$.

Given a unital positive linear map $f : A_1 \to A_2$ between complex $*$-algebras, this definition constructs the restriction of $f$ to the submodules of self-adjoint elements. The resulting map is a unital positive real-linear map from $\text{selfAdjoint } A_1$ to $\text{selfAdjoint } A_2$. This relies on the property that a positive linear map preserves self-adjointness and the identity.

Let $A_1$ and $A_2$ be complex $*$-algebras and $f: A_1 \to A_2$ be a unital positive linear map. Let $f|_{\text{sa}}: \text{selfAdjoint}(A_1) \to \text{selfAdjoint}(A_2)$ denote the restriction of $f$ to the submodules of self-adjoint elements. For any self-adjoint element $x \in \text{selfAdjoint}(A_1)$, it holds that $f|_{\text{sa}}(x) = f(x)$.

Given a unital positive complex-linear functional $f : A_1 \to \mathbb{C}$ on a complex $*$-algebra $A_1$, this definition constructs the restriction of $f$ to the real subspace of self-adjoint elements $\text{selfAdjoint } A_1$. Since a positive linear map sends self-adjoint elements to self-adjoint elements, and the self-adjoint elements of $\mathbb{C}$ are the real numbers $\mathbb{R}$, the resulting map is a unital positive real-linear functional from $\text{selfAdjoint } A_1$ to $\mathbb{R}$.

Let $A_1$ be a complex $*$-algebra and let $f : A_1 \to \mathbb{C}$ be a unital positive linear map. Let $f|_{\text{sa}} : \text{selfAdjoint } A_1 \to \mathbb{R}$ be the restriction of $f$ to the submodule of self-adjoint elements of $A_1$ (which maps to $\mathbb{R}$ because positive maps preserve self-adjointness and the self-adjoint elements of $\mathbb{C}$ are the real numbers $\mathbb{R}$). For any self-adjoint element $x \in \text{selfAdjoint } A_1$, the value $f|_{\text{sa}}(x)$, when viewed as a complex number, is equal to $f(x)$.