Documentation

TauCeti.Algebra.AlgebraicGroup.Dynamic.Points

Polynomial and Laurent-valued points of a bialgebra #

For an R-bialgebra H, write M(A) = WithConv (H →ₐ[R] A) for its convolution-points monoid over a commutative R-algebra A. If H is commutative, this is the functor of points of the affine monoid scheme M = Spec H.

The structure maps of the affine line and the punctured affine line induce constant-point inclusions, the injective map M(A[X]) → M(A[T;T⁻¹]), and evaluation at the origin. These maps are natural in A. A bialgebra morphism l : H →ₐc[R] R[T;T⁻¹] also induces the map Aˣ → M(A) on multiplicative-group points and its generic value l(T).

These constructions use no antipode. For a commutative Hopf algebra H, M is an affine group scheme and l is a cocharacter. The polynomial and Laurent point maps then provide the extension and evaluation operations used to define dynamic parabolic subgroups and their limits.

Main declarations #

source
noncomputable def BialgHom.oppositeCocharacter {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
H →ₐc[R] LaurentPolynomial R

The opposite cocharacter, obtained by precomposing the group morphism with t ↦ t⁻¹.

Instances For
    source
    @[simp]
    theorem BialgHom.oppositeCocharacter_apply {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (h : H) :
    l.oppositeCocharacter h = LaurentPolynomial.invert (l h)

    On coordinates the opposite cocharacter inverts the Laurent variable.

    source
    @[simp]
    theorem BialgHom.oppositeCocharacter_oppositeCocharacter {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
    l.oppositeCocharacter.oppositeCocharacter = l

    Taking the opposite cocharacter twice recovers the original one.

    source
    noncomputable def BialgHom.powCocharacter {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (n : ℤ) :
    H →ₐc[R] LaurentPolynomial R

    The n-th power t ↦ λ(tⁿ) of a cocharacter λ: its composite with the n-th power map of the multiplicative group.

    Instances For
      source
      @[simp]
      theorem BialgHom.powCocharacter_apply {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (n : ℤ) (h : H) :
      (l.powCocharacter n) h = AddMonoidAlgebra.mapDomain (fun (x : ℤ) => x * n) (l h)

      On coordinates the n-th power of a cocharacter substitutes Tⁿ for the Laurent variable.

      source
      @[simp]
      theorem BialgHom.powCocharacter_one {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
      l.powCocharacter 1 = l

      The first power of a cocharacter is the cocharacter itself.

      source
      @[simp]
      theorem BialgHom.powCocharacter_powCocharacter {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (m n : ℤ) :
      (l.powCocharacter m).powCocharacter n = l.powCocharacter (m * n)

      Powers of a cocharacter compose by multiplying the exponents: (λᵐ)ⁿ = λ^{mn}.

      source
      @[simp]
      theorem BialgHom.powCocharacter_neg_one {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
      l.powCocharacter (-1) = l.oppositeCocharacter

      The power λ⁻¹ of a cocharacter is its opposite cocharacter.

      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] [CommSemiring A] [Algebra R A] [Bialgebra R H] :
      WithConv (H →ₐ[R] A) →* WithConv (H →ₐ[R] LaurentPolynomial A)

      The constant-point inclusion M(A) → M(A[T;T⁻¹]), pullback of points along the structure map A → A[T;T⁻¹].

      Instances For
        source
        noncomputable def TauCeti.Cocharacter.constPolyPoint {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [CommSemiring A] [Algebra R A] [Bialgebra R H] :
        WithConv (H →ₐ[R] A) →* WithConv (H →ₐ[R] Polynomial A)

        The constant-point inclusion M(A) → M(A[X]), pullback of points along A → A[X].

        Instances For
          source
          noncomputable def TauCeti.Cocharacter.ofPolyPoint {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [CommSemiring A] [Algebra R A] [Bialgebra R H] :
          WithConv (H →ₐ[R] Polynomial A) →* WithConv (H →ₐ[R] LaurentPolynomial A)

          The inclusion M(A[X]) → M(A[T;T⁻¹]) of points over the affine line into points over the punctured affine line, pullback along Polynomial.toLaurent.

          Instances For
            source
            noncomputable def TauCeti.Cocharacter.evalZeroPoint {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [CommSemiring A] [Algebra R A] [Bialgebra R H] :
            WithConv (H →ₐ[R] Polynomial A) →* WithConv (H →ₐ[R] A)

            Evaluation at the origin, M(A[X]) → M(A).

            Instances For
              source
              theorem TauCeti.Cocharacter.constPoint_apply {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [CommSemiring A] [Algebra R A] [Bialgebra R H] (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.constPoint_mapValue_ofId {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [CommSemiring A] [Algebra R A] [Bialgebra R H] (g : WithConv (H →ₐ[R] R)) :
              (constPoint A) ((Algebra.ofId R A).mapValue g) = (Algebra.ofId R (LaurentPolynomial A)).mapValue g

              On a rational point, the constant-point inclusion agrees with pullback along the structure map R → 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] [CommSemiring A] [Algebra R A] [Bialgebra R H] (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] [CommSemiring A] [Algebra R A] [Bialgebra R H] (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] [CommSemiring A] [Algebra R A] [Bialgebra R H] (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] [CommSemiring A] [Algebra R A] [Bialgebra R H] :
              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] [CommSemiring A] [Algebra R A] [Bialgebra R H] (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] [CommSemiring A] [Algebra R A] [Bialgebra R H] (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.

              Multiplicative-group morphisms on points #

              source
              noncomputable def TauCeti.Cocharacter.pointsHom {R : Type u_1} {H : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring H] [CommSemiring A] [Algebra R A] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
              Aˣ →* WithConv (H →ₐ[R] A)

              The map 𝔾ₘ(A) = Aˣ → M(A) induced by a multiplicative-group morphism into the convolution-points monoid, presented contravariantly as a bialgebra homomorphism H →ₐc[R] R[T;T⁻¹]. For commutative H, this is the map on points of the monoid-scheme morphism 𝔾ₘ → Spec H.

              Instances For
                source
                theorem TauCeti.Cocharacter.pointsHom_apply {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [CommSemiring A] [Algebra R A] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (u : Aˣ) :
                (pointsHom A l) u = l.mapDomain (WithConv.toConv (laurentEval u))

                A multiplicative-group morphism sends a unit to the 𝔾ₘ-point precomposed with l.

                source
                @[simp]
                theorem TauCeti.Cocharacter.pointsHom_oppositeCocharacter {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [CommSemiring A] [Algebra R A] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (u : Aˣ) :
                (pointsHom A l.oppositeCocharacter) u = (pointsHom A l) u⁻¹

                The opposite cocharacter evaluates at the inverse unit.

                source
                @[simp]
                theorem BialgHom.pointsHom_powCocharacter {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [CommSemiring A] [Algebra R A] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (n : ℤ) (u : Aˣ) :
                (TauCeti.Cocharacter.pointsHom A (l.powCocharacter n)) u = (TauCeti.Cocharacter.pointsHom A l) (u ^ n)

                The n-th power of a cocharacter evaluates at the n-th power of a unit.

                source
                theorem TauCeti.Cocharacter.pointsHom_commute {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [CommSemiring A] [Algebra R A] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) (u v : Aˣ) :
                Commute ((pointsHom A l) u) ((pointsHom A l) v)

                Images of multiplicative-group points commute: 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] [CommSemiring A] [Algebra R A] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
                WithConv (H →ₐ[R] LaurentPolynomial A)

                The point l(T) with values in A[T;T⁻¹], obtained by evaluating the multiplicative-group morphism l at the tautological unit T. For commutative H, it is a point of the affine monoid scheme Spec H.

                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] [CommSemiring A] [Algebra R A] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
                  genericPoint A l = (pointsHom (LaurentPolynomial A) l) (LaurentPolynomial.genericUnit A)

                  The generic point is the image of the generic unit T.

                  source
                  theorem TauCeti.Cocharacter.genericPoint_ofConv {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [CommSemiring A] [Algebra R A] [Bialgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
                  (genericPoint A l).ofConv = (AddMonoidAlgebra.mapAlgHom ℤ (Algebra.ofId R A)).comp ↑l

                  The generic cocharacter point is its coordinate map with coefficients extended to the value algebra.

                  Naturality in the value algebra #

                  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] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [Bialgebra R H] (φ : A →ₐ[R] B) (l : H →ₐc[R] LaurentPolynomial R) (u : Aˣ) :
                  φ.mapValue ((pointsHom A l) u) = (pointsHom B l) ((Units.map ↑φ.toRingHom) u)

                  The map from multiplicative-group points is natural in the value algebra.

                  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] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [Bialgebra R H] (φ : A →ₐ[R] B) (g : WithConv (H →ₐ[R] A)) :
                  (AddMonoidAlgebra.mapAlgHom ℤ φ).mapValue ((constPoint A) g) = (constPoint B) (φ.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] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [Bialgebra R H] (φ : A →ₐ[R] B) (l : H →ₐc[R] LaurentPolynomial R) :
                  (AddMonoidAlgebra.mapAlgHom ℤ φ).mapValue (genericPoint A l) = genericPoint B l

                  The image of the generic multiplicative-group point is natural 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] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [Bialgebra R H] (φ : A →ₐ[R] B) (F : WithConv (H →ₐ[R] Polynomial A)) :
                  (AddMonoidAlgebra.mapAlgHom ℤ φ).mapValue ((ofPolyPoint A) F) = (ofPolyPoint B) ((Polynomial.mapAlgHom φ).mapValue 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] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [Bialgebra R H] (φ : A →ₐ[R] B) (F : WithConv (H →ₐ[R] Polynomial A)) :
                  φ.mapValue ((evalZeroPoint A) F) = (evalZeroPoint B) ((Polynomial.mapAlgHom φ).mapValue F)

                  Evaluation at the origin is natural in the value algebra.

                  source
                  @[simp]
                  theorem TauCeti.Cocharacter.genericPoint_oppositeCocharacter {R : Type u_1} {H : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring H] [CommSemiring A] [Algebra R A] [HopfAlgebra R H] (l : H →ₐc[R] LaurentPolynomial R) :
                  genericPoint A l.oppositeCocharacter = (genericPoint A l)⁻¹

                  The generic value of the opposite cocharacter is the inverse generic value.

                  source
                  theorem BialgHom.mapDomain_ofPolyPoint {R : Type u_1} {H : Type u_2} {K : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring H] [Semiring K] [Bialgebra R H] [Bialgebra R K] [CommSemiring A] [Algebra R A] (φ : H →ₐc[R] K) (F : WithConv (K →ₐ[R] Polynomial A)) :
                  φ.mapDomain ((TauCeti.Cocharacter.ofPolyPoint A) F) = (TauCeti.Cocharacter.ofPolyPoint A) (φ.mapDomain F)

                  Inclusion of polynomial-valued points commutes with a group homomorphism.

                  source
                  theorem BialgHom.mapDomain_evalZeroPoint {R : Type u_1} {H : Type u_2} {K : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring H] [Semiring K] [Bialgebra R H] [Bialgebra R K] [CommSemiring A] [Algebra R A] (φ : H →ₐc[R] K) (F : WithConv (K →ₐ[R] Polynomial A)) :
                  φ.mapDomain ((TauCeti.Cocharacter.evalZeroPoint A) F) = (TauCeti.Cocharacter.evalZeroPoint A) (φ.mapDomain F)

                  Evaluation at the origin commutes with a group homomorphism.