CliffordAlgebra.star_def
theorem CliffordAlgebra.star_def :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (x : CliffordAlgebra Q), star x = CliffordAlgebra.reverse (CliffordAlgebra.involute x)
The theorem `CliffordAlgebra.star_def` states that for any commutative ring `R`, an `R`-module `M` equipped with a quadratic form `Q`, and any element `x` of the Clifford Algebra formed by `Q`, the star operation on `x` is equivalent to the composition of the reverse and involute operations on `x`. In other words, the star of `x` is obtained by first applying the grade involution to `x`, which inverts the sign of each basis vector, and then applying the grade reversion to the result, which inverts the multiplication order of basis vectors.
More concisely: For any commutative ring R, an R-module M with quadratic form Q, and element x in the Clifford algebra over M and Q, the star operation on x is equivalent to the composition of the grade involution and grade reverse operations.
|
CliffordAlgebra.star_smul
theorem CliffordAlgebra.star_smul :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (r : R) (x : CliffordAlgebra Q), star (r • x) = r • star x
This theorem, named `CliffordAlgebra.star_smul`, states that for any commutative ring `R`, any additive commutative group `M` which also has a structure of `R`-module, and any quadratic form `Q` over `R` and `M`, if you have a scalar `r` from `R` and a vector `x` from the Clifford Algebra constructed from `M` and `Q`, then the "star" of the scalar multiplication of `r` and `x` (denoted as star (r • x)) is the same as the scalar multiplication of `r` and the "star" of `x` (denoted as r • star x). The "star" operation typically represents a kind of 'conjugation' process, but as the comment above the theorem notes, this theorem does not involve any conjugation on the scalars `r`, as some definitions may imply. The theorem also notes that there's no literature suggesting this scalar conjugation should be done.
More concisely: For any commutative ring R, additive commutative group M with R-module structure, quadratic form Q over R and M, scalar r from R, and vector x in the Clifford Algebra constructed from M and Q, r • star x = star (r • x).
|