Documentation

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

The represented weight-parabolic Levi decomposition #

Let w : Fin N → ℤ. The weight-unipotent subgroup U(w) is normal in the weight parabolic P(w), and the weight Levi subgroup L(w) acts on it by conjugation. The resulting represented semidirect product maps to P(w) by multiplication. This file proves that multiplication is an isomorphism:

U(w) ⋊ L(w) ≅ P(w).

On points over every commutative algebra this is the dynamic Levi decomposition. The proof transports the categorical semidirect-product points to the dynamic subgroups, uses the existing comparison of the two conjugation actions, and then applies the pointwise decomposition.

Main declarations #

References #

This completes the represented dynamic Levi decomposition for general-linear weight parabolics, in the dynamic route to parabolics and Levi decomposition in Layer 7, "Structure theory", of the ReductiveGroups roadmap.

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

The coordinate Hopf algebra of the represented semidirect product U(w) ⋊ L(w).

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

    The coordinate Hopf-algebra morphism dual to multiplication U(w) ⋊ L(w) → P(w).

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

      Points of the represented weight-unipotent-by-Levi semidirect product are canonically equivalent to represented weight-parabolic points. Under this equivalence, a pair (u, z) maps to the product u * z of its two subgroup inclusions.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.GeneralLinear.Dynamic.weightParabolicSemidirectProductPointsMulEquiv_apply (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) :
        (weightParabolicSemidirectProductPointsMulEquiv R w A) g = (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (weightParabolicSemidirectProductCoordinateMap R w)).app A)) g

        The represented weight-parabolic semidirect-product equivalence is induced by the coordinate morphism dual to multiplication.

        source
        instance TauCeti.GeneralLinear.Dynamic.isIso_weightParabolicSemidirectProductCoordinateMap (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
        CategoryTheory.IsIso (weightParabolicSemidirectProductCoordinateMap R w)

        Multiplication from the represented weight-unipotent-by-Levi semidirect product to the weight parabolic is an isomorphism.

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

        Multiplication identifies the coordinate Hopf algebra of the weight parabolic with the coordinate Hopf algebra of its represented unipotent-by-Levi semidirect product.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.GeneralLinear.Dynamic.weightParabolicSemidirectProductCoordinateIso_hom (R : Type u) [CommRing R] {N : ℕ} (w : Fin N → ℤ) :
          (weightParabolicSemidirectProductCoordinateIso R w).hom = weightParabolicSemidirectProductCoordinateMap R w

          The forward morphism of the weight-parabolic coordinate isomorphism is dual to multiplication.

          source
          theorem TauCeti.GeneralLinear.Dynamic.smoothCommHopfAlgProperty_weightParabolicSemidirectProductCoordinateHopfAlgebra {N : ℕ} (R : Type u) [CommRing R] (w : Fin N → ℤ) (hU : smoothCommHopfAlgProperty R (weightUnipotentCoordinateHopfAlgebra R w)) (hL : smoothCommHopfAlgProperty R (weightLeviCoordinateHopfAlgebra R w)) :
          smoothCommHopfAlgProperty R (weightParabolicSemidirectProductCoordinateHopfAlgebra R w)

          Smoothness of the weight-unipotent and weight-Levi factors implies smoothness of their represented semidirect product.

          source
          theorem TauCeti.GeneralLinear.Dynamic.geometricallyConnectedCommHopfAlgProperty_weightParabolicSemidirectProductCoordinateHopfAlgebra {N : ℕ} (k : Type u) [Field k] (w : Fin N → ℤ) (hU : geometricallyConnectedCommHopfAlgProperty k (weightUnipotentCoordinateHopfAlgebra k w)) (hL : geometricallyConnectedCommHopfAlgProperty k (weightLeviCoordinateHopfAlgebra k w)) :
          geometricallyConnectedCommHopfAlgProperty k (weightParabolicSemidirectProductCoordinateHopfAlgebra k w)

          Geometric connectedness of the weight-unipotent and weight-Levi factors implies geometric connectedness of their represented semidirect product.