Extension of scalars for the Lipschitz group

Extension of scalars sends each invertible Clifford generator to the corresponding pure tensor, so it induces a homomorphism of Lipschitz groups. The twisted-conjugation action commutes with this homomorphism: on a pure tensor, the extended element acts by extending the original action. Consequently the resulting map to the orthogonal group agrees with scalar extension of orthogonal automorphisms.

Main results

• CliffordAlgebra.lipschitzGroupBaseChange extends a Lipschitz element's scalars.
• CliffordAlgebra.lipschitzVectorAction_baseChange_tmul computes the extended action on pure tensors.
• CliffordAlgebra.lipschitzToOrthogonal_baseChange gives the commuting square with extension of orthogonal automorphisms.
• CliffordAlgebra.lipschitzGroupBaseChange_baseChange identifies direct and successive scalar extension.

def CliffordAlgebra.lipschitzGroupBaseChange {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) : ↥(lipschitzGroup Q) →* ↥(lipschitzGroup (QuadraticForm.baseChange A Q))

The homomorphism of Lipschitz groups induced by extension of scalars.

Equations

• CliffordAlgebra.lipschitzGroupBaseChange Q = CliffordAlgebra.lipschitzGroupMapOf (CliffordAlgebra.ofBaseChangeAux A Q).toRingHom (fun (m : M) => 1 ⊗ₜ[R] m) ⋯

@[simp]

theorem CliffordAlgebra.coe_lipschitzGroupBaseChange_apply {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (x : ↥(lipschitzGroup Q)) : ↑↑((lipschitzGroupBaseChange Q) x) = (ofBaseChangeAux A Q) ↑↑x

The Clifford value of a scalar-extended Lipschitz element is obtained from the canonical Clifford map.

@[simp]

theorem CliffordAlgebra.lipschitzGroupBaseChange_inv_coe {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (x : ↥(lipschitzGroup Q)) : (ofBaseChangeAux A Q) ↑(↑x)⁻¹ = ↑(↑((lipschitzGroupBaseChange Q) x))⁻¹

Extending the inverse of a Lipschitz unit agrees with taking the inverse after extension.

@[simp]

theorem CliffordAlgebra.lipschitzVectorAction_baseChange_tmul {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (x : ↥(lipschitzGroup Q)) (a : A) (m : M) : (lipschitzVectorAction (QuadraticForm.baseChange A Q) ((lipschitzGroupBaseChange Q) x)) (a ⊗ₜ[R] m) = a ⊗ₜ[R] (lipschitzVectorAction Q x) m

On a pure tensor, the scalar-extended Lipschitz action is the extension of the original action.

@[simp]

theorem CliffordAlgebra.lipschitzToOrthogonal_baseChange {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (x : ↥(lipschitzGroup Q)) : (TauCeti.QuadraticMap.orthogonalGroupBaseChange Q) ((lipschitzToOrthogonal Q) x) = (lipschitzToOrthogonal (QuadraticForm.baseChange A Q)) ((lipschitzGroupBaseChange Q) x)

Extension of scalars commutes with the Lipschitz homomorphism to the orthogonal group.

@[simp]

theorem CliffordAlgebra.lipschitzGroupBaseChange_baseChange {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) {B : Type x} [CommRing B] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (x : ↥(lipschitzGroup Q)) : Q.baseChangeBaseChange.toIsometry.lipschitzGroupMap ((lipschitzGroupBaseChange Q) x) = (lipschitzGroupBaseChange (QuadraticForm.baseChange A Q)) ((lipschitzGroupBaseChange Q) x)

Direct and successive scalar extension of a Lipschitz element agree after transport along the canonical scalar-tower isometry.