Clifford algebras of zero-dimensional modules

The Clifford algebra of a subsingleton module consists only of scalars. This file records the canonical algebra equivalence with the coefficient ring and the resulting elementary behavior of the grading and reversal. These statements let low-dimensional Clifford-group calculations handle dimension zero without choosing a concrete model for the zero module.

The equivalence generalizes Mathlib's CliffordAlgebraRing.equiv from its concrete zero quadratic form on Unit to any subsingleton module.

Main results

• CliffordAlgebra.equivOfSubsingleton identifies a zero-dimensional Clifford algebra with its coefficient ring.
• CliffordAlgebra.even_eq_top_of_subsingleton says that every element is even.
• CliffordAlgebra.reverse_eq_self_of_subsingleton says that reversal is the identity.
• CliffordAlgebra.unitsEquivOfSubsingleton identifies Clifford units with scalar units.

noncomputable def CliffordAlgebra.equivOfSubsingleton {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Subsingleton M] : CliffordAlgebra Q ≃ₐ[R] R

The Clifford algebra of a quadratic form on a subsingleton module is canonically isomorphic to the coefficient ring.

@[simp]

theorem CliffordAlgebra.equivOfSubsingleton_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Subsingleton M] (r : R) : (equivOfSubsingleton Q).symm r = (algebraMap R (CliffordAlgebra Q)) r

The inverse zero-dimensional Clifford equivalence is the scalar inclusion.

@[simp]

theorem CliffordAlgebra.ι_eq_zero_of_subsingleton {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Subsingleton M] (x : M) : (ι Q) x = 0

Every vector has zero image in the Clifford algebra of a subsingleton module.

theorem CliffordAlgebra.even_eq_top_of_subsingleton {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Subsingleton M] : even Q = ⊤

Every element of a zero-dimensional Clifford algebra is even.

@[simp]

theorem CliffordAlgebra.reverse_eq_self_of_subsingleton {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Subsingleton M] (x : CliffordAlgebra Q) : reverse x = x

Reversal is the identity on a zero-dimensional Clifford algebra.

noncomputable def CliffordAlgebra.unitsEquivOfSubsingleton {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Subsingleton M] : (CliffordAlgebra Q)ˣ ≃* Rˣ

Units of a zero-dimensional Clifford algebra are canonically scalar units.

@[simp]

theorem CliffordAlgebra.coe_unitsEquivOfSubsingleton_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Subsingleton M] (x : (CliffordAlgebra Q)ˣ) : ↑((unitsEquivOfSubsingleton Q) x) = (equivOfSubsingleton Q) ↑x

The scalar-unit equivalence has the expected underlying scalar value.

@[simp]

theorem CliffordAlgebra.coe_unitsEquivOfSubsingleton_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Subsingleton M] (u : Rˣ) : ↑((unitsEquivOfSubsingleton Q).symm u) = (equivOfSubsingleton Q).symm ↑u

The inverse scalar-unit equivalence has the expected underlying Clifford value.