Documentation

TauCeti.Algebra.AlgebraicGroup.Symplectic.RootSubgroup.Basic

Root subgroups of the symplectic group #

For i : Fin m, the elementary matrices

x_{2eᵢ}(c)  = 1 + c E_{i,m+i},
x_{-2eᵢ}(c) = 1 + c E_{m+i,i}

preserve the standard alternating form. For distinct i,j, products of two commuting elementary matrices similarly give the short roots eᵢ-eⱼ, eᵢ+eⱼ, and -eᵢ-eⱼ. This file promotes all five families to affine group-scheme morphisms 𝔾ₐ → Sp₂ₘ over an arbitrary commutative base ring.

The construction first selects the matrix homomorphism through TauCeti.GLSymplecticFin.RootSubgroupIndex. One shared pipeline constructs its natural map on algebra-valued points, recovers the coordinate Hopf-algebra morphism by full faithfulness of the functor of points, and applies relative spectrum. The long-root composites with the closed immersion Sp₂ₘ → GL₂ₘ are proved to be the corresponding general-linear root subgroups. Thus the factorization through the symplectic equations is recorded scheme-theoretically, over every base.

Main definitions #

References #

source
noncomputable def TauCeti.Symplectic.rootSubgroupPoints {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] (root : GLSymplecticFin.RootSubgroupIndex m) :
WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A) →* WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)

