Homotopy Type Theory geometric algebra > history (Rev #1)

Defintion

Given a commutative ring $R$ , a $R$ -geometric algebra is an $R$ -algebra $A$ with a canonical injection $\iota: R \to A$ , with a binary function $\langle (-) \rangle_{(-)}: A \times \mathbb{N} \to A$ called the grade projection operator such that

\prod_{a:A} a = \sum_{n:\mathbb{N}} \langle a \rangle_n

\prod_{a:A} \prod_{b:A} \prod_{n:\mathbb{N}} \langle a + b \rangle_n = \langle a \rangle_n + \langle b \rangle_n

\prod_{a:A} \prod_{c:A} \prod_{n:\mathbb{N}} (c = \langle c \rangle_0) \times (\langle c a \rangle_n = c \langle a \rangle_n)

\prod_{a:A} \prod_{n:\mathbb{N}} \langle \langle a \rangle_n \rangle_n = \langle a \rangle_n

\prod_{a:A} \prod_{m:\mathbb{N}} \prod_{n:\mathbb{N}} (m \neq n) \times (\langle \langle a \rangle_m \rangle_n = 0)

For a natural number $n:\mathbb{N}$ , the image of $\langle (-) \rangle_n$ under $A$ is called the $n$ -vector space and is denoted as $\langle A \rangle_n$ .

\langle A \rangle_0 \cong R

\prod_{v:\langle A \rangle_1} \Vert \sum_{r:\langle A \rangle_0} v^2 = r \Vert

Terms of $A$ are called multivectors. The terms of $\langle A \rangle_n$ are called $n$ -vectors, $0$ -vectors are called scalars and $1$ -vectors are just called vectors.

Every $R$ -geometric algebra is a $R$ -Clifford algebra.

Homotopy Type Theory geometric algebra > history (Rev #1)

Defintion

See also