Vector generators of the Lipschitz group

This file packages a vector of invertible quadratic norm as a Clifford-algebra unit and records the corresponding generator membership and inverse coercion facts, together with the triviality of the Lipschitz group of the zero module. The twisted-conjugation action itself is defined in Lipschitz.Action.

Main definitions

• CliffordAlgebra.unitι Q v is the unit represented by a vector v of invertible norm.
• CliffordAlgebra.unitι_mem_lipschitzGroup records that this unit generates the Lipschitz group.
• CliffordAlgebra.coe_unitι_inv computes its inverse as a vector.
• CliffordAlgebra.lipschitzGroup_eq_bot records that the Lipschitz group of the zero module is trivial.

def CliffordAlgebra.unitι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] : (CliffordAlgebra Q)ˣ

A vector of invertible norm, as a unit of the Clifford algebra.

Equations

• CliffordAlgebra.unitι Q v = unitOfInvertible ((CliffordAlgebra.ι Q) v)

@[simp]

theorem CliffordAlgebra.coe_unitι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (v : M) [Invertible (Q v)] : ↑(unitι Q v) = (ι Q) v

@[simp]

theorem CliffordAlgebra.coe_unitι_inv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (v : M) [Invertible (Q v)] : ↑(unitι Q v)⁻¹ = (ι Q) (⅟(Q v) • v)

The inverse of a vector of invertible norm v is the vector ⅟(Q v) • v.

theorem CliffordAlgebra.unitι_mem_lipschitzGroup {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (v : M) [Invertible (Q v)] : unitι Q v ∈ lipschitzGroup Q

The vectors of invertible norm are the generators of the Lipschitz group.

theorem CliffordAlgebra.lipschitzGroup_eq_bot {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Subsingleton M] : lipschitzGroup Q = ⊥

The Lipschitz group of a quadratic form on the zero module is trivial: its only vector is 0, which is not a unit unless the Clifford algebra is itself trivial.