CliffordAlgebra.toBaseChange_involute
theorem CliffordAlgebra.toBaseChange_involute :
∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
[inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V)
(x : CliffordAlgebra (QuadraticForm.baseChange A Q)),
(CliffordAlgebra.toBaseChange A Q) (CliffordAlgebra.involute x) =
(TensorProduct.map LinearMap.id CliffordAlgebra.involute.toLinearMap) ((CliffordAlgebra.toBaseChange A Q) x)
The theorem `CliffordAlgebra.toBaseChange_involute` states that for any commutative rings `R` and `A`, additive commutative group `V`, algebra structure of `A` over `R`, `R`-module structure of `V`, and invertible element `2`, given a quadratic form `Q` on `V` over `R` and an element `x` in the Clifford algebra of the base change of `Q` to `A`, the map `toBaseChange` from `CliffordAlgebra` applied to the involution of `x` equals the tensor product of the identity linear map and the linear map of the involution, applied to the `toBaseChange` map of `x`. Essentially, this says that the involution operation, which inverts the sign of each basis vector, acts only on the right side of the tensor product in this context.
More concisely: For any quadratic form Q over a commutative ring R, and an element x in the Clifford algebra of the base change of Q to an algebra A over R with invertible 2, the involution of x in the Clifford algebra equals the identity tensor product with the linear map of the involution on the base change of x.
|
CliffordAlgebra.toBaseChange_comp_reverseOp
theorem CliffordAlgebra.toBaseChange_comp_reverseOp :
∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
[inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V),
(AlgHom.op (CliffordAlgebra.toBaseChange A Q)).comp CliffordAlgebra.reverseOp =
(↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp
((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) CliffordAlgebra.reverseOp).comp
(CliffordAlgebra.toBaseChange A Q))
The theorem `CliffordAlgebra.toBaseChange_comp_reverseOp` is a technical result used in the proof of the key property of the Clifford algebra base change operation. It asserts that for any commutative ring `R`, a type `A` which is a commutative ring as well, and a type `V` which is an `R`-module (i.e., a vector space over `R`), if we also have a quadratic form `Q` on `V` and `2` is invertible in `R`, then composing the operation of base changing the Clifford algebra over `A` with `Q` with the Clifford algebra reversal operation is the same as first operating on the tensor product of `A` with the Clifford algebra of `Q` with the opposite algebra isomorphism, and then mapping the result through the base change operation followed by the Clifford algebra reversal operation.
More concisely: For any commutative rings `R` and `A`, `R`-module `V` with invertible 2, quadratic form `Q` on `V`, the operation of base changing the Clifford algebra of `Q` over `A` with the reverse Clifford algebra operation is equivalent to first taking the tensor product of `A` with the Clifford algebra of `Q` and applying the base change operation with reverse Clifford algebra isomorphism.
|
CliffordAlgebra.toBaseChange_reverse
theorem CliffordAlgebra.toBaseChange_reverse :
∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
[inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V)
(x : CliffordAlgebra (QuadraticForm.baseChange A Q)),
(CliffordAlgebra.toBaseChange A Q) (CliffordAlgebra.reverse x) =
(TensorProduct.map LinearMap.id CliffordAlgebra.reverse) ((CliffordAlgebra.toBaseChange A Q) x)
This theorem states that for any commutative ring `R`, commutative ring `A`, and an additive commutative group `V`, which is a module over `R`, and given an invertible element `2` in `R`, a quadratic form `Q` on `V`, as well as an element `x` in the Clifford algebra of the base change of `Q` by `A`, the action of the reverse operation on `x` prior to applying the base change is the same as first applying the base change to `x` and then acting on the result by the tensor product of the identity and reverse functions. In other words, the reverse operation commutes with the base change operation up to the action of the tensor product.
More concisely: For any commutative rings `R` and `A`, additive commutative group `V` as an `R`-module, invertible element `2` in `R`, quadratic form `Q` on `V`, and element `x` in the Clifford algebra of `Q`'s base change by `A`, the reverse operation on `x` in `A⊗ₛ(A⊗ₓ(V, Q))` commutes with the base change operation.
|