The Lipschitz group acting on its quadratic space by twisted conjugation

The Lipschitz group of a quadratic form acts on the underlying quadratic space by twisted conjugation, v ↦ involute x * ι v * x⁻¹. This common action restricts along CliffordAlgebra.pinToLipschitz to the Pin homomorphism CliffordAlgebra.pinToOrthogonal; under the usual positive-dimensional finite-dimensional nondegenerate hypotheses over a field with 2 invertible, that Pin restriction has the canonical order-two kernel generated by -1; over separably closed fields its image is the full orthogonal group, giving the double-cover statements in the Pin modules. The Lipschitz action itself is kept general here, so this module makes no kernel claim for lipschitzToOrthogonal. The twist by the grade involution CliffordAlgebra.involute is what makes a single vector act by the reflection in its orthogonal hyperplane rather than by minus that reflection, so it is the twisted conjugation, not the plain one, that carries the generators of the Lipschitz group to the generators of the orthogonal group.

Mathlib knows that twisted conjugation by a Lipschitz element keeps vectors as vectors (lipschitzGroup.involute_act_ι_mem_range_ι), but not that the resulting map of the quadratic space preserves the form, nor that it is a group homomorphism. This file supplies the action, its form-preservation theorem, and the resulting homomorphism to the orthogonal group. The form-preservation theorem is the bridge used by the Pin and Spin action comparisons and by later surjectivity results.

Main definitions

• CliffordAlgebra.vectorMap Q x: the unbundled endomorphism of the quadratic space induced by twisted conjugation by any Clifford unit x, the vector part of involute x * ι v * x⁻¹.
• CliffordAlgebra.lipschitzVectorAction Q x: the automorphism of the quadratic space induced by twisted conjugation by a Lipschitz element.
• CliffordAlgebra.lipschitzToOrthogonal Q: the resulting homomorphism to O(Q).

Main results

• CliffordAlgebra.vectorMap_map_app_of_involute_act_ι_mem_range_ι: twisted conjugation by a unit carrying vectors to vectors preserves the quadratic form, because the twisted conjugate of ι v and its grade involute multiply to the scalar Q v. This is stated for every unit of the classical Clifford group, so it also serves the identification of that group with the Lipschitz group in TauCeti.LinearAlgebra.CliffordAlgebra.Lipschitz.CliffordGroup.
• CliffordAlgebra.lipschitzVectorAction_unitι: a vector acts by the reflection in its orthogonal hyperplane. This is the identification of the generators referred to above.
• CliffordAlgebra.lipschitzVectorAction_map_app: twisted conjugation by a Lipschitz element preserves the quadratic form, so the action lands in its orthogonal group and can be composed with orthogonal actions of the Pin and Spin subgroups.

The pinToLipschitz inclusion lives in TauCeti.LinearAlgebra.CliffordAlgebra.Pin.Basic; its comparison with the Pin and Spin actions lives in TauCeti.LinearAlgebra.CliffordAlgebra.Pin.Action.

Surjectivity of lipschitzToOrthogonal Q (Cartan--Dieudonné) needs a field of characteristic not two, a nondegenerate form and finite dimension, and is not attempted here. The Pin kernel and surjectivity statements belong to the pinToOrthogonal modules; everything below holds over a commutative ring, with 2 invertible only where Mathlib's twisted-conjugation lemmas require it.

References

See H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2, and C. Chevalley, The Algebraic Theory of Spinors (1954), Chapter II.

Twisted conjugation

The induced map on the quadratic space

Twisted conjugation by a Lipschitz element carries vectors to vectors, so it descends to the quadratic space through the vector part CliffordAlgebra.ιInv. The unbundled form vectorMap below is a plain linear endomorphism, defined for every unit but characterized only on the units whose twisted conjugation preserves the vectors, the classical Clifford group; the bundled automorphism on the Lipschitz group is lipschitzVectorAction.

def CliffordAlgebra.vectorMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : (CliffordAlgebra Q)ˣ) : M →ₗ[R] M

The unbundled twisted-conjugation endomorphism of the quadratic space induced by a Clifford unit x: the vector part of involute x * ι Q m * x⁻¹. It is characterized by ι_vectorMap_apply_of_mem_range_ι whenever that twisted conjugate is again a vector, as it is for every Lipschitz element (lipschitzGroup.involute_act_ι_mem_range_ι).

Equations

• CliffordAlgebra.vectorMap Q x = CliffordAlgebra.ιInv Q ∘ₗ CliffordAlgebra.twistedConj✝ Q x ∘ₗ CliffordAlgebra.ι Q

theorem CliffordAlgebra.ι_vectorMap_apply_of_mem_range_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {x : (CliffordAlgebra Q)ˣ} {m : M} (hm : involute ↑x * (ι Q) m * ↑x⁻¹ ∈ (ι Q).range) : (ι Q) ((vectorMap Q x) m) = involute ↑x * (ι Q) m * ↑x⁻¹

