mathlib documentation

linear_algebra.clifford_algebra.equivs

Other constructions isomorphic to Clifford Algebras #

This file contains isomorphisms showing that other types are equivalent to some clifford_algebra.

Rings #

Complex numbers #

We show additionally that this equivalence sends complex.conj to clifford_algebra.involute and vice-versa:

Note that in this algebra clifford_algebra.reverse is the identity and so the clifford conjugate is the same as clifford_algebra.involute.

Quaternion algebras #

We show additionally that this equivalence sends quaternion_algebra.conj to the clifford conjugate and vice-versa:

The clifford algebra isomorphic to a ring #

@[simp]

The clifford algebra over a 0-dimensional vector space is isomorphic to its scalars.

Equations

The clifford algebra isomorphic to the complex numbers #

The quadratic form sending elements to the negation of their square.

Equations
@[instance]

The clifford algebra is commutative since it is isomorphic to the complex numbers.

TODO: prove this is true for all clifford_algebras over a 1-dimensional vector space.

Equations

The clifford algebra isomorphic to the quaternions #

def clifford_algebra_quaternion.Q {R : Type u_1} [comm_ring R] (c₁ c₂ : R) :

Q c₁ c₂ is a quadratic form over R × R such that clifford_algebra (Q c₁ c₂) is isomorphic as an R-algebra to ℍ[R,c₁,c₂].

Equations
@[simp]
theorem clifford_algebra_quaternion.Q_apply {R : Type u_1} [comm_ring R] (c₁ c₂ : R) (v : R × R) :
(clifford_algebra_quaternion.Q c₁ c₂) v = c₁ * (v.fst) * v.fst + c₂ * (v.snd) * v.snd

The quaternion basis vectors within the algebra.

Equations

Intermediate result of clifford_algebra_quaternion.equiv: clifford algebras over clifford_algebra_quaternion.Q can be converted to ℍ[R,c₁,c₂].

Equations
@[simp]

The "clifford conjugate" (aka involute ∘ reverse = reverse ∘ involute) maps to the quaternion conjugate.

Map a quaternion into the clifford algebra.

Equations
@[simp]
@[simp]

The quaternion conjugate maps to the "clifford conjugate" (aka involute ∘ reverse = reverse ∘ involute).