Other constructions isomorphic to Clifford Algebras #

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

Complex numbers #

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

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

Quaternion algebras #

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

Dual numbers #

The clifford algebra isomorphic to a ring #

@[simp]
theorem CliffordAlgebraRing.ι_eq_zero {R : Type u_1} [] :

Since the vector space is empty the ring is commutative.

Equations
• CliffordAlgebraRing.instCommRingCliffordAlgebraUnitOfNatQuadraticForm = let __src := ;
theorem CliffordAlgebraRing.reverse_apply {R : Type u_1} [] (x : ) :
CliffordAlgebra.reverse x = x
@[simp]
theorem CliffordAlgebraRing.reverse_eq_id {R : Type u_1} [] :
CliffordAlgebra.reverse = LinearMap.id
@[simp]
theorem CliffordAlgebraRing.involute_eq_id {R : Type u_1} [] :
CliffordAlgebra.involute =
def CliffordAlgebraRing.equiv {R : Type u_1} [] :

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

Equations
Instances For

The clifford algebra isomorphic to the complex numbers #

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

Equations
Instances For
@[simp]
theorem CliffordAlgebraComplex.Q_apply (r : ) :
CliffordAlgebraComplex.Q r = -(r * r)

Intermediate result for CliffordAlgebraComplex.equiv: clifford algebras over CliffordAlgebraComplex.Q above can be converted to .

Equations
Instances For
@[simp]
theorem CliffordAlgebraComplex.toComplex_ι (r : ) :
CliffordAlgebraComplex.toComplex =
@[simp]
theorem CliffordAlgebraComplex.toComplex_involute :
CliffordAlgebraComplex.toComplex (CliffordAlgebra.involute c) = () (CliffordAlgebraComplex.toComplex c)

CliffordAlgebra.involute is analogous to Complex.conj.

Intermediate result for CliffordAlgebraComplex.equiv: can be converted to CliffordAlgebraComplex.Q above can be converted to.

Equations
Instances For
@[simp]
theorem CliffordAlgebraComplex.ofComplex_I :
CliffordAlgebraComplex.ofComplex Complex.I =
@[simp]
theorem CliffordAlgebraComplex.toComplex_ofComplex (c : ) :
CliffordAlgebraComplex.toComplex (CliffordAlgebraComplex.ofComplex c) = c
@[simp]
theorem CliffordAlgebraComplex.ofComplex_toComplex :
CliffordAlgebraComplex.ofComplex (CliffordAlgebraComplex.toComplex c) = c
@[simp]
theorem CliffordAlgebraComplex.equiv_symm_apply (a : ) :
= CliffordAlgebraComplex.ofComplex a
@[simp]
theorem CliffordAlgebraComplex.equiv_apply :
CliffordAlgebraComplex.equiv a = CliffordAlgebraComplex.toComplex a

The clifford algebras over CliffordAlgebraComplex.Q is isomorphic as an -algebra to .

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

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

Equations
• One or more equations did not get rendered due to their size.
theorem CliffordAlgebraComplex.reverse_apply :
CliffordAlgebra.reverse x = x

reverse is a no-op over CliffordAlgebraComplex.Q.

@[simp]
theorem CliffordAlgebraComplex.reverse_eq_id :
CliffordAlgebra.reverse = LinearMap.id
@[simp]
theorem CliffordAlgebraComplex.ofComplex_conj (c : ) :
CliffordAlgebraComplex.ofComplex (() c) = CliffordAlgebra.involute (CliffordAlgebraComplex.ofComplex c)

Complex.conj is analogous to CliffordAlgebra.involute.

The clifford algebra isomorphic to the quaternions #

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

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

Equations
Instances For
@[simp]
theorem CliffordAlgebraQuaternion.Q_apply {R : Type u_1} [] (c₁ : R) (c₂ : R) (v : R × R) :
() v = c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)
@[simp]
theorem CliffordAlgebraQuaternion.quaternionBasis_j {R : Type u_1} [] (c₁ : R) (c₂ : R) :
= () (0, 1)
@[simp]
theorem CliffordAlgebraQuaternion.quaternionBasis_i {R : Type u_1} [] (c₁ : R) (c₂ : R) :
= () (1, 0)
@[simp]
theorem CliffordAlgebraQuaternion.quaternionBasis_k {R : Type u_1} [] (c₁ : R) (c₂ : R) :
= () (1, 0) * () (0, 1)
def CliffordAlgebraQuaternion.quaternionBasis {R : Type u_1} [] (c₁ : R) (c₂ : R) :

