Documentation

Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Other constructions isomorphic to Clifford Algebras #

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

Rings #

Complex numbers #

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

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

Quaternion algebras #

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

Dual numbers #

The clifford algebra isomorphic to a ring #

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)

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

Instances For

    The clifford algebra isomorphic to the complex numbers #

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

    Instances For

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

      Instances For

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

        Instances For

          The clifford algebras over CliffordAlgebraComplex.Q is isomorphic as an -algebra to .

          Instances For

            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.

            reverse is a no-op over CliffordAlgebraComplex.Q.

            @[simp]
            theorem CliffordAlgebraComplex.reverse_eq_id :
            CliffordAlgebra.reverse = LinearMap.id
            @[simp]

            Complex.conj is analogous to CliffordAlgebra.involute.

            The clifford algebra isomorphic to the quaternions #

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

            Instances For
              @[simp]
              theorem CliffordAlgebraQuaternion.Q_apply {R : Type u_1} [CommRing R] (c₁ : R) (c₂ : R) (v : R × R) :
              ↑(CliffordAlgebraQuaternion.Q c₁ c₂) v = c₁ * (v.fst * v.fst) + c₂ * (v.snd * v.snd)

              The quaternion basis vectors within the algebra.

              Instances For

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

                Instances For
                  @[simp]
                  theorem CliffordAlgebraQuaternion.toQuaternion_ι {R : Type u_1} [CommRing R] {c₁ : R} {c₂ : R} (v : R × R) :
                  CliffordAlgebraQuaternion.toQuaternion (↑(CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) v) = { re := 0, imI := v.fst, imJ := v.snd, imK := 0 }
                  theorem CliffordAlgebraQuaternion.toQuaternion_star {R : Type u_1} [CommRing R] {c₁ : R} {c₂ : R} (c : CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂)) :
                  CliffordAlgebraQuaternion.toQuaternion (star c) = star (CliffordAlgebraQuaternion.toQuaternion c)

                  The "clifford conjugate" maps to the quaternion conjugate.

                  Map a quaternion into the clifford algebra.

                  Instances For
                    @[simp]
                    theorem CliffordAlgebraQuaternion.ofQuaternion_mk {R : Type u_1} [CommRing R] {c₁ : R} {c₂ : R} (a₁ : R) (a₂ : R) (a₃ : R) (a₄ : R) :
                    CliffordAlgebraQuaternion.ofQuaternion { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } = ↑(algebraMap R (CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂))) a₁ + a₂ ↑(CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (1, 0) + a₃ ↑(CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (0, 1) + a₄ (↑(CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (1, 0) * ↑(CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (0, 1))
                    @[simp]
                    theorem CliffordAlgebraQuaternion.ofQuaternion_comp_toQuaternion {R : Type u_1} [CommRing R] {c₁ : R} {c₂ : R} :
                    AlgHom.comp CliffordAlgebraQuaternion.ofQuaternion CliffordAlgebraQuaternion.toQuaternion = AlgHom.id R (CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂))
                    @[simp]
                    theorem CliffordAlgebraQuaternion.ofQuaternion_toQuaternion {R : Type u_1} [CommRing R] {c₁ : R} {c₂ : R} (c : CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂)) :
                    CliffordAlgebraQuaternion.ofQuaternion (CliffordAlgebraQuaternion.toQuaternion c) = c
                    @[simp]
                    theorem CliffordAlgebraQuaternion.toQuaternion_comp_ofQuaternion {R : Type u_1} [CommRing R] {c₁ : R} {c₂ : R} :
                    AlgHom.comp CliffordAlgebraQuaternion.toQuaternion CliffordAlgebraQuaternion.ofQuaternion = AlgHom.id R (QuaternionAlgebra R c₁ c₂)
                    @[simp]
                    theorem CliffordAlgebraQuaternion.toQuaternion_ofQuaternion {R : Type u_1} [CommRing R] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra R c₁ c₂) :
                    CliffordAlgebraQuaternion.toQuaternion (CliffordAlgebraQuaternion.ofQuaternion q) = q
                    @[simp]
                    theorem CliffordAlgebraQuaternion.equiv_symm_apply {R : Type u_1} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
                    ↑(AlgEquiv.symm CliffordAlgebraQuaternion.equiv) a = CliffordAlgebraQuaternion.ofQuaternion a
                    @[simp]
                    theorem CliffordAlgebraQuaternion.equiv_apply {R : Type u_1} [CommRing R] {c₁ : R} {c₂ : R} (a : CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂)) :
                    CliffordAlgebraQuaternion.equiv a = CliffordAlgebraQuaternion.toQuaternion a

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

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

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

                      Instances For
                        @[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] :
                        ↑(AlgEquiv.symm CliffordAlgebraDualNumber.equiv) DualNumber.eps = ↑(CliffordAlgebra.ι 0) 1