« Home

Remark. [ca-000V]
✍️source

In applications to Clifford algebras \(R\) will be always assumed to be commutative.

Context

basics: from groups to modules [ca-000P]

Convention. definition style [ca-000O]

In this document, we unify the informal mathematical language for a definition to:

Let \(X\) be a concept \(X\).

A concept \(Z\) is a set/pair/triple/tuple \((Z, \mathtt {op}, ...)\), satisfying:

\(Z\) is a concept \(Y\) over \(X\) under op .
formula for all elements in \(Z\) ( property ).
for each element in concept \(X\), there exists element such that formula for all elements in concept \(Z\).
op is called op name, for all elements in \(Z\), we have
1. formula
2. formula
( property ).

By default, \(X\) is a set, op is a binary operation on \(X\).

Definition. group [garling2011clifford, 1.1] [ca-000Q]
Group AddGroup
L∃∀N

A group is a pair \((G, *)\), satisfying:

\((a * b) * c = a * (b * c)\) for all \(a, b, c \in G\) (associativity).
there exists \(1 \in G\) such that \[1 * a = a * 1 = a\] for all \(a \in G\).
for each \(a \in G\), there exists \(a^{-1} \in G\) such that \[a * a^{-1} = a^{-1} * a = 1\].

Remark. [ca-000R]

It then follows that \(1\), the identity element, is unique, and that for each \(g \in G\) the inverse \(g^{-1}\) is unique. A group G is abelian, or commutative, if \(g * h = h * g\) for all \(g, h \in G\).

Notation. product [ca-000S]

In literatures, the binary operation of a group is usually called a product. It's denoted by juxtaposition \(g h\), and is understood to be a mapping \((g, h) \mapsto g * h\) from \(G \times G\) to \(G\).

Here we use an explicit symbol for the operation. It can be denoted multiplicatively as \(*\) in Group or additively as \(+\) in AddGroup, where the identity element will be denoted by \(1\) or \(0\), respectively.

Sometimes we use notations with subscripts (e.g. \(*_G\), \(1_G\)) to indicate where they are.

\(\textsf {Mathlib}\) encodes the mapping \(G \times G \to G\) as \(G \to G \to G\), it is understood to be \(G \to (G \to G)\), that sends \(g \in G\) to a mapping that sends \(h \in G\) to \(g * h \in G\).

Furthermore, a mathematical construct, e.g. a group, is represented by a "type", as Lean has a dependent type theory foundation, see [carneiro2019type] and [ullrich2023extensible, sec. 3.2].

Definition. monoid [ca-000T]
Monoid AddMonoid
L∃∀N

A monoid is a pair \((R, *)\), satisfying:

\((a * b) * c = a * (b * c)\) for all \(a, b, c \in R\) (associativity).
there exists an element \(1 \in R\) such that \(1 * a = a * 1 = a\) for all \(a \in R\)

neutral element

Definition. ring [jadczyk2019notes, 1.1] [ca-000U]
Ring CommRing CommSemiring
L∃∀N

A ring is a triple \((R, +, *)\), satisfying:

\(R\) is a commutative group under \(+\).
\(R\) is a monoid under \(*\).
for all \(a, b, c \in R\), we have
1. \(a * (b + c) = a * b + a * c\)
2. \((a + b) * c = a * c + b * c\)
(left and right distributivity over \(+\)).

Remark. [ca-000V]
✍️source

In applications to Clifford algebras \(R\) will be always assumed to be commutative.

Definition. division ring [ca-000W]
DivisionRing
L∃∀N

A division ring is a ring \((R, +, *)\), satisfying:

\(R\) contains at least 2 elements.
for all \(a \neq 0\) in \(R\), there exists a multiplicative inverse \(a^{-1} \in R\) such that

Definition. module [jadczyk2019notes, 1.3] [ca-000X]
Module
L∃∀N

Let \(R\) be a commutative ring. A module over \(R\), called an \(R\)-module, is a pair \((M, \bullet )\), satisfying:

M is a group under \(+\).
\(\bullet : R \to M \to M\) is called scalar multiplication, for every \(a, b \in R\), \(x, y \in M\), we have
1. \(a \bullet (x + y) = a \bullet x + b \bullet y\)
2. \((a + b) \bullet x = a \bullet x + b \bullet x\)
3. \(a * (b \bullet x)=(a * b) \bullet x\)
4. \(1_R \bullet x = x\)

Remark. [ca-000Y]

The notation of scalar multiplication is generalized as heterogeneous scalar multiplication HMul in \(\textsf {Mathlib}\): \[ \bullet : \alpha \to \beta \to \gamma \] where \(\alpha \), \(\beta \), \(\gamma \) are different types.

Definition. vector space [jadczyk2019notes, 1.5] [ca-000Z]
Module
L∃∀N

If \(R\) is a division ring, then a module \(M\) over \(R\) is called a vector space.

Remark. [ca-0010]

For generality, \(\textsf {Mathlib}\) uses Module throughout for vector spaces, particularly, for a vector space \(V\), it's usually declared as

/--
    Let $K$ be a division ring, a module $V$ over $K$ is a vector space
    where being a module requires $V$ to be a commutative group over $+$.
-/
variable [DivisionRing K] [AddCommGroup V] [Module K V]

For definitions/theorems about it, and most of them can be found under Mathlib.LinearAlgebra e.g. LinearIndependent.

Definition. submodule [ca-0011]

A submodule \(N\) of \(M\) is a module \(N\) such that every element of \(N\) is also an element of \(M\). If \(M\) is a vector space then \(N\) is called a subspace.

Definition. dual module [ca-0012]
Module.Dual
L∃∀N

The dual module \(M^* : M \to _{l[R]} R\) is the \(R\)-module of all linear maps from \(M\) to \(R\).