Other constructions isomorphic to Clifford Algebras

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

Rings

• CliffordAlgebraRing.equiv: any ring is equivalent to a CliffordAlgebra over a zero-dimensional vector space.

Complex numbers

• CliffordAlgebraComplex.equiv: the Complex numbers are equivalent as an ℝ-algebra to a CliffordAlgebra over a one-dimensional vector space with a quadratic form that satisfies Q (ι Q 1) = -1.
• CliffordAlgebraComplex.toComplex: the forward direction of this equiv
• CliffordAlgebraComplex.ofComplex: the reverse direction of this equiv

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

• CliffordAlgebraComplex.toComplex_involute
• CliffordAlgebraComplex.ofComplex_conj

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

Quaternion algebras

• CliffordAlgebraQuaternion.equiv: a QuaternionAlgebra over R is equivalent as an R-algebra to a clifford algebra over R × R, sending i to (0, 1) and j to (1, 0).
• CliffordAlgebraQuaternion.toQuaternion: the forward direction of this equiv
• CliffordAlgebraQuaternion.ofQuaternion: the reverse direction of this equiv

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

• CliffordAlgebraQuaternion.toQuaternion_star
• CliffordAlgebraQuaternion.ofQuaternion_star

Dual numbers

• CliffordAlgebraDualNumber.equiv: R[ε] is equivalent as an R-algebra to a clifford algebra over R where Q = 0.

The clifford algebra isomorphic to a ring

@[simp]

theorem CliffordAlgebraRing.ι_eq_zero {R : Type u_1} [CommRing R] : CliffordAlgebra.ι 0 = 0

instance CliffordAlgebraRing.instCommRingCliffordAlgebraUnitOfNatQuadraticForm {R : Type u_1} [CommRing R] : CommRing (CliffordAlgebra 0)

Since the vector space is empty the ring is commutative.

Equations

• CliffordAlgebraRing.instCommRingCliffordAlgebraUnitOfNatQuadraticForm = { toRing := instRingCliffordAlgebra 0, mul_comm := ⋯ }

theorem CliffordAlgebraRing.reverse_apply {R : Type u_1} [CommRing R] (x : CliffordAlgebra 0) : CliffordAlgebra.reverse x = x

@[simp]

theorem CliffordAlgebraRing.reverse_eq_id {R : Type u_1} [CommRing R] : CliffordAlgebra.reverse = LinearMap.id

@[simp]

theorem CliffordAlgebraRing.involute_eq_id {R : Type u_1} [CommRing R] : CliffordAlgebra.involute = AlgHom.id R (CliffordAlgebra 0)

def CliffordAlgebraRing.equiv {R : Type u_1} [CommRing R] : CliffordAlgebra 0 ≃ₐ[R] R

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

Equations

• CliffordAlgebraRing.equiv = AlgEquiv.ofAlgHom ((CliffordAlgebra.lift 0) ⟨0, ⋯⟩) (Algebra.ofId R (CliffordAlgebra 0)) ⋯ ⋯

The clifford algebra isomorphic to the complex numbers

def CliffordAlgebraComplex.Q : QuadraticForm ℝ ℝ

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

Equations

• CliffordAlgebraComplex.Q = -QuadraticMap.sq

@[simp]

theorem CliffordAlgebraComplex.Q_apply (r : ℝ) : Q r = -(r * r)

def CliffordAlgebraComplex.toComplex : CliffordAlgebra Q →ₐ[ℝ] ℂ

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

Equations

• CliffordAlgebraComplex.toComplex = (CliffordAlgebra.lift CliffordAlgebraComplex.Q) ⟨LinearMap.toSpanSingleton ℝ ℂ Complex.I, CliffordAlgebraComplex.toComplex._proof_1⟩

@[simp]

theorem CliffordAlgebraComplex.toComplex_ι (r : ℝ) : toComplex ((CliffordAlgebra.ι Q) r) = r • Complex.I

@[simp]

theorem CliffordAlgebraComplex.toComplex_involute (c : CliffordAlgebra Q) : toComplex (CliffordAlgebra.involute c) = (starRingEnd ℂ) (toComplex c)

CliffordAlgebra.involute is analogous to Complex.conj.

def CliffordAlgebraComplex.ofComplex : ℂ →ₐ[ℝ] CliffordAlgebra Q

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

Equations

