Documentation

TauCeti.Algebra.AlgebraicGroup.Dynamic.Parabolic

The dynamic parabolic, unipotent and Levi subgroups of a cocharacter #

Let H be a Hopf algebra over R, so that Spec H is an affine group scheme G, and let l : H โ†’โ‚c[R] R[T;Tโปยน] be a cocharacter, that is, a homomorphism of group schemes ๐”พโ‚˜ โ†’ G written contravariantly on coordinate rings. The dynamic method attaches to l three subgroups of the convolution group G(A) = H โ†’โ‚[R] A of A-points, for every commutative R-algebra A, using only limits of one-parameter conjugation and no root data:

Everything is phrased on the functor of points, which is where these conditions are honest: the conjugate of g by the generic point l(T) is a point of G with values in the Laurent polynomial ring A[T;Tโปยน], and g lies in P(l)(A) exactly when that conjugate lies in the image of the points with values in A[X]. Since A[X] โ†’ A[T;Tโปยน] is injective the extension is unique, so extending and then evaluating at X = 0 is a group homomorphism limit : P(l)(A) โ†’ G(A), whose kernel is U(l)(A).

The main theorem is the Levi decomposition on points: limit takes values in Z(l)(A) and restricts to the identity there, so it is a retraction of P(l)(A) onto Z(l)(A). Consequently U(l)(A) and Z(l)(A) generate P(l)(A), meet trivially, and the resulting factorization is unique; U(l)(A) is moreover normalized by P(l)(A). That limit g is centralized by l is the generic identity l(T) ยท F(X) ยท l(T)โปยน = F(T ยท X) over A[X][T;Tโปยน], proved by comparing two substitutions inside A[T;Tโปยน][T';T'โปยน], where the cocycle relation l(T ยท T') = l(T) ยท l(T') is available; specializing that identity at X = 0 gives the statement.

All three subgroups are preserved by change of value algebra, so they are subgroup functors of the functor of points, and limit is natural. Representability of these subfunctors by closed subschemes is not addressed here. For a commutative affine group the whole construction degenerates: P(l) and Z(l) are everything and U(l) is trivial.

Main declarations #

References #

This is the "dynamic" route to parabolic, Levi and unipotent subgroups asked for in Layer 7, "Structure theory", of the ReductiveGroups roadmap, which keeps it as a parallel route that avoids full root data.

Auxiliary lemmas #

Points over the line and the punctured line #

source
noncomputable def TauCeti.Cocharacter.constPoint {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] :
WithConv (H โ†’โ‚[R] A) โ†’* WithConv (H โ†’โ‚[R] LaurentPolynomial A)

The constant-point inclusion G(A) โ†’ G(A[T;Tโปยน]), pullback of points along the structure map A โ†’ A[T;Tโปยน].

