Other constructions isomorphic to Clifford Algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

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:

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 #

source

@[simp]

theorem clifford_algebra_ring.ι_eq_zero {R : Type u_1} [comm_ring R] :

clifford_algebra.ι 0 = 0

source

@[protected, instance]

def clifford_algebra_ring.clifford_algebra.comm_ring {R : Type u_1} [comm_ring R] :

comm_ring (clifford_algebra 0)

Since the vector space is empty the ring is commutative.

Equations

clifford_algebra_ring.clifford_algebra.comm_ring = {add := ring.add (clifford_algebra.ring 0), add_assoc := _, zero := ring.zero (clifford_algebra.ring 0), zero_add := _, add_zero := _, nsmul := ring.nsmul (clifford_algebra.ring 0), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (clifford_algebra.ring 0), sub := ring.sub (clifford_algebra.ring 0), sub_eq_add_neg := _, zsmul := ring.zsmul (clifford_algebra.ring 0), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (clifford_algebra.ring 0), nat_cast := ring.nat_cast (clifford_algebra.ring 0), one := ring.one (clifford_algebra.ring 0), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul (clifford_algebra.ring 0), mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow (clifford_algebra.ring 0), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

theorem clifford_algebra_ring.reverse_apply {R : Type u_1} [comm_ring R] (x : clifford_algebra 0) :

⇑clifford_algebra.reverse x = x

source

@[simp]

theorem clifford_algebra_ring.reverse_eq_id {R : Type u_1} [comm_ring R] :

clifford_algebra.reverse = linear_map.id

source

@[simp]

theorem clifford_algebra_ring.involute_eq_id {R : Type u_1} [comm_ring R] :

clifford_algebra.involute = alg_hom.id R (clifford_algebra 0)

source

@[protected]

def clifford_algebra_ring.equiv {R : Type u_1} [comm_ring R] :

clifford_algebra 0 ≃ₐ[R] R

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

Equations

clifford_algebra_ring.equiv = alg_equiv.of_alg_hom (⇑(clifford_algebra.lift 0) ⟨0, _⟩) (algebra.of_id R (clifford_algebra 0)) clifford_algebra_ring.equiv._proof_2 clifford_algebra_ring.equiv._proof_3

The clifford algebra isomorphic to the complex numbers #

source

@[protected]

def clifford_algebra_complex.Q :

quadratic_form ℝ ℝ

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

Equations

clifford_algebra_complex.Q = -quadratic_form.sq

source

@[simp]

theorem clifford_algebra_complex.Q_apply (r : ℝ) :

⇑clifford_algebra_complex.Q r = -(r * r)

source

def clifford_algebra_complex.to_complex :

clifford_algebra clifford_algebra_complex.Q →ₐ[ℝ ] ℂ

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

Equations

clifford_algebra_complex.to_complex = ⇑(clifford_algebra.lift clifford_algebra_complex.Q) ⟨linear_map.to_span_singleton ℝ ℂ complex.I, clifford_algebra_complex.to_complex._proof_1⟩

source

@[simp]

theorem clifford_algebra_complex.to_complex_ι (r : ℝ) :

⇑clifford_algebra_complex.to_complex (⇑(clifford_algebra.ι clifford_algebra_complex.Q) r) = r • complex.I

source

@[simp]

theorem clifford_algebra_complex.to_complex_involute (c : clifford_algebra clifford_algebra_complex.Q) :

⇑clifford_algebra_complex.to_complex (⇑clifford_algebra.involute c) = ⇑(star_ring_end ℂ) (⇑clifford_algebra_complex.to_complex c)

clifford_algebra.involute is analogous to complex.conj.

source

def clifford_algebra_complex.of_complex :

ℂ →ₐ[ℝ ] clifford_algebra clifford_algebra_complex.Q

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

Equations

clifford_algebra_complex.of_complex = ⇑complex.lift ⟨⇑(clifford_algebra.ι clifford_algebra_complex.Q) 1, clifford_algebra_complex.of_complex._proof_1⟩

source

@[simp]

theorem clifford_algebra_complex.of_complex_I :

⇑clifford_algebra_complex.of_complex complex.I = ⇑(clifford_algebra.ι clifford_algebra_complex.Q) 1

source

@[simp]

theorem clifford_algebra_complex.to_complex_comp_of_complex :

clifford_algebra_complex.to_complex.comp clifford_algebra_complex.of_complex = alg_hom.id ℝ ℂ

source

@[simp]

theorem clifford_algebra_complex.to_complex_of_complex (c : ℂ) :

⇑clifford_algebra_complex.to_complex (⇑clifford_algebra_complex.of_complex c) = c

source

@[simp]

theorem clifford_algebra_complex.of_complex_comp_to_complex :

clifford_algebra_complex.of_complex.comp clifford_algebra_complex.to_complex = alg_hom.id ℝ (clifford_algebra clifford_algebra_complex.Q)

source

@[simp]

theorem clifford_algebra_complex.of_complex_to_complex (c : clifford_algebra clifford_algebra_complex.Q) :

⇑clifford_algebra_complex.of_complex (⇑clifford_algebra_complex.to_complex c) = c

source

@[protected]

def clifford_algebra_complex.equiv :

clifford_algebra clifford_algebra_complex.Q ≃ₐ[ℝ ] ℂ

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

Equations

clifford_algebra_complex.equiv = alg_equiv.of_alg_hom clifford_algebra_complex.to_complex clifford_algebra_complex.of_complex clifford_algebra_complex.to_complex_comp_of_complex clifford_algebra_complex.of_complex_comp_to_complex

source

@[simp]

theorem clifford_algebra_complex.equiv_apply (ᾰ : clifford_algebra clifford_algebra_complex.Q) :

⇑clifford_algebra_complex.equiv ᾰ = ⇑clifford_algebra_complex.to_complex ᾰ

source

@[simp]

theorem clifford_algebra_complex.equiv_symm_apply (ᾰ : ℂ) :

⇑(clifford_algebra_complex.equiv.symm) ᾰ = ⇑clifford_algebra_complex.of_complex ᾰ

source

@[protected, instance]

def clifford_algebra_complex.clifford_algebra.comm_ring :

comm_ring (clifford_algebra clifford_algebra_complex.Q)

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 := ring.add (clifford_algebra.ring clifford_algebra_complex.Q), add_assoc := clifford_algebra_complex.clifford_algebra.comm_ring._proof_1, zero := ring.zero (clifford_algebra.ring clifford_algebra_complex.Q), zero_add := clifford_algebra_complex.clifford_algebra.comm_ring._proof_2, add_zero := clifford_algebra_complex.clifford_algebra.comm_ring._proof_3, nsmul := ring.nsmul (clifford_algebra.ring clifford_algebra_complex.Q), nsmul_zero' := clifford_algebra_complex.clifford_algebra.comm_ring._proof_4, nsmul_succ' := clifford_algebra_complex.clifford_algebra.comm_ring._proof_5, neg := ring.neg (clifford_algebra.ring clifford_algebra_complex.Q), sub := ring.sub (clifford_algebra.ring clifford_algebra_complex.Q), sub_eq_add_neg := clifford_algebra_complex.clifford_algebra.comm_ring._proof_6, zsmul := ring.zsmul (clifford_algebra.ring clifford_algebra_complex.Q), 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 := ring.int_cast (clifford_algebra.ring clifford_algebra_complex.Q), nat_cast := ring.nat_cast (clifford_algebra.ring clifford_algebra_complex.Q), one := ring.one (clifford_algebra.ring clifford_algebra_complex.Q), 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 := ring.mul (clifford_algebra.ring clifford_algebra_complex.Q), 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 := ring.npow (clifford_algebra.ring clifford_algebra_complex.Q), 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}

