English
The pin group is the infimum (greatest lower bound) of the Lipschitz group and the unitary group inside Clifford algebras; it consists of those invertible Clifford elements that come from vectors via ι Q.
Русский
PinGroup — это инфимума LipschitzGroup и unitary внутри CliffordAlgebra, т.е. инвертируемые элементы, полученные из векторов через ι Q.
LaTeX
$$$$\\mathrm{pinGroup}(Q) = \\big( \\mathrm{lipschitzGroup}(Q) \\bigsqcap \\mathrm{unitary}(CliffordAlgebra Q) \\big) $$$$
Lean4
/-- `pinGroup Q` is defined as the infimum of `lipschitzGroup Q` and `unitary (CliffordAlgebra Q)`.
See `mem_iff`. -/
def pinGroup (Q : QuadraticForm R M) : Submonoid (CliffordAlgebra Q) :=
(lipschitzGroup Q).toSubmonoid.map (Units.coeHom <| CliffordAlgebra Q) ⊓ unitary _
