Extension of scalars for Spin groups and even unitary groups

Mathlib's CliffordAlgebra.ofBaseChangeAux is the canonical map from a Clifford algebra to the Clifford algebra of a scalar extension; it preserves the even part and Clifford conjugation, as recorded in TauCeti.LinearAlgebra.CliffordAlgebra.BaseChange. It therefore restricts to a homomorphism of Spin groups. For the canonical lift of an Eichler transvection, this homomorphism sends 1 + ι w * ι u to the lift determined by the pure tensors 1 ⊗ u and 1 ⊗ w.

The same map restricts to the even unitary carriers U(C₀, σ), compatibly with the inclusion of Spin. Over a field K, this is how U(C₀, σ) is read as a twisted form: after extension to a field L splitting the even Clifford algebra, the image lands in the unitary group of a matrix algebra with involution.

An isomorphism σ : A ≃ₐ[R] B of coefficient algebras induces the isomorphism CliffordAlgebra.baseChangeCongr σ Q of the Clifford algebras of Q_A and Q_B. It preserves Clifford conjugation, the even part and the vector generators, so it restricts to an isomorphism of Spin groups. For complex conjugation of ℂ over ℝ this is coefficientwise conjugation of a complexified Spin group.

Main results

• CliffordAlgebra.spinGroupBaseChange extends a Spin element's scalars.
• CliffordAlgebra.spinGroupBaseChange_injective proves injectivity for faithful flat extensions.
• CliffordAlgebra.spinVectorAction_baseChange_tmul computes the extended action on pure tensors.
• CliffordAlgebra.spinToSpecialOrthogonal_baseChange gives the commuting square with extension of special orthogonal automorphisms.
• TauCeti.CliffordAlgebra.spinToOrthogonal_baseChange gives the corresponding commuting square for orthogonal automorphisms.
• CliffordAlgebra.spinGroupBaseChange_spinTransvection identifies the scalar extension of a canonical transvection lift.
• TauCeti.CliffordAlgebra.spinGroupBaseChange_comp_transvectionLiftHom transports the entire quotient root-subgroup homomorphism.
• CliffordAlgebra.spinGroupBaseChange_baseChange identifies direct and successive scalar extension.
• CliffordAlgebra.baseChangeCongr_mem_spinGroup and CliffordAlgebra.spinGroupBaseChangeCongr: an isomorphism of coefficient algebras preserves the Spin group, and restricts to an isomorphism of Spin groups.
• CliffordAlgebra.evenUnitaryGroupBaseChange extends the scalars of an even unitary unit, and CliffordAlgebra.evenUnitaryGroupBaseChange_injective proves injectivity for faithful flat extensions.
• CliffordAlgebra.evenUnitaryGroupBaseChange_spinGroupToEvenUnitary gives the commuting square with the inclusion of Spin into the even unitary carrier.
• CliffordAlgebra.evenUnitaryGroupBaseChange_baseChange identifies direct and successive scalar extension.

def CliffordAlgebra.spinGroupBaseChange {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) : ↥(spinGroup Q) →* ↥(spinGroup (QuadraticForm.baseChange A Q))

The homomorphism of Spin groups induced by extension of scalars.

@[simp]

theorem CliffordAlgebra.coe_spinGroupBaseChange_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 : ↥(spinGroup Q)) : ↑((spinGroupBaseChange Q) x) = (ofBaseChangeAux A Q) ↑x

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

theorem CliffordAlgebra.spinGroupBaseChange_injective {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] [FaithfulSMul R A] (Q : QuadraticForm R M) [Module.Flat R (CliffordAlgebra Q)] : Function.Injective ⇑(spinGroupBaseChange Q)

Extension of scalars of Spin groups is injective when the extension is faithful and the Clifford algebra is flat; in particular, for every extension of fields.

@[simp]

theorem CliffordAlgebra.spinVectorAction_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] [Invertible 2] (Q : QuadraticForm R M) (x : ↥(spinGroup Q)) (a : A) (m : M) : (spinVectorAction (QuadraticForm.baseChange A Q) ((spinGroupBaseChange Q) x)) (a ⊗ₜ[R] m) = a ⊗ₜ[R] (spinVectorAction Q x) m

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

