Documentation

TauCeti.Algebra.AlgebraicGroup.Hopf.Translation

Translations of an affine group #

A k-point of an affine group acts on its coordinate algebra by translation. For a commutative Hopf algebra H over k, a point g : H →ₐ[k] k defines the algebra endomorphism

x ↦ ∑ x₍₁₎ g(x₍₂₎).

The regular-comodule action shows that this endomorphism is bijective, with inverse obtained from the convolution inverse point. This file packages it as an algebra equivalence, records its group action laws, and identifies its action on the prime spectrum.

Main declarations #

TauCeti.HopfAlgebra.rightTranslationAlgHom: pullback by right translation by a point.
TauCeti.HopfAlgebra.rightTranslationAlgEquiv: right translation as an algebra automorphism.
TauCeti.HopfAlgebra.rightTranslationAlgEquiv_mul and TauCeti.HopfAlgebra.rightTranslationAlgHom_mul: right translation respects the convolution product of points.
TauCeti.HopfAlgebra.rightTranslationStabilizer: the subgroup of points whose right translation fixes a given function.
TauCeti.HopfAlgebra.comap_rightTranslationAlgEquiv_augmentationPoint: the translated counit point is the given point.
TauCeti.HopfAlgebra.rightTranslationHomeomorph: right translation on the prime spectrum.
TauCeti.HopfAlgebra.height_kernel_eq_height_augmentation: translation preserves the height of the augmentation ideal.

References #

J. S. Milne, Algebraic Groups (2017), Proposition 2.37.
W. C. Waterhouse, Introduction to Affine Group Schemes, Section 6.7.

This is translation infrastructure for Layer 3, "Identity component G° and component group π₀(G)", of the ReductiveGroups roadmap.

noncomputable def TauCeti.HopfAlgebra.rightTranslationAlgHom {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g : WithConv (H →ₐ[k] k)) :

Pullback by right translation by a k-point of an affine group, on its coordinate algebra.

Equations

TauCeti.HopfAlgebra.rightTranslationAlgHom g = (WithConv.toConv (AlgHom.id k H) * WithConv.toConv ((Algebra.ofId k H).comp g.ofConv)).ofConv

Instances For

theorem TauCeti.HopfAlgebra.rightTranslationAlgHom_apply {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g : WithConv (H →ₐ[k] k)) (x : H) :

(rightTranslationAlgHom g) x = (TensorProduct.rid k H) ((TensorProduct.map LinearMap.id g.ofConv.toLinearMap) (CoalgebraStruct.comul x))

Right translation evaluates by applying the point to the second tensor factor of the comultiplication.

@[simp]

