Documentation

TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Dynamic.Weight.Normal

Weight Levi and unipotent subgroups inside weight parabolics #

For an integer weight w on the standard representation, the weight-unipotent subgroup is a closed normal subgroup of the corresponding weight parabolic. On coordinate rings, the parabolic defining Hopf ideal is contained in the unipotent defining Hopf ideal. Mapping the latter into the parabolic coordinate Hopf algebra therefore cuts out the same unipotent group scheme, now regarded as a closed subgroup of the parabolic.

The weight Levi is likewise a closed subgroup of the weight parabolic. Its relative defining Hopf ideal is the image of the ambient weight-Levi ideal in the parabolic coordinate algebra. The resulting quotient spectrum is canonically the already-defined weight-Levi group scheme, and its inclusion through the parabolic agrees with the direct inclusion into GL_N.

Normality is proved honestly at the scheme level. The functor-of-points criterion for a normal Hopf ideal reduces it to conjugation over every commutative value algebra, where it is precisely the existing dynamic statement that the weight parabolic normalizes its unipotent part.

Main declarations #

References #

This advances the dynamic Levi-decomposition milestone in Layer 7, "Structure theory", of the ReductiveGroups roadmap by supplying both represented factors inside the weight parabolic. The relative Levi is the acting factor required by the scheme-level semidirect-product decomposition.

