PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.FreeJordanTwo

Let $\mathcal{R}$ be the set of raw terms (denoted as `RawTwo`) for a non-associative algebra generated by a formal unit and two letters. The relation `FreeJordanTwoRel` is the inductive relation on $\mathcal{R}$ that generates the congruence for the free unital real Jordan algebra. This relation identifies terms according to the axioms of a unital commutative Jordan algebra, including the commutativity of multiplication ($a \circ b = b \circ a$), the Jordan identity $((a \circ a) \circ b) \circ a = (a \circ a) \circ (b \circ a)$, and the properties of a unit element ($1 \circ a = a$).

Let $\mathcal{R}$ be the set of raw terms (denoted as `RawTwo`) for a non-associative algebra generated by a formal unit and two letters. Let $\sim$ denote the relation `FreeJordanTwoRel` that defines the congruence for the free unital real Jordan algebra. For any terms $a, b, c \in \mathcal{R}$, if $b \sim c$, then $a + b \sim a + c$.

Let $\mathcal{R}$ be the set of raw terms (denoted as `RawTwo`) used in the construction of the free unital Jordan algebra on two generators. Let $\sim$ denote the relation `FreeJordanTwoRel` that defines the congruence for this algebra. For any terms $a, b \in \mathcal{R}$, if $a \sim b$, then $-a \sim -b$.

Let $\mathcal{R}$ be the set of raw terms (denoted as `RawTwo`) used in the construction of the free unital Jordan algebra on two generators. Let $\sim$ denote the relation `FreeJordanTwoRel` that defines the congruence for this algebra. For any terms $a, b, c \in \mathcal{R}$, if $b \sim c$, then $a - b \sim a - c$.

Let $\mathcal{R}$ be the set of raw terms (denoted as `RawTwo`) used in the construction of the free unital real Jordan algebra on two generators. Let $\sim$ denote the relation `FreeJordanTwoRel` that defines the congruence for this algebra. For any terms $a, b, c \in \mathcal{R}$, if $a \sim b$, then $a - c \sim b - c$.

Let $\mathcal{R}$ be the set of raw terms (denoted as `RawTwo`) used in the construction of the free unital real Jordan algebra on two generators. Let $\sim$ denote the relation `FreeJordanTwoRel` that defines the congruence for this algebra. For any natural number $n \in \mathbb{N}$ and any terms $a, b \in \mathcal{R}$, if $a \sim b$, then $n \cdot a \sim n \cdot b$.

Let $\mathcal{R}$ be the set of raw terms for the non-associative algebra generated by a formal unit and two letters, and let $\sim$ (represented by `FreeJordanTwoRel`) be the congruence relation on $\mathcal{R}$ that defines the free unital real Jordan algebra. For any integer $n \in \mathbb{Z}$ and any raw terms $a, b \in \mathcal{R}$, if $a \sim b$, then $n \cdot a \sim n \cdot b$.

Let $\mathcal{R}$ (represented by `RawTwo`) be the set of raw terms for a non-associative algebra generated by a formal unit and two generators. The free unital real Jordan algebra on two generators is defined as the quotient of $\mathcal{R}$ by the congruence relation $\sim$ (represented by `FreeJordanTwoRel`). This relation identifies terms to satisfy the axioms of a unital commutative Jordan algebra: for all elements $a$ and $b$, $a \circ b = b \circ a$, $((a \circ a) \circ b) \circ a = (a \circ a) \circ (b \circ a)$, and $1 \circ a = a$.

The zero element $0$ of the free unital real Jordan algebra on two generators is defined as the equivalence class in the quotient type represented by the zero term of the underlying raw term algebra $\mathcal{R}$.

The multiplicative identity element $1$ for the free unital real Jordan algebra on two generators. It is defined as the equivalence class of the formal unit element in the set of raw terms (the free non-associative algebra on a formal unit and two generators) under the congruence relation that imposes the Jordan algebra axioms.

This definition provides the addition operation on the free unital real Jordan algebra on two generators, denoted as $FreeJordanTwo$. Specifically, it defines addition on the quotient space by lifting the addition operation from the set of raw terms $\mathcal{R}$: for any raw terms $a, b \in \mathcal{R}$, the sum of their equivalence classes $[a]$ and $[b]$ is given by $[a] + [b] = [a + b]$.

