Documentation

TauCeti.Algebra.AlgebraicGroup.Symplectic.Scheme

Scheme-valued points of the symplectic group #

This file identifies scheme-valued points of Sp₂ₘ with the standard symplectic matrix group. This interface lets group-scheme morphisms and identities, including root-subgroup and torus actions, be computed as explicit symplectic matrix equations.

Main declarations #

References #

source
theorem TauCeti.Symplectic.groupScheme_X_left (R : Type u) [CommRing R] (m : ℕ) :
(groupScheme R m).X.left = AlgebraicGeometry.Spec ↧↑(coordinateHopfAlgebra R m)

The scheme underlying the symplectic group scheme is the spectrum of its coordinate Hopf algebra.

source
noncomputable def TauCeti.Symplectic.groupSchemePointMulEquiv (m : ℕ) {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] :
WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A) ≃* ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R m).X)

Mathlib's spectrum-points equivalence for the symplectic coordinate Hopf algebra.

Equations
Instances For
    source
    theorem TauCeti.Symplectic.groupSchemePointMulEquiv_apply_left (m : ℕ) {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)) :
    CategoryTheory.Over.Hom.left ((groupSchemePointMulEquiv m A) f) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑f.ofConv)) (CategoryTheory.eqToHom ⋯)

    The underlying spectrum map of the scheme point associated to a symplectic algebra point.

    source
    noncomputable def TauCeti.Symplectic.schemePointsMulEquiv (m : ℕ) {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] :
    ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R m).X) ≃* ↥(GLSymplecticFin m A)

    The group of scheme-valued points of Sp₂ₘ is the standard symplectic matrix group.

    Equations
    Instances For
      source
      theorem TauCeti.Symplectic.schemePointsMulEquiv_groupSchemePointMulEquiv (m : ℕ) {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (q : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)) :
      (schemePointsMulEquiv m A) ((groupSchemePointMulEquiv m A) q) = (pointsMulEquiv R m) q

      A scheme point presented by an algebra point corresponds to the same symplectic matrix.

      source
      theorem TauCeti.Symplectic.schemePointsMulEquiv_apply (m : ℕ) {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R m).X) :
      (schemePointsMulEquiv m A) p = (pointsMulEquiv R m) ((groupSchemePointMulEquiv m A).symm p)

      Evaluating the symplectic scheme-points equivalence directly on a scheme morphism.

      source
      theorem TauCeti.Symplectic.schemePointsMulEquiv_symm_apply (m : ℕ) {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (g : ↥(GLSymplecticFin m A)) :
      (schemePointsMulEquiv m A).symm g = (groupSchemePointMulEquiv m A) ((pointsMulEquiv R m).symm g)

      The inverse scheme-points equivalence sends a symplectic matrix to the spectrum point induced by its canonical coordinate-algebra point.

      source
      @[simp]
      theorem TauCeti.Symplectic.schemePointsMulEquiv_comp_inclusion (m : ℕ) {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R m).X) :
      (GeneralLinear.schemePointsMulEquiv (m + m) A) (CategoryTheory.CategoryStruct.comp p (inclusion R m).hom.hom) = ↑((schemePointsMulEquiv m A) p)

      Composing a symplectic scheme point with Sp_(2m) ⟶ GL_(2m) is the ordinary inclusion of its symplectic matrix into the general linear group.