• CliffordAlgebraComplex.ofComplex = Complex.lift ⟨(CliffordAlgebra.ι CliffordAlgebraComplex.Q) 1, CliffordAlgebraComplex.ofComplex._proof_1⟩

@[simp]

theorem CliffordAlgebraComplex.ofComplex_I : ofComplex Complex.I = (CliffordAlgebra.ι Q) 1

@[simp]

theorem CliffordAlgebraComplex.toComplex_comp_ofComplex : toComplex.comp ofComplex = AlgHom.id ℝ ℂ

@[simp]

theorem CliffordAlgebraComplex.toComplex_ofComplex (c : ℂ) : toComplex (ofComplex c) = c

@[simp]

theorem CliffordAlgebraComplex.ofComplex_comp_toComplex : ofComplex.comp toComplex = AlgHom.id ℝ (CliffordAlgebra Q)

@[simp]

theorem CliffordAlgebraComplex.ofComplex_toComplex (c : CliffordAlgebra Q) : ofComplex (toComplex c) = c

def CliffordAlgebraComplex.equiv : CliffordAlgebra Q ≃ₐ[ℝ] ℂ

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.

@[simp]

theorem CliffordAlgebraComplex.equiv_symm_apply (a : ℂ) : CliffordAlgebraComplex.equiv.symm a = ofComplex a

@[simp]

theorem CliffordAlgebraComplex.equiv_apply (a : CliffordAlgebra Q) : CliffordAlgebraComplex.equiv a = toComplex a

instance CliffordAlgebraComplex.instCommRingCliffordAlgebraRealQ : CommRing (CliffordAlgebra Q)

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 (x : CliffordAlgebra Q) : 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 : ℂ) : ofComplex ((starRingEnd ℂ) c) = CliffordAlgebra.involute (ofComplex c)

Complex.conj is analogous to CliffordAlgebra.involute.

The clifford algebra isomorphic to the quaternions

def CliffordAlgebraQuaternion.Q {R : Type u_1} [CommRing R] (c₁ c₂ : R) : QuadraticForm R (R × 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

• CliffordAlgebraQuaternion.Q c₁ c₂ = (c₁ • QuadraticMap.sq).prod (c₂ • QuadraticMap.sq)

@[simp]

theorem CliffordAlgebraQuaternion.Q_apply {R : Type u_1} [CommRing R] (c₁ c₂ : R) (v : R × R) : (Q c₁ c₂) v = c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)

def CliffordAlgebraQuaternion.quaternionBasis {R : Type u_1} [CommRing R] (c₁ c₂ : R) : QuaternionAlgebra.Basis (CliffordAlgebra (Q c₁ c₂)) c₁ 0 c₂

The quaternion basis vectors within the algebra.

Equations

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

@[simp]

theorem CliffordAlgebraQuaternion.quaternionBasis_k {R : Type u_1} [CommRing R] (c₁ c₂ : R) : (quaternionBasis c₁ c₂).k = (CliffordAlgebra.ι (Q c₁ c₂)) (1, 0) * (CliffordAlgebra.ι (Q c₁ c₂)) (0, 1)

@[simp]

theorem CliffordAlgebraQuaternion.quaternionBasis_i {R : Type u_1} [CommRing R] (c₁ c₂ : R) : (quaternionBasis c₁ c₂).i = (CliffordAlgebra.ι (Q c₁ c₂)) (1, 0)

@[simp]

theorem CliffordAlgebraQuaternion.quaternionBasis_j {R : Type u_1} [CommRing R] (c₁ c₂ : R) : (quaternionBasis c₁ c₂).j = (CliffordAlgebra.ι (Q c₁ c₂)) (0, 1)

def CliffordAlgebraQuaternion.toQuaternion {R : Type u_1} [CommRing R] {c₁ c₂ : R} : CliffordAlgebra (Q c₁ c₂) →ₐ[R] QuaternionAlgebra R c₁ 0 c₂

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.

@[simp]

theorem CliffordAlgebraQuaternion.toQuaternion_ι {R : Type u_1} [CommRing R] {c₁ c₂ : R} (v : R × R) : toQuaternion ((CliffordAlgebra.ι (Q c₁ c₂)) v) = { re := 0, imI := v.1, imJ := v.2, imK := 0 }

theorem CliffordAlgebraQuaternion.toQuaternion_star {R : Type u_1} [CommRing R] {c₁ c₂ : R} (c : CliffordAlgebra (Q c₁ c₂)) : toQuaternion (star c) = star (toQuaternion c)

