The coordinate map to the component group

Let H be the coordinate Hopf algebra of a finite-type affine group over an algebraically closed field. The connected components of Spec H form a finite group. This file constructs the algebra map from the functions on that finite group to H: a function f is sent to

  ∑ C, f(C) e_C,

where e_C is the canonical idempotent selecting the component C. Evaluation at a rational point g recovers f on the component of g. In particular, the map is injective and represents the surjective rational component homomorphism.

The compatibility of this algebra map with comultiplication and counit, and hence its upgrade to the coordinate bialgebra morphism of the component group, is developed in the remainder of this file.

Main declarations

• TauCeti.FiniteTypeCommHopfAlgCat.componentFunctionAlgHom: the algebra map from component-indexed functions to the coordinate ring.
• TauCeti.FiniteTypeCommHopfAlgCat.componentCoordinateMap: the same map on the canonical constant-group coordinate ring.
• TauCeti.FiniteTypeCommHopfAlgCat.eval_componentCoordinateMap: evaluation of the coordinate map at a rational point is evaluation at its connected component.
• TauCeti.FiniteTypeCommHopfAlgCat.componentCoordinateBialgHom: the coordinate bialgebra morphism of the component map.
• TauCeti.FiniteTypeCommHopfAlgCat.kernelHopfIdeal_componentCoordinateHom: its scheme-theoretic kernel is the identity component.

References

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

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

