Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The symmetrized product of an associative algebra is Jordan

Statement

Let k be a field with char⁡(k)≠2 and A a unital associative k-algebra. The product a∘b=(ab+ba)/2 makes A+ of Symmetrized product of an associative algebra a Jordan algebra. If A is a complex associative algebra with involution as in Complex associative algebra with involution, then its self-adjoint part Asa is a real vector subspace closed under ∘, hence a real Jordan subalgebra of A+.

Facts & Assumptions

Given: A field k of characteristic not 2, a unital associative k-algebra A, and, for the second claim, a complex algebra involution on A. Write a3:=aaa in the associative multiplication.

[F1]

The product on A+ is a∘b=(ab+ba)/2 (Symmetrized product of an associative algebra).

[F2]
[F3]

A Jordan algebra has a commutative bilinear product satisfying x∘(y∘x2)=(x∘y)∘x2 (Jordan algebra over a field of characteristic not two).

[F4]

In a complex algebra with involution, ∗ is conjugate-linear, (ab)∗=b∗a∗, (a∗)∗=a, and 1∗=1 (Complex associative algebra with involution).

Proof

1.1givenF1F2algebra

By [F1] and the bilinearity of multiplication in [F2], ∘ is bilinear; swapping a,b leaves ab+ba unchanged, so it is commutative. Also a∘2:=a∘a=aa because 2 is invertible in k.

2.1givenF1F2step 1.1algebra

Using associativity from [F2], expand a∘(b∘a∘2)=14(aba2+a3b+ba3+a2ba). Here a3=(aa)a=a(aa).

2.2givenF1F4step 1.1algebra

In the complex involutive case, Asa is closed under addition and real scalar multiplication by conjugate-linearity in [F4], and it contains the unit because 1∗=1. For a,b∈Asa, (a∘b)∗=12((ab)∗+(ba)∗)=12(ba+ab)=a∘b, so it is closed under ∘.

3.1givenF1F2step 1.1step 2.1algebra

The other side expands, using [F2], as (a∘b)∘a∘2=14(aba2+ba3+a3b+a2ba), which contains the same four terms as step 2.1.

4.1givenF1F2step 1.1step 2.1step 3.1F3

Since A is unital, [F1] gives 1∘a=(1a+a1)/2=a for every a∈A. Steps 1.1, 2.1, and 3.1 prove bilinearity, commutativity, and the Jordan identity in [F3]. Thus A+ is a unital Jordan algebra.

5.1step 4.1step 2.2F3∎

The real subspace Asa inherits commutativity, bilinearity, and the Jordan identity from A+, so it is a real Jordan subalgebra.

Depends on

Used by

Cited to discharge well-definedness by Complex associative algebra with involution.

Dependency tree · two levels

9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources