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:
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.
Equations
- lipschitzGroup Q = Subgroup.closure (Units.val ⁻¹' Set.range ⇑(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 ∈ LinearMap.range (CliffordAlgebra.ι Q)
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⁻¹ ∈ LinearMap.range (CliffordAlgebra.ι Q)
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 • LinearMap.range (CliffordAlgebra.ι Q) = LinearMap.range (CliffordAlgebra.ι Q)
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.
Equations
- pinGroup Q = Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ⊓ unitary (CliffordAlgebra Q)
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 ∈ LinearMap.range (CliffordAlgebra.ι Q)
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⁻¹ ∈ LinearMap.range (CliffordAlgebra.ι Q)
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 • LinearMap.range (CliffordAlgebra.ι Q) = LinearMap.range (CliffordAlgebra.ι Q)
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)
:
@[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)
:
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.
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))
:
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))
:
@[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))
:
@[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))
:
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.
instance
pinGroup.instStarMulSubtypeCliffordAlgebraMemSubmonoid
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
Equations
- pinGroup.instStarMulSubtypeCliffordAlgebraMemSubmonoid = StarMul.mk ⋯
instance
pinGroup.instInhabitedSubtypeCliffordAlgebraMemSubmonoid
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
Equations
- pinGroup.instInhabitedSubtypeCliffordAlgebraMemSubmonoid = { default := 1 }
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}
:
star = Inv.inv
def
pinGroup.toUnits
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
↥(pinGroup Q) →* (CliffordAlgebra Q)ˣ
The elements in pinGroup Q embed into (CliffordAlgebra Q)ˣ.
Equations
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))
:
↑(pinGroup.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 ⇑pinGroup.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.
Equations
- spinGroup Q = pinGroup Q ⊓ (CliffordAlgebra.even Q).toSubring.toSubmonoid
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}
:
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)
:
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)
:
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 ∈ LinearMap.range (CliffordAlgebra.ι Q)
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⁻¹ ∈ LinearMap.range (CliffordAlgebra.ι Q)
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 • LinearMap.range (CliffordAlgebra.ι Q) = LinearMap.range (CliffordAlgebra.ι Q)
@[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)
:
@[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)
:
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.
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))
:
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))
:
@[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))
:
@[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))
:
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.
instance
spinGroup.instStarMulSubtypeCliffordAlgebraMemSubmonoid
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
Equations
- spinGroup.instStarMulSubtypeCliffordAlgebraMemSubmonoid = StarMul.mk ⋯
instance
spinGroup.instInhabitedSubtypeCliffordAlgebraMemSubmonoid
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
Equations
- spinGroup.instInhabitedSubtypeCliffordAlgebraMemSubmonoid = { default := 1 }
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}
:
star = Inv.inv
def
spinGroup.toUnits
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
↥(spinGroup Q) →* (CliffordAlgebra Q)ˣ
The elements in spinGroup Q embed into (CliffordAlgebra Q)ˣ.
Equations
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))
:
↑(spinGroup.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 ⇑spinGroup.toUnits