Documentation

TauCeti.Algebra.AlgebraicGroup.Symplectic.DiagonalTorus.Basic

The diagonal torus of the symplectic group scheme #

This file promotes the diagonal symplectic matrices

diag(t₀, …, tₘ₋₁, t₀⁻¹, …, tₘ₋₁⁻¹)

to a morphism from the rank-m split torus to Sp₂ₘ over an arbitrary commutative base ring. The construction is made simultaneously in the functor-of-points, coordinate-Hopf-algebra, and affine-group-scheme models. On algebra-valued points it is injective, natural in the value algebra, and conjugates each symplectic root subgroup through its standard root character.

This is the torus and pinning-equation part of the standard type-C pinning. The coordinate morphism is surjective; its closed-subgroup interpretation is developed in TauCeti.Algebra.AlgebraicGroup.Symplectic.DiagonalTorus.ClosedImmersion.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.Symplectic.diagonalTorusPoints {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] :
WithConv (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin m) →₀ ℤ)) →ₐ[R] A) →* WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)

The diagonal torus of Sp₂ₘ on algebra-valued points. Under the split-torus and symplectic points equivalences it is the standard diagonal matrix with paired inverse entries.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.Symplectic.pointsMulEquiv_diagonalTorusPoints {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] (t : WithConv (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin m) →₀ ℤ)) →ₐ[R] A)) :
    (pointsMulEquiv R m) (diagonalTorusPoints t) = GLSymplecticFin.diagonal (GeneralLinear.diagonalTorusCoordinates (SplitTorus.pointsMulEquiv t))

    Reading a diagonal-torus point as a symplectic matrix gives the standard diagonal matrix.

    source
    theorem TauCeti.Symplectic.diagonalTorusPoints_injective {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] :
    Function.Injective ⇑diagonalTorusPoints

    The diagonal-torus homomorphism into symplectic points is injective.

    source
    theorem TauCeti.Symplectic.mapValue_diagonalTorusPoints {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] {B : Type v} [CommRing B] [Algebra R B] (f : A →ₐ[R] B) (t : WithConv (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin m) →₀ ℤ)) →ₐ[R] A)) :
    (AlgHom.mapValue f) (diagonalTorusPoints t) = diagonalTorusPoints ((AlgHom.mapValue f) t)

    The symplectic diagonal-torus map is natural in the value algebra.

    source
    theorem TauCeti.Symplectic.diagonalTorusPoints_mul_rootSubgroupPoints_mul_inv {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] (root : GLSymplecticFin.RootSubgroupIndex m) (t : WithConv (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin m) →₀ ℤ)) →ₐ[R] A)) (c : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) :
    diagonalTorusPoints t * (rootSubgroupPoints root) c * (diagonalTorusPoints t)⁻¹ = (rootSubgroupPoints root) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (↑(root.character (GeneralLinear.diagonalTorusCoordinates (SplitTorus.pointsMulEquiv t))) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv c))))

    The symplectic pinning equation on algebra-valued points. Conjugation by a diagonal-torus point scales the parameter of every standard root subgroup by its root character.

    source
    noncomputable def TauCeti.Symplectic.diagonalTorusPointsMap {R : Type u} [CommRing R] {m : ℕ} :
    HopfAlgebra.pointsFunctor ⟶ HopfAlgebra.pointsFunctor

    The natural transformation of group-valued points defined by the symplectic diagonal torus.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Symplectic.diagonalTorusPointsMap_app {R : Type u} [CommRing R] {m : ℕ} (A : CommAlgCat R) :
      diagonalTorusPointsMap.app A = GrpCat.ofHom diagonalTorusPoints

      The component of the natural diagonal-torus map is diagonalTorusPoints.

      source
      noncomputable def TauCeti.Symplectic.diagonalTorusCoordinateMap {R : Type u} [CommRing R] {m : ℕ} :
      coordinateHopfAlgebra R m ⟶ ↧(MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin m) →₀ ℤ)))

      The coordinate morphism of the symplectic diagonal torus, recovered from its natural action on points. Its direction is opposite to the represented group-scheme morphism.

      Equations
      Instances For
        source
        theorem TauCeti.Symplectic.mapPointsFunctor_diagonalTorusCoordinateMap {R : Type u} [CommRing R] {m : ℕ} :
        CommHopfAlgCat.mapPointsFunctor diagonalTorusCoordinateMap = diagonalTorusPointsMap

        Precomposition by the coordinate morphism is the natural point map already constructed.

        source
        @[simp]
        theorem TauCeti.Symplectic.mapPointsFunctor_diagonalTorusCoordinateMap_app {R : Type u} [CommRing R] {m : ℕ} (A : CommAlgCat R) (t : ↑(HopfAlgebra.points A)) :
        (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor diagonalTorusCoordinateMap).app A)) t = diagonalTorusPoints t

        On every value algebra, the coordinate morphism induces diagonalTorusPoints.

        source
        @[simp]
        theorem TauCeti.Symplectic.coordinateMap_comp_diagonalTorusCoordinateMap_X_castAdd {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
        (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) ((CommHopfAlgCat.Hom.hom (coordinateMap R m)) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv R (m + m)) ((GeneralLinear.coordinateRingMap R (m + m)) (MvPolynomial.X (Fin.castAdd m i, Fin.castAdd m i))))) = MonoidAlgebra.single (Multiplicative.ofAdd (Finsupp.single { down := i } 1)) 1

        The first-block diagonal generic entry restricts to its corresponding torus character.

        source
        @[simp]
        theorem TauCeti.Symplectic.coordinateMap_comp_diagonalTorusCoordinateMap_X_addNat {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
        (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) ((CommHopfAlgCat.Hom.hom (coordinateMap R m)) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv R (m + m)) ((GeneralLinear.coordinateRingMap R (m + m)) (MvPolynomial.X (i.addNat m, i.addNat m))))) = MonoidAlgebra.single (Multiplicative.ofAdd (Finsupp.single { down := i } (-1))) 1

        The second-block diagonal generic entry restricts to the inverse torus character.

        source
        @[simp]
        theorem TauCeti.Symplectic.coordinateMap_comp_diagonalTorusCoordinateMap_X_of_ne {R : Type u} [CommRing R] {m : ℕ} (i j : Fin (m + m)) (hij : i ≠ j) :
        (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) ((CommHopfAlgCat.Hom.hom (coordinateMap R m)) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv R (m + m)) ((GeneralLinear.coordinateRingMap R (m + m)) (MvPolynomial.X (i, j))))) = 0

        Every off-diagonal ambient generic matrix entry restricts to zero on the diagonal torus.

        source
        noncomputable def TauCeti.Symplectic.diagonalTorusWeight {m : ℕ} :
        Fin m ⊕ Fin m → ULift.{u, 0} (Fin m) →₀ ℤ

        The standard weights of the paired diagonal torus: εᵢ in the first block and -εᵢ in the second block. These are integral characters, irrespective of the base ring.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.Symplectic.diagonalTorusWeight_inl {m : ℕ} (i : Fin m) :
          diagonalTorusWeight (Sum.inl i) = Finsupp.single { down := i } 1
          source
          @[simp]
          theorem TauCeti.Symplectic.diagonalTorusWeight_inr {m : ℕ} (i : Fin m) :
          diagonalTorusWeight (Sum.inr i) = -Finsupp.single { down := i } 1
          source
          theorem TauCeti.Symplectic.coordinateMap_comp_diagonalTorusCoordinateMap {R : Type u} [CommRing R] {m : ℕ} :
          CategoryTheory.CategoryStruct.comp (coordinateMap R m) diagonalTorusCoordinateMap = GeneralLinear.weightTorusCoordinateMap fun (i : Fin (m + m)) => ⇑(diagonalTorusWeight (finSumFinEquiv.symm i))

          Restricting the symplectic diagonal-torus coordinate map to the ambient general linear group is the general weight-torus map for the paired weights.

          source
          theorem TauCeti.Symplectic.diagonalTorusCoordinateMap_surjective {R : Type u} [CommRing R] {m : ℕ} :
          Function.Surjective ⇑(CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap)

          The coordinate restriction from Sp₂ₘ to its diagonal torus is surjective over every commutative base ring.

          source
          theorem TauCeti.Symplectic.diagonalTorusCoordinateMap_baseChange {m : ℕ} (R K : Type u) [CommRing R] [CommRing K] [Algebra R K] :
          CategoryTheory.CategoryStruct.comp (coordinateHopfAlgebraBaseChangeIso R K m).inv (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap diagonalTorusCoordinateMap) (DiagonalizableGroup.baseChangeCoordinateHopfAlgebraIso R K (SplitTorus.characterGroup (ULift.{u, 0} (Fin m)))).hom) = diagonalTorusCoordinateMap

          The symplectic diagonal-torus coordinate morphism commutes with base change.

          source
          noncomputable def TauCeti.Symplectic.diagonalTorus {R : Type u} [CommRing R] {m : ℕ} :
          SplitTorus.groupScheme R (ULift.{u, 0} (Fin m)) ⟶ groupScheme R m

          The diagonal torus of Sp₂ₘ as a group-scheme morphism from the rank-m split torus.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem TauCeti.Symplectic.diagonalTorus_def {R : Type u} [CommRing R] {m : ℕ} :
            diagonalTorus = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map diagonalTorusCoordinateMap.op) (CategoryTheory.eqToHom ⋯))

            The diagonal torus is relative spectrum applied contravariantly to its coordinate morphism, transported across the named presentations of the split torus and symplectic group.

            source
            theorem TauCeti.Symplectic.schemePointsMulEquiv_diagonalTorus {R : Type u} [CommRing R] {m : ℕ} (A : Type u) [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (SplitTorus.groupScheme R (ULift.{u, 0} (Fin m))).X) :
            (schemePointsMulEquiv m A) (CategoryTheory.CategoryStruct.comp p diagonalTorus.hom.hom) = GLSymplecticFin.diagonal (GeneralLinear.diagonalTorusCoordinates (SplitTorus.schemePointsMulEquiv p))

            The symplectic diagonal torus on scheme-valued points is the standard paired diagonal matrix.

            source
            theorem TauCeti.Symplectic.schemePointsMulEquiv_diagonalTorus_mul_rootSubgroup_mul_inv {R : Type u} [CommRing R] {m : ℕ} (A : Type u) [CommRing A] [Algebra R A] (root : GLSymplecticFin.RootSubgroupIndex m) (t : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (SplitTorus.groupScheme R (ULift.{u, 0} (Fin m))).X) (c : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (AdditiveGroup.groupScheme R).X) :
            (schemePointsMulEquiv m A) (CategoryTheory.CategoryStruct.comp t diagonalTorus.hom.hom) * (schemePointsMulEquiv m A) (CategoryTheory.CategoryStruct.comp c (rootSubgroup root).hom.hom) * ((schemePointsMulEquiv m A) (CategoryTheory.CategoryStruct.comp t diagonalTorus.hom.hom))⁻¹ = (schemePointsMulEquiv m A) (CategoryTheory.CategoryStruct.comp ((AdditiveGroup.groupSchemePointMulEquiv A) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (↑(root.character (GeneralLinear.diagonalTorusCoordinates (SplitTorus.schemePointsMulEquiv t))) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) c))))) (rootSubgroup root).hom.hom)

            The symplectic pinning equation on scheme-valued points. Conjugating a root-subgroup point by a diagonal-torus point scales its additive parameter by the corresponding root character.