@[instance_reducible]

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.instFintypeConnectedComponentsPrimeSpectrumXObjCommHopfAlgCatFiniteTypeCommHopfAlgProperty {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : Fintype (ConnectedComponents (PrimeSpectrum ↑H.obj))

The finite instance on the connected components of a finite-type affine scheme.

Equations

• H.instFintypeConnectedComponentsPrimeSpectrumXObjCommHopfAlgCatFiniteTypeCommHopfAlgProperty = Fintype.ofFinite (ConnectedComponents (PrimeSpectrum ↑H.obj))

@[instance_reducible]

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.instDecidableEqConnectedComponentsPrimeSpectrumXObjCommHopfAlgCatFiniteTypeCommHopfAlgProperty {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : DecidableEq (ConnectedComponents (PrimeSpectrum ↑H.obj))

Classical decidable equality on the finite connected-component group.

Equations

• H.instDecidableEqConnectedComponentsPrimeSpectrumXObjCommHopfAlgCatFiniteTypeCommHopfAlgProperty = Classical.decEq (ConnectedComponents (PrimeSpectrum ↑H.obj))

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentFunctionAlgHom {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : (ConnectedComponents (PrimeSpectrum ↑H.obj) → k) →ₐ[k] ↑H.obj

The algebra map from functions on the connected-component group to the coordinate ring.

A function f is sent to the sum ∑ C, f(C) e_C, where e_C is the canonical idempotent selecting the connected component C.

Equations

• H.componentFunctionAlgHom = TauCeti.FiniteTypeCommHopfAlgCat.componentFunctionAlgHomAux✝ H

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentFunctionAlgHom_apply {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (f : ConnectedComponents (PrimeSpectrum ↑H.obj) → k) : H.componentFunctionAlgHom f = ∑ C : ConnectedComponents (PrimeSpectrum ↑H.obj), (algebraMap k ↑H.obj) (f C) * PrimeSpectrum.connectedComponentsIdempotent C

The component function algebra map is the idempotent-weighted sum over connected components.

theorem TauCeti.FiniteTypeCommHopfAlgCat.map_connectedComponentsIdempotent_eq_one {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (g : ↑(HopfAlgebra.points ↧k)) {C : ConnectedComponents (PrimeSpectrum ↑H.obj)} (hC : H.rationalComponentMap g = C) : g.ofConv (PrimeSpectrum.connectedComponentsIdempotent C) = 1

A rational point evaluates the idempotent of its connected component to one.

theorem TauCeti.FiniteTypeCommHopfAlgCat.map_connectedComponentsIdempotent_eq_zero {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (g : ↑(HopfAlgebra.points ↧k)) {C : ConnectedComponents (PrimeSpectrum ↑H.obj)} (hC : H.rationalComponentMap g ≠ C) : g.ofConv (PrimeSpectrum.connectedComponentsIdempotent C) = 0

A rational point evaluates every other component idempotent to zero.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.eval_componentFunctionAlgHom {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (g : ↑(HopfAlgebra.points ↧k)) (f : ConnectedComponents (PrimeSpectrum ↑H.obj) → k) : g.ofConv (H.componentFunctionAlgHom f) = f (H.rationalComponentMap g)

Evaluation of a component-indexed function at a rational point is evaluation at the connected component containing that point.

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentFunctionAlgHom_injective {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : Function.Injective ⇑H.componentFunctionAlgHom

The component function algebra embeds in the coordinate ring.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentCoordinateMap {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : ConstantGroup.coordinateRing k (ConnectedComponents (PrimeSpectrum ↑H.obj)) →ₐ[k] ↑H.obj

The coordinate algebra map representing projection to the finite constant group of connected components.

Equations

• H.componentCoordinateMap = H.componentFunctionAlgHom.comp ↑(TauCeti.ConstantGroup.functionAlgEquiv k (ConnectedComponents (PrimeSpectrum ↑H.obj)))

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentCoordinateMap_apply {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (x : ConstantGroup.coordinateRing k (ConnectedComponents (PrimeSpectrum ↑H.obj))) : H.componentCoordinateMap x = ∑ C : ConnectedComponents (PrimeSpectrum ↑H.obj), (algebraMap k ↑H.obj) (x.ofConv (MonoidAlgebra.single C 1)) * PrimeSpectrum.connectedComponentsIdempotent C

The component coordinate map is the idempotent-weighted sum of the values of a coordinate function on each component.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentCoordinateMap_indicator {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (C : ConnectedComponents (PrimeSpectrum ↑H.obj)) : H.componentCoordinateMap ((ConstantGroup.functionAlgEquiv k (ConnectedComponents (PrimeSpectrum ↑H.obj))).symm (Pi.single C 1)) = PrimeSpectrum.connectedComponentsIdempotent C

The component coordinate map sends the indicator of a component to its canonical component idempotent.

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentCoordinateMap_injective {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : Function.Injective ⇑H.componentCoordinateMap

The component coordinate map is injective.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.eval_componentCoordinateMap {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (g : ↑(HopfAlgebra.points ↧k)) : g.ofConv.comp H.componentCoordinateMap = ConstantGroup.eval k (ConnectedComponents (PrimeSpectrum ↑H.obj)) (H.rationalComponentMap g)

Pulling the component coordinate map back along a rational point is evaluation at that point's connected component.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentCoordinateBialgHom {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : ConstantGroup.coordinateRing k (ConnectedComponents (PrimeSpectrum ↑H.obj)) →ₐc[k] ↑H.obj

The coordinate bialgebra morphism representing projection to the finite constant group of connected components.

Equations

• H.componentCoordinateBialgHom = BialgHom.ofAlgHom H.componentCoordinateMap ⋯ ⋯

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentCoordinateBialgHom_toAlgHom {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : ↑H.componentCoordinateBialgHom = H.componentCoordinateMap

The algebra homomorphism underlying the component coordinate bialgebra morphism is the component coordinate map.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentCoordinateBialgHom_apply {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (x : ConstantGroup.coordinateRing k (ConnectedComponents (PrimeSpectrum ↑H.obj))) : H.componentCoordinateBialgHom x = H.componentCoordinateMap x

The component coordinate bialgebra morphism agrees pointwise with its underlying algebra map.

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentCoordinateBialgHom_injective {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : Function.Injective ⇑H.componentCoordinateBialgHom

The component coordinate bialgebra morphism is injective.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentCoordinateHom {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : ↧(ConstantGroup.coordinateRing k (ConnectedComponents (PrimeSpectrum ↑H.obj))) ⟶ H.obj

The component coordinate morphism in the category of commutative Hopf algebras. Relative spectrum reverses it to the canonical morphism from the affine group to the finite constant group of connected components.

Equations

• H.componentCoordinateHom = CommHopfAlgCat.ofHom H.componentCoordinateBialgHom

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentCoordinateHom_apply {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (x : ConstantGroup.coordinateRing k (ConnectedComponents (PrimeSpectrum ↑H.obj))) : (CommHopfAlgCat.Hom.hom H.componentCoordinateHom) x = H.componentCoordinateMap x

The component coordinate morphism agrees pointwise with the component coordinate map.

theorem TauCeti.FiniteTypeCommHopfAlgCat.kernelHopfIdeal_componentCoordinateHom {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : CommHopfAlgCat.kernelHopfIdeal H.componentCoordinateHom = HopfAlgebra.identityComponentHopfIdeal

The scheme-theoretic kernel of the component morphism is the identity component: the kernel Hopf ideal generated by the augmentation ideal of the constant component group is precisely the identity-component Hopf ideal.