Documentation

TauCeti.Algebra.AlgebraicGroup.Symplectic.DiagonalTorus.ClosedImmersion

The diagonal torus as a closed subgroup of the symplectic group #

Over every commutative ring, the diagonal map from the rank-m split torus to Sp₂ₘ is a closed immersion. Its defining Hopf ideal is the kernel of restriction to diagonal coordinates, the quotient is isomorphic to the split-torus coordinate Hopf algebra, and the ideal is compatible with scalar extension. These constructions make the diagonal torus available as a closed subgroup when studying maximal tori and pinnings.

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

The diagonal split torus is a closed subgroup of Sp₂ₘ over every commutative ring.

source
noncomputable def TauCeti.Symplectic.diagonalTorusClosedSubgroup (R : Type u) [CommRing R] (m : ℕ) :
ClosedSubgroupScheme (groupScheme R m)

The diagonal split torus, bundled as a closed subgroup scheme of Sp₂ₘ.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Symplectic.coe_diagonalTorusClosedSubgroup (R : Type u) [CommRing R] (m : ℕ) :
    ↑(diagonalTorusClosedSubgroup R m) = CategoryTheory.Subobject.mk diagonalTorus

    The closed diagonal torus has the subobject represented by the diagonal morphism.

    source
    noncomputable def TauCeti.Symplectic.diagonalTorusDefiningIdeal (R : Type u) [CommRing R] (m : ℕ) :
    HopfIdeal R ↑(coordinateHopfAlgebra R m)

    The defining Hopf ideal of the diagonal torus is the kernel of coordinate restriction.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Symplectic.mem_diagonalTorusDefiningIdeal (R : Type u) [CommRing R] (m : ℕ) (x : ↑(coordinateHopfAlgebra R m)) :
      x ∈ diagonalTorusDefiningIdeal R m ↔ (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) x = 0

      A function belongs to the diagonal-torus ideal precisely when its restriction vanishes.

      source
      @[simp]
      theorem TauCeti.Symplectic.hopfIdealOrderIsoClosedSubgroup_symm_apply_diagonalTorusClosedSubgroup (R : Type u) [CommRing R] (m : ℕ) :
      (CommHopfAlgCat.hopfIdealOrderIsoClosedSubgroup (coordinateHopfAlgebra R m)).symm (diagonalTorusClosedSubgroup R m) = OrderDual.toDual (diagonalTorusDefiningIdeal R m)

      The closed-subgroup classification recovers the diagonal torus's defining Hopf ideal.

      source
      noncomputable def TauCeti.Symplectic.diagonalTorusCoordinateIso (R : Type u) [CommRing R] (m : ℕ) :
      FiniteTypeCommHopfAlgCat.quotient { obj := coordinateHopfAlgebra R m, property := ⋯ } (diagonalTorusDefiningIdeal R m) ≅ DiagonalizableGroup.coordinateRing R (SplitTorus.characterGroup (ULift.{u, 0} (Fin m)))

      The quotient by the diagonal-torus ideal is the rank-m split-torus coordinate algebra.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.Symplectic.mkQuotient_comp_diagonalTorusCoordinateIso_hom (R : Type u) [CommRing R] (m : ℕ) :
        CategoryTheory.CategoryStruct.comp (FiniteTypeCommHopfAlgCat.mkQuotient { obj := coordinateHopfAlgebra R m, property := ⋯ } (diagonalTorusDefiningIdeal R m)) (diagonalTorusCoordinateIso R m).hom = CategoryTheory.ObjectProperty.homMk diagonalTorusCoordinateMap

        The quotient isomorphism identifies the quotient map with restriction to the torus.

        source
        theorem TauCeti.Symplectic.splitTorusCommHopfAlgProperty_quotient_diagonalTorusDefiningIdeal (R : Type u) [CommRing R] (m : ℕ) :
        splitTorusCommHopfAlgProperty R (FiniteTypeCommHopfAlgCat.quotient { obj := coordinateHopfAlgebra R m, property := ⋯ } (diagonalTorusDefiningIdeal R m))

        The coordinate quotient defining the symplectic diagonal torus is a split torus.

        source
        @[simp]
        theorem TauCeti.Symplectic.map_baseChangeHopfIdeal_diagonalTorusDefiningIdeal (R : Type u) [CommRing R] (m : ℕ) (K : Type u) [CommRing K] [Algebra R K] :
        (CommHopfAlgCat.baseChangeHopfIdeal (diagonalTorusDefiningIdeal R m)).map (CommHopfAlgCat.Hom.hom (coordinateHopfAlgebraBaseChangeIso R K m).hom) = diagonalTorusDefiningIdeal K m

        The base-change isomorphism of symplectic coordinate Hopf algebras carries the base-changed diagonal-torus ideal onto the diagonal-torus ideal over the extended base.

        source
        theorem TauCeti.Symplectic.torusCommHopfAlgProperty_quotient_diagonalTorusDefiningIdeal (k : Type u) [Field k] (m : ℕ) :
        torusCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.quotient { obj := coordinateHopfAlgebra k m, property := ⋯ } (diagonalTorusDefiningIdeal k m))

        Over a field, the coordinate quotient defining the symplectic diagonal torus is a torus.