# mathlibdocumentation

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 #

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

## Complex numbers #

• clifford_algebra_complex.equiv: the complex numbers are equivalent as an ℝ-algebra to a clifford_algebra over a one-dimensional vector space with a quadratic form that satisfies Q (ι Q 1) = -1.
• clifford_algebra_complex.to_complex: the forward direction of this equiv
• clifford_algebra_complex.of_complex: the reverse direction of this equiv

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

• clifford_algebra_complex.to_complex_involute
• clifford_algebra_complex.of_complex_conj

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 #

• clifford_algebra_quaternion.equiv: a quaternion_algebra 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).
• clifford_algebra_quaternion.to_quaternion: the forward direction of this equiv
• clifford_algebra_quaternion.of_quaternion: the reverse direction of this equiv

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

• clifford_algebra_quaternion.to_quaternion_star
• clifford_algebra_quaternion.of_quaternion_conj

## Dual numbers #

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

### The clifford algebra isomorphic to a ring #

@[simp]
theorem clifford_algebra_ring.ι_eq_zero {R : Type u_1} [comm_ring R] :
@[protected, instance]

Since the vector space is empty the ring is commutative.

Equations
@[simp]
theorem clifford_algebra_ring.reverse_eq_id {R : Type u_1} [comm_ring R] :
@[simp]
theorem clifford_algebra_ring.involute_eq_id {R : Type u_1} [comm_ring R] :
@[protected]
def clifford_algebra_ring.equiv {R : Type u_1} [comm_ring R] :

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
@[simp]
theorem clifford_algebra_complex.Q_apply (r : ) :
= -(r * r)

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

Equations
@[simp]
@[simp]

clifford_algebra.involute is analogous to complex.conj.

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

Equations
@[simp]
@[protected]

The clifford algebras over clifford_algebra_complex.Q is isomorphic as an ℝ-algebra to ℂ.

Equations
@[simp]
@[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
• clifford_algebra_complex.clifford_algebra.comm_ring = {add := , add_assoc := clifford_algebra_complex.clifford_algebra.comm_ring._proof_1, zero := , zero_add := clifford_algebra_complex.clifford_algebra.comm_ring._proof_2, add_zero := clifford_algebra_complex.clifford_algebra.comm_ring._proof_3, nsmul := , nsmul_zero' := clifford_algebra_complex.clifford_algebra.comm_ring._proof_4, nsmul_succ' := clifford_algebra_complex.clifford_algebra.comm_ring._proof_5, neg := , sub := , sub_eq_add_neg := clifford_algebra_complex.clifford_algebra.comm_ring._proof_6, zsmul := , zsmul_zero' := clifford_algebra_complex.clifford_algebra.comm_ring._proof_7, zsmul_succ' := clifford_algebra_complex.clifford_algebra.comm_ring._proof_8, zsmul_neg' := clifford_algebra_complex.clifford_algebra.comm_ring._proof_9, add_left_neg := clifford_algebra_complex.clifford_algebra.comm_ring._proof_10, add_comm := clifford_algebra_complex.clifford_algebra.comm_ring._proof_11, int_cast := , nat_cast := , one := , nat_cast_zero := clifford_algebra_complex.clifford_algebra.comm_ring._proof_12, nat_cast_succ := clifford_algebra_complex.clifford_algebra.comm_ring._proof_13, int_cast_of_nat := clifford_algebra_complex.clifford_algebra.comm_ring._proof_14, int_cast_neg_succ_of_nat := clifford_algebra_complex.clifford_algebra.comm_ring._proof_15, mul := , mul_assoc := clifford_algebra_complex.clifford_algebra.comm_ring._proof_16, one_mul := clifford_algebra_complex.clifford_algebra.comm_ring._proof_17, mul_one := clifford_algebra_complex.clifford_algebra.comm_ring._proof_18, npow := , npow_zero' := clifford_algebra_complex.clifford_algebra.comm_ring._proof_19, npow_succ' := clifford_algebra_complex.clifford_algebra.comm_ring._proof_20, left_distrib := clifford_algebra_complex.clifford_algebra.comm_ring._proof_21, right_distrib := clifford_algebra_complex.clifford_algebra.comm_ring._proof_22, mul_comm := clifford_algebra_complex.clifford_algebra.comm_ring._proof_23}

reverse is a no-op over clifford_algebra_complex.Q.

@[simp]
@[simp]

complex.conj is analogous to clifford_algebra.involute.

### The clifford algebra isomorphic to the quaternions #

@[protected]
def clifford_algebra_quaternion.Q {R : Type u_1} [comm_ring R] (c₁ c₂ : R) :
(R × 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) :
v = c₁ * (v.fst * v.fst) + c₂ * (v.snd * v.snd)
def clifford_algebra_quaternion.quaternion_basis {R : Type u_1} [comm_ring R] (c₁ c₂ : R) :

The quaternion basis vectors within the algebra.

Equations
@[simp]
theorem clifford_algebra_quaternion.quaternion_basis_i {R : Type u_1} [comm_ring R] (c₁ c₂ : R) :
= (1, 0)
@[simp]
theorem clifford_algebra_quaternion.quaternion_basis_j {R : Type u_1} [comm_ring R] (c₁ c₂ : R) :
= (0, 1)
@[simp]
theorem clifford_algebra_quaternion.quaternion_basis_k {R : Type u_1} [comm_ring R] (c₁ c₂ : R) :
= (1, 0) * (0, 1)
def clifford_algebra_quaternion.to_quaternion {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
→ₐ[R] c₂

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

Equations
@[simp]
theorem clifford_algebra_quaternion.to_quaternion_ι {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (v : R × R) :
= {re := 0, im_i := v.fst, im_j := v.snd, im_k := 0}
theorem clifford_algebra_quaternion.to_quaternion_star {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (c : clifford_algebra ) :

The "clifford conjugate" maps to the quaternion conjugate.

def clifford_algebra_quaternion.of_quaternion {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
c₂ →ₐ[R]

Map a quaternion into the clifford algebra.

Equations
@[simp]
theorem clifford_algebra_quaternion.of_quaternion_mk {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a₁ a₂ a₃ a₄ : R) :
clifford_algebra_quaternion.of_quaternion {re := a₁, im_i := a₂, im_j := a₃, im_k := a₄} = a₁ + a₂ (1, 0) + a₃ (0, 1) + a₄ ( (1, 0) * (0, 1))
@[simp]
theorem clifford_algebra_quaternion.of_quaternion_comp_to_quaternion {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
@[simp]
theorem clifford_algebra_quaternion.of_quaternion_to_quaternion {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (c : clifford_algebra ) :
@[simp]
theorem clifford_algebra_quaternion.to_quaternion_comp_of_quaternion {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
@[simp]
theorem clifford_algebra_quaternion.to_quaternion_of_quaternion {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (q : c₂) :
@[simp]
theorem clifford_algebra_quaternion.equiv_symm_apply {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (ᾰ : c₂) :
@[simp]
theorem clifford_algebra_quaternion.equiv_apply {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (ᾰ : clifford_algebra ) :
@[protected]
def clifford_algebra_quaternion.equiv {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
≃ₐ[R] c₂

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

Equations
@[simp]
theorem clifford_algebra_quaternion.of_quaternion_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (q : c₂) :

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) :
r₁ * r₂ = 0
@[protected]
def clifford_algebra_dual_number.equiv {R : Type u_1} [comm_ring R] :

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

Equations
@[simp]
theorem clifford_algebra_dual_number.equiv_ι {R : Type u_1} [comm_ring R] (r : R) :
@[simp]