Left translations of an affine group

Left translation by a base-valued point is an automorphism of the coordinate algebra. Its pullback is convolution of the constant point with the universal point, in that order. This is the source translation that intertwines a representation's orbit map with the linear action on its target. The formula holds on points over every commutative algebra.

References

• J. S. Milne, Algebraic Groups (2017), §§2 and 7.c.
• Formal precursors: HopfAlgebra.rightTranslationAlgEquiv and HopfAlgebra.pointConjugationBialgEquiv.

noncomputable def TauCeti.HopfAlgebra.leftTranslationAlgEquiv {R : Type u_1} {H : Type u_2} [CommRing R] [CommRing H] [HopfAlgebra R H] (g : WithConv (H →ₐ[R] R)) : H ≃ₐ[R] H

Pullback by left translation by a base-valued point.

Equations

• TauCeti.HopfAlgebra.leftTranslationAlgEquiv g = (TauCeti.HopfAlgebra.pointConjugationBialgEquiv g).toAlgEquiv.trans (TauCeti.HopfAlgebra.rightTranslationAlgEquiv g)

theorem TauCeti.HopfAlgebra.toConv_leftTranslationAlgEquiv {R : Type u_1} {H : Type u_2} [CommRing R] [CommRing H] [HopfAlgebra R H] (g : WithConv (H →ₐ[R] R)) : WithConv.toConv ↑(leftTranslationAlgEquiv g) = (AlgHom.mapValue (Algebra.ofId R H)) g * WithConv.toConv (AlgHom.id R H)

The coordinate map of left translation is convolution of the constant translating point with the universal point.

theorem TauCeti.HopfAlgebra.toConv_comp_leftTranslationAlgEquiv {R : Type u_1} {H : Type u_2} [CommRing R] [CommRing H] [HopfAlgebra R H] {A : Type u_3} [CommRing A] [Algebra R A] (g : WithConv (H →ₐ[R] R)) (x : WithConv (H →ₐ[R] A)) : WithConv.toConv (x.ofConv.comp ↑(leftTranslationAlgEquiv g)) = (AlgHom.mapValue (Algebra.ofId R A)) g * x

Precomposition by left translation multiplies an arbitrary algebra-valued point on the left by the constant translating point.

@[simp]

theorem TauCeti.HopfAlgebra.leftTranslationAlgEquiv_one {R : Type u_1} {H : Type u_2} [CommRing R] [CommRing H] [HopfAlgebra R H] : leftTranslationAlgEquiv 1 = 1

Left translation by the identity point is the identity algebra automorphism.

@[simp]

theorem TauCeti.HopfAlgebra.leftTranslationAlgEquiv_mul {R : Type u_1} {H : Type u_2} [CommRing R] [CommRing H] [HopfAlgebra R H] (g h : WithConv (H →ₐ[R] R)) : leftTranslationAlgEquiv (g * h) = leftTranslationAlgEquiv h * leftTranslationAlgEquiv g

Pullback by left translation reverses the order of convolution products.

@[simp]

theorem TauCeti.HopfAlgebra.leftTranslationAlgEquiv_inv {R : Type u_1} {H : Type u_2} [CommRing R] [CommRing H] [HopfAlgebra R H] (g : WithConv (H →ₐ[R] R)) : leftTranslationAlgEquiv g⁻¹ = (leftTranslationAlgEquiv g)⁻¹

Left translation by the inverse point is the inverse algebra automorphism.