CliffordAlgebra.changeForm_contractLeft
theorem CliffordAlgebra.changeForm_contractLeft :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : B.toQuadraticForm = Q' - Q) (d : Module.Dual R M)
(x : CliffordAlgebra Q),
(CliffordAlgebra.changeForm h) ((CliffordAlgebra.contractLeft d) x) =
(CliffordAlgebra.contractLeft d) ((CliffordAlgebra.changeForm h) x)
This theorem, known as Theorem 23 from Grinberg's paper on Clifford algebra, states that for any commutative ring `R`, an `R`-module `M` equipped with two quadratic forms `Q` and `Q'`, and a bilinear form `B` on `M` such that `B` converted into a quadratic form equals the difference of `Q'` and `Q`, a change of quadratic form from `Q` to `Q'` applied to the Clifford contraction (a specific operation in Clifford algebra) of an element `x` of the Clifford algebra of `Q` with an element `d` from the dual space of `M`, is equal to the Clifford contraction of `x` with `d` after changing the quadratic form from `Q` to `Q'`. In particular, this theorem indicates a certain commutativity of the operations of changing the form of a Clifford algebra and performing a Clifford contraction.
More concisely: For any commutative ring `R`, `R`-module `M` with quadratic forms `Q` and `Q'`, and a bilinear form `B` on `M` such that `B`'s quadratic form equals `Q' - Q`, the change of quadratic form from `Q` to `Q'` commutes with the Clifford contraction operation in the Clifford algebra of `Q`, i.e., applying a change of quadratic form to the Clifford contraction of an element `x` in the Clifford algebra with an element `d` from the dual space is equal to the Clifford contraction of `x` with `d` after the change of quadratic form.
|
CliffordAlgebra.contractRight_comm
theorem CliffordAlgebra.contractRight_comm :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (d d' : Module.Dual R M) (x : CliffordAlgebra Q),
(CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d)) d' =
-(CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d')) d
The theorem `CliffordAlgebra.contractRight_comm` states that for any commutative ring `R`, any `R`-module `M` equipped with a quadratic form `Q`, any elements `d` and `d'` of the dual module of `M` (the module of linear maps from `M` to `R`), and any element `x` of the Clifford algebra of `M` with respect to `Q`, the operation of contracting `d` and `d'` on the right of `x` commutes up to a sign. More specifically, if you first contract `d` on the right of `x`, and then contract `d'` on the result, you get the same as if you first contracted `d'` on the right of `x`, and then contracted `d`, but with the opposite sign.
More concisely: For any commutative ring R, module M with quadratic form Q, and elements d, d' in M^*, and x in the Clifford algebra of M with respect to Q, the right contractions d' ∘ x ∘ d and d ∘ x ∘ d' commute up to a sign.
|
CliffordAlgebra.contractRight_mul_ι
theorem CliffordAlgebra.contractRight_mul_ι :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (d : Module.Dual R M) (a : M) (b : CliffordAlgebra Q),
(CliffordAlgebra.contractRight (b * (CliffordAlgebra.ι Q) a)) d =
d a • b - (CliffordAlgebra.contractRight b) d * (CliffordAlgebra.ι Q) a
This theorem, called Grinberg's Theorem 12, states that for any commutative ring `R`, an `R`-module `M`, a quadratic form `Q` on `M`, a dual module element `d` of `M`, an element `a` of `M`, and an element `b` of the Clifford algebra of `M` with respect to `Q`, the contraction of the product of `b` and the canonical map of `a` into the Clifford algebra with `d`, equals the scalar multiplication of `d` applied to `a` with `b`, minus the product of the contraction of `b` with `d` and the canonical map of `a` into the Clifford algebra.
In mathematical terms, this theorem can be written as
`contraction_{right}(b * ι(a))(d) = d(a) * b - contraction_{right}(b)(d) * ι(a)`
where `ι` is the canonical linear map from `M` to the Clifford Algebra, `contraction_{right}` represents the operation of contraction on the right, and `*` represents the multiplication operation in the Clifford Algebra.
More concisely: For any commutative ring `R`, `R`-module `M`, quadratic form `Q` on `M`, dual module element `d`, element `a` of `M`, and element `b` of the Clifford algebra of `M` with respect to `Q`, the contraction of `b` with the canonical map of `a` into the Clifford algebra, and the scalar multiplication of `d` with `a`, differ by the contraction of `b` with `d` and the product of the canonical map of `a` with `b`. In symbols: `contraction_{right}(b * ι(a))(d) = d(a) * b - contraction_{right}(b)(d) * ι(a)`.
|
CliffordAlgebra.contractLeft_ι_mul
theorem CliffordAlgebra.contractLeft_ι_mul :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (d : Module.Dual R M) (a : M) (b : CliffordAlgebra Q),
(CliffordAlgebra.contractLeft d) ((CliffordAlgebra.ι Q) a * b) =
d a • b - (CliffordAlgebra.ι Q) a * (CliffordAlgebra.contractLeft d) b
The theorem `CliffordAlgebra.contractLeft_ι_mul` is a statement about the Clifford algebra of an `R`-module `M` equipped with a quadratic form `Q`. Specifically, it says that for any element `d` from the dual space of the `R`-module `M`, any element `a` from the `R`-module `M`, and any element `b` from the Clifford algebra, the result of contracting `d` with the product of `a` and `b` (where `a` is first embedded into the Clifford algebra) is equal to the scalar multiplication of `d` and `a` applied to `b` minus the product of the embedding of `a` and the contraction of `d` with `b`. This is a fundamental property in the theory of Clifford algebras, and is a key result in Grinberg's 2016 paper.
More concisely: For any element `d` in the dual space of an `R`-module `M` equipped with a quadratic form `Q`, the contraction of `d` with the product of an element `a` from `M` and any `b` from the Clifford algebra of `M` equals the scalar multiplication of `d` by `a` applied to `b` minus the embedding of `a` times the contraction of `d` with `b`.
|
CliffordAlgebra.contractLeft_contractLeft
theorem CliffordAlgebra.contractLeft_contractLeft :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (d : Module.Dual R M) (x : CliffordAlgebra Q),
(CliffordAlgebra.contractLeft d) ((CliffordAlgebra.contractLeft d) x) = 0
The theorem `CliffordAlgebra.contractLeft_contractLeft` is a result in the context of Clifford algebras, specifically Theorem 7 from Grinberg's 2016 paper. This theorem states the following: Given a commutative ring `R`, an additive group `M` which is also a module over `R`, a quadratic form `Q` on `M`, a dual module `d` which contains linear maps from `M` to `R`, and an element `x` from the Clifford algebra created from `Q`, if we apply the operation `CliffordAlgebra.contractLeft` with dual module `d` two times on `x`, we will always get zero. In other words, for any dual module `d` and any element `x` in the Clifford algebra, the successive contraction of `x` by `d` is always zero.
More concisely: For any commutative ring R, additive group M as an R-module, quadratic form Q on M, dual module d containing linear maps from M to R, and element x in the Clifford algebra generated by Q, the repeated application of CliffordAlgebra.contractLeft operation with dual module d on x equals zero.
|
CliffordAlgebra.contractRight_eq
theorem CliffordAlgebra.contractRight_eq :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (d : Module.Dual R M) (x : CliffordAlgebra Q),
(CliffordAlgebra.contractRight x) d =
CliffordAlgebra.reverse ((CliffordAlgebra.contractLeft d) (CliffordAlgebra.reverse x))
This theorem states that for any commutative ring `R`, any `R`-module `M` equipped with a quadratic form `Q`, any dual module `d` of `M`, and any element `x` of the Clifford Algebra constructed from `M` and `Q`, the operation of contracting `x` with `d` on the right is equal to the operation of first reversing `x`, then contracting with `d` on the left, and then reversing the result again. This theorem essentially describes a certain symmetry property of the operations of contraction and reversion in the context of Clifford algebras.
More concisely: For any commutative ring `R`, any `R`-module `M` with quadratic form `Q`, and any element `x` in the Clifford algebra of `M` and `Q`, contracting `x` with the dual module `d` on the right equals reversing `x`, contracting with `d` on the left, and then reversing the result again.
|
CliffordAlgebra.changeForm_changeForm
theorem CliffordAlgebra.changeForm_changeForm :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q Q' Q'' : QuadraticForm R M} {B B' : LinearMap.BilinForm R M} (h : B.toQuadraticForm = Q' - Q)
(h' : B'.toQuadraticForm = Q'' - Q') (x : CliffordAlgebra Q),
(CliffordAlgebra.changeForm h') ((CliffordAlgebra.changeForm h) x) = (CliffordAlgebra.changeForm ⋯) x
The theorem `CliffordAlgebra.changeForm_changeForm` states the following: for any commutative ring `R`, an additive commutative group `M` that is also an `R`-module, any three quadratic forms `Q`, `Q'` and `Q''` on `M` over `R`, and any two bilinear forms `B` and `B'` on `M` over `R`, such that the quadratic form associated with `B` is equal to `Q'` minus `Q`, and the quadratic form associated with `B'` is equal to `Q''` minus `Q'`, then for any element `x` of the Clifford algebra of `Q`, the result of applying the operation `CliffordAlgebra.changeForm` first with `h` and then with `h'` to `x` is equal to the result of applying the operation `CliffordAlgebra.changeForm` with ... to `x`. This theorem corresponds to Lemma 3, section 9 in Bourbaki's Algebra book (2007 edition).
More concisely: For any commutative ring `R`, `R`-module `M`, quadratic forms `Q`, `Q'`, `Q''`, and bilinear forms `B` and `B'` on `M` satisfying certain conditions, the application of `CliffordAlgebra.changeForm` with respect to `h` followed by `h'` equals the application of `CliffordAlgebra.changeForm` with respect to `h'` followed by `h` on any element of the Clifford algebra of `Q`.
|
CliffordAlgebra.changeForm.add_proof
theorem CliffordAlgebra.changeForm.add_proof :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q Q' Q'' : QuadraticForm R M} {B B' : LinearMap.BilinForm R M},
B.toQuadraticForm = Q' - Q → B'.toQuadraticForm = Q'' - Q' → (B + B').toQuadraticForm = Q'' - Q
The theorem `CliffordAlgebra.changeForm.add_proof` states that for every commutative ring `R`, an additive commutative group `M` and `M` as a module over `R`, given three quadratic forms `Q`, `Q'` and `Q''` on `M` with coefficients in `R`, and two bilinear forms `B` and `B'` from `M` to `R`, if `B` corresponds to the difference of `Q'` and `Q` and `B'` corresponds to the difference of `Q''` and `Q'` when converted to quadratic forms, then the quadratic form corresponding to the sum of `B` and `B'` is equal to the difference of `Q''` and `Q`.
More concisely: If bilinear forms B and B' on a module M over a commutative ring R correspond to the differences of quadratic forms Q', Q, Q'' respectively, then the quadratic form corresponding to the sum of B and B' is equal to the difference of Q'' and Q.
|
CliffordAlgebra.changeForm.neg_proof
theorem CliffordAlgebra.changeForm.neg_proof :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M},
B.toQuadraticForm = Q' - Q → (-B).toQuadraticForm = Q - Q'
This theorem, named `CliffordAlgebra.changeForm.neg_proof`, states that for any commutative ring `R` and any module `M` over `R`, given any two quadratic forms `Q` and `Q'` on `M` and any bilinear form `B` on `M`, if the quadratic form associated to `B` is equal to the difference `Q' - Q`, then the quadratic form associated to `-B` (the negation of `B`) is equal to the difference `Q - Q'`. This theorem is used as a utility lemma in some context involving changing the form in Clifford algebras.
More concisely: If the quadratic form associated to a bilinear form is the difference between two quadratic forms, then the quadratic form associated to the negation of that bilinear form is the difference of the negation of the first quadratic form and the second quadratic form.
|
CliffordAlgebra.contractLeftAux_contractLeftAux
theorem CliffordAlgebra.contractLeftAux_contractLeftAux :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(Q : QuadraticForm R M) (d : Module.Dual R M) (v : M) (x fx : CliffordAlgebra Q),
((CliffordAlgebra.contractLeftAux Q d) v)
((CliffordAlgebra.ι Q) v * x, ((CliffordAlgebra.contractLeftAux Q d) v) (x, fx)) =
Q v • fx
This theorem states that for any commutative ring `R`, additive commutative group `M`, and `M` being an `R`-module, given a quadratic form `Q` of `R` and `M`, a dual module `d` of `R` and `M`, a vector `v` in `M`, and two elements `x` and `fx` of the Clifford algebra of `Q`, the result of applying the contractLeftAux function of the Clifford algebra to `d` and `v`, and then applying it to the product of the canonical linear map applied to `v` and `x`, and the pair `(x, fx)`, is equal to the result of scaling `fx` by the value of the quadratic form `Q` applied to `v`. This expresses a property of the contractLeftAux function in the context of Clifford algebras.
More concisely: For any commutative ring `R`, additive commutative group `M`, `R`-module `M`, quadratic form `Q` on `M`, its dual module `d`, vector `v` in `M`, and elements `x` and `fx` in the Clifford algebra of `Q`, the scalar value obtained by contracting `d` with `v` using `contractLeftAux` and then scaling `fx` by `Q(v)` is equal.
|
CliffordAlgebra.changeForm.zero_proof
theorem CliffordAlgebra.changeForm.zero_proof :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M}, LinearMap.BilinForm.toQuadraticForm 0 = Q - Q
This theorem, named `CliffordAlgebra.changeForm.zero_proof`, states that for any commutative ring `R`, any additive commutative group `M`, and any `R`-module structure on `M`, for any quadratic form `Q` on `M`, the quadratic form derived from the zero bilinear map by applying the argument twice is equal to the difference of `Q` and itself. In simpler terms, it shows that the quadratic form corresponding to the zero bilinear map is essentially the zero quadratic form, as subtracting a quadratic form from itself yields the zero quadratic form.
More concisely: For any commutative ring R, additive commutative group M with an R-module structure, and quadratic form Q on M, the quadratic form derived from the zero bilinear map is equal to the difference of Q and its square.
|
CliffordAlgebra.contractLeft_comm
theorem CliffordAlgebra.contractLeft_comm :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (d d' : Module.Dual R M) (x : CliffordAlgebra Q),
(CliffordAlgebra.contractLeft d) ((CliffordAlgebra.contractLeft d') x) =
-(CliffordAlgebra.contractLeft d') ((CliffordAlgebra.contractLeft d) x)
The theorem `CliffordAlgebra.contractLeft_comm` is a representation of Theorem 8 from Grinberg's 2016 paper on Clifford Algebras. It states that for any commutative ring `R`, module `M` over `R`, quadratic form `Q` on `M`, dual module element `d` and `d'` of `M`, and element `x` of the Clifford Algebra of `Q`, applying the `contractLeft` operation on `d` and then on `d'` to `x` is equal to the negative of the operation of applying `contractLeft` on `d'` and then on `d` to `x`. In other words, the `contractLeft` operation on different dual module elements anticommutes on the Clifford Algebra.
More concisely: For any commutative ring `R`, module `M` over `R`, quadratic form `Q` on `M`, and elements `x` of the Clifford algebra of `Q`, `d`, `d'` of `M` being dual module elements, the operation `contractLeft on d * contractLeft on d' = - (contractLeft on d' * contractLeft on d)` holds true.
|
CliffordAlgebra.contractRight_contractRight
theorem CliffordAlgebra.contractRight_contractRight :
∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (d : Module.Dual R M) (x : CliffordAlgebra Q),
(CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d)) d = 0
The theorem `CliffordAlgebra.contractRight_contractRight` is a result about Clifford algebras, stated in the context of a commutative ring `R` and an `R`-module `M` equipped with a quadratic form `Q`. Specifically, it says that for any element `x` of the Clifford algebra of `Q` and any element `d` in the dual space of `M`, applying the `contractRight` operation twice on `x` with `d` as the argument, and then applying it once more with `d`, results in zero. This theorem is referenced as Theorem 13 from the work of Grinberg and Clifford in 2016.
More concisely: For any element `x` in the Clifford algebra of a quadratic form `Q` over a commutative ring `R` and an `R`-module `M`, and any element `d` in the dual space of `M`, the application of the `contractRight` operation three times, first with `x` and then with `d`, equals zero.
|