CliffordAlgebra.reverse_involute_commute
theorem CliffordAlgebra.reverse_involute_commute :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M}, Function.Commute ⇑CliffordAlgebra.reverse ⇑CliffordAlgebra.involute
The theorem `CliffordAlgebra.reverse_involute_commute` states that the operations of reverse and involute on a Clifford algebra commute with each other. This means that for any type `R` with a commutative ring structure, any type `M` with an additive commutative group structure and a module structure over `R`, and any quadratic form `Q` on `M`, applying the reverse and then the involute operation to an element of the Clifford algebra yields the same result as applying the involute and then the reverse operation. This combined operation is sometimes referred to as the "Clifford conjugate".
More concisely: For any commutative ring `R`, additive commutative group `M` with `R`-module structure, and quadratic form `Q` on `M`, the reverse and involute operations on the Clifford algebra commute, i.e., `(r * a).inv.reverse = a.reverse.inv` for all `r` in `R` and `a` in the Clifford algebra generated by `M` and `i(Q)`.
|
CliffordAlgebra.involute_prod_map_ι
theorem CliffordAlgebra.involute_prod_map_ι :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (l : List M),
CliffordAlgebra.involute (List.map (⇑(CliffordAlgebra.ι Q)) l).prod =
(-1) ^ l.length • (List.map (⇑(CliffordAlgebra.ι Q)) l).prod
This theorem states that for any given commutative ring `R`, an additive commutative group `M`, and a module `R M`, along with a quadratic form `Q` over `R M`, the involution of the product of a list `l` of `n` vectors (from `M`), where each vector is first lifted via the canonical linear map `ι`, is equivalent to multiplying the product of the lifted list by `(-1) ^ n`. In other words, applying the involution to the product of a list of vectors lifted to the Clifford Algebra is the same as scaling the original product by the factor `(-1) ^ n`, where `n` is the length of the list.
More concisely: For any commutative ring `R`, additive commutative group `M`, module `R M`, and quadratic form `Q` over `R M`, the involution of the product of a list `l` of `n` vectors in `M` in the Clifford algebra is equivalent to multiplying the product of the lifted list by `(-1) ^ n`.
|
CliffordAlgebra.involute_ι
theorem CliffordAlgebra.involute_ι :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (m : M), CliffordAlgebra.involute ((CliffordAlgebra.ι Q) m) = -(CliffordAlgebra.ι Q) m
The theorem `CliffordAlgebra.involute_ι` states that for any commutative ring `R`, any additive commutative group `M`, any `R`-module structure on `M`, and any quadratic form `Q` on `M` with coefficients in `R`, if you apply the canonical linear map `CliffordAlgebra.ι Q` on an element `m` of `M` and then apply the grade involution `CliffordAlgebra.involute`, it is equivalent to flipping the sign of the canonical linear map `CliffordAlgebra.ι Q` applied to `m`. In mathematical terms, this can be written as: for all `m` in `M`, the involution of the image of `m` under the canonical linear map is equal to the negative of the image of `m` under the canonical linear map.
More concisely: For any quadratic form `Q` on an additive commutative group `M` over a commutative ring `R`, and for all `m` in `M`, the involution of `CliffordAlgebra.ι Q(m)` is equal to `-CliffordAlgebra.ι Q(m)`.
|
CliffordAlgebra.reverse_ι
theorem CliffordAlgebra.reverse_ι :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (m : M), CliffordAlgebra.reverse ((CliffordAlgebra.ι Q) m) = (CliffordAlgebra.ι Q) m
The theorem `CliffordAlgebra.reverse_ι` states that for any commutative ring `R`, an additive commutative group `M`, a module `M` over `R`, and a quadratic form `Q` on `M`, the reverse of the image of any element `m` of `M` under the canonical linear map `ι` from `M` to the Clifford Algebra of `Q`, is equal to the same image. This means, in mathematical terms, if you map an element from the module to the Clifford Algebra and then apply the grade reversion operation, you get the same element in the Clifford Algebra.
More concisely: For any commutative ring R, additive commutative group M with a quadratic form Q, and module M over R, the map ι from M to the Clifford Algebra of Q satisfies ι(m) = ι(−m) for all m in M.
|
CliffordAlgebra.reverse.map_mul
theorem CliffordAlgebra.reverse.map_mul :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (a b : CliffordAlgebra Q),
CliffordAlgebra.reverse (a * b) = CliffordAlgebra.reverse b * CliffordAlgebra.reverse a
The theorem `CliffordAlgebra.reverse.map_mul` states that for any commutative ring `R`, any additive commutative group `M` which is also a module over `R`, and any quadratic form `Q` on `M`, the operation of grade reversion (or reversing the multiplication order of basis vectors) in the Clifford algebra of `M` under `Q` over `R` has the property that the grade reversion of the product of two elements `a` and `b` in this Clifford algebra is equal to the product of the grade reversions of `b` and `a`, in that order. In other words, the grade reversion operation reverses the order of multiplication in the Clifford algebra.
More concisely: In the Clifford algebra of a commutative ring `R` over an additive commutative group `M` with quadratic form `Q`, the grade reversal of the product of two elements is equal to the product of their grade reversals in reverse order.
|
CliffordAlgebra.reverse.commutes
theorem CliffordAlgebra.reverse.commutes :
∀ {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),
CliffordAlgebra.reverse ((algebraMap R (CliffordAlgebra Q)) r) = (algebraMap R (CliffordAlgebra Q)) r
The theorem `CliffordAlgebra.reverse.commutes` states that for any commutative ring `R`, any additive commutative group `M` which is also a module over `R`, and any quadratic form `Q` on `M`, the reverse operation on the Clifford Algebra of `Q` commutes with the algebra map from `R` to the Clifford Algebra of `Q`. In simpler terms, if we map an element `r` from `R` to the Clifford Algebra, then the order in which we apply the reverse operation and the algebra map doesn't matter.
More concisely: For any commutative ring R, additive commutative group M as an R-module, and quadratic form Q on M, the reverse operation on the Clifford Algebra of Q and the algebra map from R to the Clifford Algebra of Q commute.
|
CliffordAlgebra.reverse_prod_map_ι
theorem CliffordAlgebra.reverse_prod_map_ι :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (l : List M),
CliffordAlgebra.reverse (List.map (⇑(CliffordAlgebra.ι Q)) l).prod =
(List.map (⇑(CliffordAlgebra.ι Q)) l).reverse.prod
This theorem states that for any list of vectors `l` from an additive commutative group `M` over a commutative ring `R` with a given quadratic form `Q`, taking the reverse of the product of these vectors lifted into the Clifford Algebra via the canonical linear map `ι` is equivalent to taking the product of the reverse of the list of these lifted vectors.
More concisely: For any list of vectors `l` from an additive commutative group `M` over a commutative ring `R` with a given quadratic form `Q`, the reversed order product of their lifted vectors in the Clifford Algebra via the canonical map `ι` is equivalent to the product of the reversed order lifted vectors.
|
CliffordAlgebra.submodule_map_mul_reverse
theorem CliffordAlgebra.submodule_map_mul_reverse :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(Q : QuadraticForm R M) (p q : Submodule R (CliffordAlgebra Q)),
Submodule.map CliffordAlgebra.reverse (p * q) =
Submodule.map CliffordAlgebra.reverse q * Submodule.map CliffordAlgebra.reverse p
The theorem `CliffordAlgebra.submodule_map_mul_reverse` states that for any commutative ring `R`, additive commutative group `M`, `M` being a module over `R`, and a quadratic form `Q` on `M`, if `p` and `q` are submodules of the Clifford algebra of `Q`, then mapping the product of `p` and `q` under the grade reversion function (which reverses the multiplication order of basis vectors) is equal to the product of the images of `q` and `p` (in that order) under the same grade reversion function. This theorem essentially explores how reversing the multiplication order in a Clifford algebra affects the product of two submodules when mapped under a reversion function.
More concisely: For any commutative ring `R`, additive commutative group `M` being an `R`-module, and quadratic form `Q` on `M`, if `p` and `q` are submodules of the Clifford algebra of `Q`, then the product of `p` and `q` under grade reversion function is equal to the reverse order product of their images.
|
CliffordAlgebra.submodule_map_pow_reverse
theorem CliffordAlgebra.submodule_map_pow_reverse :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(Q : QuadraticForm R M) (p : Submodule R (CliffordAlgebra Q)) (n : ℕ),
Submodule.map CliffordAlgebra.reverse (p ^ n) = Submodule.map CliffordAlgebra.reverse p ^ n
The theorem `CliffordAlgebra.submodule_map_pow_reverse` states that for any commutative ring `R`, additive commutative group `M`, module `M` over `R`, and a quadratic form `Q` defined on `M`, if you have a submodule `p` of the Clifford algebra of `M` equipped with `Q`, and a natural number `n`, then the `n`-th power of the submodule `p` under the map defined by the grade reversion (also known as the reverse) of the Clifford algebra is equal to the `n`-th power of the image of submodule `p` under the same grade reversion map. In other words, the order of taking `n`-th power and applying the grade reversion map can be interchanged without affecting the result.
More concisely: For any commutative ring `R`, additive commutative group `M`, module `M` over `R`, quadratic form `Q` on `M`, and submodule `p` of the Clifford algebra of `M` equipped with `Q`, the `n`-th power of `p` under the grade reversion map is equal to the `n`-th power of the image of `p` under the same grade reversal map.
|