This definition provides the negation operation (unary minus) for the free unital real Jordan algebra on two generators, denoted by $J$. It is defined by lifting the negation operation from the underlying set of raw terms $\mathcal{R}$ to the quotient $J = \mathcal{R} / \sim$, such that for any term $a \in \mathcal{R}$, the negation of its equivalence class is the equivalence class of its negation: $-[a] = [-a]$.

Let $J$ (denoted as `FreeJordanTwo`) be the free unital real Jordan algebra on two generators, defined as the quotient of the set of raw terms $\mathcal{R}$ by the relation $\sim$. This definition provides the subtraction operation $- : J \times J \to J$. For any $a, b \in J$, the difference $a - b$ is defined by lifting the subtraction of raw terms to the quotient, which is well-defined as the relation $\sim$ is preserved under subtraction.

The multiplication operation $\circ$ on the free unital real Jordan algebra on two generators. This operation is defined by lifting the multiplication of the underlying raw terms (from the set of non-associative terms $\mathcal{R}$) to the quotient space defined by the Jordan algebra relations.

Let $\mathcal{J}$ be the free unital real Jordan algebra on two generators. For any natural number $n \in \mathbb{N}$ and any element $x \in \mathcal{J}$, this definition defines the scalar multiplication $n \cdot x$. It is constructed by lifting the natural scalar multiplication from the set of raw terms $\mathcal{R}$ to the quotient space $\mathcal{J} = \mathcal{R}/\sim$, using the property that the congruence relation $\sim$ is preserved under scalar multiplication by $n$.

Integer scalar multiplication on the free unital real Jordan algebra on two generators, denoted by $\text{FreeJordanTwo}$. For any integer $n \in \mathbb{Z}$ and any element $x$ in the algebra, the scalar product $n \cdot x$ is defined by lifting the integer scalar multiplication from the underlying space of raw terms to the quotient space.

The scalar multiplication operation $\cdot : \mathbb{R} \times \text{FreeJordanTwo} \to \text{FreeJordanTwo}$ on the free unital real Jordan algebra on two generators, defined by lifting the scalar multiplication from the underlying raw terms to the quotient space.

The free unital real Jordan algebra on two generators, denoted by $\text{FreeJordanTwo}$, forms an additive commutative group. This structure is obtained by lifting the additive commutative group properties from the underlying space of raw terms $\mathcal{R}$ to the quotient space $\text{FreeJordanTwo} = \mathcal{R}/\sim$.

The free unital real Jordan algebra on two generators, denoted by $\text{FreeJordanTwo}$, is equipped with a module structure over the field of real numbers $\mathbb{R}$. This structure is defined by lifting the module operations from the underlying raw terms to the quotient space.

The free unital real Jordan algebra on two generators, denoted by $\text{FreeJordanTwo}$, carries the structure of a non-associative commutative ring. This means that $\text{FreeJordanTwo}$ is an additive commutative group equipped with a multiplication operation $\circ$ and a multiplicative identity $1$ such that for all elements $x, y, z$: 1. Multiplication is commutative: $x \circ y = y \circ x$. 2. It satisfies the distributive laws: $x \circ (y + z) = x \circ y + x \circ z$ and $(x + y) \circ z = x \circ z + y \circ z$. 3. The element $1$ acts as a unit: $1 \circ x = x$ and $x \circ 1 = x$. While the multiplication is commutative and distributive, it is not required to be associative.

The free unital real Jordan algebra on two generators, denoted by $\text{FreeJordanTwo}$, satisfies the axioms of a commutative Jordan algebra. Specifically, for all elements $a, b \in \text{FreeJordanTwo}$, the multiplication $\circ$ is commutative ($a \circ b = b \circ a$) and satisfies the Jordan identity: $((a \circ a) \circ b) \circ a = (a \circ a) \circ (b \circ a)$.

Let $J_2$ (represented by `FreeJordanTwo`) be the free unital real Jordan algebra on two generators. The element $x \in J_2$ is the first of the two free abstract Jordan generators.

In the free unital real Jordan algebra on two generators (denoted by `FreeJordanTwo`), $y$ is the element representing the second of the two abstract generators.

Given a map $f : \{0, 1\} \to E$ where $E$ is a unital real Jordan algebra, this function is the non-associative $\mathbb{R}$-algebra homomorphism from the free non-unital non-associative algebra on a formal unit and two generators (denoted `RawTwo`) to $E$. It maps the formal unit to $1 \in E$ and the generators to $f(0)$ and $f(1)$, respectively.

