definition. Pin group [pr-spin] [spin-000Y]

✍️source

pinGroup

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}. \]