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 aclifford_algebraover a zero-dimensional vector space.
Complex numbers #
clifford_algebra_complex.equiv: thecomplexnumbers are equivalent as anℝ-algebra to aclifford_algebraover a one-dimensional vector space with a quadratic form that satisfiesQ (ι Q 1) = -1.clifford_algebra_complex.to_complex: the forward direction of this equivclifford_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: aquaternion_algebraoverRis equivalent as anR-algebra to a clifford algebra overR × R, sendingito(0, 1)andjto(1, 0).clifford_algebra_quaternion.to_quaternion: the forward direction of this equivclifford_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 anR-algebra to a clifford algebra overRwhereQ = 0.
The clifford algebra isomorphic to a ring #
@[simp]
@[protected, instance]
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 := _}
@[simp]
@[simp]
@[protected]
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 #
@[protected]
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
- 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⟩
@[simp]
@[simp]
theorem
clifford_algebra_complex.to_complex_involute
(c : clifford_algebra clifford_algebra_complex.Q) :
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
- clifford_algebra_complex.of_complex = ⇑complex.lift ⟨⇑(clifford_algebra.ι clifford_algebra_complex.Q) 1, clifford_algebra_complex.of_complex._proof_1⟩
@[simp]
@[protected]
The clifford algebras over clifford_algebra_complex.Q is isomorphic as an ℝ-algebra to
ℂ.
@[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 := 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}
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) :
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)
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 := _}
@[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)
@[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)
@[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)
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₂].
@[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}
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₂)) :
The "clifford conjugate" maps to the quaternion conjugate.
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.
@[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))
@[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 (clifford_algebra_quaternion.Q c₁ c₂)) :
@[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 : quaternion_algebra R c₁ c₂) :
@[simp]
theorem
clifford_algebra_quaternion.equiv_symm_apply
{R : Type u_1}
[comm_ring R]
{c₁ c₂ : R}
(ᾰ : quaternion_algebra R c₁ c₂) :
@[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₂)) :
@[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₂].
@[simp]
theorem
clifford_algebra_quaternion.of_quaternion_conj
{R : Type u_1}
[comm_ring R]
{c₁ c₂ : R}
(q : quaternion_algebra R c₁ 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) :
⇑(clifford_algebra.ι 0) r₁ * ⇑(clifford_algebra.ι 0) r₂ = 0
@[protected]
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_3 clifford_algebra_dual_number.equiv._proof_4
@[simp]
@[simp]