Documentation

TauCeti.LinearAlgebra.CliffordAlgebra.Even.Scaling

Even Clifford algebras of scalar multiples #

Multiplying a quadratic form by a unit does not change its even Clifford algebra up to isomorphism. The equivalence sends a pair of generating vectors to the corresponding pair multiplied by the inverse scalar. This allows a represented unit to be normalized to -1 before applying the dimension-shift equivalence for Clifford algebras. Scaling preserves reversal, and dimension reduction turns reversal into Clifford conjugation.

The construction uses the universal property of the even subalgebra, following Mathlib's CliffordAlgebra.evenToNeg and CliffordAlgebra.evenEquivEvenNeg for negation.

References #

source
def TauCeti.CliffordAlgebra.evenEquivEvenSMul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a : Rˣ) :
↥(CliffordAlgebra.even Q) ≃ₐ[R] ↥(CliffordAlgebra.even (↑a • Q))

Scaling a quadratic form by a unit preserves its even Clifford algebra. On products of two generating vectors the equivalence multiplies by the inverse unit.

Instances For
    source
    @[simp]
    theorem TauCeti.CliffordAlgebra.evenEquivEvenSMul_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a : Rˣ) (m n : M) :
    (evenEquivEvenSMul Q a) (((CliffordAlgebra.even.ι Q).bilin m) n) = ↑a⁻¹ • ((CliffordAlgebra.even.ι (↑a • Q)).bilin m) n

    The scaling equivalence multiplies each bilinear generator by the inverse scalar.

    source
    @[simp]
    theorem TauCeti.CliffordAlgebra.evenEquivEvenSMul_symm_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a : Rˣ) (m n : M) :
    (evenEquivEvenSMul Q a).symm (((CliffordAlgebra.even.ι (↑a • Q)).bilin m) n) = ↑a • ((CliffordAlgebra.even.ι Q).bilin m) n

    The inverse scaling equivalence multiplies a bilinear generator by the scalar.

    source
    theorem TauCeti.CliffordAlgebra.evenEquivEvenSMul_reverseEven {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a : Rˣ) (x : ↥(CliffordAlgebra.even Q)) :
    (evenEquivEvenSMul Q a) ((CliffordAlgebra.reverseEven Q) x) = (CliffordAlgebra.reverseEven (↑a • Q)) ((evenEquivEvenSMul Q a) x)

    The even-algebra scaling equivalence preserves Clifford reversal.

    source
    noncomputable def TauCeti.CliffordAlgebra.evenProdSMulSqEquiv {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a : Rˣ) :
    ↥(CliffordAlgebra.even (QuadraticMap.prod Q (↑a • QuadraticMap.sq))) ≃ₐ[R] CliffordAlgebra (-↑a⁻¹ • Q)

    The even Clifford algebra of q ⊥ ⟨a⟩ is the Clifford algebra of -a⁻¹ • q. This reduces the even algebra of a regular space to a Clifford algebra in one lower dimension.

    Instances For
      source
      @[simp]
      theorem TauCeti.CliffordAlgebra.evenProdSMulSqEquiv_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a : Rˣ) (x y : M × R) :
      (evenProdSMulSqEquiv Q a) (((CliffordAlgebra.even.ι (QuadraticMap.prod Q (↑a • QuadraticMap.sq))).bilin x) y) = -↑a • (((CliffordAlgebra.ι (-↑a⁻¹ • Q)) x.1 + (algebraMap R (CliffordAlgebra (-↑a⁻¹ • Q))) x.2) * ((CliffordAlgebra.ι (-↑a⁻¹ • Q)) y.1 - (algebraMap R (CliffordAlgebra (-↑a⁻¹ • Q))) y.2))

      On a pair of generators, the dimension-reduction equivalence is Mathlib's ofEven formula multiplied by -a.

      source
      @[simp]
      theorem TauCeti.CliffordAlgebra.evenProdSMulSqEquiv_symm_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a : Rˣ) (m : M) :
      (evenProdSMulSqEquiv Q a).symm ((CliffordAlgebra.ι (-↑a⁻¹ • Q)) m) = -↑a⁻¹ • ((CliffordAlgebra.even.ι (QuadraticMap.prod Q (↑a • QuadraticMap.sq))).bilin (0, 1)) (m, 0)

      The inverse dimension-reduction equivalence sends a vector to the last basis vector times that vector, multiplied by -a⁻¹.

      source
      theorem TauCeti.CliffordAlgebra.evenProdSMulSqEquiv_reverseEven {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a : Rˣ) (x : ↥(CliffordAlgebra.even (QuadraticMap.prod Q (↑a • QuadraticMap.sq)))) :
      (evenProdSMulSqEquiv Q a) ((CliffordAlgebra.reverseEven (QuadraticMap.prod Q (↑a • QuadraticMap.sq))) x) = star ((evenProdSMulSqEquiv Q a) x)

      Dimension reduction sends reversal on the even algebra to Clifford conjugation.