PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Power.Generated

A real submodule $J \subseteq E$ is a Jordan submodule if it contains the identity element $1$ and is closed under the Jordan product, meaning that for any $x, y \in J$, their product $x \circ y$ is also in $J$.

Given a set $s \subseteq E$ in a Jordan algebra $E$ over $\mathbb{R}$, the Jordan subalgebra generated by $s$ is the smallest real submodule of $E$ that contains $s$, contains the identity element $1$, and is closed under the Jordan product $x \circ y$. It is defined as the intersection of all Jordan submodules $J$ such that $s \subseteq J$.

For any subset $s \subseteq E$ of a Jordan algebra $E$, the set $s$ is contained in the Jordan subalgebra generated by $s$.

Let $E$ be a Jordan algebra and $s \subseteq E$ be a set. The identity element $1 \in E$ is contained in the Jordan subalgebra generated by $s$.

Let $E$ be a Jordan algebra over $\mathbb{R}$ and $s \subseteq E$ be a set. If $x$ and $y$ are elements of the Jordan subalgebra generated by $s$ (denoted as `generatedBySet s`), then their Jordan product $x \cdot y$ is also an element of the Jordan subalgebra generated by $s$. In other words, the Jordan subalgebra generated by a set is closed under the Jordan product.

Let $E$ be a Jordan algebra over $\mathbb{R}$ and $s \subseteq E$ be a set. The submodule generated by $s$, denoted as $\text{generatedBySet}(s)$, is a Jordan submodule. That is, it contains the identity element $1$ and is closed under the Jordan product $x \circ y$.

Let $E$ be a Jordan algebra over $\mathbb{R}$. Let $s \subseteq E$ be a set of elements and $J \subseteq E$ be a real submodule. If $s$ is contained in $J$ and $J$ is a Jordan submodule (meaning it contains the identity element $1$ and is closed under the Jordan product $x \circ y$), then the Jordan subalgebra generated by $s$ is contained in $J$.

Let $E$ be a Jordan algebra over $\mathbb{R}$. For any two sets of elements $s, t \subseteq E$, if $s \subseteq t$, then the Jordan subalgebra generated by $s$ is contained within the Jordan subalgebra generated by $t$, denoted as $\text{generatedBySet}(s) \le \text{generatedBySet}(t)$.

Given a set of observables $s \subseteq E$ in a Jordan algebra $E$, `GeneratedBySet s` is the carrier type representing the Jordan subalgebra generated by $s$. This type consists of the elements belonging to the smallest real submodule of $E$ that contains $s$, contains the identity element $1$, and is closed under the Jordan product $x \circ y$.

Given a set $s \subseteq E$ in a Jordan algebra $E$, this defines the multiplication operation for the Jordan subalgebra $\text{GeneratedBySet}(s)$. For any two elements $x, y$ in this subalgebra, their product is the Jordan product $x \circ y$ defined in $E$.

Let $E$ be a Jordan algebra and $s \subseteq E$ be a set. For any two elements $x$ and $y$ in the Jordan subalgebra generated by $s$, the Jordan product $x \circ y$ computed within the subalgebra is equal to the Jordan product $x \circ y$ computed in the parent algebra $E$.

Given a set $s$ in a Jordan algebra $E$, the identity element $1 \in E$ is contained within the Jordan subalgebra generated by $s$. This instance defines the identity element $1$ for the type `GeneratedBySet s`, representing that subalgebra.

Let $E$ be a Jordan algebra and $s \subseteq E$ be a set. Let $\text{GeneratedBySet } s$ be the Jordan subalgebra generated by $s$ (the smallest unital submodule containing $s$ that is closed under the Jordan product). The identity element $1$ of the Jordan subalgebra $\text{GeneratedBySet } s$, when viewed as an element of the ambient algebra $E$, is equal to the identity element $1$ of $E$.

Given a set $s$ in a Jordan algebra $E$ over $\mathbb{R}$, let $\text{GeneratedBySet } s$ be the Jordan subalgebra generated by $s$ (the smallest unital submodule containing $s$ that is closed under the Jordan product). This definition is the canonical $\mathbb{R}$-linear inclusion map from the generated Jordan subalgebra $\text{GeneratedBySet } s$ into its ambient algebra $E$, which maps each element $x$ in the subalgebra to itself as an element of $E$.

