Documentation

TauCeti.Algebra.Coalgebra.Comodule.PointsAction

The points action of a comodule #

A right comodule V over a bialgebra H makes the A-points of H — those of the corresponding affine monoid scheme, when H is commutative — act on the scalar extension A ⊗[R] V: a point g : H →ₐ[R] A acts by pushing the coaction coefficients through g, A-linearly. The two comodule axioms are exactly the two monoid-action laws: the counit law sends the convolution unit to the identity, and coassociativity sends convolution products to composites. (The upgrade to automorphisms over a Hopf algebra is in TauCeti.Algebra.AlgebraicGroup.Representation.PointsAction, with the group of points.) On the comodule attached to a group-like element x, this action is scalar multiplication by g x.

This is the comodule-to-representation direction of the "representations = comodules" dictionary (ReductiveGroups roadmap, Layer 1): it realizes a comodule as an action of the functor of points on scalar extensions of V.

Main declarations #

References #

source
noncomputable def TauCeti.Comodule.endOfPoint {R : Type u_1} {H : Type u_2} (V : Type u_3) {A : Type u_4} [CommSemiring R] [Semiring H] [Algebra R H] [Coalgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] (g : H →ₐ[R] A) :
TensorProduct R A V →ₗ[A] TensorProduct R A V

The endomorphism of the scalar extension A ⊗[R] V attached to an A-point: push the coaction coefficients through the point. Only the coalgebra structure of H enters; the bialgebra compatibility is needed for the action laws, not the map.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Comodule.endOfPoint_tmul {R : Type u_1} {H : Type u_2} (V : Type u_3) {A : Type u_4} [CommSemiring R] [Semiring H] [Algebra R H] [Coalgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] (g : H →ₐ[R] A) (a : A) (v : V) :
    (endOfPoint V g) (a ⊗ₜ[R] v) = a • (TensorProduct.comm R V A) ((LinearMap.lTensor V g.toLinearMap) (coact v))
    source
    theorem TauCeti.Comodule.rTensor_comp_endOfPoint {R : Type u_1} {H : Type u_2} (V : Type u_3) {A : Type u_4} [CommSemiring R] [Semiring H] [Algebra R H] [Coalgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] {A' : Type u_5} [CommSemiring A'] [Algebra R A'] (φ : A →ₐ[R] A') (g : H →ₐ[R] A) :
    LinearMap.rTensor V φ.toLinearMap ∘ₗ ↑R (endOfPoint V g) = ↑R (endOfPoint V (φ.comp g)) ∘ₗ LinearMap.rTensor V φ.toLinearMap

    Base-change compatibility of the action: pushing a point forward along a morphism of value algebras and acting agrees with acting first and then extending scalars. Stated on the underlying R-linear maps, where both composites live.

    source
    theorem TauCeti.Comodule.baseChange_comp_endOfPoint {R : Type u_1} {H : Type u_2} {V : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring H] [Algebra R H] [Coalgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] {W : Type u_5} [AddCommMonoid W] [Module R W] [Comodule R H W] (f : Hom R H V W) (g : H →ₐ[R] A) :
    LinearMap.baseChange A f.toLinearMap ∘ₗ endOfPoint V g = endOfPoint W g ∘ₗ LinearMap.baseChange A f.toLinearMap

    Scalar extension of a comodule morphism intertwines the point actions: the action is functorial in the comodule.

    source
    theorem TauCeti.Comodule.Hom.map_endOfPoint_baseChange_eq_iff {R : Type u_1} {H : Type u_2} {V : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring H] [Algebra R H] [Coalgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] {W : Type u_5} [AddCommMonoid W] [Module R W] [Comodule R H W] [Module.Flat R A] (f : Hom R H V W) (hf : Function.Injective ⇑f) (L : Submodule R V) (g : H →ₐ[R] A) :
    Submodule.map (endOfPoint W g) (Submodule.baseChange A (Submodule.map f.toLinearMap L)) = Submodule.baseChange A (Submodule.map f.toLinearMap L) ↔ Submodule.map (endOfPoint V g) (Submodule.baseChange A L) = Submodule.baseChange A L

    An injective comodule morphism preserves and reflects the stabilizer of a subspace after flat scalar extension. Thus a subspace has the same stabilizer in a subrepresentation and in the ambient representation.

    source
    @[simp]
    theorem TauCeti.Comodule.endOfPoint_corestrict {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {V : Type u_4} {A : Type u_5} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] [AddCommMonoid V] [Module R V] [Comodule R H₁ V] [CommSemiring A] [Algebra R A] (φ : H₁ →ₐc[R] H₂) (g : H₂ →ₐ[R] A) :
    endOfPoint V g = endOfPoint V (g.comp ↑φ)

    Acting on a comodule corestricted along a bialgebra morphism agrees with acting by the point precomposed with the underlying algebra morphism.

    source
    @[simp]
    theorem TauCeti.Comodule.endOfPoint_groupLike {R : Type u_1} {H : Type u_2} {V : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring H] [Algebra R H] [Coalgebra R H] [AddCommMonoid V] [Module R V] [CommSemiring A] [Algebra R A] (x : GroupLike R H) (g : H →ₐ[R] A) :
    endOfPoint V g = g ↑x • LinearMap.id

    On a group-like comodule, a point acts by scalar multiplication by its value on the group-like element.

    source
    theorem TauCeti.Comodule.endOfPoint_tensor_tmul_of_coact_eq {R : Type u_1} {H : Type u_2} {V : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring H] [Bialgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] {W : Type u_5} [AddCommMonoid W] [Module R W] [Comodule R H W] [Comodule R H (TensorProduct R V W)] (hcoact : coact = tensorCoact) (g : H →ₐ[R] A) (a b : A) (v : V) (w : W) :
    (TensorProduct.AlgebraTensorModule.distribBaseChange R A V W).symm ((endOfPoint V g) (a ⊗ₜ[R] v) ⊗ₜ[A] (endOfPoint W g) (b ⊗ₜ[R] w)) = (endOfPoint (TensorProduct R V W) g) ((a * b) ⊗ₜ[R] (v ⊗ₜ[R] w))

    On pure tensors, acting separately on two comodules and applying the scalar-extension tensor comparison agrees with acting on any tensor-product comodule whose coaction is the diagonal one.

    source
    theorem TauCeti.Comodule.endOfPoint_tensor_of_coact_eq {R : Type u_1} {H : Type u_2} {V : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring H] [Bialgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] {W : Type u_5} [AddCommMonoid W] [Module R W] [Comodule R H W] [Comodule R H (TensorProduct R V W)] (hcoact : coact = tensorCoact) (g : H →ₐ[R] A) :
    ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A V W).symm ∘ₗ TensorProduct.map (endOfPoint V g) (endOfPoint W g) = endOfPoint (TensorProduct R V W) g ∘ₗ ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A V W).symm

    A point action preserves tensor products. Under the canonical comparison (A ⊗ M) ⊗[A] (A ⊗ N) ≃ A ⊗ (M ⊗ N), acting on the two factors separately equals acting on any tensor-product comodule whose coaction is the diagonal one.

    source
    theorem TauCeti.Comodule.endOfPoint_tensor_tmul {R : Type u_1} {H : Type u_2} {V : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring H] [Bialgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] {W : Type u_5} [AddCommMonoid W] [Module R W] [Comodule R H W] (g : H →ₐ[R] A) (a b : A) (v : V) (w : W) :
    (TensorProduct.AlgebraTensorModule.distribBaseChange R A V W).symm ((endOfPoint V g) (a ⊗ₜ[R] v) ⊗ₜ[A] (endOfPoint W g) (b ⊗ₜ[R] w)) = (endOfPoint (TensorProduct R V W) g) ((a * b) ⊗ₜ[R] (v ⊗ₜ[R] w))

    On pure tensors, acting separately on two comodules and applying the scalar-extension tensor comparison agrees with acting on their diagonal tensor-product comodule.

    source
    theorem TauCeti.Comodule.endOfPoint_tensor {R : Type u_1} {H : Type u_2} {V : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring H] [Bialgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] {W : Type u_5} [AddCommMonoid W] [Module R W] [Comodule R H W] (g : H →ₐ[R] A) :
    ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A V W).symm ∘ₗ TensorProduct.map (endOfPoint V g) (endOfPoint W g) = endOfPoint (TensorProduct R V W) g ∘ₗ ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A V W).symm

    A point action preserves the diagonal tensor product of two comodules.

    source
    @[simp]
    theorem TauCeti.Comodule.endOfPoint_convOne {R : Type u_1} {H : Type u_2} (V : Type u_3) {A : Type u_4} [CommSemiring R] [Semiring H] [Bialgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] :
    endOfPoint V (WithConv.ofConv 1) = LinearMap.id

    The convolution unit acts as the identity: the counit law of the comodule.

    source
    @[simp]
    theorem TauCeti.Comodule.endOfPoint_convMul {R : Type u_1} {H : Type u_2} (V : Type u_3) {A : Type u_4} [CommSemiring R] [Semiring H] [Bialgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] (g h : WithConv (H →ₐ[R] A)) :
    endOfPoint V (g * h).ofConv = endOfPoint V g.ofConv ∘ₗ endOfPoint V h.ofConv

    Convolution products act as composites: the coassociativity law of the comodule.

    source
    theorem TauCeti.Comodule.map_endOfPoint_eq_of_mapsTo {R : Type u_1} {H : Type u_2} (V : Type u_3) {A : Type u_4} [CommSemiring R] [Semiring H] [Bialgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] (g h : WithConv (H →ₐ[R] A)) (hgh : g * h = 1) (p : Submodule A (TensorProduct R A V)) (hg : Set.MapsTo ⇑(endOfPoint V g.ofConv) ↑p ↑p) (hh : Set.MapsTo ⇑(endOfPoint V h.ofConv) ↑p ↑p) :
    Submodule.map (endOfPoint V g.ofConv) p = p

    If two points whose convolution product is one both preserve a submodule, the first point carries that submodule onto itself.

    source
    noncomputable def TauCeti.Comodule.pointsRepresentation {R : Type u_1} {H : Type u_2} (V : Type u_3) {A : Type u_4} [CommSemiring R] [Semiring H] [Bialgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] :
    Representation A (WithConv (H →ₐ[R] A)) (TensorProduct R A V)

    The points action of a comodule, as a representation of the convolution monoid of points on the scalar extension.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Comodule.pointsRepresentation_apply {R : Type u_1} {H : Type u_2} (V : Type u_3) {A : Type u_4} [CommSemiring R] [Semiring H] [Bialgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) :
      (pointsRepresentation V) g = endOfPoint V g.ofConv
      source
      theorem TauCeti.Comodule.endOfPoint_inv_comp {R : Type u_1} {H : Type u_2} (V : Type u_3) {A : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) :
      endOfPoint V g⁻¹.ofConv ∘ₗ endOfPoint V g.ofConv = LinearMap.id

      The inverse point action cancels the point action on the left.

      source
      theorem TauCeti.Comodule.endOfPoint_comp_inv {R : Type u_1} {H : Type u_2} (V : Type u_3) {A : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) :
      endOfPoint V g.ofConv ∘ₗ endOfPoint V g⁻¹.ofConv = LinearMap.id

      The inverse point action cancels the point action on the right.

      source
      theorem BialgHom.baseChange_comp_endOfPoint_regular {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] (f : H →ₐc[R] K) (g : K →ₐ[R] A) :
      LinearMap.baseChange A f.toLinearMap ∘ₗ TauCeti.Comodule.endOfPoint H (g.comp ↑f) = TauCeti.Comodule.endOfPoint K g ∘ₗ LinearMap.baseChange A f.toLinearMap

      A bialgebra morphism intertwines the regular point actions, with the point pulled back along the morphism on the source.

      source
      theorem TauCeti.Comodule.endOfPoint_trivial {R : Type u_1} {H : Type u_2} {V : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring H] [Bialgebra R H] [AddCommMonoid V] [Module R V] [CommSemiring A] [Algebra R A] (g : H →ₐ[R] A) :
      endOfPoint V g = LinearMap.id

      Every point acts as the identity on a trivial comodule.