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:

Dual numbers #

The clifford algebra isomorphic to a ring #

@[simp]
@[protected]

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

Equations

The clifford algebra isomorphic to the complex numbers #

@[protected]

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

Equations
@[protected, 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 #

@[protected]
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]
@[simp]
@[simp]

The quaternion conjugate maps to the "clifford conjugate" (aka star).

The clifford algebra isomorphic to the dual numbers #

theorem clifford_algebra_dual_number.ι_mul_ι {R : Type u_1} [comm_ring R] (r₁ r₂ : R) :
@[protected]

The clifford algebra over a 1-dimensional vector space with 0 quadratic form is isomorphic to the dual numbers.

Equations