Left translations on the coinvariant algebra

Functions invariant under right translation by a closed subgroup remain invariant after left translation by an ambient rational point. Thus left translations act on the spectrum of the coinvariant algebra, compatibly with the map from the ambient group. No normality of the subgroup is needed.

References

• J. S. Milne, Algebraic Groups (2017), §§7 and 12.

theorem TauCeti.HopfIdeal.leftTranslationAlgEquiv_mem_coinvariants {R : Type u} [CommRing R] {H : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (g : WithConv (↑H →ₐ[R] R)) {x : ↑H} (hx : x ∈ I.coinvariants) : (HopfAlgebra.leftTranslationAlgEquiv g) x ∈ I.coinvariants

Left translation preserves functions invariant under right translation by a subgroup.

noncomputable def TauCeti.HopfIdeal.coinvariantsLeftTranslation {R : Type u} [CommRing R] {H : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (g : WithConv (↑H →ₐ[R] R)) : ↥I.coinvariants ≃ₐ[R] ↥I.coinvariants

The automorphism of the coinvariant algebra induced by an ambient left translation.

@[simp]

theorem TauCeti.HopfIdeal.coe_coinvariantsLeftTranslation {R : Type u} [CommRing R] {H : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (g : WithConv (↑H →ₐ[R] R)) (x : ↥I.coinvariants) : ↑((I.coinvariantsLeftTranslation g) x) = (HopfAlgebra.leftTranslationAlgEquiv g) ↑x

The inclusion of coinvariants intertwines the two left translations.

@[simp]

theorem TauCeti.HopfIdeal.coe_coinvariantsLeftTranslation_symm {R : Type u} [CommRing R] {H : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (g : WithConv (↑H →ₐ[R] R)) (x : ↥I.coinvariants) : ↑((I.coinvariantsLeftTranslation g).symm x) = (HopfAlgebra.leftTranslationAlgEquiv g⁻¹) ↑x

The inverse restricted translation is left translation by the inverse point.

@[simp]

theorem TauCeti.HopfIdeal.coinvariantsLeftTranslation_one {R : Type u} [CommRing R] {H : CommHopfAlgCat R} (I : HopfIdeal R ↑H) : I.coinvariantsLeftTranslation 1 = 1

Left translation by the identity point fixes the coinvariant algebra.

@[simp]

theorem TauCeti.HopfIdeal.coinvariantsLeftTranslation_mul {R : Type u} [CommRing R] {H : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (g h : WithConv (↑H →ₐ[R] R)) : I.coinvariantsLeftTranslation (g * h) = I.coinvariantsLeftTranslation h * I.coinvariantsLeftTranslation g

Pullback on coinvariants reverses the order of convolution products.

@[simp]

theorem TauCeti.HopfIdeal.coinvariantsLeftTranslation_inv {R : Type u} [CommRing R] {H : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (g : WithConv (↑H →ₐ[R] R)) : I.coinvariantsLeftTranslation g⁻¹ = (I.coinvariantsLeftTranslation g)⁻¹

Translation by the inverse point inverts the automorphism of coinvariants.

theorem TauCeti.HopfIdeal.comp_coinvariantsLeftTranslation {R : Type u} [CommRing R] {H : CommHopfAlgCat R} (I : HopfIdeal R ↑H) (g : WithConv (↑H →ₐ[R] R)) {A : Type u_1} [CommRing A] [Algebra R A] (a : WithConv (↑H →ₐ[R] A)) : (a.ofConv.comp I.coinvariants.val).comp ↑(I.coinvariantsLeftTranslation g) = ((Algebra.ofId R A).mapValue g * a).ofConv.comp I.coinvariants.val

Pulling a restricted point back by a coinvariant left translation multiplies the original point on the left before restricting it.