Documentation

TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Dynamic.Weight.Levi.Action

The represented conjugation action in a weight parabolic #

Let P(w), U(w), and L(w) be the represented weight parabolic, unipotent subgroup, and Levi subgroup of GL_N. Normality of U(w) in P(w) supplies a categorical conjugation action of L(w) on U(w). This file transports that action through the coordinate identifications of the two relative quotient subgroups and proves that it is exactly the dynamic conjugation action used in the pointwise Levi decomposition.

Thus the categorical semidirect product constructed from the two closed subgroup schemes has the same multiplication law on algebra-valued points as the dynamic semidirect product.

Main declarations #

References #

This advances the dynamic route to parabolic subgroups and Levi decomposition in Layer 7, "Structure theory", of the ReductiveGroups roadmap. It supplies the action comparison needed to identify the represented categorical semidirect product with the pointwise dynamic one.

source
noncomputable def TauCeti.GeneralLinear.Dynamic.weightLeviInParabolicPointsMulEquiv (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (A : CommAlgCat R) :
↑(HopfAlgebra.points A) ≃* ↥(Cocharacter.levi (↑A) (weightCocharacter w))

Points of the relative Levi quotient inside the weight parabolic are canonically the dynamic Levi points of the weight cocharacter.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def TauCeti.GeneralLinear.Dynamic.weightUnipotentInParabolicPointsMulEquiv (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (A : CommAlgCat R) :
    ↑(HopfAlgebra.points A) ≃* ↥(Cocharacter.unipotent (↑A) (weightCocharacter w))

    Points of the relative unipotent quotient inside the weight parabolic are canonically the dynamic unipotent points of the weight cocharacter.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.GeneralLinear.Dynamic.coe_weightLeviInParabolicPointsMulEquiv_apply (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (A : CommAlgCat R) (z : ↑(HopfAlgebra.points A)) :
      ↑((weightLeviInParabolicPointsMulEquiv R w A) z) = (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (coordinateHopfAlgebra R N) (weightParabolicDefiningHopfIdeal R w) A)) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (weightParabolicCoordinateHopfAlgebra R w) (weightLeviInParabolicHopfIdeal R w) A)) z)

      The relative Levi point equivalence preserves the underlying point of the ambient general linear group.

      source
      @[simp]
      theorem TauCeti.GeneralLinear.Dynamic.coe_weightUnipotentInParabolicPointsMulEquiv_apply (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) :
      ↑((weightUnipotentInParabolicPointsMulEquiv R w A) g) = (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (coordinateHopfAlgebra R N) (weightParabolicDefiningHopfIdeal R w) A)) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (weightParabolicCoordinateHopfAlgebra R w) (weightUnipotentInParabolicHopfIdeal R w) A)) g)

      The relative unipotent point equivalence preserves the underlying point of the ambient general linear group.

      source
      noncomputable def TauCeti.GeneralLinear.Dynamic.representedWeightLeviConjugation (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (A : CommAlgCat R) :
      ↥(Cocharacter.levi (↑A) (weightCocharacter w)) →* MulAut ↥(Cocharacter.unipotent (↑A) (weightCocharacter w))

      The categorical conjugation action of the represented relative Levi subgroup on the represented relative unipotent subgroup, transported to dynamic points.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem TauCeti.GeneralLinear.Dynamic.representedWeightLeviConjugation_apply (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (A : CommAlgCat R) (z : Opposite.op A ⟶ CommHopfAlgCat.grpObj (CommHopfAlgCat.quotient (weightParabolicCoordinateHopfAlgebra R w) (weightLeviInParabolicHopfIdeal R w))) (g : Opposite.op A ⟶ CommHopfAlgCat.grpObj (CommHopfAlgCat.quotient (weightParabolicCoordinateHopfAlgebra R w) (weightUnipotentInParabolicHopfIdeal R w))) :
        ((representedWeightLeviConjugation R w A) ((weightLeviInParabolicPointsMulEquiv R w A) ((CommHopfAlgCat.grpObjPointsMulEquiv (CommHopfAlgCat.quotient (weightParabolicCoordinateHopfAlgebra R w) (weightLeviInParabolicHopfIdeal R w)) (Opposite.op A)) z))) ((weightUnipotentInParabolicPointsMulEquiv R w A) ((CommHopfAlgCat.grpObjPointsMulEquiv (CommHopfAlgCat.quotient (weightParabolicCoordinateHopfAlgebra R w) (weightUnipotentInParabolicHopfIdeal R w)) (Opposite.op A)) g)) = (weightUnipotentInParabolicPointsMulEquiv R w A) ((CommHopfAlgCat.grpObjPointsMulEquiv (CommHopfAlgCat.quotient (weightParabolicCoordinateHopfAlgebra R w) (weightUnipotentInParabolicHopfIdeal R w)) (Opposite.op A)) ((((CommHopfAlgCat.quotientNormalConjugation (weightParabolicCoordinateHopfAlgebra R w) (weightUnipotentInParabolicHopfIdeal R w) (weightLeviInParabolicHopfIdeal R w) ⋯).toMulAutHom (Opposite.op A)) z) g))

        The represented conjugation action on categorical quotient points is conjugation after transporting both quotient-point groups to their dynamic models.

        source
        @[simp]
        theorem TauCeti.GeneralLinear.Dynamic.representedWeightLeviConjugation_eq_dynamic (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (A : CommAlgCat R) :
        representedWeightLeviConjugation R w A = Cocharacter.leviConjugation (↑A) (weightCocharacter w)

        The categorical conjugation action of the represented Levi subgroup is exactly the dynamic Levi conjugation action on every commutative algebra of points.