CliffordAlgebra.invOf_ι
theorem CliffordAlgebra.invOf_ι :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(Q : QuadraticForm R M) (m : M) [inst_3 : Invertible (Q m)] [inst_4 : Invertible ((CliffordAlgebra.ι Q) m)],
⅟((CliffordAlgebra.ι Q) m) = (CliffordAlgebra.ι Q) (⅟(Q m) • m)
This theorem states that for a vector with an invertible quadratic form, the inverse of the vector can be expressed as the vector itself divided by its quadratic form. More formally, given a commutative ring `R`, an additive commutative group `M`, and a module `M` over `R`, if `Q` is a quadratic form on `M` and `m` is a member of `M` such that both `Q(m)` and the Clifford algebra of `Q` mapped over `m` are invertible, then the inverse of the Clifford algebra of `Q` mapped over `m` is equal to the Clifford algebra of `Q` mapped over `m` scaled by the inverse of `Q(m)`. The scaling operation is performed in the module `M`, which means that it involves scalar multiplication of the vector `m`.
More concisely: If a quadratic form `Q` on a commutative ring `R`-module `M` has an invertible quadratic form `Q(m)` and invertible Clifford algebra `Q^+(m)`, then `(Q^+(m))^{-1} = Q^+(m) * (Q(m))^{-1}` in `M`.
|
CliffordAlgebra.ι_mul_ι_mul_invOf_ι
theorem CliffordAlgebra.ι_mul_ι_mul_invOf_ι :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(Q : QuadraticForm R M) (a b : M) [inst_3 : Invertible ((CliffordAlgebra.ι Q) a)] [inst_4 : Invertible (Q a)],
(CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b * ⅟((CliffordAlgebra.ι Q) a) =
(CliffordAlgebra.ι Q) ((⅟(Q a) * QuadraticForm.polar (⇑Q) a b) • a - b)
This theorem states that in the Clifford Algebra associated with a Quadratic Form Q over a Commutative Ring R and an Additive Commutative Group M, for any two vectors a and b from M, the expression a*b*a^-1 (where * represents the algebra multiplication and a^-1 is the multiplicative inverse of a in the algebra) is equal to another vector given by the formula ((1/Q(a)) * Q.polar(a, b)) * a - b. Here, Q.polar is the associated bilinear form of the quadratic form Q, and 1/Q(a) represents the multiplicative inverse of the value of Q at a in the ring R.
More concisely: In the Clifford Algebra of a quadratic form Q over a commutative ring R and additive commutative group M, the product of vectors a and b followed by the multiplicative inverse of a is equal to the vector ((Q(a)^(-1) * Q.polar(a, b)) * a - b).
|
CliffordAlgebra.invOf_ι_mul_ι_mul_ι
theorem CliffordAlgebra.invOf_ι_mul_ι_mul_ι :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(Q : QuadraticForm R M) (a b : M) [inst_3 : Invertible ((CliffordAlgebra.ι Q) a)] [inst_4 : Invertible (Q a)],
⅟((CliffordAlgebra.ι Q) a) * (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a =
(CliffordAlgebra.ι Q) ((⅟(Q a) * QuadraticForm.polar (⇑Q) a b) • a - b)
This theorem states that for a given commutative ring `R` and an additive commutative group `M` which is also an `R`-module, given a quadratic form `Q : QuadraticForm R M` and two elements `a` and `b` of `M`, if `a` is invertible in the Clifford algebra of `Q` and `Q(a)` is invertible in `R`, then the product of the inverse of `(CliffordAlgebra.ι Q) a`, `(CliffordAlgebra.ι Q) b`, and `(CliffordAlgebra.ι Q) a` equals the image under the canonical linear map `CliffordAlgebra.ι Q` of the difference of the scalar product of the inverse `Q(a)` and the polar form of `Q` at `a` and `b`, and `b`.
In other words, if `a` is invertible both in the Clifford algebra and the quadratic form, the conjugation by `a` of `b` in the Clifford algebra corresponds to the mapped difference under the quadratic form between a scalar multiple of `a` and `b`.
More concisely: Given a commutative ring `R`, an additive commutative `R`-module `M`, a quadratic form `Q` over `M`, and invertible elements `a, b` in the Clifford algebra of `Q` with invertible `Q(a)` in `R`, the product of the inverses of `(CliffordAlgebra.ι Q) a`, `(CliffordAlgebra.ι Q) b`, and `(CliffordAlgebra.ι Q) a` equals the difference of the scalar product of `Q(a)` and the polar form of `Q` at `a` and `b`, and the scalar multiple of `a` and `b` under `Q`.
|