The quaternion basis vectors within the algebra.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CliffordAlgebraQuaternion.toQuaternion {R : Type u_1} [] {c₁ : R} {c₂ : R} :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CliffordAlgebraQuaternion.toQuaternion_ι {R : Type u_1} [] {c₁ : R} {c₂ : R} (v : R × R) :
CliffordAlgebraQuaternion.toQuaternion (() v) = { re := 0, imI := v.1, imJ := v.2, imK := 0 }
theorem CliffordAlgebraQuaternion.toQuaternion_star {R : Type u_1} [] {c₁ : R} {c₂ : R} (c : ) :
CliffordAlgebraQuaternion.toQuaternion (star c) = star (CliffordAlgebraQuaternion.toQuaternion c)

The "clifford conjugate" maps to the quaternion conjugate.

def CliffordAlgebraQuaternion.ofQuaternion {R : Type u_1} [] {c₁ : R} {c₂ : R} :

Map a quaternion into the clifford algebra.

Equations
• CliffordAlgebraQuaternion.ofQuaternion = .liftHom
Instances For
@[simp]
theorem CliffordAlgebraQuaternion.ofQuaternion_mk {R : Type u_1} [] {c₁ : R} {c₂ : R} (a₁ : R) (a₂ : R) (a₃ : R) (a₄ : R) :
CliffordAlgebraQuaternion.ofQuaternion { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } = () a₁ + a₂ () (1, 0) + a₃ () (0, 1) + a₄ (() (1, 0) * () (0, 1))
@[simp]
theorem CliffordAlgebraQuaternion.ofQuaternion_comp_toQuaternion {R : Type u_1} [] {c₁ : R} {c₂ : R} :
CliffordAlgebraQuaternion.ofQuaternion.comp CliffordAlgebraQuaternion.toQuaternion =
@[simp]
theorem CliffordAlgebraQuaternion.ofQuaternion_toQuaternion {R : Type u_1} [] {c₁ : R} {c₂ : R} (c : ) :
CliffordAlgebraQuaternion.ofQuaternion (CliffordAlgebraQuaternion.toQuaternion c) = c
@[simp]
theorem CliffordAlgebraQuaternion.toQuaternion_comp_ofQuaternion {R : Type u_1} [] {c₁ : R} {c₂ : R} :
CliffordAlgebraQuaternion.toQuaternion.comp CliffordAlgebraQuaternion.ofQuaternion = AlgHom.id R (QuaternionAlgebra R c₁ c₂)
@[simp]
theorem CliffordAlgebraQuaternion.toQuaternion_ofQuaternion {R : Type u_1} [] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra R c₁ c₂) :
CliffordAlgebraQuaternion.toQuaternion (CliffordAlgebraQuaternion.ofQuaternion q) = q
@[simp]
theorem CliffordAlgebraQuaternion.equiv_apply {R : Type u_1} [] {c₁ : R} {c₂ : R} (a : ) :
CliffordAlgebraQuaternion.equiv a = CliffordAlgebraQuaternion.toQuaternion a
@[simp]
theorem CliffordAlgebraQuaternion.equiv_symm_apply {R : Type u_1} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
CliffordAlgebraQuaternion.equiv.symm a = CliffordAlgebraQuaternion.ofQuaternion a
def CliffordAlgebraQuaternion.equiv {R : Type u_1} [] {c₁ : R} {c₂ : R} :

The clifford algebra over CliffordAlgebraQuaternion.Q c₁ c₂ is isomorphic as an R-algebra to ℍ[R,c₁,c₂].

Equations
• CliffordAlgebraQuaternion.equiv = AlgEquiv.ofAlgHom CliffordAlgebraQuaternion.toQuaternion CliffordAlgebraQuaternion.ofQuaternion
Instances For
@[simp]
theorem CliffordAlgebraQuaternion.ofQuaternion_star {R : Type u_1} [] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra R c₁ c₂) :
CliffordAlgebraQuaternion.ofQuaternion (star q) = star (CliffordAlgebraQuaternion.ofQuaternion q)

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

The clifford algebra isomorphic to the dual numbers #

theorem CliffordAlgebraDualNumber.ι_mul_ι {R : Type u_1} [] (r₁ : R) (r₂ : R) :
r₁ * r₂ = 0

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CliffordAlgebraDualNumber.equiv_ι {R : Type u_1} [] (r : R) :
CliffordAlgebraDualNumber.equiv ( r) = r DualNumber.eps
@[simp]
theorem CliffordAlgebraDualNumber.equiv_symm_eps {R : Type u_1} [] :