The even unitary carrier as a symplectic group

An algebra isomorphism from the even Clifford algebra C₀ to a matrix algebra of even size which carries reversal σ to the standard symplectic adjoint X ↦ J⁻¹ Xᵀ J = -(J Xᵀ J) identifies the reverse-unitary carrier U(C₀, σ) with Mathlib's Matrix.symplecticGroup. This is a specialisation of CliffordAlgebra.evenUnitaryGroupEquivOfAlgEquiv, valid over any commutative ring and with no assumption on the dimension.

When C₀ only becomes a matrix algebra after extending scalars to an R-algebra A, the same transport is applied there: an isomorphism C₀ ⊗ A ≃ M(A) carrying the extended reversal to the symplectic adjoint maps U(C₀, σ) into the symplectic group over A. For a faithful flat extension this map is injective, and its image is exactly the set of symplectic matrices whose preimage in C₀ ⊗ A comes from C₀. This is how U(C₀, σ) is read as the group Sp(C₀, σ) of a twisted form of the symplectic group.

Main definitions

• CliffordAlgebra.evenUnitaryGroupEquivSymplecticGroup: an algebra isomorphism from C₀ to a matrix algebra carrying σ to the symplectic adjoint identifies U(C₀, σ) with the symplectic group.
• CliffordAlgebra.evenUnitaryGroupToSymplecticGroup: the same after extension of scalars, a homomorphism from U(C₀, σ) to the symplectic group over the extension.

Main results

• CliffordAlgebra.evenUnitaryGroupToSymplecticGroup_injective: the map is injective for faithful flat extensions.
• CliffordAlgebra.mem_range_evenUnitaryGroupToSymplecticGroup_iff: its image consists of the symplectic matrices whose preimage under the splitting is defined over R.

References

• M.-A. Knus, A. Merkurjev, M. Rost and J.-P. Tignol, The Book of Involutions (1998), §8.D.

