The Pin group inside the Lipschitz group

The Pin group is the subgroup of the Lipschitz group whose elements have unit Clifford norm. This file packages its inclusion into the Lipschitz group, the vector generators with norm -1, and the Spin inclusion used when transporting norms and actions along those maps.

TauCeti.CliffordAlgebra.coe_inv_pinToLipschitz identifies the inverse unit coordinate of a Pin element's image in the Lipschitz group with its Clifford star.

theorem CliffordAlgebra.ι_mem_pinGroup {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {v : M} (hv : Q v = -1) : (ι Q) v ∈ pinGroup Q

A vector of norm -1 lies in the Pin group. The sign is Mathlib's convention: star is the reversal composed with the grade involution, so the unitarity condition reads -Q v = 1.

def CliffordAlgebra.pinToLipschitz {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : ↥(pinGroup Q) →* ↥(lipschitzGroup Q)

The Pin group includes into the Lipschitz group.

Equations

• CliffordAlgebra.pinToLipschitz Q = { toFun := fun (x : ↥(pinGroup Q)) => ⟨pinGroup.toUnits x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CliffordAlgebra.coe_pinToLipschitz_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : ↥(pinGroup Q)) : ↑↑((pinToLipschitz Q) x) = ↑x

@[simp]

theorem TauCeti.CliffordAlgebra.coe_inv_pinToLipschitz {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : ↥(pinGroup Q)) : ↑(↑((CliffordAlgebra.pinToLipschitz Q) x))⁻¹ = star ↑x

The inverse unit coordinate of a Pin element in the Lipschitz group is its Clifford star.

def CliffordAlgebra.spinToPin {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : ↥(spinGroup Q) →* ↥(pinGroup Q)

The spin group sits inside the Pin group.

Equations

• CliffordAlgebra.spinToPin Q = Submonoid.inclusion ⋯

@[simp]

theorem CliffordAlgebra.coe_spinToPin_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : ↥(spinGroup Q)) : ↑((spinToPin Q) x) = ↑x