PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Power.Ring

`J[a]` is a commutative associative unital algebra

i. Overview

This is the payoff of `Power/Associative.lean` and `Power/GeneratedByOne.lean`: the subalgebra `J[a] = generatedByOne a`, equipped with the Jordan product `∘` restricted to it (`mul_mem_generatedByOne` shows this restriction lands back in `J[a]`), is a genuine commutative **associative** unital `ℝ`-algebra. Associativity is not assumed — it is *proved*, by expanding any three elements of `J[a]` into finite linear combinations of powers of `a` and reducing to `pow_add`'s monomial identity `a^{[m]} \circ a^{[n]} = a^{[m+n]}` (itself associative on the nose, since `ℕ`-addition is). This is exactly the classical reduction the module docstring of `Power/Associative.lean` describes: $C(\sigma(a), \mathbb R) \xrightarrow{\text{CFC}} J[a] \xrightarrow{\iota} E,$ and this file is what makes the left-hand associative algebra `J[a]` an honest object mathlib's ordinary `CommRing`/`Algebra ℝ` machinery applies to, rather than needing any bespoke non-associative functional calculus.

`J[a]` is packaged as a `Submodule ℝ E` (from `GeneratedByOne.lean`) rather than a fresh type: the `Subtype`/coercion API this gives for free (`Submodule.subtype`, `AddSubmonoid`, ...) is exactly what is needed, and it keeps the inclusion `ι : J[a] → E` (the second arrow above) definitionally trivial rather than something to construct.

The power-associativity theorem in `Power/Associative.lean` is proved from the polarized Jordan identity, so the associative ring structure produced here is unconditional.

ii. Key definitions and results

`JordanAlgebra.GeneratedByOne` : the subtype packaging of `generatedByOne a`
`JordanAlgebra.GeneratedByOne.instCommRing` : the associative commutative ring structure
`JordanAlgebra.GeneratedByOne.instAlgebra` : the `ℝ`-algebra structure

iii. Table of contents

A. The carrier type and its multiplication
B. The commutative ring structure
C. The `ℝ`-algebra structure and inclusion

A. The carrier type and its multiplication

B. The commutative ring structure

C. The `ℝ`-algebra structure and inclusion

16 declarations

abbrev

The subalgebra $J[a]$ generated by $a$

#GeneratedByOne

For an element $a$ in a Jordan algebra $E$ , the type $J[a]$ (or `JordanAlgebra.GeneratedByOne a`) is defined as the subtype of $E$ consisting of the elements in the subalgebra generated by the identity $1$ and $a$ under the Jordan product. This subtype is constructed to serve as the carrier for an associative commutative unital $\mathbb{R}$ -algebra structure, a property that does not generally hold for the ambient space $E$ .

instance

Multiplication on $J[a]$

#instMul

The multiplication operation on the subalgebra $J[a]$ generated by an element $a$ in a Jordan algebra $E$ . For any elements $x, y \in J[a]$ , their product $x \cdot y$ is defined by the restriction of the Jordan product $x \circ y$ from the ambient algebra $E$ to the subtype $J[a]$ .

theorem

Multiplication in $J[a]$ coincides with the Jordan Product in $E$

#val_mul

For any element $a$ in a Jordan algebra $E$ , let $J[a]$ be the subalgebra generated by $a$ . For any elements $x, y \in J[a]$ , the product $x \cdot y$ calculated within the subalgebra $J[a]$ is equal to the Jordan product $x \circ y$ calculated in the ambient space $E$ .

instance

Identity element of $J[a]$

#instOne

For an element $a$ in a Jordan algebra $E$ , the multiplicative identity element $1$ of the subalgebra $J[a]$ is defined as the identity element $1$ of the ambient algebra $E$ .

theorem

The identity of $J[a]$ is the identity of $E$

#val_one

In a Jordan algebra $E$ , let $J[a]$ be the subalgebra generated by an element $a$ and the identity element $1 \in E$ . The multiplicative identity of $J[a]$ , when viewed as an element of the ambient algebra $E$ , is equal to $1$ .

theorem

Multiplication in $J[a]$ is associative

#mul_assoc

Let $E$ be a Jordan algebra and $a \in E$ . Let $J[a]$ be the subalgebra of $E$ generated by $a$ and the identity element. For any elements $x, y, z \in J[a]$ , the multiplication operation is associative, satisfying $(x \cdot y) \cdot z = x \cdot (y \cdot z)$ .

theorem

Multiplication in $J[a]$ is commutative

#mul_comm

For any elements $x, y$ in the subalgebra $J[a]$ generated by an element $a$ in a Jordan algebra $E$ , the multiplication operation satisfies $x \cdot y = y \cdot x$ .

theorem

$1 \cdot x = x$ for all $x \in J[a]$

#one_mul

Let $J[a]$ be the subalgebra of a Jordan algebra generated by an element $a$ and the identity element $1$ . For any element $x \in J[a]$ , the product of the multiplicative identity $1 \in J[a]$ and $x$ is equal to $x$ , that is, $1 \cdot x = x$ .

theorem

$x \cdot 1 = x$ in the subalgebra $J[a]$

#mul_one

Let $a$ be an element of a Jordan algebra $E$ , and let $J[a]$ be the subalgebra generated by $a$ and the identity element $1$ . For any element $x \in J[a]$ , multiplying $x$ by the identity element $1$ on the right satisfies $x \cdot 1 = x$ .

