Documentation

TauCeti.Algebra.AlgebraicGroup.Symplectic.IsotropicFlag.DiagonalTorus

The diagonal torus in the symplectic isotropic flag subgroup #

The standard diagonal torus of Sp₂ₘ factors through the standard complete isotropic flag subgroup over every commutative ring. The factored coordinate restriction is surjective, so the torus inclusion is a closed immersion. Its composite with the flag subgroup inclusion recovers the ambient symplectic torus, and its algebra-valued points are the same diagonal symplectic matrices.

The factorization follows TauCeti.Algebra.AlgebraicGroup.SpecialLinear.UpperTriangular.DiagonalTorus, using CommHopfAlgCat.liftQuotient and Symplectic.diagonalTorusCoordinateMap.

References #

source
theorem TauCeti.Symplectic.IsotropicFlag.definingHopfIdeal_le_diagonalTorusDefiningIdeal (R : Type u) [CommRing R] (m : ℕ) :
definingHopfIdeal R m ≤ diagonalTorusDefiningIdeal R m

The diagonal symplectic torus lies in the standard isotropic flag subgroup. The order of defining ideals reverses the inclusion of closed subgroups.

source
noncomputable def TauCeti.Symplectic.IsotropicFlag.diagonalTorusCoordinateMap (R : Type u) [CommRing R] (m : ℕ) :
coordinateHopfAlgebra R m ⟶ (DiagonalizableGroup.coordinateRing R (SplitTorus.characterGroup (ULift.{u, 0} (Fin m)))).obj

Restriction from the isotropic flag subgroup to its diagonal symplectic torus.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.Symplectic.IsotropicFlag.coordinateMap_comp_diagonalTorusCoordinateMap (R : Type u) [CommRing R] (m : ℕ) :
    CategoryTheory.CategoryStruct.comp (coordinateMap R m) (diagonalTorusCoordinateMap R m) = Symplectic.diagonalTorusCoordinateMap

    The factored torus restriction recovers the original restriction from the symplectic group.

    source
    @[simp]
    theorem TauCeti.Symplectic.IsotropicFlag.coordinateMap_comp_diagonalTorusCoordinateMap_assoc (R : Type u) [CommRing R] (m : ℕ) {Z : CommHopfAlgCat R} (h : ↧(MonoidAlgebra R ↑(SplitTorus.characterGroup (ULift.{u, 0} (Fin m)))) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (coordinateMap R m) (CategoryTheory.CategoryStruct.comp (diagonalTorusCoordinateMap R m) h) = CategoryTheory.CategoryStruct.comp Symplectic.diagonalTorusCoordinateMap h

    The factored torus restriction recovers the original restriction from the symplectic group.

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

    The torus restriction from the isotropic flag subgroup is surjective.

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

    The standard diagonal torus as a morphism into the isotropic flag subgroup scheme.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.Symplectic.IsotropicFlag.diagonalTorus_comp_inclusion (R : Type u) [CommRing R] (m : ℕ) :
      CategoryTheory.CategoryStruct.comp (diagonalTorus R m) (inclusion R m) = Symplectic.diagonalTorus

      Inclusion of the factored diagonal torus recovers the ambient symplectic diagonal torus.

      source
      @[simp]
      theorem TauCeti.Symplectic.IsotropicFlag.diagonalTorus_comp_inclusion_assoc (R : Type u) [CommRing R] (m : ℕ) {Z : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))} (h : (AlgebraicGeometry.algSpec ↧R).mapGrp.obj ((commHopfAlgCatEquivCogrpCommAlgCat R).functor.leftOp.obj (Opposite.op (Symplectic.coordinateHopfAlgebra R m))) ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (diagonalTorus R m) (CategoryTheory.CategoryStruct.comp (inclusion R m) h) = CategoryTheory.CategoryStruct.comp Symplectic.diagonalTorus h

      Inclusion of the factored diagonal torus recovers the ambient symplectic diagonal torus.

      source
      instance TauCeti.Symplectic.IsotropicFlag.isClosedImmersion_diagonalTorus (R : Type u) [CommRing R] (m : ℕ) :
      AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (diagonalTorus R m).hom.hom)

      The standard diagonal torus is a closed subgroup scheme of the isotropic flag subgroup.

      source
      @[simp]
      theorem TauCeti.Symplectic.IsotropicFlag.pointsMulEquiv_diagonalTorusCoordinateMap (R : Type u) [CommRing R] (m : ℕ) {A : Type w} [CommRing A] [Algebra R A] (f : WithConv (MonoidAlgebra R ↑(SplitTorus.characterGroup (ULift.{u, 0} (Fin m))) →ₐ[R] A)) :
      ↑((pointsMulEquiv R m) (WithConv.toConv (f.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap R m))))) = (Symplectic.pointsMulEquiv R m) (diagonalTorusPoints f)

      The factored torus map gives the same symplectic diagonal matrix as the ambient torus map.