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 oflipschitzGroupandunitary.spinGroup: the Spin group defined as the infimum ofpinGroupandCliffordAlgebra.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:
- [fulton2004][], Chapter 20
- https://en.wikipedia.org/wiki/Clifford_algebra#Lipschitz_group
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.
def
lipschitzGroup
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
:
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.
Instances For
theorem
lipschitzGroup.conjAct_smul_ι_mem_range_ι
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : (CliffordAlgebra Q)ˣ}
(hx : x ∈ lipschitzGroup Q)
[Invertible 2]
(m : M)
:
ConjAct.toConjAct x • (CliffordAlgebra.ι Q) m ∈ (CliffordAlgebra.ι Q).range
The conjugation action by elements of the Lipschitz group keeps vectors as vectors.
theorem
lipschitzGroup.involute_act_ι_mem_range_ι
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
[Invertible 2]
{x : (CliffordAlgebra Q)ˣ}
(hx : x ∈ lipschitzGroup Q)
(b : M)
:
CliffordAlgebra.involute ↑x * (CliffordAlgebra.ι Q) b * ↑x⁻¹ ∈ (CliffordAlgebra.ι Q).range
This is another version of lipschitzGroup.conjAct_smul_ι_mem_range_ι which uses involute.
theorem
lipschitzGroup.conjAct_smul_range_ι
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : (CliffordAlgebra Q)ˣ}
(hx : x ∈ lipschitzGroup Q)
[Invertible 2]
:
ConjAct.toConjAct x • (CliffordAlgebra.ι Q).range = (CliffordAlgebra.ι Q).range
If x is in lipschitzGroup Q, then (ι Q).range is closed under twisted conjugation.
The reverse statement presumably is true only in finite dimensions.
theorem
lipschitzGroup.coe_mem_iff_mem
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : (CliffordAlgebra Q)ˣ}
:
↑x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ↔ x ∈ lipschitzGroup Q
def
pinGroup
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
:
pinGroup Q is defined as the infimum of lipschitzGroup Q and unitary (CliffordAlgebra Q).
See mem_iff.
Instances For
theorem
pinGroup.mem_iff
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : CliffordAlgebra Q}
:
x ∈ pinGroup Q ↔ x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ∧ x ∈ unitary (CliffordAlgebra Q)
An element is in pinGroup Q if and only if it is in lipschitzGroup Q and unitary.
theorem
pinGroup.mem_lipschitzGroup
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : CliffordAlgebra Q}
(hx : x ∈ pinGroup Q)
:
x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid
theorem
pinGroup.mem_unitary
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : CliffordAlgebra Q}
(hx : x ∈ pinGroup Q)
:
x ∈ unitary (CliffordAlgebra Q)
theorem
pinGroup.units_mem_iff
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : (CliffordAlgebra Q)ˣ}
:
↑x ∈ pinGroup Q ↔ x ∈ lipschitzGroup Q ∧ ↑x ∈ unitary (CliffordAlgebra Q)
theorem
pinGroup.units_mem_lipschitzGroup
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : (CliffordAlgebra Q)ˣ}
(hx : ↑x ∈ pinGroup Q)
:
x ∈ lipschitzGroup Q
theorem
pinGroup.conjAct_smul_ι_mem_range_ι
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : (CliffordAlgebra Q)ˣ}
(hx : ↑x ∈ pinGroup Q)
[Invertible 2]
(y : M)
:
ConjAct.toConjAct x • (CliffordAlgebra.ι Q) y ∈ (CliffordAlgebra.ι Q).range
The conjugation action by elements of the spin group keeps vectors as vectors.
theorem
pinGroup.involute_act_ι_mem_range_ι
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : (CliffordAlgebra Q)ˣ}
(hx : ↑x ∈ pinGroup Q)
[Invertible 2]
(y : M)
:
CliffordAlgebra.involute ↑x * (CliffordAlgebra.ι Q) y * ↑x⁻¹ ∈ (CliffordAlgebra.ι Q).range
This is another version of conjAct_smul_ι_mem_range_ι which uses involute.
theorem
pinGroup.conjAct_smul_range_ι
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : (CliffordAlgebra Q)ˣ}
(hx : ↑x ∈ pinGroup Q)
[Invertible 2]
:
ConjAct.toConjAct x • (CliffordAlgebra.ι Q).range = (CliffordAlgebra.ι Q).range
If x is in pinGroup Q, then (ι Q).range is closed under twisted conjugation. The reverse
statement presumably being true only in finite dimensions.
@[simp]
theorem
pinGroup.star_mul_self_of_mem
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : CliffordAlgebra Q}
(hx : x ∈ pinGroup Q)
:
star x * x = 1
@[simp]
theorem
pinGroup.mul_star_self_of_mem
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : CliffordAlgebra Q}
(hx : x ∈ pinGroup Q)
:
x * star x = 1
theorem
pinGroup.star_mem
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : CliffordAlgebra Q}
(hx : x ∈ pinGroup Q)
:
See star_mem_iff for both directions.
@[simp]
theorem
pinGroup.star_mem_iff
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : CliffordAlgebra Q}
:
An element is in pinGroup Q if and only if star x is in pinGroup Q.
See star_mem for only one direction.
@[implicit_reducible]
instance
pinGroup.instStarSubtypeCliffordAlgebraMemSubmonoid
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
@[simp]
theorem
pinGroup.coe_star
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : ↥(pinGroup Q)}
:
theorem
pinGroup.coe_star_mul_self
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(x : ↥(pinGroup Q))
:
star ↑x * ↑x = 1
theorem
pinGroup.coe_mul_star_self
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(x : ↥(pinGroup Q))
:
↑x * ↑(star x) = 1
@[simp]
theorem
pinGroup.star_mul_self
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(x : ↥(pinGroup Q))
:
star x * x = 1
@[simp]
theorem
pinGroup.mul_star_self
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(x : ↥(pinGroup Q))
:
x * star x = 1
@[implicit_reducible]
instance
pinGroup.instGroupSubtypeCliffordAlgebraMemSubmonoid
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
pinGroup Q forms a group where the inverse is star.
@[implicit_reducible]
instance
pinGroup.instStarMulSubtypeCliffordAlgebraMemSubmonoid
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
@[implicit_reducible]
instance
pinGroup.instInhabitedSubtypeCliffordAlgebraMemSubmonoid
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
Inhabited ↥(pinGroup Q)
theorem
pinGroup.star_eq_inv
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(x : ↥(pinGroup Q))
:
theorem
pinGroup.star_eq_inv'
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
def
pinGroup.toUnits
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
The elements in pinGroup Q embed into (CliffordAlgebra Q)ˣ.
Instances For
@[simp]
theorem
pinGroup.val_toUnits_apply
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(x : ↥(pinGroup Q))
:
↑(toUnits x) = ↑x
@[simp]
theorem
pinGroup.val_inv_toUnits_apply
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(x : ↥(pinGroup Q))
:
theorem
pinGroup.toUnits_injective
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
Function.Injective ⇑toUnits
def
spinGroup
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
:
spinGroup Q is defined as the infimum of pinGroup Q and CliffordAlgebra.even Q.
See mem_iff.
Instances For
theorem
spinGroup.mem_iff
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : CliffordAlgebra Q}
:
x ∈ spinGroup Q ↔ x ∈ pinGroup Q ∧ x ∈ CliffordAlgebra.even Q
An element is in spinGroup Q if and only if it is in pinGroup Q and even Q.
theorem
spinGroup.mem_pin
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : CliffordAlgebra Q}
(hx : x ∈ spinGroup Q)
:
x ∈ pinGroup Q
theorem
spinGroup.mem_even
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : CliffordAlgebra Q}
(hx : x ∈ spinGroup Q)
:
x ∈ CliffordAlgebra.even Q
theorem
spinGroup.units_mem_lipschitzGroup
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : (CliffordAlgebra Q)ˣ}
(hx : ↑x ∈ spinGroup Q)
:
x ∈ lipschitzGroup Q
theorem
spinGroup.involute_eq
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : CliffordAlgebra Q}
(hx : x ∈ spinGroup Q)
:
CliffordAlgebra.involute x = x
If x is in spinGroup Q, then involute x is equal to x.
theorem
spinGroup.units_involute_act_eq_conjAct
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : (CliffordAlgebra Q)ˣ}
(hx : ↑x ∈ spinGroup Q)
(y : M)
:
CliffordAlgebra.involute ↑x * (CliffordAlgebra.ι Q) y * ↑x⁻¹ = ConjAct.toConjAct x • (CliffordAlgebra.ι Q) y
theorem
spinGroup.conjAct_smul_ι_mem_range_ι
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : (CliffordAlgebra Q)ˣ}
(hx : ↑x ∈ spinGroup Q)
[Invertible 2]
(y : M)
:
ConjAct.toConjAct x • (CliffordAlgebra.ι Q) y ∈ (CliffordAlgebra.ι Q).range
The conjugation action by elements of the spin group keeps vectors as vectors.
theorem
spinGroup.involute_act_ι_mem_range_ι
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : (CliffordAlgebra Q)ˣ}
(hx : ↑x ∈ spinGroup Q)
[Invertible 2]
(y : M)
:
CliffordAlgebra.involute ↑x * (CliffordAlgebra.ι Q) y * ↑x⁻¹ ∈ (CliffordAlgebra.ι Q).range
theorem
spinGroup.conjAct_smul_range_ι
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : (CliffordAlgebra Q)ˣ}
(hx : ↑x ∈ spinGroup Q)
[Invertible 2]
:
ConjAct.toConjAct x • (CliffordAlgebra.ι Q).range = (CliffordAlgebra.ι Q).range
@[simp]
theorem
spinGroup.star_mul_self_of_mem
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : CliffordAlgebra Q}
(hx : x ∈ spinGroup Q)
:
star x * x = 1
@[simp]
theorem
spinGroup.mul_star_self_of_mem
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : CliffordAlgebra Q}
(hx : x ∈ spinGroup Q)
:
x * star x = 1
theorem
spinGroup.star_mem
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : CliffordAlgebra Q}
(hx : x ∈ spinGroup Q)
:
See star_mem_iff for both directions.
@[simp]
theorem
spinGroup.star_mem_iff
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : CliffordAlgebra Q}
:
An element is in spinGroup Q if and only if star x is in spinGroup Q.
See star_mem for only one direction.
@[implicit_reducible]
instance
spinGroup.instStarSubtypeCliffordAlgebraMemSubmonoid
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
@[simp]
theorem
spinGroup.coe_star
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{x : ↥(spinGroup Q)}
:
theorem
spinGroup.coe_star_mul_self
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(x : ↥(spinGroup Q))
:
star ↑x * ↑x = 1
theorem
spinGroup.coe_mul_star_self
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(x : ↥(spinGroup Q))
:
↑x * ↑(star x) = 1
@[simp]
theorem
spinGroup.star_mul_self
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(x : ↥(spinGroup Q))
:
star x * x = 1
@[simp]
theorem
spinGroup.mul_star_self
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(x : ↥(spinGroup Q))
:
x * star x = 1
@[implicit_reducible]
instance
spinGroup.instGroupSubtypeCliffordAlgebraMemSubmonoid
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
spinGroup Q forms a group where the inverse is star.
@[implicit_reducible]
instance
spinGroup.instStarMulSubtypeCliffordAlgebraMemSubmonoid
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
@[implicit_reducible]
instance
spinGroup.instInhabitedSubtypeCliffordAlgebraMemSubmonoid
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
Inhabited ↥(spinGroup Q)
theorem
spinGroup.star_eq_inv
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(x : ↥(spinGroup Q))
:
theorem
spinGroup.star_eq_inv'
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
def
spinGroup.toUnits
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
The elements in spinGroup Q embed into (CliffordAlgebra Q)ˣ.
Instances For
@[simp]
theorem
spinGroup.val_inv_toUnits_apply
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(x : ↥(spinGroup Q))
:
@[simp]
theorem
spinGroup.val_toUnits_apply
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(x : ↥(spinGroup Q))
:
↑(toUnits x) = ↑x
theorem
spinGroup.toUnits_injective
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
Function.Injective ⇑toUnits