theorem

Left Distributive Law for the Subalgebra $J[a]$

#left_distrib

Let $a$ be an element of a Jordan algebra $E$ . In the subalgebra $J[a]$ generated by $a$ and the identity element $1$ , the multiplication operation satisfies the left distributive law: for all $x, y, z \in J[a]$ , $x(y + z) = xy + xz$ .

theorem

Right Distributive Law in $J[a]$

#right_distrib

Let $E$ be a Jordan algebra and $a \in E$ . Let $J[a]$ be the associative commutative unital subalgebra generated by $a$ and the identity element $1$ . For any $x, y, z \in J[a]$ , the multiplication (defined as the restriction of the Jordan product to $J[a]$ ) satisfies the right distributive law: $(x + y) \cdot z = x \cdot z + y \cdot z$

instance

$J[a]$ is a commutative ring

#instCommRing

For an element $a$ in a Jordan algebra $E$ , the subalgebra $J[a]$ generated by $a$ and the identity element $1$ is a commutative associative ring. The multiplication in $J[a]$ is defined as the restriction of the Jordan product from $E$ to $J[a]$ , and the additive structure is inherited from the ambient space.

definition

Inclusion map $\iota: J[a] \to E$

#inclusion

For an element $a$ in a Jordan algebra $E$ , let $J[a]$ be the associative commutative unital subalgebra generated by $a$ and the identity. This map is the canonical inclusion $\iota: J[a] \hookrightarrow E$ which sends an element $x \in J[a]$ to its underlying value in the ambient space $E$ . This represents the second stage of the functional calculus sequence $C(\sigma(a), \mathbb{R}) \to J[a] \to E$ .

theorem

The inclusion map $\iota: J[a] \to E$ satisfies $\iota(x) = x$

#inclusion_apply

For an element $a$ in a Jordan algebra $E$ , let $J[a]$ be the associative commutative unital subalgebra generated by $a$ and the identity. For any element $x \in J[a]$ , the inclusion map $\iota : J[a] \to E$ maps $x$ to itself, where the result is viewed as an element of the ambient space $E$ .

theorem

The inclusion map $\iota: J[a] \to E$ is injective

#inclusion_injective

Let $a$ be an element in a Jordan algebra $E$ , and let $J[a]$ be the associative commutative unital $\mathbb{R}$ -subalgebra generated by $a$ and the identity. The canonical inclusion map $\iota: J[a] \to E$ , which maps each element of the subalgebra to its corresponding element in the ambient space $E$ , is injective.

instance

$J[a]$ is an $\mathbb{R}$ -algebra

#instAlgebra

For an element $a$ in a Jordan algebra $E$ , the commutative ring $J[a]$ (the subalgebra generated by $a$ and the identity $1$ ) is an $\mathbb{R}$ -algebra. The scalar multiplication of $c \in \mathbb{R}$ on $x \in J[a]$ is inherited from the ambient module structure of $E$ . The structure map (algebra map) $\eta : \mathbb{R} \to J[a]$ is defined by $c \mapsto c \cdot 1$ .

PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Power.Ring

`J[a]` is a commutative associative unital algebra

i. Overview

ii. Key definitions and results

iii. Table of contents

A. The carrier type and its multiplication

B. The commutative ring structure

C. The `ℝ`-algebra structure and inclusion

The subalgebra J[a]J[a]J[a] generated by aaa

Multiplication on J[a]J[a]J[a]

Multiplication in J[a]J[a]J[a] coincides with the Jordan Product in EEE

Identity element of J[a]J[a]J[a]

The identity of J[a]J[a]J[a] is the identity of EEE

Multiplication in J[a]J[a]J[a] is associative

Multiplication in J[a]J[a]J[a] is commutative

1⋅x=x1 \cdot x = x1⋅x=x for all x∈J[a]x \in J[a]x∈J[a]

x⋅1=xx \cdot 1 = xx⋅1=x in the subalgebra J[a]J[a]J[a]

Left Distributive Law for the Subalgebra J[a]J[a]J[a]

Right Distributive Law in J[a]J[a]J[a]

J[a]J[a]J[a] is a commutative ring

Inclusion map ι:J[a]→E\iota: J[a] \to Eι:J[a]→E

The inclusion map ι:J[a]→E\iota: J[a] \to Eι:J[a]→E satisfies ι(x)=x\iota(x) = xι(x)=x

The inclusion map ι:J[a]→E\iota: J[a] \to Eι:J[a]→E is injective

J[a]J[a]J[a] is an R\mathbb{R}R-algebra

The subalgebra $J[a]$ generated by $a$

Multiplication on $J[a]$

Multiplication in $J[a]$ coincides with the Jordan Product in $E$

Identity element of $J[a]$

The identity of $J[a]$ is the identity of $E$

Multiplication in $J[a]$ is associative

Multiplication in $J[a]$ is commutative

$1 \cdot x = x$ for all $x \in J[a]$

$x \cdot 1 = x$ in the subalgebra $J[a]$

Left Distributive Law for the Subalgebra $J[a]$

Right Distributive Law in $J[a]$

$J[a]$ is a commutative ring

Inclusion map $\iota: J[a] \to E$

The inclusion map $\iota: J[a] \to E$ satisfies $\iota(x) = x$

The inclusion map $\iota: J[a] \to E$ is injective

$J[a]$ is an $\mathbb{R}$ -algebra