Let $s$ be a subset of a Jordan algebra $E$ over $\mathbb{R}$. For any element $x$ in the Jordan subalgebra generated by $s$ ($\text{GeneratedBySet } s$), the application of the inclusion map $\iota: \text{GeneratedBySet } s \to E$ to $x$ is equal to the element $x$ viewed as an element of the ambient algebra $E$.

Let $E$ be a Jordan algebra over $\mathbb{R}$ and $s \subseteq E$ be a set of elements. The canonical inclusion map $\text{inclusion } s$ from the Jordan subalgebra generated by $s$ into $E$ is injective.

The Jordan subalgebra generated by a set $s$, denoted as $\text{GeneratedBySet}(s)$, forms a unital commutative non-associative ring. The operations of addition and multiplication (the Jordan product $\circ$), as well as the multiplicative identity $1$, are inherited from the ambient Jordan algebra. This structure satisfies commutativity and distributivity, but does not necessarily satisfy associativity.

Let $E$ be a Jordan algebra over $\mathbb{R}$ and $s \subseteq E$ be a set of elements. Let $\text{GeneratedBySet } s$ be the Jordan subalgebra generated by $s$ (the smallest unital submodule containing $s$ that is closed under the Jordan product). This definition is the canonical inclusion map from $\text{GeneratedBySet } s$ into its ambient algebra $E$, bundled as a unital $\mathbb{R}$-linear Jordan homomorphism. It maps each element $x \in \text{GeneratedBySet } s$ to itself in $E$, preserving the identity element $1$ and the Jordan product $x \circ y$.

Let $E$ be a Jordan algebra over $\mathbb{R}$ and $s \subseteq E$ be a set of elements. Let $\text{GeneratedBySet}(s)$ be the Jordan subalgebra generated by $s$. For any scalar $r \in \mathbb{R}$ and any elements $x, y \in \text{GeneratedBySet}(s)$, the scalar multiplication by $r$ commutes with the Jordan product such that $r \cdot (x \circ y) = x \circ (r \cdot y)$.

Let $E$ be a Jordan algebra over the real numbers $\mathbb{R}$, and let $s \subseteq E$ be a set of elements. Let $J$ be the Jordan subalgebra generated by $s$ (defined as the smallest unital submodule containing $s$ that is closed under the Jordan product). For any scalar $r \in \mathbb{R}$ and any elements $x, y \in J$, the scalar multiplication and Jordan product $\circ$ satisfy the identity $(r \cdot x) \circ y = r \cdot (x \circ y)$.

Let $E$ be a Jordan algebra and $s \subseteq E$ be a set of elements. The Jordan subalgebra generated by $s$, denoted as $\text{GeneratedBySet}(s)$, satisfies the Jordan identity. That is, for all $x, y \in \text{GeneratedBySet}(s)$, the Jordan product $\circ$ satisfies $(x^2 \circ y) \circ x = x^2 \circ (y \circ x)$, where $x^2 = x \circ x$.

Let $E$ be a Jordan algebra over $\mathbb{R}$ and $s \subseteq E$. Let $\text{GeneratedBySet } s$ be the Jordan subalgebra generated by $s$, and let $\iota : \text{GeneratedBySet } s \to E$ be the canonical inclusion map. Then the image of the identity element $1$ of the subalgebra under the inclusion is the identity element $1$ of $E$, i.e., $\iota(1) = 1$.

Let $E$ be a Jordan algebra over $\mathbb{R}$ and $s \subseteq E$ be a set. Let $\text{GeneratedBySet } s$ denote the Jordan subalgebra generated by $s$, and let $\iota : \text{GeneratedBySet } s \to E$ be the canonical inclusion map. For any elements $x, y \in \text{GeneratedBySet } s$, the inclusion map preserves the Jordan product: $$\iota(x \circ y) = \iota(x) \circ \iota(y)$$ where $\circ$ denotes the Jordan product.

Let $E$ be a Jordan algebra over $\mathbb{R}$. For any element $a \in E$, the Jordan subalgebra generated by the singleton set $\{a\}$ is equal to the $\mathbb{R}$-submodule spanned by the set of all Jordan powers $\{a^n\}_{n \in \mathbb{N}}$ (where $a^0 = 1$ and $a^{n+1} = a \circ a^n$).