source

theorem clifford_algebra_complex.reverse_apply (x : clifford_algebra clifford_algebra_complex.Q) :

⇑clifford_algebra.reverse x = x

reverse is a no-op over clifford_algebra_complex.Q.

source

@[simp]

theorem clifford_algebra_complex.reverse_eq_id :

clifford_algebra.reverse = linear_map.id

source

@[simp]

theorem clifford_algebra_complex.of_complex_conj (c : ℂ) :

⇑clifford_algebra_complex.of_complex (⇑(star_ring_end ℂ) c) = ⇑clifford_algebra.involute (⇑clifford_algebra_complex.of_complex c)

complex.conj is analogous to clifford_algebra.involute.

The clifford algebra isomorphic to the quaternions #

source

@[protected]

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

quadratic_form 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

clifford_algebra_quaternion.Q c₁ c₂ = (c₁ • quadratic_form.sq).prod (c₂ • quadratic_form.sq)

source

@[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)

source

def clifford_algebra_quaternion.quaternion_basis {R : Type u_1} [comm_ring R] (c₁ c₂ : R) :

quaternion_algebra.basis (clifford_algebra (clifford_algebra_quaternion.Q c₁ c₂)) c₁ c₂

The quaternion basis vectors within the algebra.

Equations

clifford_algebra_quaternion.quaternion_basis c₁ c₂ = {i := ⇑(clifford_algebra.ι (clifford_algebra_quaternion.Q c₁ c₂)) (1, 0), j := ⇑(clifford_algebra.ι (clifford_algebra_quaternion.Q c₁ c₂)) (0, 1), k := ⇑(clifford_algebra.ι (clifford_algebra_quaternion.Q c₁ c₂)) (1, 0) * ⇑(clifford_algebra.ι (clifford_algebra_quaternion.Q c₁ c₂)) (0, 1), i_mul_i := _, j_mul_j := _, i_mul_j := _, j_mul_i := _}