Equations
Instances For
    source
    noncomputable def TauCeti.Cocharacter.constPolyPoint {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] :
    WithConv (H โ†’โ‚[R] A) โ†’* WithConv (H โ†’โ‚[R] Polynomial A)

    The constant-point inclusion G(A) โ†’ G(A[X]), pullback of points along A โ†’ A[X].

    Equations
    Instances For
      source
      noncomputable def TauCeti.Cocharacter.ofPolyPoint {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] :
      WithConv (H โ†’โ‚[R] Polynomial A) โ†’* WithConv (H โ†’โ‚[R] LaurentPolynomial A)

      The inclusion G(A[X]) โ†’ G(A[T;Tโปยน]) of points over the affine line into points over the punctured affine line, pullback along Polynomial.toLaurent.

      Equations
      Instances For
        source
        noncomputable def TauCeti.Cocharacter.evalZeroPoint {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] :
        WithConv (H โ†’โ‚[R] Polynomial A) โ†’* WithConv (H โ†’โ‚[R] A)

        Evaluation at the origin, G(A[X]) โ†’ G(A).

        Equations
        Instances For
          source
          theorem TauCeti.Cocharacter.constPoint_apply {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (g : WithConv (H โ†’โ‚[R] A)) :
          (constPoint A) g = WithConv.toConv ((IsScalarTower.toAlgHom R A (LaurentPolynomial A)).comp g.ofConv)

          The constant-point inclusion post-composes a point with the structure map A โ†’ A[T;Tโปยน].

          source
          theorem TauCeti.Cocharacter.constPolyPoint_apply {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (g : WithConv (H โ†’โ‚[R] A)) :
          (constPolyPoint A) g = WithConv.toConv ((IsScalarTower.toAlgHom R A (Polynomial A)).comp g.ofConv)

          The constant-point inclusion post-composes a point with the structure map A โ†’ A[X].

          source
          theorem TauCeti.Cocharacter.ofPolyPoint_apply {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (F : WithConv (H โ†’โ‚[R] Polynomial A)) :
          (ofPolyPoint A) F = WithConv.toConv ((AlgHom.restrictScalars R Polynomial.toLaurentAlg).comp F.ofConv)

          The inclusion of points over the affine line post-composes with Polynomial.toLaurent.

          source
          theorem TauCeti.Cocharacter.evalZeroPoint_apply {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (F : WithConv (H โ†’โ‚[R] Polynomial A)) :
          (evalZeroPoint A) F = WithConv.toConv ((AlgHom.restrictScalars R (Polynomial.aeval 0)).comp F.ofConv)

          Evaluation at the origin post-composes a point over A[X] with X โ†ฆ 0.

          source
          theorem TauCeti.Cocharacter.ofPolyPoint_injective {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] :
          Function.Injective โ‡‘(ofPolyPoint A)

          A point over A[X] is determined by the point over A[T;Tโปยน] that it induces.

          source
          @[simp]
          theorem TauCeti.Cocharacter.ofPolyPoint_constPolyPoint {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (g : WithConv (H โ†’โ‚[R] A)) :
          (ofPolyPoint A) ((constPolyPoint A) g) = (constPoint A) g

          A constant point over A[X] induces the constant point over A[T;Tโปยน].

          source
          @[simp]
          theorem TauCeti.Cocharacter.evalZeroPoint_constPolyPoint {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (g : WithConv (H โ†’โ‚[R] A)) :
          (evalZeroPoint A) ((constPolyPoint A) g) = g

          A constant point over A[X] evaluates at the origin to the point it came from.

          The generic point of a cocharacter and conjugation by it #

          source
          noncomputable def TauCeti.Cocharacter.pointsHom {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H โ†’โ‚c[R] LaurentPolynomial R) :
          Aหฃ โ†’* WithConv (H โ†’โ‚[R] A)

          A cocharacter on points: the group homomorphism ๐”พโ‚˜(A) = Aหฃ โ†’ G(A) obtained from a cocharacter l : ๐”พโ‚˜ โ†’ G, presented contravariantly as a bialgebra homomorphism H โ†’โ‚c[R] R[T;Tโปยน].

          Equations
          Instances For
            source
            theorem TauCeti.Cocharacter.pointsHom_apply {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H โ†’โ‚c[R] LaurentPolynomial R) (u : Aหฃ) :
            (pointsHom A l) u = (AlgHom.mapDomain l) (WithConv.toConv (MultiplicativeGroup.point u))

            A cocharacter sends a unit to the corresponding ๐”พโ‚˜-point precomposed with l.

            source
            theorem TauCeti.Cocharacter.pointsHom_commute {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H โ†’โ‚c[R] LaurentPolynomial R) (u v : Aหฃ) :
            Commute ((pointsHom A l) u) ((pointsHom A l) v)

            Values of a cocharacter commute with one another: they lie in the image of the commutative group ๐”พโ‚˜(A).

            source
            noncomputable def TauCeti.Cocharacter.genericPoint {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H โ†’โ‚c[R] LaurentPolynomial R) :
            WithConv (H โ†’โ‚[R] LaurentPolynomial A)

            The point l(T) of the affine group Spec H with values in A[T;Tโปยน]: the cocharacter l evaluated at the tautological point T of the multiplicative group.

            Equations
            Instances For
              source
              theorem TauCeti.Cocharacter.genericPoint_eq_pointsHom {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H โ†’โ‚c[R] LaurentPolynomial R) :
              genericPoint A l = (pointsHom (LaurentPolynomial A) l) (MultiplicativeGroup.genericUnit A)

              The generic point is the value of the cocharacter at the generic unit T.

              source
              noncomputable def TauCeti.Cocharacter.conjugate {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H โ†’โ‚c[R] LaurentPolynomial R) :
              WithConv (H โ†’โ‚[R] A) โ†’* WithConv (H โ†’โ‚[R] LaurentPolynomial A)

              Conjugation by the generic point of a cocharacter: the group homomorphism G(A) โ†’ G(A[T;Tโปยน]) sending an A-point g to l(T) ยท g ยท l(T)โปยน.

              Equations
              Instances For
                source
                @[simp]
                theorem TauCeti.Cocharacter.conjugate_apply {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H โ†’โ‚c[R] LaurentPolynomial R) (g : WithConv (H โ†’โ‚[R] A)) :
                (conjugate A l) g = genericPoint A l * (constPoint A) g * (genericPoint A l)โปยน

                Conjugation by the generic point acts as g โ†ฆ l(T) ยท g ยท l(T)โปยน.

                Naturality in the value algebra #

                source
                theorem TauCeti.Cocharacter.mapValue_mapDomain {R : Type u_1} {H : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] (ฯ† : A โ†’โ‚[R] B) (l : H โ†’โ‚c[R] LaurentPolynomial R) (x : WithConv (LaurentPolynomial R โ†’โ‚[R] A)) :
                (AlgHom.mapValue ฯ†) ((AlgHom.mapDomain l) x) = (AlgHom.mapDomain l) ((AlgHom.mapValue ฯ†) x)

                Change of value algebra commutes with change of source Hopf algebra on points.

                source
                theorem TauCeti.Cocharacter.mapValue_pointsHom {R : Type u_1} {H : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] (ฯ† : A โ†’โ‚[R] B) (l : H โ†’โ‚c[R] LaurentPolynomial R) (u : Aหฃ) :
                (AlgHom.mapValue ฯ†) ((pointsHom A l) u) = (pointsHom B l) ((Units.map โ†‘ฯ†.toRingHom) u)

                A cocharacter, read on points, is natural in the value algebra.

                source
                theorem TauCeti.Cocharacter.map_genericUnit {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] (ฯ† : A โ†’โ‚[R] B) :
                (Units.map โ†‘(AddMonoidAlgebra.mapAlgHom โ„ค ฯ†).toRingHom) (MultiplicativeGroup.genericUnit A) = MultiplicativeGroup.genericUnit B

                The induced map on Laurent coefficient algebras fixes the Laurent variable.

                source
                theorem TauCeti.Cocharacter.mapValue_constPoint {R : Type u_1} {H : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] (ฯ† : A โ†’โ‚[R] B) (g : WithConv (H โ†’โ‚[R] A)) :
                (AlgHom.mapValue (AddMonoidAlgebra.mapAlgHom โ„ค ฯ†)) ((constPoint A) g) = (constPoint B) ((AlgHom.mapValue ฯ†) g)

                The constant-point inclusion is natural in the value algebra.

                source
                theorem TauCeti.Cocharacter.mapValue_genericPoint {R : Type u_1} {H : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] (ฯ† : A โ†’โ‚[R] B) (l : H โ†’โ‚c[R] LaurentPolynomial R) :
                (AlgHom.mapValue (AddMonoidAlgebra.mapAlgHom โ„ค ฯ†)) (genericPoint A l) = genericPoint B l

                The generic point of a cocharacter is natural in the value algebra.

                source
                theorem TauCeti.Cocharacter.mapValue_conjugate {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H โ†’โ‚c[R] LaurentPolynomial R) {C : Type u_5} [CommSemiring C] [Algebra R C] (ฯˆ : LaurentPolynomial A โ†’โ‚[R] C) (g : WithConv (H โ†’โ‚[R] A)) :
                (AlgHom.mapValue ฯˆ) ((conjugate A l) g) = (pointsHom C l) ((Units.map โ†‘ฯˆ.toRingHom) (MultiplicativeGroup.genericUnit A)) * (AlgHom.mapValue (ฯˆ.comp (IsScalarTower.toAlgHom R A (LaurentPolynomial A)))) g * ((pointsHom C l) ((Units.map โ†‘ฯˆ.toRingHom) (MultiplicativeGroup.genericUnit A)))โปยน

                Conjugation by the generic point, pushed forward along an arbitrary homomorphism ฯˆ out of A[T;Tโปยน]: it becomes conjugation by the value of the cocharacter at the image of T.

                source
                theorem TauCeti.Cocharacter.mapValue_conjugate_mapAlgHom {R : Type u_1} {H : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] (ฯ† : A โ†’โ‚[R] B) (l : H โ†’โ‚c[R] LaurentPolynomial R) (g : WithConv (H โ†’โ‚[R] A)) :
                (AlgHom.mapValue (AddMonoidAlgebra.mapAlgHom โ„ค ฯ†)) ((conjugate A l) g) = (conjugate B l) ((AlgHom.mapValue ฯ†) g)

                Conjugation by the generic point is natural in the value algebra.

                The dynamic parabolic and its limit homomorphism #

                source
                noncomputable def TauCeti.Cocharacter.parabolic {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H โ†’โ‚c[R] LaurentPolynomial R) :
                Subgroup (WithConv (H โ†’โ‚[R] A))

                The dynamic parabolic subgroup P(l)(A): the A-points g of the affine group such that the conjugate l(T) ยท g ยท l(T)โปยน extends over the origin, that is, lies in the image of the A[X]-points. Geometrically, these are the points for which lim_{t โ†’ 0} l(t) g l(t)โปยน exists.

                Equations
                Instances For
                  source
                  theorem TauCeti.Cocharacter.mem_parabolic_iff {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} {g : WithConv (H โ†’โ‚[R] A)} :
                  g โˆˆ parabolic A l โ†” โˆƒ (F : WithConv (H โ†’โ‚[R] Polynomial A)), (ofPolyPoint A) F = (conjugate A l) g

                  Membership in the dynamic parabolic is the existence of an extension over the origin.

                  source
                  theorem TauCeti.Cocharacter.mem_parabolic_of_eq {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} {g : WithConv (H โ†’โ‚[R] A)} {F : WithConv (H โ†’โ‚[R] Polynomial A)} (hF : (ofPolyPoint A) F = (conjugate A l) g) :
                  g โˆˆ parabolic A l

                  An extension over the origin exhibits membership in the dynamic parabolic.

                  source
                  noncomputable def TauCeti.Cocharacter.extend {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H โ†’โ‚c[R] LaurentPolynomial R) :
                  โ†ฅ(parabolic A l) โ†’* WithConv (H โ†’โ‚[R] Polynomial A)

                  The unique A[X]-point extending the conjugate of a point of the dynamic parabolic.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem TauCeti.Cocharacter.ofPolyPoint_extend {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} (g : โ†ฅ(parabolic A l)) :
                    (ofPolyPoint A) ((extend A l) g) = (conjugate A l) โ†‘g

                    The chosen extension does induce the conjugate it extends.

                    source
                    theorem TauCeti.Cocharacter.extend_unique {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} {g : โ†ฅ(parabolic A l)} {F : WithConv (H โ†’โ‚[R] Polynomial A)} (hF : (ofPolyPoint A) F = (conjugate A l) โ†‘g) :
                    (extend A l) g = F

                    The extension over the origin is unique.

                    source
                    noncomputable def TauCeti.Cocharacter.limit {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H โ†’โ‚c[R] LaurentPolynomial R) :
                    โ†ฅ(parabolic A l) โ†’* WithConv (H โ†’โ‚[R] A)

                    The limit homomorphism P(l)(A) โ†’ G(A), g โ†ฆ lim_{t โ†’ 0} l(t) g l(t)โปยน. It is a group homomorphism because it is the composite of two group homomorphisms: extension over the origin and evaluation there.

                    Equations
                    Instances For
                      source
                      theorem TauCeti.Cocharacter.limit_apply {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} (g : โ†ฅ(parabolic A l)) :
                      (limit A l) g = (evalZeroPoint A) ((extend A l) g)

                      The limit is the extension over the origin, evaluated there.

                      The Levi and unipotent parts #

                      source
                      noncomputable def TauCeti.Cocharacter.levi {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H โ†’โ‚c[R] LaurentPolynomial R) :
                      Subgroup (WithConv (H โ†’โ‚[R] A))

                      The dynamic Levi subgroup Z(l)(A): the A-points centralized by the cocharacter, that is, those fixed by conjugation by the generic point l(T).

                      Equations
                      Instances For
                        source
                        theorem TauCeti.Cocharacter.mem_levi_iff {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} {g : WithConv (H โ†’โ‚[R] A)} :
                        g โˆˆ levi A l โ†” (conjugate A l) g = (constPoint A) g

                        Membership in the Levi subgroup means being fixed by conjugation by l(T).

                        source
                        theorem TauCeti.Cocharacter.levi_le_parabolic {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} :
                        levi A l โ‰ค parabolic A l

                        The Levi subgroup is contained in the dynamic parabolic: a fixed point extends by a constant.

                        source
                        theorem TauCeti.Cocharacter.extend_of_mem_levi {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} {g : WithConv (H โ†’โ‚[R] A)} (hg : g โˆˆ levi A l) :
                        (extend A l) โŸจg, โ‹ฏโŸฉ = (constPolyPoint A) g

                        The extension of a point of the Levi subgroup is the constant point.

                        source
                        theorem TauCeti.Cocharacter.limit_of_mem_levi {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} {g : WithConv (H โ†’โ‚[R] A)} (hg : g โˆˆ levi A l) :
                        (limit A l) โŸจg, โ‹ฏโŸฉ = g

                        The limit homomorphism restricts to the identity on the Levi subgroup: it is a retraction of the dynamic parabolic onto its Levi part.

                        source
                        noncomputable def TauCeti.Cocharacter.unipotent {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] (l : H โ†’โ‚c[R] LaurentPolynomial R) :
                        Subgroup (WithConv (H โ†’โ‚[R] A))

                        The dynamic unipotent subgroup U(l)(A): the points of the dynamic parabolic whose limit is the identity. It is the kernel of the limit homomorphism, hence normal in P(l)(A).

                        Equations
                        Instances For
                          source
                          theorem TauCeti.Cocharacter.mem_unipotent_iff {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} {g : WithConv (H โ†’โ‚[R] A)} :
                          g โˆˆ unipotent A l โ†” โˆƒ (hg : g โˆˆ parabolic A l), (limit A l) โŸจg, hgโŸฉ = 1

                          Membership in the dynamic unipotent subgroup means lying in the parabolic with trivial limit.

                          source
                          theorem TauCeti.Cocharacter.unipotent_le_parabolic {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} :
                          unipotent A l โ‰ค parabolic A l

                          The dynamic unipotent subgroup is contained in the dynamic parabolic.

                          source
                          theorem TauCeti.Cocharacter.unipotent_inf_levi {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} :
                          unipotent A l โŠ“ levi A l = โŠฅ

                          The dynamic unipotent subgroup meets the Levi subgroup trivially.

                          Cocharacter values, and the commutative case #

                          source
                          theorem TauCeti.Cocharacter.pointsHom_mem_levi {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} (u : Aหฃ) :
                          (pointsHom A l) u โˆˆ levi A l

                          The values of the cocharacter lie in its own Levi subgroup. They commute with the generic point because the multiplicative group is commutative.

                          source
                          theorem TauCeti.Cocharacter.levi_eq_top {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} [Coalgebra.IsCocomm R H] :
                          levi A l = โŠค

                          For a commutative affine group every point is fixed by conjugation, so the dynamic Levi subgroup attached to any cocharacter is everything.

                          source
                          theorem TauCeti.Cocharacter.parabolic_eq_top {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} [Coalgebra.IsCocomm R H] :
                          parabolic A l = โŠค

                          For a commutative affine group the dynamic parabolic attached to any cocharacter is everything.

                          source
                          theorem TauCeti.Cocharacter.unipotent_eq_bot {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} [Coalgebra.IsCocomm R H] :
                          unipotent A l = โŠฅ

                          For a commutative affine group the dynamic unipotent subgroup attached to any cocharacter is trivial.

                          Functoriality of the dynamic subgroups in the value algebra #

                          source
                          theorem TauCeti.Cocharacter.mapValue_ofPolyPoint {R : Type u_1} {H : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] (ฯ† : A โ†’โ‚[R] B) (F : WithConv (H โ†’โ‚[R] Polynomial A)) :
                          (AlgHom.mapValue (AddMonoidAlgebra.mapAlgHom โ„ค ฯ†)) ((ofPolyPoint A) F) = (ofPolyPoint B) ((AlgHom.mapValue (Polynomial.mapAlgHom ฯ†)) F)

                          The inclusion of points over the affine line is natural in the value algebra.

                          source
                          theorem TauCeti.Cocharacter.mapValue_evalZeroPoint {R : Type u_1} {H : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] (ฯ† : A โ†’โ‚[R] B) (F : WithConv (H โ†’โ‚[R] Polynomial A)) :
                          (AlgHom.mapValue ฯ†) ((evalZeroPoint A) F) = (evalZeroPoint B) ((AlgHom.mapValue (Polynomial.mapAlgHom ฯ†)) F)

                          Evaluation at the origin is natural in the value algebra.

                          source
                          theorem TauCeti.Cocharacter.parabolic_le_comap {R : Type u_1} {H : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] {l : H โ†’โ‚c[R] LaurentPolynomial R} (ฯ† : A โ†’โ‚[R] B) :
                          parabolic A l โ‰ค Subgroup.comap (AlgHom.mapValue ฯ†) (parabolic B l)

                          The dynamic parabolic is a subgroup functor: it is preserved by change of value algebra.

                          source
                          theorem TauCeti.Cocharacter.levi_le_comap {R : Type u_1} {H : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] {l : H โ†’โ‚c[R] LaurentPolynomial R} (ฯ† : A โ†’โ‚[R] B) :
                          levi A l โ‰ค Subgroup.comap (AlgHom.mapValue ฯ†) (levi B l)

                          The Levi subgroup is preserved by change of value algebra.

                          source
                          theorem TauCeti.Cocharacter.extend_mapValue {R : Type u_1} {H : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] {l : H โ†’โ‚c[R] LaurentPolynomial R} (ฯ† : A โ†’โ‚[R] B) (g : โ†ฅ(parabolic A l)) :
                          (extend B l) โŸจ(AlgHom.mapValue ฯ†) โ†‘g, โ‹ฏโŸฉ = (AlgHom.mapValue (Polynomial.mapAlgHom ฯ†)) ((extend A l) g)

                          The extension over the origin is natural in the value algebra.

                          source
                          theorem TauCeti.Cocharacter.mapValue_limit {R : Type u_1} {H : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] {l : H โ†’โ‚c[R] LaurentPolynomial R} (ฯ† : A โ†’โ‚[R] B) (g : โ†ฅ(parabolic A l)) :
                          (AlgHom.mapValue ฯ†) ((limit A l) g) = (limit B l) โŸจ(AlgHom.mapValue ฯ†) โ†‘g, โ‹ฏโŸฉ

                          The limit homomorphism is natural in the value algebra.

                          source
                          theorem TauCeti.Cocharacter.unipotent_le_comap {R : Type u_1} {H : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] {l : H โ†’โ‚c[R] LaurentPolynomial R} (ฯ† : A โ†’โ‚[R] B) :
                          unipotent A l โ‰ค Subgroup.comap (AlgHom.mapValue ฯ†) (unipotent B l)

                          The unipotent subgroup is preserved by change of value algebra.

                          The limit lies in the Levi subgroup #

                          source
                          theorem TauCeti.Cocharacter.limit_mem_levi {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} (g : โ†ฅ(parabolic A l)) :
                          (limit A l) g โˆˆ levi A l

                          The limit of a point of the dynamic parabolic lies in the Levi subgroup. Together with limit_of_mem_levi this exhibits the limit homomorphism as a retraction of the dynamic parabolic onto its Levi subgroup.

                          The Levi decomposition of the dynamic parabolic #

                          source
                          theorem TauCeti.Cocharacter.mul_limit_inv_mem_unipotent {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} {g : WithConv (H โ†’โ‚[R] A)} (hg : g โˆˆ parabolic A l) :
                          g * ((limit A l) โŸจg, hgโŸฉ)โปยน โˆˆ unipotent A l

                          Dividing a point of the dynamic parabolic by its limit lands in the unipotent part.

                          source
                          theorem TauCeti.Cocharacter.exists_mem_unipotent_mem_levi {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} {g : WithConv (H โ†’โ‚[R] A)} (hg : g โˆˆ parabolic A l) :
                          โˆƒ u โˆˆ unipotent A l, โˆƒ z โˆˆ levi A l, g = u * z

                          The dynamic Levi decomposition, on points: every point of the dynamic parabolic is a point of its unipotent part times a point of its Levi part.

                          source
                          theorem TauCeti.Cocharacter.unipotent_sup_levi {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} :
                          unipotent A l โŠ” levi A l = parabolic A l

                          The unipotent part and the Levi part generate the dynamic parabolic.

                          source
                          theorem TauCeti.Cocharacter.conj_mem_unipotent {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} {p u : WithConv (H โ†’โ‚[R] A)} (hp : p โˆˆ parabolic A l) (hu : u โˆˆ unipotent A l) :
                          p * u * pโปยน โˆˆ unipotent A l

                          The dynamic unipotent subgroup is normalized by the dynamic parabolic: it is the kernel of a homomorphism defined on the parabolic.

                          source
                          theorem TauCeti.Cocharacter.eq_of_unipotent_mul_levi_eq {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [CommSemiring A] [Algebra R A] {l : H โ†’โ‚c[R] LaurentPolynomial R} {uโ‚ uโ‚‚ zโ‚ zโ‚‚ : WithConv (H โ†’โ‚[R] A)} (huโ‚ : uโ‚ โˆˆ unipotent A l) (huโ‚‚ : uโ‚‚ โˆˆ unipotent A l) (hzโ‚ : zโ‚ โˆˆ levi A l) (hzโ‚‚ : zโ‚‚ โˆˆ levi A l) (h : uโ‚ * zโ‚ = uโ‚‚ * zโ‚‚) :
                          uโ‚ = uโ‚‚ โˆง zโ‚ = zโ‚‚

                          The Levi decomposition of a point of the dynamic parabolic is unique.