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.
Universal property of the Clifford algebra
Statement
Let be as in Universal Clifford algebra of a quadratic space, and let be a unital associative -algebra. For every -linear map satisfying for all , there is a unique unital -algebra homomorphism such that .
Facts & Assumptions
Given: The quadratic space , a unital associative -algebra , and a -linear map satisfying the stated quadratic relations.
Every linear map from to a unital associative -algebra extends uniquely to a unital algebra homomorphism from (Universal property of the tensor algebra).
A homomorphism from that kills every Clifford relation factors uniquely through (Factorization through the Clifford quotient).
The canonical map is , and the quotient map is surjective (Universal Clifford algebra of a quadratic space).
A unital -algebra is a unital ring with a central unital structure map from (Algebras over a commutative ring, central structure maps, and algebra homomorphisms).
Proof
By [F4], has the central unital -algebra structure required by [F1], so extends uniquely to a unital -algebra homomorphism with .
For every , . Thus [F2] gives a unique unital homomorphism satisfying .
Since , step 2.1 gives . Let be any other unital -algebra homomorphism with . Then and are unital algebra extensions of the same map along , because . Uniqueness in [F1] gives . Since is surjective by [F3], .
Remarks
For a -linear map satisfying , the universal property is the commutative triangle below. The maps and are -linear; the dashed arrow is the unique unital -algebra homomorphism with . The triangle is viewed on underlying vector spaces, so it does not assign an algebra structure to .
The figure summarizes step 3.1; the proof above establishes both existence and uniqueness independently of the illustration.