source

@[simp]

theorem clifford_algebra_quaternion.quaternion_basis_i {R : Type u_1} [comm_ring R] (c₁ c₂ : R) :

(clifford_algebra_quaternion.quaternion_basis c₁ c₂).i = ⇑(clifford_algebra.ι (clifford_algebra_quaternion.Q c₁ c₂)) (1, 0)

source

@[simp]

theorem clifford_algebra_quaternion.quaternion_basis_j {R : Type u_1} [comm_ring R] (c₁ c₂ : R) :

(clifford_algebra_quaternion.quaternion_basis c₁ c₂).j = ⇑(clifford_algebra.ι (clifford_algebra_quaternion.Q c₁ c₂)) (0, 1)

source

@[simp]

theorem clifford_algebra_quaternion.quaternion_basis_k {R : Type u_1} [comm_ring R] (c₁ c₂ : R) :

(clifford_algebra_quaternion.quaternion_basis c₁ c₂).k = ⇑(clifford_algebra.ι (clifford_algebra_quaternion.Q c₁ c₂)) (1, 0) * ⇑(clifford_algebra.ι (clifford_algebra_quaternion.Q c₁ c₂)) (0, 1)

source

def clifford_algebra_quaternion.to_quaternion {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :

clifford_algebra (clifford_algebra_quaternion.Q c₁ c₂) →ₐ[R] quaternion_algebra 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

clifford_algebra_quaternion.to_quaternion = ⇑(clifford_algebra.lift (clifford_algebra_quaternion.Q c₁ c₂)) ⟨{to_fun := λ (v : R × R), {re := 0, im_i := v.fst, im_j := v.snd, im_k := 0}, map_add' := _, map_smul' := _}, _⟩

source

@[simp]

theorem clifford_algebra_quaternion.to_quaternion_ι {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (v : R × R) :

⇑clifford_algebra_quaternion.to_quaternion (⇑(clifford_algebra.ι (clifford_algebra_quaternion.Q c₁ c₂)) v) = {re := 0, im_i := v.fst, im_j := v.snd, im_k := 0}

source

theorem clifford_algebra_quaternion.to_quaternion_star {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (c : clifford_algebra (clifford_algebra_quaternion.Q c₁ c₂)) :

⇑clifford_algebra_quaternion.to_quaternion (has_star.star c) = has_star.star (⇑clifford_algebra_quaternion.to_quaternion c)

The "clifford conjugate" maps to the quaternion conjugate.

source

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

quaternion_algebra R c₁ c₂ →ₐ[R] clifford_algebra (clifford_algebra_quaternion.Q c₁ c₂)

Map a quaternion into the clifford algebra.

Equations

clifford_algebra_quaternion.of_quaternion = (clifford_algebra_quaternion.quaternion_basis c₁ c₂).lift_hom

source

@[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₄} = ⇑(algebra_map R (clifford_algebra (clifford_algebra_quaternion.Q c₁ c₂))) a₁ + a₂ • ⇑(clifford_algebra.ι (clifford_algebra_quaternion.Q c₁ c₂)) (1, 0) + a₃ • ⇑(clifford_algebra.ι (clifford_algebra_quaternion.Q c₁ c₂)) (0, 1) + a₄ • (⇑(clifford_algebra.ι (clifford_algebra_quaternion.Q c₁ c₂)) (1, 0) * ⇑(clifford_algebra.ι (clifford_algebra_quaternion.Q c₁ c₂)) (0, 1))

source

@[simp]

theorem clifford_algebra_quaternion.of_quaternion_comp_to_quaternion {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :

clifford_algebra_quaternion.of_quaternion.comp clifford_algebra_quaternion.to_quaternion = alg_hom.id R (clifford_algebra (clifford_algebra_quaternion.Q c₁ c₂))

source

@[simp]

theorem clifford_algebra_quaternion.of_quaternion_to_quaternion {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (c : clifford_algebra (clifford_algebra_quaternion.Q c₁ c₂)) :

⇑clifford_algebra_quaternion.of_quaternion (⇑clifford_algebra_quaternion.to_quaternion c) = c

source

@[simp]

theorem clifford_algebra_quaternion.to_quaternion_comp_of_quaternion {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :

clifford_algebra_quaternion.to_quaternion.comp clifford_algebra_quaternion.of_quaternion = alg_hom.id R (quaternion_algebra R c₁ c₂)

source

@[simp]

theorem clifford_algebra_quaternion.to_quaternion_of_quaternion {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (q : quaternion_algebra R c₁ c₂) :

⇑clifford_algebra_quaternion.to_quaternion (⇑clifford_algebra_quaternion.of_quaternion q) = q

source

@[simp]

theorem clifford_algebra_quaternion.equiv_symm_apply {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (ᾰ : quaternion_algebra R c₁ c₂) :

⇑(clifford_algebra_quaternion.equiv.symm) ᾰ = ⇑clifford_algebra_quaternion.of_quaternion ᾰ

source

@[simp]

theorem clifford_algebra_quaternion.equiv_apply {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (ᾰ : clifford_algebra (clifford_algebra_quaternion.Q c₁ c₂)) :

⇑clifford_algebra_quaternion.equiv ᾰ = ⇑clifford_algebra_quaternion.to_quaternion ᾰ

source

@[protected]

def clifford_algebra_quaternion.equiv {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :

clifford_algebra (clifford_algebra_quaternion.Q c₁ c₂) ≃ₐ[R] quaternion_algebra R c₁ c₂

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

Equations

clifford_algebra_quaternion.equiv = alg_equiv.of_alg_hom clifford_algebra_quaternion.to_quaternion clifford_algebra_quaternion.of_quaternion clifford_algebra_quaternion.to_quaternion_comp_of_quaternion clifford_algebra_quaternion.of_quaternion_comp_to_quaternion

source

@[simp]

theorem clifford_algebra_quaternion.of_quaternion_star {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (q : quaternion_algebra R c₁ c₂) :

⇑clifford_algebra_quaternion.of_quaternion (has_star.star q) = has_star.star (⇑clifford_algebra_quaternion.of_quaternion q)

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

The clifford algebra isomorphic to the dual numbers #

source

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

⇑(clifford_algebra.ι 0) r₁ * ⇑(clifford_algebra.ι 0) r₂ = 0

source

@[protected]

def clifford_algebra_dual_number.equiv {R : Type u_1} [comm_ring R] :

clifford_algebra 0 ≃ₐ[R] dual_number R

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

Equations

clifford_algebra_dual_number.equiv = alg_equiv.of_alg_hom (⇑(clifford_algebra.lift 0) ⟨triv_sq_zero_ext.inr_hom R R semiring.to_module, _⟩) (⇑dual_number.lift ⟨⇑(clifford_algebra.ι 0) 1, _⟩) clifford_algebra_dual_number.equiv._proof_9 clifford_algebra_dual_number.equiv._proof_10

source

@[simp]

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

⇑clifford_algebra_dual_number.equiv (⇑(clifford_algebra.ι 0) r) = r • dual_number.eps

source

@[simp]

theorem clifford_algebra_dual_number.equiv_symm_eps {R : Type u_1} [comm_ring R] :

⇑(clifford_algebra_dual_number.equiv.symm) dual_number.eps = ⇑(clifford_algebra.ι 0) 1