PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Power.GeneratedByOne

The subalgebra generated by a single element

i. Overview

`J[a] := \operatorname{span}_ℝ\{1, a, a^2, a^3, \dots\}`: the smallest ℝ-subspace of a Jordan order-unit algebra containing `1` and closed under `∘`-multiplication by `a`. Every element of `J[a]` is (by definition of `span`) a finite real-linear combination of powers `a^{[n]}`.

This file only builds the *module*-level object and its membership API; the payoff — that `J[a]` carries a genuine commutative *associative* ring structure, reducing single-observable spectral theory to mathlib's ordinary associative machinery (`Power/Associative.lean`'s module docstring spells out the architecture) — is `Ring.lean`.

ii. Key definitions and results

- `IsJordanOrderUnit.generatedByOne` - `IsJordanOrderUnit.jpow_mem_generatedByOne`, `IsJordanOrderUnit.one_mem_generatedByOne`, `IsJordanOrderUnit.self_mem_generatedByOne` - `IsJordanOrderUnit.mul_mem_generatedByOne` : `J[a]` is closed under `∘`

iii. Table of contents

A. The generated submodule
B. Closure under the Jordan product

A. The generated submodule

B. Closure under the Jordan product

5 declarations

definition

Subalgebra $J[a]$ generated by $1$ and $a$

#generatedByOne

For an element $a$ in a Jordan algebra $E$ over $\mathbb{R}$ , this definition denotes the $\mathbb{R}$ -submodule spanned by the set of all Jordan powers $\{a^{[n]} \mid n \in \mathbb{N}\}$ . This submodule, often denoted as $J[a]$ , represents the subalgebra generated by the identity element $1$ and the element $a$ .

theorem

$a^{[n]} \in J[a]$

#jpow_mem_generatedByOne

For an element $a$ in a Jordan algebra $E$ over $\mathbb{R}$ and any natural number $n$ , the $n$ -th Jordan power $a^{[n]}$ is an element of the subalgebra $J[a]$ generated by $1$ and $a$ . Here, $J[a]$ is defined as the $\mathbb{R}$ -submodule of $E$ spanned by the set of all Jordan powers $\{a^{[k]} \mid k \in \mathbb{N}\}$ .

theorem

$1 \in J[a]$

#one_mem_generatedByOne

Let $E$ be a Jordan algebra and $a \in E$ . Let $J[a]$ be the $\mathbb{R}$ -submodule of $E$ spanned by the set of all Jordan powers $\{a^{[n]} \mid n \in \mathbb{N}\}$ . Then the identity element $1 \in E$ belongs to $J[a]$ .

theorem

$a \in J[a]$

#self_mem_generatedByOne

Let $E$ be a Jordan algebra over $\mathbb{R}$ . For any element $a \in E$ , $a$ is an element of the $\mathbb{R}$ -submodule $J[a]$ generated by the identity element $1$ and $a$ . (Note: $J[a]$ is defined as the span of the set of all Jordan powers $\{a^{[n]} \mid n \in \mathbb{N}\}$ .)

theorem

$J[a]$ is closed under the Jordan product

#mul_mem_generatedByOne

Let $E$ be a Jordan algebra over $\mathbb{R}$ and let $a \in E$ . Let $J[a]$ denote the $\mathbb{R}$ -submodule spanned by the set of Jordan powers $\{a^{[n]} \mid n \in \mathbb{N}\}$ , representing the subalgebra generated by the identity and $a$ . For any elements $x, y \in E$ , if $x \in J[a]$ and $y \in J[a]$ , then their Jordan product $x \circ y$ is also in $J[a]$ .

PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Power.GeneratedByOne

The subalgebra generated by a single element

i. Overview

ii. Key definitions and results

iii. Table of contents

A. The generated submodule

B. Closure under the Jordan product

Subalgebra J[a]J[a]J[a] generated by 111 and aaa

a[n]∈J[a]a^{[n]} \in J[a]a[n]∈J[a]

1∈J[a]1 \in J[a]1∈J[a]

a∈J[a]a \in J[a]a∈J[a]

J[a]J[a]J[a] is closed under the Jordan product

Subalgebra $J[a]$ generated by $1$ and $a$

$a^{[n]} \in J[a]$

$1 \in J[a]$

$a \in J[a]$

$J[a]$ is closed under the Jordan product