noncomputable def CliffordAlgebra.evenUnitaryGroupEquivSymplecticGroup {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {l : Type u_3} [Fintype l] [DecidableEq l] (e : ↥(even Q) ≃ₐ[R] Matrix (l ⊕ l) (l ⊕ l) R) (he : ∀ (x : ↥(even Q)), e ((reverseEven Q) x) = -(Matrix.J l R * (e x).transpose * Matrix.J l R)) : ↥(evenUnitaryGroup Q) ≃* ↥(Matrix.symplecticGroup l R)

An algebra isomorphism from the even Clifford algebra to a matrix algebra of even size which carries reversal to the symplectic adjoint X ↦ -(J Xᵀ J) identifies the even unitary carrier U(C₀, σ) with the symplectic group.

@[simp]

theorem CliffordAlgebra.coe_evenUnitaryGroupEquivSymplecticGroup_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {l : Type u_3} [Fintype l] [DecidableEq l] (e : ↥(even Q) ≃ₐ[R] Matrix (l ⊕ l) (l ⊕ l) R) (he : ∀ (x : ↥(even Q)), e ((reverseEven Q) x) = -(Matrix.J l R * (e x).transpose * Matrix.J l R)) (x : ↥(evenUnitaryGroup Q)) : ↑((evenUnitaryGroupEquivSymplecticGroup Q e he) x) = e ((evenUnitaryGroupEvenPart Q) x)

The symplectic transport applies the algebra isomorphism to the even Clifford value.

@[simp]

theorem CliffordAlgebra.evenUnitaryGroupEvenPart_evenUnitaryGroupEquivSymplecticGroup_symm_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {l : Type u_3} [Fintype l] [DecidableEq l] (e : ↥(even Q) ≃ₐ[R] Matrix (l ⊕ l) (l ⊕ l) R) (he : ∀ (x : ↥(even Q)), e ((reverseEven Q) x) = -(Matrix.J l R * (e x).transpose * Matrix.J l R)) (g : ↥(Matrix.symplecticGroup l R)) : (evenUnitaryGroupEvenPart Q) ((evenUnitaryGroupEquivSymplecticGroup Q e he).symm g) = e.symm ↑g

The inverse symplectic transport applies the inverse algebra isomorphism.

After extension of scalars

noncomputable def CliffordAlgebra.evenUnitaryGroupToSymplecticGroup {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {l : Type u_3} [Fintype l] [DecidableEq l] {A : Type u_4} [CommRing A] [Algebra R A] [Invertible 2] (e : ↥(even (QuadraticForm.baseChange A Q)) ≃ₐ[A] Matrix (l ⊕ l) (l ⊕ l) A) (he : ∀ (x : ↥(even (QuadraticForm.baseChange A Q))), e ((reverseEven (QuadraticForm.baseChange A Q)) x) = -(Matrix.J l A * (e x).transpose * Matrix.J l A)) : ↥(evenUnitaryGroup Q) →* ↥(Matrix.symplecticGroup l A)

An algebra isomorphism from the scalar-extended even Clifford algebra C₀ ⊗ A to a matrix algebra of even size which carries reversal to the symplectic adjoint X ↦ -(J Xᵀ J) maps the even unitary carrier U(C₀, σ) into the symplectic group over A: extend scalars by CliffordAlgebra.evenUnitaryGroupBaseChange, then apply CliffordAlgebra.evenUnitaryGroupEquivSymplecticGroup.

@[simp]

theorem CliffordAlgebra.coe_evenUnitaryGroupToSymplecticGroup_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {l : Type u_3} [Fintype l] [DecidableEq l] {A : Type u_4} [CommRing A] [Algebra R A] [Invertible 2] (e : ↥(even (QuadraticForm.baseChange A Q)) ≃ₐ[A] Matrix (l ⊕ l) (l ⊕ l) A) (he : ∀ (x : ↥(even (QuadraticForm.baseChange A Q))), e ((reverseEven (QuadraticForm.baseChange A Q)) x) = -(Matrix.J l A * (e x).transpose * Matrix.J l A)) (x : ↥(evenUnitaryGroup Q)) : ↑((evenUnitaryGroupToSymplecticGroup Q e he) x) = e ((evenUnitaryGroupEvenPart (QuadraticForm.baseChange A Q)) ((evenUnitaryGroupBaseChange Q) x))

The symplectic matrix attached to an even unitary element is the splitting applied to its scalar extension.

theorem CliffordAlgebra.evenUnitaryGroupToSymplecticGroup_injective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {l : Type u_3} [Fintype l] [DecidableEq l] {A : Type u_4} [CommRing A] [Algebra R A] [Invertible 2] [FaithfulSMul R A] [Module.Flat R (CliffordAlgebra Q)] (e : ↥(even (QuadraticForm.baseChange A Q)) ≃ₐ[A] Matrix (l ⊕ l) (l ⊕ l) A) (he : ∀ (x : ↥(even (QuadraticForm.baseChange A Q))), e ((reverseEven (QuadraticForm.baseChange A Q)) x) = -(Matrix.J l A * (e x).transpose * Matrix.J l A)) : Function.Injective ⇑(evenUnitaryGroupToSymplecticGroup Q e he)

The map from U(C₀, σ) to the symplectic group over a faithful flat extension is injective.

theorem CliffordAlgebra.mem_range_evenUnitaryGroupToSymplecticGroup_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {l : Type u_3} [Fintype l] [DecidableEq l] {A : Type u_4} [CommRing A] [Algebra R A] [Invertible 2] [FaithfulSMul R A] [Module.Flat R (CliffordAlgebra Q)] (e : ↥(even (QuadraticForm.baseChange A Q)) ≃ₐ[A] Matrix (l ⊕ l) (l ⊕ l) A) (he : ∀ (x : ↥(even (QuadraticForm.baseChange A Q))), e ((reverseEven (QuadraticForm.baseChange A Q)) x) = -(Matrix.J l A * (e x).transpose * Matrix.J l A)) (g : ↥(Matrix.symplecticGroup l A)) : g ∈ (evenUnitaryGroupToSymplecticGroup Q e he).range ↔ ∃ y ∈ even Q, (ofBaseChangeAux A Q) y = ↑(e.symm ↑g)

The image of U(C₀, σ) in the symplectic group over a splitting extension. Over a faithful flat extension A splitting (C₀, σ) symplectically, a symplectic matrix g comes from an even unitary element exactly when its preimage in C₀ ⊗ A lies in the image of C₀.