The Pin group and the Spin group #
In this file we define lipschitzGroup
, pinGroup
and spinGroup
and show they form a group.
Main definitions #
lipschitzGroup
: the Lipschitz group with a quadratic form.pinGroup
: the Pin group defined as the infimum oflipschitzGroup
andunitary
.spinGroup
: the Spin group defined as the infimum ofpinGroup
andCliffordAlgebra.even
.
Implementation Notes #
The definition of the Lipschitz group $\{ x \in \mathop{\mathcal{C}\ell} | x \text{ is invertible and } x v x^{-1} ∈ V \}$ is given by:
But they presumably form a group only in finite dimensions. So we define lipschitzGroup
with
closure of all the invertible elements in the form of ι Q m
, and we show this definition is
at least as large as the other definition (See lipschitzGroup.conjAct_smul_range_ι
and
lipschitzGroup.involute_act_ι_mem_range_ι
).
The reverse statement presumably is true only in finite dimensions.
Here are some discussions about the latent ambiguity of definition : https://mathoverflow.net/q/427881/172242 and https://mathoverflow.net/q/251288/172242
TODO #
Try to show the reverse statement is true in finite dimensions.
lipschitzGroup
is the subgroup closure of all the invertible elements in the form of ι Q m
where ι
is the canonical linear map M →ₗ[R] CliffordAlgebra Q
.
Equations
- lipschitzGroup Q = Subgroup.closure (Units.val ⁻¹' Set.range ⇑(CliffordAlgebra.ι Q))
Instances For
The conjugation action by elements of the Lipschitz group keeps vectors as vectors.
This is another version of lipschitzGroup.conjAct_smul_ι_mem_range_ι
which uses involute
.
If x is in lipschitzGroup Q
, then (ι Q).range
is closed under twisted conjugation.
The reverse statement presumably is true only in finite dimensions.
pinGroup Q
is defined as the infimum of lipschitzGroup Q
and unitary (CliffordAlgebra Q)
.
See mem_iff
.
Equations
- pinGroup Q = Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ⊓ unitary (CliffordAlgebra Q)
Instances For
An element is in pinGroup Q
if and only if it is in lipschitzGroup Q
and unitary
.
The conjugation action by elements of the spin group keeps vectors as vectors.
This is another version of conjAct_smul_ι_mem_range_ι
which uses involute
.
If x is in pinGroup Q
, then (ι Q).range
is closed under twisted conjugation. The reverse
statement presumably being true only in finite dimensions.
See star_mem_iff
for both directions.
An element is in pinGroup Q
if and only if star x
is in pinGroup Q
.
See star_mem
for only one direction.
Equations
- pinGroup.instStarSubtypeCliffordAlgebraMemSubmonoid = { star := fun (x : { x : CliffordAlgebra Q // x ∈ pinGroup Q }) => ⟨star ↑x, ⋯⟩ }
pinGroup Q
forms a group where the inverse is star
.
Equations
- pinGroup.instStarMulSubtypeCliffordAlgebraMemSubmonoid = StarMul.mk ⋯
Equations
- pinGroup.instInhabitedSubtypeCliffordAlgebraMemSubmonoid = { default := 1 }
The elements in pinGroup Q
embed into (CliffordAlgebra Q)ˣ.
Equations
- pinGroup.toUnits = { toFun := fun (x : { x : CliffordAlgebra Q // x ∈ pinGroup Q }) => { val := ↑x, inv := ↑x⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }
Instances For
spinGroup Q
is defined as the infimum of pinGroup Q
and CliffordAlgebra.even Q
.
See mem_iff
.
Equations
- spinGroup Q = pinGroup Q ⊓ (CliffordAlgebra.even Q).toSubring.toSubmonoid
Instances For
An element is in spinGroup Q
if and only if it is in pinGroup Q
and even Q
.
If x is in spinGroup Q
, then involute x
is equal to x.
The conjugation action by elements of the spin group keeps vectors as vectors.
See star_mem_iff
for both directions.
An element is in spinGroup Q
if and only if star x
is in spinGroup Q
.
See star_mem
for only one direction.
Equations
- spinGroup.instStarSubtypeCliffordAlgebraMemSubmonoid = { star := fun (x : { x : CliffordAlgebra Q // x ∈ spinGroup Q }) => ⟨star ↑x, ⋯⟩ }
spinGroup Q
forms a group where the inverse is star
.
Equations
- spinGroup.instStarMulSubtypeCliffordAlgebraMemSubmonoid = StarMul.mk ⋯
Equations
- spinGroup.instInhabitedSubtypeCliffordAlgebraMemSubmonoid = { default := 1 }
The elements in spinGroup Q
embed into (CliffordAlgebra Q)ˣ.
Equations
- spinGroup.toUnits = { toFun := fun (x : { x : CliffordAlgebra Q // x ∈ spinGroup Q }) => { val := ↑x, inv := ↑x⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }