The identity-component affine group scheme

Let H be a finite-type commutative Hopf algebra over an algebraically closed field. The ideal cutting out the connected component of the counit point is a Hopf ideal. This file takes its quotient Hopf algebra and packages the corresponding Hopf spectrum as the identity-component affine group scheme G⁰.

The underlying prime spectrum is canonically homeomorphic to the connected component of the augmentation point in Spec H. The morphism G⁰ ⟶ G is the closed immersion induced by the quotient coordinate map. On rational points its image consists exactly of the points whose kernel belongs to the augmentation point's connected component.

The identity component is geometrically connected: over the algebraically closed ground field, ordinary connectedness is already geometric connectedness. This provides the connectedness hypothesis used when testing identity components of closed subgroups against a geometric radical.

Main declarations

• TauCeti.FiniteTypeCommHopfAlgCat.identityComponent: the quotient coordinate Hopf algebra of the identity component.
• TauCeti.FiniteTypeCommHopfAlgCat.geometricallyConnected_identityComponent: geometric connectedness of the identity component.
• TauCeti.FiniteTypeCommHopfAlgCat.identityComponentSpec: its affine group scheme.
• TauCeti.FiniteTypeCommHopfAlgCat.geometricallyConnected_identityComponentSpec: geometric connectedness of its structural morphism.
• TauCeti.FiniteTypeCommHopfAlgCat.identityComponentSpecι: the canonical closed immersion into the ambient affine group scheme.
• TauCeti.FiniteTypeCommHopfAlgCat.identityComponentPrimeSpectrumHomeomorph: the identification of its spectrum with the augmentation point's connected component.
• TauCeti.FiniteTypeCommHopfAlgCat.identityComponentPointsHom: the inclusion on points.
• TauCeti.FiniteTypeCommHopfAlgCat.mem_range_identityComponentPointsHom_iff: the corresponding characterization on rational points.

