Documentation

TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Symplectic.Center

The center of the symplectic group #

Over any commutative ring, a matrix commuting with every symplectic matrix is scalar. Consequently the center of Sp₂ₘ in positive rank consists of scalar matrices whose scalar squares to one. This description retains the infinitesimal center in characteristic two.

The scalar homomorphism realizes square roots of one as central symplectic matrices, providing the pointwise description used for the center of the symplectic group scheme.

References #

The elementary matrices are those of TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Symplectic.Basic.

source
theorem Matrix.mem_range_scalar_of_commute_symplectic {R : Type u_1} [CommRing R] {m : ℕ} (M : Matrix (Fin (m + m)) (Fin (m + m)) R) (hM : ∀ (g : ↥(TauCeti.GLSymplecticFin m R)), Commute M ↑↑g) :
M ∈ Set.range ⇑(scalar (Fin (m + m)))

A matrix commuting with all symplectic matrices is scalar, over any commutative ring.

source
theorem TauCeti.GLSymplecticFin.mem_center_of_val_eq_scalar {R : Type u_1} [CommRing R] {m : ℕ} {g : ↥(GLSymplecticFin m R)} {c : R} (hc : ↑↑g = (Matrix.scalar (Fin (m + m))) c) :
g ∈ Subgroup.center ↥(GLSymplecticFin m R)

A symplectic element whose underlying matrix is scalar is central.

source
theorem TauCeti.GLSymplecticFin.mem_center_iff {R : Type u_1} [CommRing R] {m : ℕ} (hm : m ≠ 0) (g : ↥(GLSymplecticFin m R)) :
g ∈ Subgroup.center ↥(GLSymplecticFin m R) ↔ ∃ (c : R), ↑↑g = (Matrix.scalar (Fin (m + m))) c ∧ c ^ 2 = 1

In positive rank the center of the symplectic group consists exactly of scalar matrices whose scalar squares to one. No reducedness or characteristic assumption is needed.

source
instance TauCeti.GLSymplecticFin.instNontrivialQuotientCenter {R : Type u_1} [CommRing R] {m : ℕ} [Nontrivial R] [NeZero m] :
Nontrivial (↥(GLSymplecticFin m R) ⧸ Subgroup.center ↥(GLSymplecticFin m R))

In positive rank over a nontrivial ring, the central quotient of the symplectic group is nontrivial: a long-root transvection with parameter one is not scalar.

source
noncomputable def TauCeti.GLSymplecticFin.rootsOfUnityScalar (m : ℕ) {A : Type u_2} [CommRing A] :
↥(rootsOfUnity 2 A) →* ↥(GLSymplecticFin m A)

A square root of one acts by a scalar symplectic matrix.

Instances For
    source
    @[simp]
    theorem TauCeti.GLSymplecticFin.coe_rootsOfUnityScalar (m : ℕ) {A : Type u_2} [CommRing A] (ζ : ↥(rootsOfUnity 2 A)) :
    ↑↑((rootsOfUnityScalar m) ζ) = (Matrix.scalar (Fin (m + m))) ↑↑ζ

    The underlying matrix of a scalar symplectic point is its scalar matrix.