Representability of the component group

Let H be the coordinate Hopf algebra of a finite-type affine group over an algebraically closed field. This file identifies the fppf quotient H / H⁰ with the fppf points sheaf of the finite constant group of connected components of Spec H.

The key point is stronger than local surjectivity. Every point of the constant component group over a test algebra lifts to a point of H: its orthogonal idempotents split the test algebra into components, and on each component one uses a chosen rational point of the corresponding connected component of Spec H. The kernel calculation for the component coordinate morphism then identifies the pointwise quotient with the constant-group points. Sheafifying this natural isomorphism gives the desired representability.

Main declarations

• TauCeti.FiniteTypeCommHopfAlgCat.componentPointsHom_surjective: the component morphism is surjective on points over every test algebra.
• TauCeti.FiniteTypeCommHopfAlgCat.componentPointwiseQuotientMulEquiv: the pointwise quotient by the identity component is the constant component group.
• TauCeti.FiniteTypeCommHopfAlgCat.componentGroupFppfGroupObjectIso: the fppf component-group quotient is represented by the finite constant group scheme, compatibly with its group structure.
• componentGroupFppfProjection_comp_componentGroupFppfGroupObjectIso_hom: the representability isomorphism identifies the quotient projection with the sheafified component-coordinate morphism.

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 completes the algebraically closed-field representability step of Layer 3, "Identity component G° and component group π₀(G)", of the ReductiveGroups roadmap.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentPointsHom {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (A : CommAlgCat k) : ↑(HopfAlgebra.points A) →* ↑(HopfAlgebra.points A)

The component-coordinate morphism on points over a commutative test algebra.

Equations

• H.componentPointsHom A = TauCeti.AlgHom.mapDomain (CommHopfAlgCat.Hom.hom H.componentCoordinateHom)

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentPointsHom_apply {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (A : CommAlgCat k) (g : ↑(HopfAlgebra.points A)) : (H.componentPointsHom A) g = WithConv.toConv (g.ofConv.comp ↑(CommHopfAlgCat.Hom.hom H.componentCoordinateHom))

The component morphism on points is precomposition with the component coordinate map.

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentPointsHom_surjective {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (A : CommAlgCat k) : Function.Surjective ⇑(H.componentPointsHom A)

The component-coordinate morphism is surjective on points over every commutative test algebra.

@[instance_reducible]

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentPointwiseQuotientGroup {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (A : CommAlgCat k) : Group ↑(CommHopfAlgCat.pointwiseQuotientGroup H.obj HopfAlgebra.identityComponentHopfIdeal ⋯ A)

The group structure on the pointwise quotient, exposed locally for the first isomorphism theorem.

Equations

• H.componentPointwiseQuotientGroup A = (TauCeti.CommHopfAlgCat.pointwiseQuotientGroup H.obj TauCeti.HopfAlgebra.identityComponentHopfIdeal ⋯ A).str

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentPointwiseQuotientMulEquiv {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (A : CommAlgCat k) : ↑(CommHopfAlgCat.pointwiseQuotientGroup H.obj HopfAlgebra.identityComponentHopfIdeal ⋯ A) ≃* ↑(HopfAlgebra.points A)

The pointwise quotient by the identity component is canonically the group of points of the finite constant component group.

Equations

• H.componentPointwiseQuotientMulEquiv A = (QuotientGroup.quotientMulEquivOfEq ⋯).trans (QuotientGroup.quotientKerEquivOfSurjective (H.componentPointsHom A) ⋯)

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentPointwiseQuotientMulEquiv_mk {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (A : CommAlgCat k) (g : ↑(HopfAlgebra.points A)) : (H.componentPointwiseQuotientMulEquiv A) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.pointwiseQuotientMk H.obj HopfAlgebra.identityComponentHopfIdeal ⋯ A)) g) = (H.componentPointsHom A) g

The pointwise component-group equivalence sends the class of an ambient point to its image under the component-coordinate morphism.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.mapPoints_componentPointsHom {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) {A B : CommAlgCat k} (f : A ⟶ B) (g : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints f)) ((H.componentPointsHom A) g) = (H.componentPointsHom B) ((CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints f)) g)

The component morphism on points commutes with extension of the value algebra.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentPointwiseQuotientNatIso {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : CommHopfAlgCat.pointwiseQuotientFunctor H.obj HopfAlgebra.identityComponentHopfIdeal ⋯ ≅ HopfAlgebra.pointsFunctor

The pointwise quotient functor by the identity component is naturally isomorphic to the functor of points of the finite constant component group.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentPointwiseQuotientPresheafGrpIso {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : CommHopfAlgCat.pointwiseQuotientPresheafGrp H.obj HopfAlgebra.identityComponentHopfIdeal ⋯ ≅ CommHopfAlgCat.pointsPresheafGrp ↧(ConstantGroup.coordinateRing k (ConnectedComponents (PrimeSpectrum ↑H.obj)))

Before sheafification, the pointwise component quotient and the constant component group are isomorphic as group objects in type-valued presheaves on the affine fppf site.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentPointwiseQuotientPresheafIso {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : (CommHopfAlgCat.pointwiseQuotientPresheafGrp H.obj HopfAlgebra.identityComponentHopfIdeal ⋯).X ≅ (CommHopfAlgCat.pointsPresheafGrp ↧(ConstantGroup.coordinateRing k (ConnectedComponents (PrimeSpectrum ↑H.obj)))).X

Before sheafification, the pointwise component quotient and the constant component group are isomorphic as type-valued presheaves on the affine fppf site.

Equations

• H.componentPointwiseQuotientPresheafIso = (CategoryTheory.Grp.forget (CategoryTheory.Functor (CommAlgCat k)ᵒᵖᵒᵖ (Type (?u.1 + 1)))).mapIso H.componentPointwiseQuotientPresheafGrpIso

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentGroupFppfGroupObjectIso {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : H.componentGroupFppfSheaf ≅ CommHopfAlgCat.pointsFppfGroupObject ↧(ConstantGroup.coordinateRing k (ConnectedComponents (PrimeSpectrum ↑H.obj)))

The fppf component-group quotient is represented by the finite constant group scheme, compatibly with multiplication, the unit, and inversion.

Equations

• One or more equations did not get rendered due to their size.

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

The component-coordinate morphism on fppf points, obtained by sheafifying precomposition with componentCoordinateHom.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentGroupFppfProjection_comp_componentGroupFppfGroupObjectIso_hom {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : CategoryTheory.CategoryStruct.comp H.componentGroupFppfProjection H.componentGroupFppfGroupObjectIso.hom = H.componentCoordinateFppfGroupObjectHom

The representability isomorphism carries the component-group quotient projection to the sheafification of the component-coordinate morphism on points.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentGroupFppfSheafIso {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : H.componentGroupFppfSheaf.X ≅ (CommHopfAlgCat.pointsFppfGroupObject ↧(ConstantGroup.coordinateRing k (ConnectedComponents (PrimeSpectrum ↑H.obj)))).X

The underlying fppf sheaf of the component-group quotient is represented by the finite constant group scheme on the connected components of the prime spectrum.

Equations

• H.componentGroupFppfSheafIso = (CategoryTheory.Grp.forget (CategoryTheory.Sheaf (TauCeti.CommAlgCat.fppfTopology k) (Type (?u.1 + 1)))).mapIso H.componentGroupFppfGroupObjectIso