References

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

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteTypeCommHopfAlgCat.identityComponent {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : FiniteTypeCommHopfAlgCat k

The finite-type coordinate Hopf algebra of the identity component.

It is the quotient by the Hopf ideal cutting out the connected component of the counit point.

Equations

• H.identityComponent = H.quotient TauCeti.HopfAlgebra.identityComponentHopfIdeal

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.identityComponentCoordinateMap {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : H ⟶ H.identityComponent

The coordinate morphism from an affine group to its identity component. Contravariantly, this is the inclusion of the identity-component group scheme into the ambient group scheme.

Equations

• H.identityComponentCoordinateMap = H.mkQuotient TauCeti.HopfAlgebra.identityComponentHopfIdeal

theorem TauCeti.FiniteTypeCommHopfAlgCat.identityComponentCoordinateMap_ker {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : RingHom.ker (↑(toBialgHom H.identityComponentCoordinateMap)).toRingHom = PrimeSpectrum.connectedComponentIdeal (Bialgebra.augmentationPoint k ↑H.obj)

The kernel of the identity-component coordinate morphism is the ideal cutting out the connected component of the augmentation point.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.identityComponentPrimeSpectrumHomeomorph {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : PrimeSpectrum ↑H.identityComponent.obj ≃ₜ ↑(connectedComponent (Bialgebra.augmentationPoint k ↑H.obj))

The prime spectrum of the identity-component coordinate algebra is canonically homeomorphic to the connected component of the augmentation point.

Equations

• H.identityComponentPrimeSpectrumHomeomorph = id ((PrimeSpectrum.quotientHomeomorphZeroLocus TauCeti.HopfAlgebra.identityComponentHopfIdeal.toIdeal).trans (Homeomorph.setCongr ⋯))

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.identityComponentPrimeSpectrumHomeomorph_apply_coe {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (x : PrimeSpectrum ↑H.identityComponent.obj) : ↑(H.identityComponentPrimeSpectrumHomeomorph x) = PrimeSpectrum.comap (↑(toBialgHom H.identityComponentCoordinateMap)).toRingHom x

After coercion to the ambient prime spectrum, the identity-component homeomorphism sends a point to its contraction along the identity-component coordinate map.

instance TauCeti.FiniteTypeCommHopfAlgCat.connectedSpace_identityComponent {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : ConnectedSpace (PrimeSpectrum ↑H.identityComponent.obj)

The spectrum of the identity-component coordinate algebra is connected.

theorem TauCeti.FiniteTypeCommHopfAlgCat.geometricallyConnected_identityComponent {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : geometricallyConnectedCommHopfAlgProperty k H.identityComponent.obj

The identity component of a finite-type affine group over an algebraically closed field is geometrically connected, even when the group is not smooth.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.identityComponentSpec {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))

The identity-component affine group scheme represented by identityComponent H.

Equations

• H.identityComponentSpec = TauCeti.CommHopfAlgCat.quotientSpec H.obj TauCeti.HopfAlgebra.identityComponentHopfIdeal

instance TauCeti.FiniteTypeCommHopfAlgCat.geometricallyConnected_identityComponentSpec {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : AlgebraicGeometry.GeometricallyConnected H.identityComponentSpec.X.hom

The structural morphism of the identity-component affine group scheme is geometrically connected.

theorem TauCeti.FiniteTypeCommHopfAlgCat.identityComponentSpec_X_left {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : H.identityComponentSpec.X.left = AlgebraicGeometry.Spec ↧↑H.identityComponent.obj

The identity-component group scheme is represented by its coordinate Hopf algebra.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.identityComponentSpecPrimeSpectrumHomeomorph {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : ↥H.identityComponentSpec.X.left ≃ₜ PrimeSpectrum ↑H.identityComponent.obj

The carrier of the identity-component group scheme is canonically the prime spectrum of its coordinate Hopf algebra.

Equations

• H.identityComponentSpecPrimeSpectrumHomeomorph = (CategoryTheory.eqToIso ⋯).schemeIsoToHomeo

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.identityComponentSpecι {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : H.identityComponentSpec ⟶ (AlgebraicGeometry.hopfSpec ↧k).obj (Opposite.op H.obj)

The canonical morphism from the identity-component affine group scheme to the ambient affine group scheme.

Equations

• H.identityComponentSpecι = TauCeti.CommHopfAlgCat.quotientSpecι H.obj TauCeti.HopfAlgebra.identityComponentHopfIdeal

instance TauCeti.FiniteTypeCommHopfAlgCat.isClosedImmersion_identityComponentSpecι {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left H.identityComponentSpecι.hom.hom)

The canonical inclusion of the identity-component affine group scheme is a closed immersion.

instance TauCeti.FiniteTypeCommHopfAlgCat.connectedSpace_identityComponentSpec {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : ConnectedSpace ↥H.identityComponentSpec.X.left

The scheme underlying the identity-component group scheme has connected carrier.

theorem TauCeti.FiniteTypeCommHopfAlgCat.identityComponentSpecι_apply {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (x : ↥H.identityComponentSpec.X.left) : (CategoryTheory.Over.Hom.left H.identityComponentSpecι.hom.hom) x = PrimeSpectrum.comap (↑(toBialgHom H.identityComponentCoordinateMap)).toRingHom (H.identityComponentSpecPrimeSpectrumHomeomorph x)

On underlying topological spaces, the identity-component inclusion is contraction along the quotient coordinate map.

theorem TauCeti.FiniteTypeCommHopfAlgCat.range_identityComponentSpecι {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : Set.range ⇑(CategoryTheory.Over.Hom.left H.identityComponentSpecι.hom.hom) = connectedComponent (Bialgebra.augmentationPoint k ↑H.obj)

The image of the identity-component inclusion on underlying topological spaces is exactly the connected component of the augmentation point.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.identityComponentPointsHom {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (A : CommAlgCat k) : HopfAlgebra.points A ⟶ HopfAlgebra.points A

The canonical inclusion from the identity component to the ambient group on A-points.

Equations

• H.identityComponentPointsHom A = TauCeti.CommHopfAlgCat.quotientPointsHom H.obj TauCeti.HopfAlgebra.identityComponentHopfIdeal A

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.range_identityComponentPointsHom {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (A : CommAlgCat k) : (GrpCat.Hom.hom (H.identityComponentPointsHom A)).range = CommHopfAlgCat.quotientPointsSubgroup H.obj HopfAlgebra.identityComponentHopfIdeal A

The range of the identity-component point inclusion is the subgroup cut out by the identity-component Hopf ideal.

theorem TauCeti.FiniteTypeCommHopfAlgCat.mem_range_identityComponentPointsHom_iff {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (g : ↑(HopfAlgebra.points ↧k)) : g ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (H.identityComponentPointsHom ↧k)) ↔ AlgHom.kernelPoint g.ofConv ∈ connectedComponent (Bialgebra.augmentationPoint k ↑H.obj)

A rational point of the ambient affine group lies in the image of the identity-component points exactly when its kernel point belongs to the connected component of the augmentation point.