The homomorphism on A-valued points selected by a symplectic root index.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Symplectic.pointsMulEquiv_rootSubgroupPoints {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] (root : GLSymplecticFin.RootSubgroupIndex m) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) :
    (pointsMulEquiv R m) ((rootSubgroupPoints root) q) = root.hom (AdditiveGroup.gaPointsMulEquiv q)

    Under the symplectic point equivalence, a root point is the selected matrix homomorphism.

    source
    theorem TauCeti.Symplectic.rootSubgroupPoints_injective {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] (root : GLSymplecticFin.RootSubgroupIndex m) :
    Function.Injective ⇑(rootSubgroupPoints root)

    Every symplectic root subgroup is injective on algebra-valued points.

    source
    theorem TauCeti.Symplectic.mapValue_rootSubgroupPoints {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] {B : Type v} [CommRing B] [Algebra R B] (root : GLSymplecticFin.RootSubgroupIndex m) (φ : A →ₐ[R] B) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) :
    (AlgHom.mapValue φ) ((rootSubgroupPoints root) q) = (rootSubgroupPoints root) ((AlgHom.mapValue φ) q)

    Symplectic root point homomorphisms are natural in the value algebra.

    source
    noncomputable def TauCeti.Symplectic.positiveLongRootSubgroupPoints {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] (i : Fin m) :
    WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A) →* WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)

    The positive long-root homomorphism on A-points, sending c to 1 + c E_{i,m+i} in Sp₂ₘ(A).

    Equations
    Instances For
      source
      noncomputable def TauCeti.Symplectic.negativeLongRootSubgroupPoints {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] (i : Fin m) :
      WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A) →* WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)

      The negative long-root homomorphism on A-points, sending c to 1 + c E_{m+i,i} in Sp₂ₘ(A).

      Equations
      Instances For
        source
        noncomputable def TauCeti.Symplectic.shortRootSubgroupPoints {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} {A : Type w} [CommRing A] [Algebra R A] (family : GLSymplecticFin.ShortRootFamily) (hij : i ≠ j) :
        WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A) →* WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)

        The short-root homomorphism on algebra-valued points.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.Symplectic.pointsMulEquiv_positiveLongRootSubgroupPoints {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] (i : Fin m) (f : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) :
          (pointsMulEquiv R m) ((positiveLongRootSubgroupPoints i) f) = GLSymplecticFin.positiveLongRootTransvectionUnit i (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f))

          Under the symplectic point equivalence, the positive long-root point is its elementary transvection.

          source
          @[simp]
          theorem TauCeti.Symplectic.pointsMulEquiv_negativeLongRootSubgroupPoints {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] (i : Fin m) (f : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) :
          (pointsMulEquiv R m) ((negativeLongRootSubgroupPoints i) f) = GLSymplecticFin.negativeLongRootTransvectionUnit i (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f))

          Under the symplectic point equivalence, the negative long-root point is its elementary transvection.

          source
          @[simp]
          theorem TauCeti.Symplectic.pointsMulEquiv_shortRootSubgroupPoints {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} {A : Type w} [CommRing A] [Algebra R A] (family : GLSymplecticFin.ShortRootFamily) (hij : i ≠ j) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) :
          (pointsMulEquiv R m) ((shortRootSubgroupPoints family hij) q) = (family.hom hij) (AdditiveGroup.gaPointsMulEquiv q)

          Under the symplectic point equivalence, a short-root point is its paired elementary-matrix one-parameter subgroup.

          source
          theorem TauCeti.Symplectic.positiveLongRootSubgroupPoints_injective {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] (i : Fin m) :
          Function.Injective ⇑(positiveLongRootSubgroupPoints i)

          The positive long-root subgroup is injective on algebra-valued points.

          source
          theorem TauCeti.Symplectic.negativeLongRootSubgroupPoints_injective {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] (i : Fin m) :
          Function.Injective ⇑(negativeLongRootSubgroupPoints i)

          The negative long-root subgroup is injective on algebra-valued points.

          source
          theorem TauCeti.Symplectic.shortRootSubgroupPoints_injective {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} {A : Type w} [CommRing A] [Algebra R A] (family : GLSymplecticFin.ShortRootFamily) (hij : i ≠ j) :
          Function.Injective ⇑(shortRootSubgroupPoints family hij)

          A short-root subgroup is injective on points over every value algebra.

          source
          theorem TauCeti.Symplectic.mapValue_positiveLongRootSubgroupPoints {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] {B : Type v} [CommRing B] [Algebra R B] (phi : A →ₐ[R] B) (i : Fin m) (f : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) :
          (AlgHom.mapValue phi) ((positiveLongRootSubgroupPoints i) f) = (positiveLongRootSubgroupPoints i) ((AlgHom.mapValue phi) f)

          The positive long-root subgroup on points is natural in the value algebra.

          source
          theorem TauCeti.Symplectic.mapValue_negativeLongRootSubgroupPoints {R : Type u} [CommRing R] {m : ℕ} {A : Type w} [CommRing A] [Algebra R A] {B : Type v} [CommRing B] [Algebra R B] (phi : A →ₐ[R] B) (i : Fin m) (f : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) :
          (AlgHom.mapValue phi) ((negativeLongRootSubgroupPoints i) f) = (negativeLongRootSubgroupPoints i) ((AlgHom.mapValue phi) f)

          The negative long-root subgroup on points is natural in the value algebra.

          source
          theorem TauCeti.Symplectic.mapValue_shortRootSubgroupPoints {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} {A : Type w} [CommRing A] [Algebra R A] {B : Type v} [CommRing B] [Algebra R B] (family : GLSymplecticFin.ShortRootFamily) (φ : A →ₐ[R] B) (hij : i ≠ j) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra R) →ₐ[R] A)) :
          (AlgHom.mapValue φ) ((shortRootSubgroupPoints family hij) q) = (shortRootSubgroupPoints family hij) ((AlgHom.mapValue φ) q)

          Short-root point homomorphisms are natural in the value algebra.

          source
          noncomputable def TauCeti.Symplectic.rootSubgroupPointsMap {R : Type u} [CommRing R] {m : ℕ} (root : GLSymplecticFin.RootSubgroupIndex m) :
          HopfAlgebra.pointsFunctor ⟶ HopfAlgebra.pointsFunctor

          The natural transformation of group-valued points selected by a symplectic root index.

          Equations
          Instances For
            source
            noncomputable def TauCeti.Symplectic.positiveLongRootSubgroupPointsMap {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
            HopfAlgebra.pointsFunctor ⟶ HopfAlgebra.pointsFunctor

            The natural transformation of group-valued points for the positive long root 2eᵢ.

            Equations
            Instances For
              source
              noncomputable def TauCeti.Symplectic.negativeLongRootSubgroupPointsMap {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
              HopfAlgebra.pointsFunctor ⟶ HopfAlgebra.pointsFunctor

              The natural transformation of group-valued points for the negative long root -2eᵢ.

              Equations
              Instances For
                source
                noncomputable def TauCeti.Symplectic.shortRootSubgroupPointsMap {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (family : GLSymplecticFin.ShortRootFamily) (hij : i ≠ j) :
                HopfAlgebra.pointsFunctor ⟶ HopfAlgebra.pointsFunctor

                The natural transformation of group-valued points attached to a short root.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem TauCeti.Symplectic.rootSubgroupPointsMap_app {R : Type u} [CommRing R] {m : ℕ} (root : GLSymplecticFin.RootSubgroupIndex m) (A : CommAlgCat R) :
                  (rootSubgroupPointsMap root).app A = GrpCat.ofHom (rootSubgroupPoints root)

                  A component of the generic root points map is the constructed point homomorphism.

                  source
                  @[simp]
                  theorem TauCeti.Symplectic.positiveLongRootSubgroupPointsMap_app {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) (A : CommAlgCat R) :
                  (positiveLongRootSubgroupPointsMap i).app A = GrpCat.ofHom (positiveLongRootSubgroupPoints i)

                  A component of the positive long-root natural transformation is the corresponding point homomorphism.

                  source
                  @[simp]
                  theorem TauCeti.Symplectic.negativeLongRootSubgroupPointsMap_app {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) (A : CommAlgCat R) :
                  (negativeLongRootSubgroupPointsMap i).app A = GrpCat.ofHom (negativeLongRootSubgroupPoints i)

                  A component of the negative long-root natural transformation is the corresponding point homomorphism.

                  source
                  @[simp]
                  theorem TauCeti.Symplectic.shortRootSubgroupPointsMap_app {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (family : GLSymplecticFin.ShortRootFamily) (hij : i ≠ j) (A : CommAlgCat R) :
                  (shortRootSubgroupPointsMap family hij).app A = GrpCat.ofHom (shortRootSubgroupPoints family hij)

                  A component of the natural short-root points map is the constructed point homomorphism.

                  source
                  noncomputable def TauCeti.Symplectic.rootSubgroupCoordinateMap {R : Type u} [CommRing R] {m : ℕ} (root : GLSymplecticFin.RootSubgroupIndex m) :
                  coordinateHopfAlgebra R m ⟶ AdditiveGroup.coordinateHopfAlgebra R

                  The coordinate Hopf-algebra morphism selected by a symplectic root index.

                  Equations
                  Instances For
                    source
                    noncomputable def TauCeti.Symplectic.positiveLongRootSubgroupCoordinateMap {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
                    coordinateHopfAlgebra R m ⟶ AdditiveGroup.coordinateHopfAlgebra R

                    The coordinate morphism of the positive long-root subgroup, recovered from its natural action on points.

                    Equations
                    Instances For
                      source
                      noncomputable def TauCeti.Symplectic.negativeLongRootSubgroupCoordinateMap {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
                      coordinateHopfAlgebra R m ⟶ AdditiveGroup.coordinateHopfAlgebra R

                      The coordinate morphism of the negative long-root subgroup, recovered from its natural action on points.

                      Equations
                      Instances For
                        source
                        noncomputable def TauCeti.Symplectic.shortRootSubgroupCoordinateMap {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (family : GLSymplecticFin.ShortRootFamily) (hij : i ≠ j) :
                        coordinateHopfAlgebra R m ⟶ AdditiveGroup.coordinateHopfAlgebra R

                        The coordinate Hopf-algebra morphism of a short-root subgroup.

                        Equations
                        Instances For
                          source
                          theorem TauCeti.Symplectic.mapPointsFunctor_rootSubgroupCoordinateMap {R : Type u} [CommRing R] {m : ℕ} (root : GLSymplecticFin.RootSubgroupIndex m) :
                          CommHopfAlgCat.mapPointsFunctor (rootSubgroupCoordinateMap root) = rootSubgroupPointsMap root

                          Precomposition by a root coordinate morphism is its natural map on points.

                          source
                          theorem TauCeti.Symplectic.mapPointsFunctor_positiveLongRootSubgroupCoordinateMap {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
                          CommHopfAlgCat.mapPointsFunctor (positiveLongRootSubgroupCoordinateMap i) = positiveLongRootSubgroupPointsMap i

                          Precomposition by the positive long-root coordinate morphism gives its natural point map.

                          source
                          theorem TauCeti.Symplectic.mapPointsFunctor_negativeLongRootSubgroupCoordinateMap {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
                          CommHopfAlgCat.mapPointsFunctor (negativeLongRootSubgroupCoordinateMap i) = negativeLongRootSubgroupPointsMap i

                          Precomposition by the negative long-root coordinate morphism gives its natural point map.

                          source
                          theorem TauCeti.Symplectic.mapPointsFunctor_shortRootSubgroupCoordinateMap {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (family : GLSymplecticFin.ShortRootFamily) (hij : i ≠ j) :
                          CommHopfAlgCat.mapPointsFunctor (shortRootSubgroupCoordinateMap family hij) = shortRootSubgroupPointsMap family hij

                          Precomposition by the short-root coordinate morphism is its natural map on points.

                          source
                          @[simp]
                          theorem TauCeti.Symplectic.mapPointsFunctor_rootSubgroupCoordinateMap_app {R : Type u} [CommRing R] {m : ℕ} (root : GLSymplecticFin.RootSubgroupIndex m) (A : CommAlgCat R) (q : ↑(HopfAlgebra.points A)) :
                          (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (rootSubgroupCoordinateMap root)).app A)) q = (rootSubgroupPoints root) q

                          On a same-universe algebra, a root coordinate morphism induces the constructed point map.

                          source
                          @[simp]
                          theorem TauCeti.Symplectic.mapPointsFunctor_positiveLongRootSubgroupCoordinateMap_app {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) :
                          (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (positiveLongRootSubgroupCoordinateMap i)).app A)) f = (positiveLongRootSubgroupPoints i) f

                          On a same-universe algebra, the positive coordinate morphism induces the constructed point homomorphism.

                          source
                          @[simp]
                          theorem TauCeti.Symplectic.mapPointsFunctor_negativeLongRootSubgroupCoordinateMap_app {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) :
                          (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (negativeLongRootSubgroupCoordinateMap i)).app A)) f = (negativeLongRootSubgroupPoints i) f

                          On a same-universe algebra, the negative coordinate morphism induces the constructed point homomorphism.

                          source
                          @[simp]
                          theorem TauCeti.Symplectic.mapPointsFunctor_shortRootSubgroupCoordinateMap_app {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (family : GLSymplecticFin.ShortRootFamily) (hij : i ≠ j) (A : CommAlgCat R) (q : ↑(HopfAlgebra.points A)) :
                          (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (shortRootSubgroupCoordinateMap family hij)).app A)) q = (shortRootSubgroupPoints family hij) q

                          On a same-universe algebra, a short-root coordinate morphism induces its point homomorphism.

                          source
                          @[simp]
                          theorem TauCeti.Symplectic.rootSubgroupCoordinateMap_apply_X {R : Type u} [CommRing R] {m : ℕ} (root : GLSymplecticFin.RootSubgroupIndex m) (a b : Fin m ⊕ Fin m) :
                          (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap root)) ((CommHopfAlgCat.Hom.hom (coordinateMap R m)) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv R (m + m)) ((GeneralLinear.coordinateRingMap R (m + m)) (MvPolynomial.X (finSumFinEquiv a, finSumFinEquiv b))))) = (1 + root.tangentMatrix ((SymmetricAlgebra.ι R R) 1)) a b

                          A root coordinate morphism sends the generic symplectic matrix to the identity plus its normalized linear term. Entries are indexed in paired coordinates.

                          source
                          @[simp]
                          theorem TauCeti.Symplectic.coordinateMap_comp_positiveLongRootSubgroupCoordinateMap {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
                          CategoryTheory.CategoryStruct.comp (coordinateMap R m) (positiveLongRootSubgroupCoordinateMap i) = GeneralLinear.rootSubgroupCoordinateMap ⋯

                          The positive long-root coordinate morphism factors the matching general-linear root coordinate morphism through the symplectic quotient.

                          source
                          @[simp]
                          theorem TauCeti.Symplectic.coordinateMap_comp_negativeLongRootSubgroupCoordinateMap {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
                          CategoryTheory.CategoryStruct.comp (coordinateMap R m) (negativeLongRootSubgroupCoordinateMap i) = GeneralLinear.rootSubgroupCoordinateMap ⋯

                          The negative long-root coordinate morphism factors the matching general-linear root coordinate morphism through the symplectic quotient.

                          source
                          noncomputable def TauCeti.Symplectic.rootSubgroup {R : Type u} [CommRing R] {m : ℕ} (root : GLSymplecticFin.RootSubgroupIndex m) :
                          AdditiveGroup.groupScheme R ⟶ groupScheme R m

                          The affine group-scheme morphism selected by a symplectic root index.

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

                            A root subgroup is relative spectrum applied to its coordinate morphism.

                            source
                            theorem TauCeti.Symplectic.schemePointsMulEquiv_rootSubgroup {R : Type u} [CommRing R] {m : ℕ} (A : Type u) [CommRing A] [Algebra R A] (root : GLSymplecticFin.RootSubgroupIndex m) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (AdditiveGroup.groupScheme R).X) :
                            (schemePointsMulEquiv m A) (CategoryTheory.CategoryStruct.comp p (rootSubgroup root).hom.hom) = root.hom ((AdditiveGroup.schemePointsMulEquiv A) p)

                            A symplectic root subgroup on scheme-valued points is its standard root matrix.

                            source
                            noncomputable def TauCeti.Symplectic.positiveLongRootSubgroup {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
                            AdditiveGroup.groupScheme R ⟶ groupScheme R m

                            The positive long-root subgroup of Sp₂ₘ attached to 2eᵢ, as an affine group-scheme morphism.

                            Equations
                            Instances For
                              source
                              theorem TauCeti.Symplectic.positiveLongRootSubgroup_def {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
                              positiveLongRootSubgroup i = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (positiveLongRootSubgroupCoordinateMap i).op) (CategoryTheory.eqToHom ⋯))

                              The positive long-root subgroup is the relative spectrum of its coordinate morphism, transported to the named source and target schemes.

                              source
                              noncomputable def TauCeti.Symplectic.negativeLongRootSubgroup {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
                              AdditiveGroup.groupScheme R ⟶ groupScheme R m

                              The negative long-root subgroup of Sp₂ₘ attached to -2eᵢ, as an affine group-scheme morphism.

                              Equations
                              Instances For
                                source
                                theorem TauCeti.Symplectic.negativeLongRootSubgroup_def {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
                                negativeLongRootSubgroup i = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (negativeLongRootSubgroupCoordinateMap i).op) (CategoryTheory.eqToHom ⋯))

                                The negative long-root subgroup is the relative spectrum of its coordinate morphism, transported to the named source and target schemes.

                                source
                                noncomputable def TauCeti.Symplectic.shortRootSubgroup {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (family : GLSymplecticFin.ShortRootFamily) (hij : i ≠ j) :
                                AdditiveGroup.groupScheme R ⟶ groupScheme R m

                                The affine group-scheme morphism 𝔾ₐ → Sp₂ₘ attached to a short root.

                                Equations
                                Instances For
                                  source
                                  theorem TauCeti.Symplectic.shortRootSubgroup_def {R : Type u} [CommRing R] {m : ℕ} {i j : Fin m} (family : GLSymplecticFin.ShortRootFamily) (hij : i ≠ j) :
                                  shortRootSubgroup family hij = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (shortRootSubgroupCoordinateMap family hij).op) (CategoryTheory.eqToHom ⋯))

                                  The short-root subgroup is relative spectrum applied to its coordinate morphism.

                                  source
                                  @[simp]
                                  theorem TauCeti.Symplectic.positiveLongRootSubgroup_comp_inclusion {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
                                  CategoryTheory.CategoryStruct.comp (positiveLongRootSubgroup i) (inclusion R m) = GeneralLinear.rootSubgroup ⋯

                                  The positive long-root subgroup followed by the symplectic inclusion is the corresponding general-linear root subgroup.

                                  source
                                  @[simp]
                                  theorem TauCeti.Symplectic.negativeLongRootSubgroup_comp_inclusion {R : Type u} [CommRing R] {m : ℕ} (i : Fin m) :
                                  CategoryTheory.CategoryStruct.comp (negativeLongRootSubgroup i) (inclusion R m) = GeneralLinear.rootSubgroup ⋯

                                  The negative long-root subgroup followed by the symplectic inclusion is the corresponding general-linear root subgroup.