Let $E$ be a unital real Jordan algebra and $f: \{0, 1\} \to E$ be a map that assigns values in $E$ to two generators. Let $\text{liftAux}_f: \text{RawTwo} \to E$ be the non-associative $\mathbb{R}$-algebra homomorphism from the free non-unital non-associative algebra on a formal unit and two generators (denoted $\text{RawTwo}$) to $E$, which maps the formal unit to $1 \in E$ and the generators to $f(0)$ and $f(1)$. For any scalar $r \in \mathbb{R}$ and any element $a \in \text{RawTwo}$, the map preserves scalar multiplication: $$\text{liftAux}_f(r \cdot a) = r \cdot \text{liftAux}_f(a)$$

Let $E$ be a unital real Jordan algebra and $f: \{0, 1\} \to E$ be a map that assigns values to two generators. Let $\text{liftAux}_f: \text{RawTwo} \to E$ be the non-associative $\mathbb{R}$-algebra homomorphism from the free non-unital non-associative algebra on a formal unit and two generators (denoted `RawTwo`) to $E$, which maps the formal unit to $1 \in E$ and the generators to $f(0)$ and $f(1)$. For any elements $a, b \in \text{RawTwo}$, the map preserves addition: $$\text{liftAux}_f(a + b) = \text{liftAux}_f(a) + \text{liftAux}_f(b)$$

Let $E$ be a unital real Jordan algebra and $f: \{0, 1\} \to E$ be a map assigning values to two generators. Let $\text{liftAux}_f: \text{RawTwo} \to E$ be the non-associative $\mathbb{R}$-algebra homomorphism from the free non-unital non-associative algebra on a formal unit and two generators (denoted $\text{RawTwo}$) to $E$, which maps the formal unit to $1 \in E$ and the generators to $f(0)$ and $f(1)$. For any elements $a, b \in \text{RawTwo}$, the map preserves multiplication: $$\text{liftAux}_f(a \cdot b) = \text{liftAux}_f(a) \cdot \text{liftAux}_f(b)$$

Let $E$ be a unital real Jordan algebra and $f: \{0, 1\} \to E$ be a map assigning values to two generators. The non-associative $\mathbb{R}$-algebra homomorphism $\text{liftAux}_f$, which maps expressions from the free non-unital non-associative algebra on a formal unit and two generators (denoted `RawTwo`) to $E$, maps the formal unit (represented by the term `none`) to the identity element $1 \in E$.

Let $E$ be a unital real Jordan algebra and $f: \{0, 1\} \to E$ be a map assigning values to two generators. Let $\mathcal{R}$ be the set of raw terms for the free non-associative algebra on a formal unit and two generators, and let $\sim$ denote the congruence relation (defined by `FreeJordanTwoRel`) that imposes the axioms of a unital commutative Jordan algebra. If two terms $a, b \in \mathcal{R}$ are related such that $a \sim b$, then their evaluations in $E$ under the homomorphism $\text{liftAux}_f : \mathcal{R} \to E$ are equal: $$\text{liftAux}_f(a) = \text{liftAux}_f(b)$$

Let $E$ be a unital real Jordan algebra. For any map $f : \{0, 1\} \to E$ that assigns values in $E$ to two generators, the function $\text{lift}(f)$ is the unital Jordan homomorphism from the free unital real Jordan algebra on two generators ($\text{FreeJordanTwo}$) to $E$. This homomorphism is obtained by lifting the evaluation map from the underlying raw terms to the quotient algebra, ensuring that the free generators are mapped to $f(0)$ and $f(1)$, and the multiplicative identity is preserved.

Let $E$ be a unital real Jordan algebra and let $f : \{0, 1\} \to E$ be a map. Let $\text{lift}_f: \text{FreeJordanTwo} \to E$ be the unital Jordan homomorphism from the free unital real Jordan algebra on two generators to $E$ associated with $f$. If $x$ is the first generator of $\text{FreeJordanTwo}$, then the image of $x$ under $\text{lift}_f$ is $f(0)$, i.e., $$\text{lift}_f(x) = f(0)$$

Let $E$ be a unital real Jordan algebra and $f: \{0, 1\} \to E$ be a map. Let $\text{lift}_f: \text{FreeJordanTwo} \to E$ be the unital Jordan homomorphism from the free unital real Jordan algebra on two generators to $E$ that extends $f$. Then the image of the second generator $y$ under this homomorphism is $f(1)$, i.e., $\text{lift}_f(y) = f(1)$.