When the twisted conjugate of a vector is again a vector, vectorMap recovers it.

theorem CliffordAlgebra.vectorMap_map_app_of_involute_act_ι_mem_range_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {x : (CliffordAlgebra Q)ˣ} (hx : ∀ (m : M), involute ↑x * (ι Q) m * ↑x⁻¹ ∈ (ι Q).range) (m : M) : Q ((vectorMap Q x) m) = Q m

Twisted conjugation by a unit carrying vectors to vectors preserves the quadratic form. The twisted conjugate of ι Q m and its grade involute x * ι Q m * involute x⁻¹ multiply to the scalar Q m.

The action of the Lipschitz group

def CliffordAlgebra.lipschitzVectorAction {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(lipschitzGroup Q)) : M ≃ₗ[R] M

The automorphism of the quadratic space induced by twisted conjugation by an element of the Lipschitz group. It is characterized by ι_lipschitzVectorAction_apply, which identifies it with twisted conjugation inside the Clifford algebra.

Equations

• CliffordAlgebra.lipschitzVectorAction Q x = (CliffordAlgebra.vectorActionHom✝ Q) x

@[simp]

theorem CliffordAlgebra.lipschitzVectorAction_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : lipschitzVectorAction Q 1 = LinearEquiv.refl R M

The identity Lipschitz element acts by the identity linear equivalence.

@[simp]

theorem CliffordAlgebra.lipschitzVectorAction_mul {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x y : ↥(lipschitzGroup Q)) : lipschitzVectorAction Q (x * y) = lipschitzVectorAction Q x * lipschitzVectorAction Q y

The action homomorphism sends products to composition of linear equivalences.

@[simp]

theorem CliffordAlgebra.ι_lipschitzVectorAction_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (x : ↥(lipschitzGroup Q)) (m : M) : (ι Q) ((lipschitzVectorAction Q x) m) = involute ↑↑x * (ι Q) m * ↑(↑x)⁻¹

A Lipschitz element acts on a vector by twisted conjugation inside the Clifford algebra.

@[simp]

theorem CliffordAlgebra.lipschitzVectorAction_unitι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (v : M) [Invertible (Q v)] : lipschitzVectorAction Q ⟨unitι Q v, ⋯⟩ = TauCeti.QuadraticMap.reflection Q v

A vector acts by the reflection in its orthogonal hyperplane. These are the generators of the Lipschitz group, so this identification is what Cartan--Dieudonné turns into surjectivity of lipschitzToOrthogonal.

@[simp]

theorem CliffordAlgebra.lipschitzVectorAction_map_app {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (x : ↥(lipschitzGroup Q)) (m : M) : Q ((lipschitzVectorAction Q x) m) = Q m

Twisted conjugation by a Lipschitz element preserves the quadratic form. This identity shows that the bundled action defines an element of the orthogonal group and is used to construct lipschitzToOrthogonal.

def CliffordAlgebra.lipschitzToOrthogonal {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : ↥(lipschitzGroup Q) →* ↥(TauCeti.QuadraticMap.orthogonalGroup Q)

The twisted-conjugation homomorphism from the Lipschitz group to the orthogonal group of the quadratic form.

Equations

• CliffordAlgebra.lipschitzToOrthogonal Q = { toFun := fun (x : ↥(lipschitzGroup Q)) => ⟨CliffordAlgebra.lipschitzVectorAction Q x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CliffordAlgebra.coe_lipschitzToOrthogonal_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(lipschitzGroup Q)) (m : M) : ↑((lipschitzToOrthogonal Q) x) m = (lipschitzVectorAction Q x) m

@[instance_reducible]

noncomputable instance CliffordAlgebra.instDistribMulActionLipschitzGroup {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : DistribMulAction (↥(lipschitzGroup Q)) M

The standard additive action induced by the orthogonal-group homomorphism.

Equations

• CliffordAlgebra.instDistribMulActionLipschitzGroup Q = { toMulAction := MulAction.compHom M (CliffordAlgebra.lipschitzToOrthogonal Q), smul_zero := ⋯, smul_add := ⋯ }

@[simp]

theorem CliffordAlgebra.lipschitzGroup_smul_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(lipschitzGroup Q)) (m : M) : x • m = (lipschitzVectorAction Q x) m

Pointwise form of the standard Lipschitz-group action.

@[simp]

theorem CliffordAlgebra.lipschitzToOrthogonal_unitι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (v : M) [Invertible (Q v)] : (lipschitzToOrthogonal Q) ⟨unitι Q v, ⋯⟩ = TauCeti.QuadraticMap.reflectionOrthogonal Q v

A generating vector acts by its bundled orthogonal reflection.