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 of lipschitzGroup and unitary.
• spinGroup: the Spin group defined as the infimum of pinGroup and CliffordAlgebra.even.

Implementation Notes

The definition of the Lipschitz group $\{x\in \mathcal{C}\ell |x\text{ is invertible and }xv{x}^{-1}\in 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) : Subgroup (CliffordAlgebra Q)ˣ

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))

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) : Submonoid (CliffordAlgebra Q)

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)

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) : 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) : star 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} : star x ∈ pinGroup Q ↔ x ∈ pinGroup 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} : Star ↥(pinGroup Q)

Equations

• pinGroup.instStarSubtypeCliffordAlgebraMemSubmonoid = { star := fun (x : ↥(pinGroup Q)) => ⟨star ↑x, ⋯⟩ }

@[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)} : ↑(star x) = star ↑x

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

instance pinGroup.instGroupSubtypeCliffordAlgebraMemSubmonoid {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} : Group ↥(pinGroup Q)

pinGroup Q forms a group where the inverse is star.

Equations

• pinGroup.instGroupSubtypeCliffordAlgebraMemSubmonoid = Group.mk ⋯

instance pinGroup.instStarMulSubtypeCliffordAlgebraMemSubmonoid {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} : StarMul ↥(pinGroup Q)

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} : Inhabited ↥(pinGroup Q)

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)) : star x = x⁻¹

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

• pinGroup.toUnits = { toFun := fun (x : ↥(pinGroup Q)) => { val := ↑x, inv := ↑x⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

@[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)) : ↑(pinGroup.toUnits x)⁻¹ = ↑x⁻¹

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) : Submonoid (CliffordAlgebra Q)

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

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 ∈ 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) : 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) : star 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} : star x ∈ spinGroup Q ↔ x ∈ spinGroup 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} : Star ↥(spinGroup Q)

Equations

• spinGroup.instStarSubtypeCliffordAlgebraMemSubmonoid = { star := fun (x : ↥(spinGroup Q)) => ⟨star ↑x, ⋯⟩ }

@[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)} : ↑(star x) = star ↑x

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

instance spinGroup.instGroupSubtypeCliffordAlgebraMemSubmonoid {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} : Group ↥(spinGroup Q)

spinGroup Q forms a group where the inverse is star.

Equations

• spinGroup.instGroupSubtypeCliffordAlgebraMemSubmonoid = Group.mk ⋯

instance spinGroup.instStarMulSubtypeCliffordAlgebraMemSubmonoid {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} : StarMul ↥(spinGroup Q)

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} : Inhabited ↥(spinGroup Q)

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)) : star x = x⁻¹

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

• spinGroup.toUnits = { toFun := fun (x : ↥(spinGroup Q)) => { val := ↑x, inv := ↑x⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

@[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)) : ↑(spinGroup.toUnits x)⁻¹ = ↑x⁻¹

@[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