CliffordAlgebraComplex.toComplex_involute
theorem CliffordAlgebraComplex.toComplex_involute :
∀ (c : CliffordAlgebra CliffordAlgebraComplex.Q),
CliffordAlgebraComplex.toComplex (CliffordAlgebra.involute c) =
(starRingEnd ℂ) (CliffordAlgebraComplex.toComplex c)
The theorem `CliffordAlgebraComplex.toComplex_involute` states that for every element `c` in the Clifford algebra over the quadratic form `CliffordAlgebraComplex.Q` (which maps elements to the negative of their square), the action of the grade involution `CliffordAlgebra.involute` on `c` and then converting to complex numbers, is equivalent to first converting `c` to a complex number, then applying the complex conjugate (denoted by `starRingEnd ℂ`). The grade involution here is a function which inverts the sign of each basis vector in the Clifford algebra, and the complex conjugate operation on a complex number swaps the sign of its imaginary part.
More concisely: The theorem `CliffordAlgebraComplex.toComplex_involute` asserts that for all `c` in the Clifford algebra over the quadratic form `CliffordAlgebraComplex.Q`, the grade involution `CliffordAlgebra.involute` followed by converting to complex numbers equals converting to complex numbers and then applying complex conjugation.
|
CliffordAlgebraRing.ι_eq_zero
theorem CliffordAlgebraRing.ι_eq_zero : ∀ {R : Type u_1} [inst : CommRing R], CliffordAlgebra.ι 0 = 0
The theorem `CliffordAlgebraRing.ι_eq_zero` states that for any type `R` that is a commutative ring, the canonical linear map from `R` to the Clifford Algebra with respect to the zero quadratic form is the zero map. In other words, this theorem says that when the quadratic form is zero, every element of `R` is mapped to zero by the canonical linear map to the Clifford Algebra.
More concisely: For any commutative ring R and the Clifford Algebra over R with respect to the zero quadratic form, the canonical linear map from R to the Clifford Algebra is the zero map.
|
CliffordAlgebraComplex.ofComplex_conj
theorem CliffordAlgebraComplex.ofComplex_conj :
∀ (c : ℂ),
CliffordAlgebraComplex.ofComplex ((starRingEnd ℂ) c) =
CliffordAlgebra.involute (CliffordAlgebraComplex.ofComplex c)
This theorem states that the conjugation operation in the complex numbers is analogous to the grade involution in the Clifford algebra. Specifically, for every complex number `c`, applying the conjugation operation (denoted by `starRingEnd ℂ`) to `c` and then mapping the result to the Clifford algebra using the function `CliffordAlgebraComplex.ofComplex` produces the same result as first mapping `c` to the Clifford algebra and then applying the grade involution (denoted by `CliffordAlgebra.involute`). In other words, the diagram commutes between the Complex conjugation and the Clifford Algebra involution operation through the `CliffordAlgebraComplex.ofComplex` morphism.
More concisely: The complex conjugation and the grade involution in the Clifford algebra of complex numbers commute via the morphism `CliffordAlgebraComplex.ofComplex`.
|
CliffordAlgebraComplex.reverse_apply
theorem CliffordAlgebraComplex.reverse_apply :
∀ (x : CliffordAlgebra CliffordAlgebraComplex.Q), CliffordAlgebra.reverse x = x
The theorem `CliffordAlgebraComplex.reverse_apply` states that, for every element `x` of the Clifford algebra generated over the real numbers by the quadratic form that sends elements to the negation of their square (denoted by `CliffordAlgebra CliffordAlgebraComplex.Q`), the grade reversion operation (or reverse operation) on `x` results in `x` itself. In other words, the grade reversion operation is a no-op over the Clifford algebra defined by this particular quadratic form. In mathematical terms, if $x$ is an element of the Clifford algebra defined over $\mathbb{R}$ by the quadratic form that maps each element to the negation of its square, then applying the grade reversion operation to $x$ yields $x$.
More concisely: The grade reversion operation leaves elements of the Clifford algebra generated over the real numbers by the quadratic form mapping elements to the negation of their squares unchanged.
|
CliffordAlgebraQuaternion.ofQuaternion_star
theorem CliffordAlgebraQuaternion.ofQuaternion_star :
∀ {R : Type u_1} [inst : CommRing R] {c₁ c₂ : R} (q : QuaternionAlgebra R c₁ c₂),
CliffordAlgebraQuaternion.ofQuaternion (star q) = star (CliffordAlgebraQuaternion.ofQuaternion q)
This theorem states that, for any commutative ring `R` and any elements `c₁` and `c₂` of `R`, the function `ofQuaternion` preserves the conjugation operation. In other words, applying the conjugate function (`star`) to a quaternion `q` in the quaternion algebra `QuaternionAlgebra R c₁ c₂`, then mapping the result to the Clifford algebra using `ofQuaternion`, yields the same result as mapping `q` to the Clifford algebra first and then taking the Clifford algebra's conjugate (`star`). This is a property that is usually required of a map between algebraic structures that both possess a conjugation operation.
More concisely: For any commutative ring `R`, the conjugation operation in the Quaternion Algebra `QuaternionAlgebra R c₁ c₂` is preserved by the `ofQuaternion` map to the Clifford Algebra, i.e., `(ofQuaternion (q.star)) = (ofQuaternion q).star` for all quaternions `q` in `QuaternionAlgebra R c₁ c₂`.
|
CliffordAlgebraQuaternion.toQuaternion_star
theorem CliffordAlgebraQuaternion.toQuaternion_star :
∀ {R : Type u_1} [inst : CommRing R] {c₁ c₂ : R} (c : CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂)),
CliffordAlgebraQuaternion.toQuaternion (star c) = star (CliffordAlgebraQuaternion.toQuaternion c)
The theorem `CliffordAlgebraQuaternion.toQuaternion_star` states that for any commutative ring `R` and any two elements `c₁` and `c₂` from `R`, the Clifford conjugate of a certain Clifford Algebra maps to the quaternion conjugate. More precisely, for any element `c` in the Clifford Algebra structured by `CliffordAlgebraQuaternion.Q c₁ c₂`, the application of `CliffordAlgebraQuaternion.toQuaternion` to the Clifford conjugate of `c` is equal to the quaternion conjugate of the `CliffordAlgebraQuaternion.toQuaternion` applied to `c`.
More concisely: For any commutative ring R and any elements c₁, c₂ in R, the quaternion conjugate of the image of a Clifford algebra element c in CliffordAlgebraQuaternion.Q c₁ c₂ under the map CliffordAlgebraQuaternion.toQuaternion is equal to the image of the Clifford conjugate of c under the same map.
|
CliffordAlgebraComplex.toComplex_ι
theorem CliffordAlgebraComplex.toComplex_ι :
∀ (r : ℝ), CliffordAlgebraComplex.toComplex ((CliffordAlgebra.ι CliffordAlgebraComplex.Q) r) = r • Complex.I := by
sorry
This theorem states that for any real number `r`, applying the function `CliffordAlgebraComplex.toComplex` to the result of applying `CliffordAlgebra.ι` (the canonical linear map from a module to the Clifford Algebra of a quadratic form) with the quadratic form `CliffordAlgebraComplex.Q` (which sends elements to the negation of their square) to `r`, will yield `r` scaled by the imaginary unit `Complex.I` in the complex number field. In essence, it connects Clifford algebras over the specific quadratic form `CliffordAlgebraComplex.Q` with the field of complex numbers, stating that the complex scalar multiple of the imaginary unit can be obtained from the Clifford algebra of the real number using these functions.
More concisely: For any real number `r`, `CliffordAlgebraComplex.toComplex (CliffordAlgebra.ι CliffordAlgebraComplex.Q r) = r * Complex.I`.
|