# 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_involute_reverse
• clifford_algebra_quaternion.of_quaternion_conj

### The clifford algebra isomorphic to a ring #

@[simp]
theorem clifford_algebra_ring.ι_eq_zero {R : Type u_1} [comm_ring R] :
@[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] :
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 #

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

Equations
@[simp]

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]

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

Equations
@[simp]
@[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, gsmul := , gsmul_zero' := clifford_algebra_complex.clifford_algebra.comm_ring._proof_7, gsmul_succ' := clifford_algebra_complex.clifford_algebra.comm_ring._proof_8, gsmul_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, mul := , mul_assoc := clifford_algebra_complex.clifford_algebra.comm_ring._proof_12, one := , one_mul := clifford_algebra_complex.clifford_algebra.comm_ring._proof_13, mul_one := clifford_algebra_complex.clifford_algebra.comm_ring._proof_14, npow := , npow_zero' := clifford_algebra_complex.clifford_algebra.comm_ring._proof_15, npow_succ' := clifford_algebra_complex.clifford_algebra.comm_ring._proof_16, left_distrib := clifford_algebra_complex.clifford_algebra.comm_ring._proof_17, right_distrib := clifford_algebra_complex.clifford_algebra.comm_ring._proof_18, mul_comm := clifford_algebra_complex.clifford_algebra.comm_ring._proof_19}

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 #

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] ℍ[R,c₁,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}

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

def clifford_algebra_quaternion.of_quaternion {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
ℍ[R,c₁,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 : ℍ[R,c₁,c₂]) :
@[simp]
theorem clifford_algebra_quaternion.equiv_symm_apply {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (ᾰ : ℍ[R,c₁,c₂]) :
@[simp]
theorem clifford_algebra_quaternion.equiv_apply {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (ᾰ : clifford_algebra ) :
def clifford_algebra_quaternion.equiv {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
≃ₐ[R] ℍ[R,c₁,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 : ℍ[R,c₁,c₂]) :

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