Documentation

TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Weight.Levi.Basic

Weight-Levi subgroup schemes of the general linear group #

An integer weight w i on each coordinate of GL_N decomposes the standard representation into its weight spaces. The corresponding Levi subgroup consists of the invertible matrices preserving every weight space, so its (i,j) entry vanishes whenever w i ≠ w j.

This file represents that subgroup over an arbitrary commutative base ring. Its defining Hopf ideal is the join of the weight-parabolic ideals for w and -w: intersecting the two opposite block-triangular subgroups leaves precisely the block-diagonal Levi. This construction reuses the weight-parabolic Hopf-ideal and closed-subgroup API rather than repeating its comultiplication and antipode calculations.

Main declarations #

References #

This advances the dynamic-parabolic route in Layer 7, "Structure theory", of the ReductiveGroups roadmap by constructing the scheme-level Levi attached to a weight cocharacter.

source
noncomputable def TauCeti.GeneralLinear.weightLeviDefiningHopfIdeal (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
HopfIdeal R ↑(coordinateHopfAlgebra R N)

The Hopf ideal cutting out the matrices preserving every weight space. It is the join of the weight-parabolic ideals for the two opposite filtrations.

Equations
Instances For
    source
    theorem TauCeti.GeneralLinear.weightLeviDefiningHopfIdeal_def (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
    weightLeviDefiningHopfIdeal R w = weightParabolicDefiningHopfIdeal R w ⊔ weightParabolicDefiningHopfIdeal R (-w)

    The weight-Levi ideal is the join of the ideals for the two opposite weight parabolics.

    source
    theorem TauCeti.GeneralLinear.weightLeviDefiningHopfIdeal_toIdeal_le_ker (R : Type u) [CommRing R] {N : ℕ} {A : Type u_1} [CommRing A] [Algebra R A] (w : Fin N → ℤ) (f : ↑(coordinateHopfAlgebra R N) →ₐ[R] A) (hf : ∀ (i j : Fin N), w i ≠ w j → f ((coordinateHopfAlgebraAlgEquiv R N) ((coordinateRingMap R N) (MvPolynomial.X (i, j)))) = 0) :
    (weightLeviDefiningHopfIdeal R w).toIdeal ≤ RingHom.ker f.toRingHom

    A morphism out of the coordinate algebra of GL_N kills the weight-Levi defining Hopf ideal as soon as it kills every matrix coordinate between distinct weight blocks.

    source
    @[reducible, inline]
    noncomputable abbrev TauCeti.GeneralLinear.weightLeviCoordinateHopfAlgebra (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
    CommHopfAlgCat R

    The coordinate Hopf algebra of the weight Levi attached to w.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def TauCeti.GeneralLinear.weightLeviFiniteTypeCoordinateHopfAlgebra (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
      FiniteTypeCommHopfAlgCat R

      The weight-Levi coordinate Hopf algebra with its finite-type property.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.GeneralLinear.weightLeviFiniteTypeCoordinateHopfAlgebra_obj (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
        (weightLeviFiniteTypeCoordinateHopfAlgebra R w).obj = weightLeviCoordinateHopfAlgebra R w

        The finite-type package has the weight-Levi coordinate Hopf algebra as its object.

        source
        @[reducible, inline]
        noncomputable abbrev TauCeti.GeneralLinear.weightLeviGroupScheme (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
        CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

        The affine group scheme represented by the weight-Levi coordinate Hopf algebra.

        Equations
        Instances For
          source
          noncomputable def TauCeti.GeneralLinear.weightLeviInclusion (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
          weightLeviGroupScheme R w ⟶ groupScheme R N

          The closed immersion from the weight Levi into the named general linear group scheme.

          Equations
          Instances For
            source
            theorem TauCeti.GeneralLinear.weightLeviInclusion_def (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
            weightLeviInclusion R w = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.quotientSpecι (coordinateHopfAlgebra R N) (weightLeviDefiningHopfIdeal R w)) (CategoryTheory.eqToIso ⋯).hom

            The weight-Levi inclusion is the quotient-spectrum inclusion followed by the named identification with GL_N.

            source
            instance TauCeti.GeneralLinear.isClosedImmersion_weightLeviInclusion (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
            AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (weightLeviInclusion R w).hom.hom)

            The weight-Levi inclusion into GL_N is a closed immersion.

            source
            instance TauCeti.GeneralLinear.locallyOfFiniteType_weightLeviGroupScheme (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
            AlgebraicGeometry.LocallyOfFiniteType (weightLeviGroupScheme R w).X.hom

            The weight-Levi group scheme is locally of finite type over the base.

            source
            @[simp]
            theorem TauCeti.GeneralLinear.mem_weightLeviDefiningPointsSubgroup_iff_apply_eq_zero (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) {A : Type u_1} [CommRing A] [Algebra R A] (g : ↑(HopfAlgebra.points ↧A)) :
            g ∈ CommHopfAlgCat.quotientPointsSubgroup (coordinateHopfAlgebra R N) (weightLeviDefiningHopfIdeal R w) ↧A ↔ ∀ (i j : Fin N), w i ≠ w j → ↑((pointsMulEquiv N) g) i j = 0

            The subgroup cut out by the weight-Levi ideal consists exactly of matrices preserving every weight space: entries between distinct weights vanish.