theorem TauCeti.HopfAlgebra.toConv_comp_rightTranslationAlgHom {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (f g : WithConv (H →ₐ[k] k)) :

WithConv.toConv (f.ofConv.comp (rightTranslationAlgHom g)) = f * g

Composing a point with right translation is convolution by the translating point.

@[simp]

theorem TauCeti.HopfAlgebra.ofConv_rightTranslationAlgHom {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (f g : WithConv (H →ₐ[k] k)) (x : H) :

f.ofConv ((rightTranslationAlgHom g) x) = (f * g).ofConv x

Applying a point to a right-translated function is convolution by the translating point.

noncomputable def TauCeti.HopfAlgebra.rightTranslationAlgEquiv {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g : WithConv (H →ₐ[k] k)) :

Pullback by right translation by a k-point, as an algebra automorphism of the coordinate algebra.

Equations

TauCeti.HopfAlgebra.rightTranslationAlgEquiv g = AlgEquiv.ofBijective (TauCeti.HopfAlgebra.rightTranslationAlgHom g) ⋯

Instances For

@[simp]

theorem TauCeti.HopfAlgebra.rightTranslationAlgEquiv_toAlgHom {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g : WithConv (H →ₐ[k] k)) :

↑(rightTranslationAlgEquiv g) = rightTranslationAlgHom g

The algebra equivalence underlying right translation is the right-translation algebra homomorphism.

theorem TauCeti.HopfAlgebra.toConv_rightTranslationAlgEquiv {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g : WithConv (H →ₐ[k] k)) :

WithConv.toConv ↑(rightTranslationAlgEquiv g) = WithConv.toConv (AlgHom.id k H) * (AlgHom.mapValue (Algebra.ofId k H)) g

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

@[simp]

theorem TauCeti.HopfAlgebra.rightTranslationAlgEquiv_one {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] :

rightTranslationAlgEquiv 1 = 1

Translation by the identity point is the identity algebra automorphism.

@[simp]

theorem TauCeti.HopfAlgebra.rightTranslationAlgEquiv_mul {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g h : WithConv (H →ₐ[k] k)) :

rightTranslationAlgEquiv (g * h) = rightTranslationAlgEquiv g * rightTranslationAlgEquiv h

Translation by a convolution product is the composite of the two translations.

@[simp]

theorem TauCeti.HopfAlgebra.rightTranslationAlgHom_one {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] :

rightTranslationAlgHom 1 = AlgHom.id k H

Translation by the identity point is the identity algebra endomorphism.

@[simp]

theorem TauCeti.HopfAlgebra.rightTranslationAlgHom_mul {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g h : WithConv (H →ₐ[k] k)) :

rightTranslationAlgHom (g * h) = (rightTranslationAlgHom g).comp (rightTranslationAlgHom h)

Translation by a convolution product is the composite of the two translation algebra endomorphisms.

@[simp]

theorem TauCeti.HopfAlgebra.rightTranslationAlgEquiv_inv {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g : WithConv (H →ₐ[k] k)) :

rightTranslationAlgEquiv g⁻¹ = (rightTranslationAlgEquiv g)⁻¹

Translation by an inverse point is the inverse algebra automorphism.

noncomputable def TauCeti.HopfAlgebra.rightTranslationStabilizer {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (x : H) :

Subgroup (WithConv (H →ₐ[k] k))

The points whose right translation fixes a given function form a subgroup.

Equations

TauCeti.HopfAlgebra.rightTranslationStabilizer x = { carrier := {g : WithConv (H →ₐ[k] k) | (TauCeti.HopfAlgebra.rightTranslationAlgHom g) x = x}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

Instances For

@[simp]

theorem TauCeti.HopfAlgebra.mem_rightTranslationStabilizer {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] {x : H} {g : WithConv (H →ₐ[k] k)} :

g ∈ rightTranslationStabilizer x ↔ (rightTranslationAlgHom g) x = x

A point lies in the stabilizer of a function exactly when its right translation fixes it.

theorem TauCeti.HopfAlgebra.rightTranslationAlgEquiv_apply {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g : WithConv (H →ₐ[k] k)) (x : H) :

(rightTranslationAlgEquiv g) x = (TensorProduct.rid k H) ((TensorProduct.map LinearMap.id g.ofConv.toLinearMap) (CoalgebraStruct.comul x))

Right translation as an algebra equivalence has the expected evaluation formula.

@[simp]

theorem TauCeti.HopfAlgebra.counitAlgHom_comp_rightTranslationAlgHom {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g : WithConv (H →ₐ[k] k)) :

(Bialgebra.counitAlgHom k H).comp (rightTranslationAlgHom g) = g.ofConv

Evaluating a right-translated function at the identity evaluates the original function at the translating point.

@[simp]

theorem TauCeti.HopfAlgebra.height_kernel_eq_height_augmentation {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g : WithConv (H →ₐ[k] k)) :

(RingHom.ker ↑g.ofConv).height = (RingHom.ker ↑(Bialgebra.counitAlgHom k H)).height

Translation identifies the height of the ideal of any rational point with the height of the augmentation ideal.

noncomputable def TauCeti.HopfAlgebra.rightTranslationHomeomorph {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g : WithConv (H →ₐ[k] k)) :

↥(AlgebraicGeometry.Spec ↧H) ≃ₜ ↥(AlgebraicGeometry.Spec ↧H)

Right translation on the prime spectrum. The inverse algebra equivalence occurs because Spec is contravariant.

Equations

TauCeti.HopfAlgebra.rightTranslationHomeomorph g = PrimeSpectrum.homeomorphOfRingEquiv (TauCeti.HopfAlgebra.rightTranslationAlgEquiv g).symm.toRingEquiv

Instances For

@[simp]

theorem TauCeti.HopfAlgebra.rightTranslationHomeomorph_apply {k : Type u} [CommRing k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g : WithConv (H →ₐ[k] k)) (x : ↥(AlgebraicGeometry.Spec ↧H)) :

(rightTranslationHomeomorph g) x = PrimeSpectrum.comap (↑(rightTranslationAlgEquiv g).toRingEquiv) x

Right translation on the prime spectrum is contraction along the right-translation algebra automorphism.

@[simp]

theorem TauCeti.HopfAlgebra.comap_rightTranslationAlgEquiv_augmentationPoint {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g : WithConv (H →ₐ[k] k)) :

PrimeSpectrum.comap (↑(rightTranslationAlgEquiv g)) (Bialgebra.augmentationPoint k H) = AlgHom.kernelPoint g.ofConv

Contraction of the augmentation point along right translation gives the translating point.

theorem BialgHom.comp_rightTranslationAlgHom {R : Type u_1} {H : Type u_2} {K : Type u_3} [CommRing R] [CommRing H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (g : WithConv (K →ₐ[R] R)) :

(↑f).comp (TauCeti.HopfAlgebra.rightTranslationAlgHom ((TauCeti.AlgHom.mapDomain f) g)) = (TauCeti.HopfAlgebra.rightTranslationAlgHom g).comp ↑f

A homomorphism of affine groups commutes with right translation by a point and its image.