@[simp]

theorem CliffordAlgebra.spinToSpecialOrthogonal_baseChange {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] [Module.Free R M] [Module.Finite R M] [Invertible 2] (Q : QuadraticForm R M) (x : ↥(spinGroup Q)) : (TauCeti.QuadraticMap.specialOrthogonalGroupBaseChange Q) ((spinToSpecialOrthogonal Q) x) = (spinToSpecialOrthogonal (QuadraticForm.baseChange A Q)) ((spinGroupBaseChange Q) x)

Extension of scalars commutes with the Spin homomorphism to the special orthogonal group.

@[simp]

theorem CliffordAlgebra.spinGroupBaseChange_spinTransvection {K : Type u} {L : Type v} {V : Type w} [Field K] [Field L] [Algebra K L] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] {Q : QuadraticForm K V} {u w : V} [Invertible 2] (hQ : QuadraticMap.Nondegenerate) (hu : Q u = 0) (huw : QuadraticMap.polar (⇑Q) u w = 0) : (spinGroupBaseChange Q) (spinTransvection hQ hu huw) = spinTransvection ⋯ ⋯ ⋯

Extension of scalars carries the canonical Spin lift of E_{u,w} to the canonical lift of E_{1 ⊗ u,1 ⊗ w}.

@[simp]

theorem CliffordAlgebra.spinGroupBaseChange_baseChange {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] {B : Type x} [CommRing B] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (Q : QuadraticForm R M) (z : ↥(spinGroup Q)) : Q.baseChangeBaseChange.toIsometry.spinGroupMap ((spinGroupBaseChange Q) z) = (spinGroupBaseChange (QuadraticForm.baseChange A Q)) ((spinGroupBaseChange Q) z)

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

Isomorphisms of the coefficient algebra

theorem CliffordAlgebra.baseChangeCongr_mem_spinGroup {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] {B : Type x} [CommRing B] [Algebra R B] (σ : A ≃ₐ[R] B) (Q : QuadraticForm R M) {x : CliffordAlgebra (QuadraticForm.baseChange A Q)} (hx : x ∈ spinGroup (QuadraticForm.baseChange A Q)) : (baseChangeCongr σ Q) x ∈ spinGroup (QuadraticForm.baseChange B Q)

The isomorphism CliffordAlgebra.baseChangeCongr σ Q : Cℓ(A ⊗ M) ≃ Cℓ(B ⊗ M) induced by an isomorphism of coefficient algebras sends Spin elements to Spin elements.

def CliffordAlgebra.spinGroupBaseChangeCongr {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] {B : Type x} [CommRing B] [Algebra R B] (σ : A ≃ₐ[R] B) (Q : QuadraticForm R M) : ↥(spinGroup (QuadraticForm.baseChange A Q)) ≃* ↥(spinGroup (QuadraticForm.baseChange B Q))

Coefficient isomorphisms act on Spin groups. An isomorphism σ : A ≃ₐ[R] B of coefficient algebras restricts CliffordAlgebra.baseChangeCongr σ Q to an isomorphism of the Spin groups of Q_A and Q_B. For complex conjugation of ℂ over ℝ this is coefficientwise conjugation of the Spin group of a complexified real quadratic form.

@[simp]

theorem CliffordAlgebra.coe_spinGroupBaseChangeCongr_apply {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] {B : Type x} [CommRing B] [Algebra R B] (σ : A ≃ₐ[R] B) (Q : QuadraticForm R M) (x : ↥(spinGroup (QuadraticForm.baseChange A Q))) : ↑((spinGroupBaseChangeCongr σ Q) x) = (baseChangeCongr σ Q) ↑x

The Clifford value of CliffordAlgebra.spinGroupBaseChangeCongr is computed by CliffordAlgebra.baseChangeCongr.

@[simp]

theorem CliffordAlgebra.spinGroupBaseChangeCongr_symm {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] {B : Type x} [CommRing B] [Algebra R B] (σ : A ≃ₐ[R] B) (Q : QuadraticForm R M) : (spinGroupBaseChangeCongr σ Q).symm = spinGroupBaseChangeCongr σ.symm Q

The inverse of CliffordAlgebra.spinGroupBaseChangeCongr is induced by the inverse coefficient isomorphism.

