Documentation

Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Isomorphisms with the even subalgebra of a Clifford algebra #

This file provides some notable isomorphisms regarding the even subalgebra, CliffordAlgebra.even.

Main definitions #

Main results #

Constructions needed for CliffordAlgebra.equivEven #

@[reducible, inline]
abbrev CliffordAlgebra.EquivEven.Q' {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :

The quadratic form on the augmented vector space M × R sending v + r•e0 to Q v - r^2.

Equations
Instances For
    theorem CliffordAlgebra.EquivEven.Q'_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M × R) :
    (CliffordAlgebra.EquivEven.Q' Q) m = Q m.1 - m.2 * m.2

    The unit vector in the new dimension

    Equations
    Instances For

      The embedding from the existing vector space

      Equations
      Instances For
        @[simp]
        theorem CliffordAlgebra.EquivEven.reverse_v {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) :
        CliffordAlgebra.reverse ((CliffordAlgebra.EquivEven.v Q) m) = (CliffordAlgebra.EquivEven.v Q) m
        @[simp]
        theorem CliffordAlgebra.EquivEven.involute_v {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) :
        CliffordAlgebra.involute ((CliffordAlgebra.EquivEven.v Q) m) = -(CliffordAlgebra.EquivEven.v Q) m
        @[simp]
        @[simp]

        The embedding from the smaller algebra into the new larger one.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The embedding from the even subalgebra with an extra dimension into the original algebra.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Any clifford algebra is isomorphic to the even subalgebra of a clifford algebra with an extra dimension (that is, with vector space M × R), with a quadratic form evaluating to -1 on that new basis vector.

            Equations
            Instances For
              theorem CliffordAlgebra.coe_toEven_reverse_involute {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : CliffordAlgebra Q) :
              ((CliffordAlgebra.toEven Q) (CliffordAlgebra.reverse (CliffordAlgebra.involute x))) = CliffordAlgebra.reverse ((CliffordAlgebra.toEven Q) x)

              The representation of the clifford conjugate (i.e. the reverse of the involute) in the even subalgebra is just the reverse of the representation.

              Constructions needed for CliffordAlgebra.evenEquivEvenNeg #

              def CliffordAlgebra.evenToNeg {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (Q' : QuadraticForm R M) (h : Q' = -Q) :

              One direction of CliffordAlgebra.evenEquivEvenNeg

              Equations
              Instances For
                @[simp]
                theorem CliffordAlgebra.evenToNeg_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (Q' : QuadraticForm R M) (h : Q' = -Q) (m₁ : M) (m₂ : M) :
                (CliffordAlgebra.evenToNeg Q Q' h) (((CliffordAlgebra.even.ι Q).bilin m₁) m₂) = -((CliffordAlgebra.even.ι Q').bilin m₁) m₂
                theorem CliffordAlgebra.evenToNeg_comp_evenToNeg {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (Q' : QuadraticForm R M) (h : Q' = -Q) (h' : Q = -Q') :

                The even subalgebras of the algebras with quadratic form Q and -Q are isomorphic.

                Stated another way, 𝒞ℓ⁺(p,q,r) and 𝒞ℓ⁺(q,p,r) are isomorphic.

                Equations
                Instances For