Our definition [spin-000X]
Our definition [spin-000X]
definition 1. Clifford algebra [pr-spin] [ca-0002]
definition 1. Clifford algebra [pr-spin] [ca-0002]
Let \(M\) be a module over a commutative ring \(R\), equipped with a quadratic form \(Q: M \to R\).
A Clifford algebra over \(Q\) is \[ \mathcal {C}\kern -2pt\ell (Q) \equiv T(M)/I_Q \] where \(T(M)\) is the tensor algebra of \(M\), \(I_Q\) is the two-sided ideal generated from the set \[ \{ m \otimes m - Q(m) \mid m \in M \}. \]
We denote the canonical linear map \(M \to \mathcal {C}\kern -2pt\ell (Q)\) as \(\iota _Q\).
definition 2. Lipschitz-Clifford group [pr-spin] [spin-000W]
definition 2. Lipschitz-Clifford group [pr-spin] [spin-000W]
The Lipschitz-Clifford group is defined as the subgroup closure of all the invertible elements in the form of \(\iota _Q(m)\), \[ \Gamma \equiv \left \{ x_1 \ldots x_k \in \mathcal {C}\kern -2pt\ell ^{\times }(Q) \mid x_i \in V \right \} \] where \[ \mathcal {C}\kern -2pt\ell ^{\times }(Q) \equiv \left \{ x \in \mathcal {C}\kern -2pt\ell (Q) \mid \exists x^{-1} \in \mathcal {C}\kern -2pt\ell (Q), x^{-1} x = x x^{-1}=1\right \} \] is the group of units (i.e. invertible elements) of \(\mathcal {C}\kern -2pt\ell (Q)\), \[ V \equiv \left \{ \iota _Q(m) \in \mathcal {C}\kern -2pt\ell (Q) \mid m \in M \right \} \] is the subset \(V\) of \(\mathcal {C}\kern -2pt\ell (Q)\) in the form of \(\iota _Q(m)\).
definition 3. Pin group [pr-spin] [spin-000Y]
L∃∀N
definition 3. Pin group [pr-spin] [spin-000Y]
L∃∀N
The Pin group is defined as \[ \operatorname {Pin}(Q) \equiv \Gamma \sqcap \operatorname {U}(\mathcal {C}\kern -2pt\ell (Q)) \] where \(\sqcap \) is the infimum (or greatest lower bound, or meet), and the infimum of two submonoids is just their intersection \(\cap \), \[ \operatorname {U}(S) \equiv \left \{ x \in S \mid x^{*} * x = x * x^{*} = 1 \right \} \] are the unitary elements of the Clifford algebra as a \(*\)-monid, and we have defined the star operation of Clifford algebra as Clifford conjugate [wieser2022formalizing], denoted \(\bar {x}\).
This definition is equivalent to the following: \[ \operatorname {Pin}(Q) \equiv \left \{ x \in \Gamma \mid \operatorname {N}(x) = 1 \right \} \] where \[ \operatorname {N}(x) \equiv x \bar {x}. \]
definition 4. Spin group [pr-spin] [spin-0012]
L∃∀N
definition 4. Spin group [pr-spin] [spin-0012]
L∃∀N
The Spin group is defined as \[ \operatorname {Spin}(Q) \equiv \operatorname {Pin}(Q) \sqcap \mathcal {C}\kern -2pt\ell ^{+}(Q) \] where \(\mathcal {C}\kern -2pt\ell ^{+}(Q)\) is the even subalgebra of the Clifford algebra.