The even unitary carrier

def CliffordAlgebra.evenUnitaryGroupBaseChange {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) : ↥(evenUnitaryGroup Q) →* ↥(evenUnitaryGroup (QuadraticForm.baseChange A Q))

The homomorphism of even unitary carriers U(C₀, σ) → U(C₀ ⊗ A, σ) induced by extension of scalars.

@[simp]

theorem CliffordAlgebra.coe_evenUnitaryGroupBaseChange_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 : ↥(evenUnitaryGroup Q)) : ↑↑((evenUnitaryGroupBaseChange Q) x) = (ofBaseChangeAux A Q) ↑↑x

The Clifford value of a scalar-extended even unitary unit is obtained from the canonical Clifford map.

theorem CliffordAlgebra.evenUnitaryGroupBaseChange_injective {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] [FaithfulSMul R A] (Q : QuadraticForm R M) [Module.Flat R (CliffordAlgebra Q)] : Function.Injective ⇑(evenUnitaryGroupBaseChange Q)

Extension of scalars of even unitary carriers is injective when the extension is faithful and the Clifford algebra is flat; in particular, for every extension of fields.

@[simp]

theorem CliffordAlgebra.evenUnitaryGroupBaseChange_spinGroupToEvenUnitary {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 : ↥(spinGroup Q)) : (evenUnitaryGroupBaseChange Q) ((spinGroupToEvenUnitary Q) x) = (spinGroupToEvenUnitary (QuadraticForm.baseChange A Q)) ((spinGroupBaseChange Q) x)

Extension of scalars commutes with the inclusion of Spin into the even unitary carrier.

@[simp]

theorem CliffordAlgebra.evenUnitaryGroupBaseChange_baseChange {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] {B : Type x} [CommRing B] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (Q : QuadraticForm R M) (z : ↥(evenUnitaryGroup Q)) : Q.baseChangeBaseChange.toIsometry.evenUnitaryGroupMap ((evenUnitaryGroupBaseChange Q) z) = (evenUnitaryGroupBaseChange (QuadraticForm.baseChange A Q)) ((evenUnitaryGroupBaseChange Q) z)

Direct and successive scalar extension of an even unitary unit agree after transport along the canonical scalar-tower isometry.

@[simp]

theorem TauCeti.CliffordAlgebra.spinToOrthogonal_baseChange {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] [Invertible 2] (Q : QuadraticForm R M) (x : ↥(spinGroup Q)) : (CliffordAlgebra.spinToOrthogonal (QuadraticForm.baseChange A Q)) ((CliffordAlgebra.spinGroupBaseChange Q) x) = (QuadraticMap.orthogonalGroupBaseChange Q) ((CliffordAlgebra.spinToOrthogonal Q) x)

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

theorem TauCeti.CliffordAlgebra.spinGroupBaseChange_comp_transvectionLiftHom {K : Type u_4} {L : Type u_5} {V : Type u_6} [Field K] [Field L] [Algebra K L] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] [Invertible 2] {Q : QuadraticForm K V} {u : V} (hQ : QuadraticMap.Nondegenerate) (hu : Q u = 0) : (MonoidHom.toAdditive (CliffordAlgebra.spinGroupBaseChange Q)).comp (CliffordAlgebra.transvectionLiftHom hQ hu) = (CliffordAlgebra.transvectionLiftHom ⋯ ⋯).comp (QuadraticMap.transvectionParameterBaseChange Q u).toAddMonoidHom

Extending scalars along a field extension carries the canonical Spin root-subgroup homomorphism to that of the extended quotient parameters, preserving its additive composition law.

theorem QuadraticMap.IsometryEquiv.spinGroupBaseChange_spinGroupEquiv {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Invertible 2] {Q : QuadraticForm R M} {Q' : QuadraticForm R N} (e : IsometryEquiv Q Q') (s : ↥(spinGroup Q)) : (CliffordAlgebra.spinGroupBaseChange Q') (e.spinGroupEquiv s) = (e.baseChange A).spinGroupEquiv ((CliffordAlgebra.spinGroupBaseChange Q) s)

Scalar extension commutes with the Spin equivalence induced by a quadratic isometry.