The "clifford conjugate" maps to the quaternion conjugate.

def CliffordAlgebraQuaternion.ofQuaternion {R : Type u_1} [CommRing R] {c₁ c₂ : R} : QuaternionAlgebra R c₁ 0 c₂ →ₐ[R] CliffordAlgebra (Q c₁ c₂)

Map a quaternion into the clifford algebra.

Equations

• CliffordAlgebraQuaternion.ofQuaternion = (CliffordAlgebraQuaternion.quaternionBasis c₁ c₂).liftHom

@[simp]

theorem CliffordAlgebraQuaternion.ofQuaternion_mk {R : Type u_1} [CommRing R] {c₁ c₂ : R} (a₁ a₂ a₃ a₄ : R) : ofQuaternion { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } = (algebraMap R (CliffordAlgebra (Q c₁ c₂))) a₁ + a₂ • (CliffordAlgebra.ι (Q c₁ c₂)) (1, 0) + a₃ • (CliffordAlgebra.ι (Q c₁ c₂)) (0, 1) + a₄ • ((CliffordAlgebra.ι (Q c₁ c₂)) (1, 0) * (CliffordAlgebra.ι (Q c₁ c₂)) (0, 1))

@[simp]

theorem CliffordAlgebraQuaternion.ofQuaternion_comp_toQuaternion {R : Type u_1} [CommRing R] {c₁ c₂ : R} : ofQuaternion.comp toQuaternion = AlgHom.id R (CliffordAlgebra (Q c₁ c₂))

@[simp]

theorem CliffordAlgebraQuaternion.ofQuaternion_toQuaternion {R : Type u_1} [CommRing R] {c₁ c₂ : R} (c : CliffordAlgebra (Q c₁ c₂)) : ofQuaternion (toQuaternion c) = c

@[simp]

theorem CliffordAlgebraQuaternion.toQuaternion_comp_ofQuaternion {R : Type u_1} [CommRing R] {c₁ c₂ : R} : toQuaternion.comp ofQuaternion = AlgHom.id R (QuaternionAlgebra R c₁ 0 c₂)

@[simp]

theorem CliffordAlgebraQuaternion.toQuaternion_ofQuaternion {R : Type u_1} [CommRing R] {c₁ c₂ : R} (q : QuaternionAlgebra R c₁ 0 c₂) : toQuaternion (ofQuaternion q) = q

def CliffordAlgebraQuaternion.equiv {R : Type u_1} [CommRing R] {c₁ c₂ : R} : CliffordAlgebra (Q c₁ c₂) ≃ₐ[R] QuaternionAlgebra R c₁ 0 c₂

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 ⋯ ⋯

@[simp]

theorem CliffordAlgebraQuaternion.equiv_apply {R : Type u_1} [CommRing R] {c₁ c₂ : R} (a : CliffordAlgebra (Q c₁ c₂)) : CliffordAlgebraQuaternion.equiv a = toQuaternion a

@[simp]

theorem CliffordAlgebraQuaternion.equiv_symm_apply {R : Type u_1} [CommRing R] {c₁ c₂ : R} (a : QuaternionAlgebra R c₁ 0 c₂) : CliffordAlgebraQuaternion.equiv.symm a = ofQuaternion a

@[simp]

theorem CliffordAlgebraQuaternion.ofQuaternion_star {R : Type u_1} [CommRing R] {c₁ c₂ : R} (q : QuaternionAlgebra R c₁ 0 c₂) : ofQuaternion (star q) = star (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} [CommRing R] (r₁ r₂ : R) : (CliffordAlgebra.ι 0) r₁ * (CliffordAlgebra.ι 0) r₂ = 0

def CliffordAlgebraDualNumber.equiv {R : Type u_1} [CommRing R] : CliffordAlgebra 0 ≃ₐ[R] DualNumber R

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.

@[simp]

theorem CliffordAlgebraDualNumber.equiv_ι {R : Type u_1} [CommRing R] (r : R) : CliffordAlgebraDualNumber.equiv ((CliffordAlgebra.ι 0) r) = r • DualNumber.eps

@[simp]

theorem CliffordAlgebraDualNumber.equiv_symm_eps {R : Type u_1} [CommRing R] : CliffordAlgebraDualNumber.equiv.symm DualNumber.eps = (CliffordAlgebra.ι 0) 1