1.1 Basics: from groups to modules
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\).
It then follows that \(e\), 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\).
In literatures, the binary operation are usually denoted by juxtaposition, and is understood to be a mapping \((g, h) \mapsto g * h\) from \(G \times G\) to \(G\).
Mathlib uses a slightly different way to encode this, \(G \to G \to G\) 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 is represented by a “type", as Lean has a dependent type theory foundation, see [ Carneiro(2019) ] and [ Ullrich(2023) , section 3.2 ] .
It can be denoted multiplicatively as \(*\) in Group or additively as \(+\) in AddGroup, where \(e\) will be denoted by \(1\) or \(0\), respectively.
Sometimes we use notations with subscripts (e.g. \(*_G\), \(1_G\)) to indicate where they are.
We will use the corresponding notation in Mathlib for future operations without further explanation.
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\)
i.e. \(1\) is the multiplicative identity (neutral element).
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
\(a * (b + c) = a * b + a * c\)
\((a + b) * c = a * c + b * c\)
(left and right distributivity over \(+\)).
In applications to Clifford algebras \(R\) will be always assumed to be commutative.
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
\[ a * a^{-1} = a^{-1} * a = 1 \]
Let \(R\) be a commutative ring. A module over \(R\) (in short \(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
\(a \bullet (x + y) = a \bullet x + b \bullet y\)
\((a + b) \bullet x = a \bullet x + b \bullet x\)
\(a * (b \bullet x)=(a * b) \bullet x\)
\(1_R \bullet x = x\)
The notation of scalar multiplication is generalized as heterogeneous scalar multiplication HMul in Mathlib :
where \(\alpha \), \(\beta \), \(\gamma \) are different types.
If \(R\) is a division ring, then a module \(M\) over \(R\) is called a vector space.
For generality, 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.
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.
The dual module \(M^* : M \to _{l[R]} R\) is the \(R\)-module of all linear maps from \(M\) to \(R\).