Basic Clifford algebra API

This file records general scalar properties of a Clifford algebra obtained from Mathlib's linear equivalence with the exterior algebra.

theorem CliffordAlgebra.equivExterior_algebraMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (r : R) : (equivExterior Q) ((algebraMap R (CliffordAlgebra Q)) r) = (algebraMap R (ExteriorAlgebra R M)) r

CliffordAlgebra.equivExterior sends a scalar to the corresponding scalar of the exterior algebra.

theorem CliffordAlgebra.algebraMap_injective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : Function.Injective ⇑(algebraMap R (CliffordAlgebra Q))

The scalars of a Clifford algebra are a faithful copy of R.

instance CliffordAlgebra.faithfulSMul {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : FaithfulSMul R (CliffordAlgebra Q)

The scalar action on a Clifford algebra is faithful when 2 is invertible. With this instance, Mathlib's scalar iff lemmas apply directly.

theorem CliffordAlgebra.exists_eq_algebraMap_of_contractLeft_eq_zero {M : Type v} [AddCommGroup M] {K : Type u} [Field K] [Module K M] [FiniteDimensional K M] [Invertible 2] (Q : QuadraticForm K M) (x : CliffordAlgebra Q) (hx : ∀ (d : Module.Dual K M), (contractLeft d) x = 0) : ∃ (r : K), x = (algebraMap K (CliffordAlgebra Q)) r

A Clifford element annihilated by every left contraction is a scalar.

theorem CliffordAlgebra.exists_eq_algebraMap_of_involute_mul_ι_eq_ι_mul {M : Type v} [AddCommGroup M] {K : Type u} [Field K] [Module K M] [FiniteDimensional K M] [Invertible 2] (Q : QuadraticForm K M) (hQ : QuadraticMap.Nondegenerate) (x : CliffordAlgebra Q) (hx : ∀ (v : M), involute x * (ι Q) v = (ι Q) v * x) : ∃ (r : K), x = (algebraMap K (CliffordAlgebra Q)) r

A Clifford element that graded-commutes with every generating vector is a scalar. Here involute x * ι v = ι v * x is the uniform equation combining commutation of the even part with anticommutation of the odd part.

theorem CliffordAlgebra.exists_eq_algebraMap_of_mem_even_of_commute {M : Type v} [AddCommGroup M] {K : Type u} [Field K] [Module K M] [FiniteDimensional K M] [Invertible 2] (Q : QuadraticForm K M) (hQ : QuadraticMap.Nondegenerate) (x : CliffordAlgebra Q) (hx_even : x ∈ even Q) (hx_comm : ∀ (v : M), Commute x ((ι Q) v)) : ∃ (r : K), x = (algebraMap K (CliffordAlgebra Q)) r

An even Clifford element that commutes with every generating vector is a scalar.