Translations of the identity component

Right translation by a k-rational point induces a homeomorphism of the prime spectrum. This file proves that a point in the connected component of the counit translates that component onto itself and preserves its defining idempotent and ideal.

Main declarations

• rightTranslationHomeomorph_image_connectedComponent_augmentationPoint_eq_self: a point in the identity component translates that component to itself.
• rightTranslationHomeomorph_kernelPoint: right translation sends the kernel point of g to the kernel point of the convolution product.
• map_connectedComponentIdempotent_augmentationPoint_eq_one_of_mem: a point in the identity component evaluates its component idempotent to one.
• map_rightTranslationAlgEquiv_connectedComponentIdeal_eq_self: translation by an identity-component point fixes its defining ideal.

References

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

This is the translation prerequisite for Layer 3, "Identity component G° and component group π₀(G)", of the ReductiveGroups roadmap. The next step uses these automorphisms to prove that multiplication carries the product of the identity component with itself into the identity component, giving comultiplication closure of its defining ideal.

theorem TauCeti.HopfAlgebra.rightTranslationHomeomorph_kernelPoint {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g h : WithConv (H →ₐ[k] k)) : (rightTranslationHomeomorph h) (AlgHom.kernelPoint g.ofConv) = AlgHom.kernelPoint (g * h).ofConv

Right translation sends the kernel point of g to the kernel point of the convolution product g * h.

theorem TauCeti.HopfAlgebra.rightTranslationHomeomorph_image_connectedComponent {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g : WithConv (H →ₐ[k] k)) (x : ↥(AlgebraicGeometry.Spec ↧H)) : ⇑(rightTranslationHomeomorph g) '' connectedComponent x = connectedComponent ((rightTranslationHomeomorph g) x)

Right translation transports the connected component of a point to the connected component of its translate.

theorem TauCeti.HopfAlgebra.rightTranslationHomeomorph_image_connectedComponent_augmentationPoint_eq_self {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] (g : WithConv (H →ₐ[k] k)) (hg : AlgHom.kernelPoint g.ofConv ∈ connectedComponent (Bialgebra.augmentationPoint k H)) : ⇑(rightTranslationHomeomorph g) '' connectedComponent (Bialgebra.augmentationPoint k H) = connectedComponent (Bialgebra.augmentationPoint k H)

A point in the identity component right-translates that component onto itself.

@[simp]

theorem TauCeti.HopfAlgebra.connectedComponentIdempotent_kernelPoint_eq_augmentationPoint {k : Type u} [Field k] {H : Type v} [CommRing H] [LocallyConnectedSpace (PrimeSpectrum H)] [Bialgebra k H] (g : WithConv (H →ₐ[k] k)) (hg : AlgHom.kernelPoint g.ofConv ∈ connectedComponent (Bialgebra.augmentationPoint k H)) : PrimeSpectrum.connectedComponentIdempotent (AlgHom.kernelPoint g.ofConv) = PrimeSpectrum.connectedComponentIdempotent (Bialgebra.augmentationPoint k H)

Points in the identity component have the same connected-component idempotent as the augmentation point.

theorem TauCeti.HopfAlgebra.map_connectedComponentIdempotent_augmentationPoint_eq_one_of_mem {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [LocallyConnectedSpace (PrimeSpectrum H)] (g : WithConv (H →ₐ[k] k)) (hg : AlgHom.kernelPoint g.ofConv ∈ connectedComponent (Bialgebra.augmentationPoint k H)) : g.ofConv (PrimeSpectrum.connectedComponentIdempotent (Bialgebra.augmentationPoint k H)) = 1

A rational point in the identity component evaluates the idempotent selecting that component to one.

@[simp]

theorem TauCeti.HopfAlgebra.rightTranslationAlgEquiv_symm_connectedComponentIdempotent_eq_self {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [LocallyConnectedSpace (PrimeSpectrum H)] (g : WithConv (H →ₐ[k] k)) (hg : AlgHom.kernelPoint g.ofConv ∈ connectedComponent (Bialgebra.augmentationPoint k H)) : (rightTranslationAlgEquiv g).symm (PrimeSpectrum.connectedComponentIdempotent (Bialgebra.augmentationPoint k H)) = PrimeSpectrum.connectedComponentIdempotent (Bialgebra.augmentationPoint k H)

The inverse coordinate-algebra automorphism of translation by an identity-component point fixes the idempotent selecting the identity component.

@[simp]

theorem TauCeti.HopfAlgebra.rightTranslationAlgEquiv_connectedComponentIdempotent_eq_self {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [LocallyConnectedSpace (PrimeSpectrum H)] (g : WithConv (H →ₐ[k] k)) (hg : AlgHom.kernelPoint g.ofConv ∈ connectedComponent (Bialgebra.augmentationPoint k H)) : (rightTranslationAlgEquiv g) (PrimeSpectrum.connectedComponentIdempotent (Bialgebra.augmentationPoint k H)) = PrimeSpectrum.connectedComponentIdempotent (Bialgebra.augmentationPoint k H)

The coordinate-algebra automorphism of translation by an identity-component point fixes the idempotent selecting the identity component.

@[simp]

theorem TauCeti.HopfAlgebra.map_rightTranslationAlgEquiv_connectedComponentIdeal_eq_self {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [LocallyConnectedSpace (PrimeSpectrum H)] (g : WithConv (H →ₐ[k] k)) (hg : AlgHom.kernelPoint g.ofConv ∈ connectedComponent (Bialgebra.augmentationPoint k H)) : Ideal.map (rightTranslationAlgEquiv g) (PrimeSpectrum.connectedComponentIdeal (Bialgebra.augmentationPoint k H)) = PrimeSpectrum.connectedComponentIdeal (Bialgebra.augmentationPoint k H)

Translation by a point in the identity component fixes the ideal cutting out that component.

@[simp]

theorem TauCeti.HopfAlgebra.rightTranslationAlgEquiv_mem_connectedComponentIdeal_iff {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [LocallyConnectedSpace (PrimeSpectrum H)] (g : WithConv (H →ₐ[k] k)) (hg : AlgHom.kernelPoint g.ofConv ∈ connectedComponent (Bialgebra.augmentationPoint k H)) {x : H} : (rightTranslationAlgEquiv g) x ∈ PrimeSpectrum.connectedComponentIdeal (Bialgebra.augmentationPoint k H) ↔ x ∈ PrimeSpectrum.connectedComponentIdeal (Bialgebra.augmentationPoint k H)

Membership in the identity-component ideal is invariant under translation by a point of the identity component.