source
theorem TauCeti.GeneralLinear.Dynamic.weightParabolicDefiningHopfIdeal_le_weightUnipotent (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
weightParabolicDefiningHopfIdeal R w ≤ weightUnipotentDefiningHopfIdeal R w

The defining Hopf ideal of the weight parabolic is contained in that of the weight-unipotent subgroup. Contravariantly, the weight-unipotent group scheme is a closed subgroup of the weight parabolic group scheme.

source
theorem TauCeti.GeneralLinear.Dynamic.weightParabolicDefiningHopfIdeal_le_weightLevi (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
weightParabolicDefiningHopfIdeal R w ≤ weightLeviDefiningHopfIdeal R w

The defining Hopf ideal of the weight parabolic is contained in that of the weight Levi. Contravariantly, the weight-Levi group scheme is a closed subgroup of the weight-parabolic group scheme.

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

The Hopf ideal in the weight-parabolic coordinate algebra which cuts out the weight Levi.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.GeneralLinear.Dynamic.weightLeviInParabolicHopfIdeal_comapOfSurjective (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
    (weightLeviInParabolicHopfIdeal R w).comapOfSurjective (CommHopfAlgCat.Hom.hom (weightParabolicCoordinateMap R w)) ⋯ = weightLeviDefiningHopfIdeal R w

    Pulling the relative weight-Levi Hopf ideal back to the ambient general linear coordinate algebra recovers the original weight-Levi defining ideal.

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

    The Hopf ideal in the weight-parabolic coordinate algebra which cuts out the weight-unipotent subgroup.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.GeneralLinear.Dynamic.weightUnipotentInParabolicHopfIdeal_comapOfSurjective (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
      (weightUnipotentInParabolicHopfIdeal R w).comapOfSurjective (CommHopfAlgCat.Hom.hom (weightParabolicCoordinateMap R w)) ⋯ = weightUnipotentDefiningHopfIdeal R w

      Pulling the relative weight-unipotent Hopf ideal back to the ambient general linear coordinate algebra recovers the original weight-unipotent defining ideal.

      source
      @[simp]
      theorem TauCeti.GeneralLinear.Dynamic.mem_weightLeviInParabolicPointsSubgroup_iff (R : Type u) [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (w : Fin N → ℤ) (f : ↑(HopfAlgebra.points ↧A)) :
      f ∈ CommHopfAlgCat.quotientPointsSubgroup (weightParabolicCoordinateHopfAlgebra R w) (weightLeviInParabolicHopfIdeal R w) ↧A ↔ (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (coordinateHopfAlgebra R N) (weightParabolicDefiningHopfIdeal R w) ↧A)) f ∈ CommHopfAlgCat.quotientPointsSubgroup (coordinateHopfAlgebra R N) (weightLeviDefiningHopfIdeal R w) ↧A

      A parabolic point belongs to the subgroup cut out by the relative Levi Hopf ideal exactly when its ambient general linear point belongs to the weight-Levi subgroup.

      source
      @[simp]
      theorem TauCeti.GeneralLinear.Dynamic.mem_weightUnipotentInParabolicPointsSubgroup_iff (R : Type u) [CommRing R] {N : ℕ} {A : Type v} [CommRing A] [Algebra R A] (w : Fin N → ℤ) (f : ↑(HopfAlgebra.points ↧A)) :
      f ∈ CommHopfAlgCat.quotientPointsSubgroup (weightParabolicCoordinateHopfAlgebra R w) (weightUnipotentInParabolicHopfIdeal R w) ↧A ↔ (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (coordinateHopfAlgebra R N) (weightParabolicDefiningHopfIdeal R w) ↧A)) f ∈ CommHopfAlgCat.quotientPointsSubgroup (coordinateHopfAlgebra R N) (weightUnipotentDefiningHopfIdeal R w) ↧A

      A parabolic point belongs to the subgroup cut out by the relative unipotent Hopf ideal exactly when its ambient general linear point belongs to the weight-unipotent subgroup.

      source
      theorem TauCeti.GeneralLinear.Dynamic.isNormal_weightUnipotentInParabolicHopfIdeal (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
      (weightUnipotentInParabolicHopfIdeal R w).IsNormal

      The relative weight-unipotent Hopf ideal is normal in the weight-parabolic coordinate Hopf algebra. Equivalently, the represented weight-unipotent subgroup is normal in the represented weight parabolic over every commutative value algebra.

      source
      noncomputable def TauCeti.GeneralLinear.Dynamic.weightLeviInParabolicCoordinateIso (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
      weightLeviCoordinateHopfAlgebra R w ≅ CommHopfAlgCat.quotient (weightParabolicCoordinateHopfAlgebra R w) (weightLeviInParabolicHopfIdeal R w)

      The quotient-coordinate isomorphism underlying the identification of the relative weight-Levi quotient spectrum.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.GeneralLinear.Dynamic.mkQuotient_weightLevi_comp_weightLeviInParabolicCoordinateIso_hom (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
        CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (coordinateHopfAlgebra R N) (weightLeviDefiningHopfIdeal R w)) (weightLeviInParabolicCoordinateIso R w).hom = CategoryTheory.CategoryStruct.comp (weightParabolicCoordinateMap R w) (CommHopfAlgCat.mkQuotient (weightParabolicCoordinateHopfAlgebra R w) (weightLeviInParabolicHopfIdeal R w))

        The relative Levi coordinate identification commutes with the two inclusions into the ambient general linear coordinate algebra.

        source
        noncomputable def TauCeti.GeneralLinear.Dynamic.weightLeviInParabolicGroupSchemeIso (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
        CommHopfAlgCat.quotientSpec (weightParabolicCoordinateHopfAlgebra R w) (weightLeviInParabolicHopfIdeal R w) ≅ weightLeviGroupScheme R w

        The relative quotient spectrum cut out inside the weight parabolic is canonically isomorphic to the weight-Levi group scheme.

        Equations
        Instances For
          source
          noncomputable def TauCeti.GeneralLinear.Dynamic.weightLeviToParabolicCoordinateMap (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
          weightParabolicCoordinateHopfAlgebra R w ⟶ weightLeviCoordinateHopfAlgebra R w

          The coordinate morphism representing the inclusion L(w) → P(w). It is the canonical map between the two quotient coordinate Hopf algebras induced by containment of their defining Hopf ideals.

          Equations
          Instances For
            source
            theorem TauCeti.GeneralLinear.Dynamic.weightLeviToParabolicCoordinateMap_def (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
            weightLeviToParabolicCoordinateMap R w = CommHopfAlgCat.quotientMapOfLe (coordinateHopfAlgebra R N) ⋯

            The coordinate map of the weight-Levi inclusion is the quotient map induced by containment of the defining Hopf ideals.

            source
            @[simp]
            theorem TauCeti.GeneralLinear.Dynamic.mapPointsFunctor_weightLeviToParabolicCoordinateMap_app (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (A : CommAlgCat R) (z : ↑(HopfAlgebra.points A)) :
            (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (weightLeviToParabolicCoordinateMap R w)).app A)) z = (CategoryTheory.ConcreteCategory.hom ((weightParabolicPointsIso R w).inv.app A)) ((Cocharacter.leviToParabolic (↑A) (weightCocharacter w)) ((CategoryTheory.ConcreteCategory.hom ((weightLeviPointsIso R w).hom.app A)) z))

            On points over every commutative value algebra, the canonical quotient coordinate map is the dynamic Levi inclusion transported through the representing isomorphisms.

            source
            noncomputable def TauCeti.GeneralLinear.Dynamic.weightLeviToParabolic (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
            weightLeviGroupScheme R w ⟶ weightParabolicGroupScheme R w

            The closed immersion of the weight-Levi group scheme into the weight-parabolic group scheme induced by inclusion of their defining Hopf ideals.

            Equations
            Instances For
              source
              theorem TauCeti.GeneralLinear.Dynamic.weightLeviToParabolic_def (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
              weightLeviToParabolic R w = CommHopfAlgCat.quotientSpecMapOfLe (coordinateHopfAlgebra R N) ⋯

              The weight-Levi inclusion is the quotient-spectrum map induced by containment of the defining Hopf ideals.

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

              The weight-Levi-to-parabolic morphism is a closed immersion.

              source
              @[simp]
              theorem TauCeti.GeneralLinear.Dynamic.weightLeviToParabolic_comp_inclusion (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
              CategoryTheory.CategoryStruct.comp (weightLeviToParabolic R w) (weightParabolicInclusion R w) = weightLeviInclusion R w

              Including the weight-Levi group scheme through the weight parabolic agrees with its direct inclusion into the general linear group scheme.

              source
              @[simp]
              theorem TauCeti.GeneralLinear.Dynamic.weightLeviInParabolicGroupSchemeIso_hom_comp_weightLeviToParabolic (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
              CategoryTheory.CategoryStruct.comp (weightLeviInParabolicGroupSchemeIso R w).hom (weightLeviToParabolic R w) = CommHopfAlgCat.quotientSpecι (weightParabolicCoordinateHopfAlgebra R w) (weightLeviInParabolicHopfIdeal R w)

              Under the canonical identification with the weight-Levi group scheme, the relative quotient-spectrum inclusion is weightLeviToParabolic.

              source
              noncomputable def TauCeti.GeneralLinear.Dynamic.weightUnipotentInParabolicCoordinateIso (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
              weightUnipotentCoordinateHopfAlgebra R w ≅ CommHopfAlgCat.quotient (weightParabolicCoordinateHopfAlgebra R w) (weightUnipotentInParabolicHopfIdeal R w)

              The quotient-coordinate isomorphism underlying the identification of the relative weight-unipotent quotient spectrum.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem TauCeti.GeneralLinear.Dynamic.mkQuotient_weightUnipotent_comp_weightUnipotentInParabolicCoordinateIso_hom (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
                CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (coordinateHopfAlgebra R N) (weightUnipotentDefiningHopfIdeal R w)) (weightUnipotentInParabolicCoordinateIso R w).hom = CategoryTheory.CategoryStruct.comp (weightParabolicCoordinateMap R w) (CommHopfAlgCat.mkQuotient (weightParabolicCoordinateHopfAlgebra R w) (weightUnipotentInParabolicHopfIdeal R w))

                The relative unipotent coordinate identification commutes with the two inclusions into the ambient general linear coordinate algebra.

                source
                noncomputable def TauCeti.GeneralLinear.Dynamic.weightUnipotentInParabolicGroupSchemeIso (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
                CommHopfAlgCat.quotientSpec (weightParabolicCoordinateHopfAlgebra R w) (weightUnipotentInParabolicHopfIdeal R w) ≅ weightUnipotentGroupScheme R w

                The relative quotient spectrum cut out inside the weight parabolic is canonically isomorphic to the weight-unipotent group scheme.

                Equations
                Instances For
                  source
                  noncomputable def TauCeti.GeneralLinear.Dynamic.weightUnipotentToParabolic (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
                  weightUnipotentGroupScheme R w ⟶ weightParabolicGroupScheme R w

                  The closed immersion of the weight-unipotent group scheme into the weight-parabolic group scheme induced by inclusion of their defining Hopf ideals.

                  Equations
                  Instances For
                    source
                    instance TauCeti.GeneralLinear.Dynamic.isClosedImmersion_weightUnipotentToParabolic (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
                    AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (weightUnipotentToParabolic R w).hom.hom)

                    The weight-unipotent-to-parabolic morphism is a closed immersion.

                    source
                    @[simp]
                    theorem TauCeti.GeneralLinear.Dynamic.weightUnipotentToParabolic_comp_inclusion (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
                    CategoryTheory.CategoryStruct.comp (weightUnipotentToParabolic R w) (weightParabolicInclusion R w) = weightUnipotentInclusion R w

                    Including the weight-unipotent group scheme through the weight parabolic agrees with its direct inclusion into the general linear group scheme.

                    source
                    @[simp]
                    theorem TauCeti.GeneralLinear.Dynamic.weightUnipotentInParabolicGroupSchemeIso_hom_comp_weightUnipotentToParabolic (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
                    CategoryTheory.CategoryStruct.comp (weightUnipotentInParabolicGroupSchemeIso R w).hom (weightUnipotentToParabolic R w) = CommHopfAlgCat.quotientSpecι (weightParabolicCoordinateHopfAlgebra R w) (weightUnipotentInParabolicHopfIdeal R w)

                    Under the canonical identification with the weight-unipotent group scheme, the relative quotient-spectrum inclusion is weightUnipotentToParabolic.