Constant finite group schemes

For a finite group G and a commutative ring R, this file applies relative spectrum to the Hopf algebra of functions G → R. The result is the constant affine group scheme associated to G. A group homomorphism induces a morphism of these group schemes in the same direction, contravariantly to pullback of coordinate functions.

The structural morphism of a constant finite group scheme is finite and étale. Finiteness comes from the finite free function algebra, while étaleness is the scheme-side form of the finite-product étaleness proved for the coordinate ring.

This is the scheme-side representer required for the identity-component and component-group milestone in Layer 3 of the ReductiveGroups roadmap. Once the component coordinate morphism is available, its relative spectrum has this object as target; identifying that morphism with the fppf quotient remains downstream.

Main declarations

• TauCeti.ConstantGroup.groupScheme: the constant affine group scheme attached to G.
• TauCeti.ConstantGroup.groupSchemeMap: the group-scheme morphism induced by a group homomorphism.
• TauCeti.ConstantGroup.groupSchemePointMulEquiv: the canonical comparison between algebra-valued coordinate points and scheme-valued points.
• TauCeti.ConstantGroup.isFinite_groupScheme: the structural morphism is finite.
• TauCeti.ConstantGroup.etale_groupScheme: the structural morphism is étale.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 2.
• J. S. Milne, Algebraic Groups (2017), Section 2.a.

The groupScheme and groupSchemeMap constructions follow the scheme-level pattern in TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.Scheme.Basic. The scheme-points presentation follows TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.Scheme.Points and TauCeti.Algebra.AlgebraicGroup.AdditiveGroup.Scheme, using the generic TauCeti.Algebra.AlgebraicGroup.CommHopfAlgCat.SchemePoints interface.

noncomputable def TauCeti.ConstantGroup.groupScheme (R : Type u) [CommRing R] (G : Type u) [Group G] [Finite G] : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The constant affine group scheme attached to a finite group G over R.

Equations

• TauCeti.ConstantGroup.groupScheme R G = (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op ↧(TauCeti.ConstantGroup.coordinateRing R G))

theorem TauCeti.ConstantGroup.groupScheme_def (R : Type u) [CommRing R] (G : Type u) [Group G] [Finite G] : groupScheme R G = (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op ↧(coordinateRing R G))

The constant group scheme is relative spectrum applied to its coordinate Hopf algebra.

@[simp]

theorem TauCeti.ConstantGroup.groupScheme_X_left (R : Type u) [CommRing R] (G : Type u) [Group G] [Finite G] : (groupScheme R G).X.left = AlgebraicGeometry.Spec ↧(coordinateRing R G)

The scheme underlying the constant group scheme is the spectrum of its function algebra.

@[simp]

theorem TauCeti.ConstantGroup.groupScheme_X_hom (R : Type u) [CommRing R] (G : Type u) [Group G] [Finite G] : (groupScheme R G).X.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (coordinateRing R G))))

The structural morphism of the constant group scheme is induced by the scalar inclusion into its function algebra.

noncomputable def TauCeti.ConstantGroup.groupSchemeMap (R : Type u) [CommRing R] {G : Type u} [Group G] [Finite G] {H : Type u} [Group H] [Finite H] (f : G →* H) : groupScheme R G ⟶ groupScheme R H

A homomorphism of finite groups induces a morphism of their constant group schemes.

Equations

• TauCeti.ConstantGroup.groupSchemeMap R f = (AlgebraicGeometry.hopfSpec ↧R).map (CommHopfAlgCat.ofHom (TauCeti.ConstantGroup.coordinateBialgHom R G H f)).op

theorem TauCeti.ConstantGroup.groupSchemeMap_def (R : Type u) [CommRing R] {G : Type u} [Group G] [Finite G] {H : Type u} [Group H] [Finite H] (f : G →* H) : groupSchemeMap R f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (CommHopfAlgCat.ofHom (coordinateBialgHom R G H f)).op) (CategoryTheory.eqToHom ⋯))

The constant-group-scheme morphism is relative spectrum applied to pullback of coordinate functions.

@[simp]

theorem TauCeti.ConstantGroup.groupSchemeMap_hom_left (R : Type u) [CommRing R] {G : Type u} [Group G] [Finite G] {H : Type u} [Group H] [Finite H] (f : G →* H) : CategoryTheory.Over.Hom.left (groupSchemeMap R f).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(coordinateMap R G H f))) (CategoryTheory.eqToHom ⋯))

The underlying scheme map of groupSchemeMap f is spectrum applied to pullback of coordinate functions along f.

@[simp]

theorem TauCeti.ConstantGroup.groupSchemeMap_id (R : Type u) [CommRing R] {G : Type u} [Group G] [Finite G] : groupSchemeMap R (MonoidHom.id G) = CategoryTheory.CategoryStruct.id (groupScheme R G)

The identity group homomorphism induces the identity morphism of constant group schemes.

@[simp]

theorem TauCeti.ConstantGroup.groupSchemeMap_comp (R : Type u) [CommRing R] {G : Type u} [Group G] [Finite G] {H K : Type u} [Group H] [Finite H] [Group K] [Finite K] (f : G →* H) (q : H →* K) : groupSchemeMap R (q.comp f) = CategoryTheory.CategoryStruct.comp (groupSchemeMap R f) (groupSchemeMap R q)

Composition of homomorphisms is preserved by the associated constant-group-scheme maps.

noncomputable def TauCeti.ConstantGroup.groupSchemePointMulEquiv (R : Type u) [CommRing R] (G : Type u) [Group G] [Finite G] (A : Type u) [CommRing A] [Algebra R A] : WithConv (coordinateRing R G →ₐ[R] A) ≃* ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R G).X)

Algebra-valued points of the coordinate Hopf algebra are canonically the scheme-valued points of the constant group scheme.

Equations

• TauCeti.ConstantGroup.groupSchemePointMulEquiv R G A = TauCeti.CommHopfAlgCat.mapMulEquivOfPresentation (↧(TauCeti.ConstantGroup.coordinateRing R G)) A ⋯

@[simp]

theorem TauCeti.ConstantGroup.groupSchemePointMulEquiv_apply_left (R : Type u) [CommRing R] (G : Type u) [Group G] [Finite G] (A : Type u) [CommRing A] [Algebra R A] (p : WithConv (coordinateRing R G →ₐ[R] A)) : CategoryTheory.Over.Hom.left ((groupSchemePointMulEquiv R G A) p) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑p.ofConv)) (CategoryTheory.eqToHom ⋯)

Under groupSchemePointMulEquiv, an algebra point is represented by its spectrum map.

@[simp]

theorem TauCeti.ConstantGroup.groupSchemePointMulEquiv_groupSchemeMap (R : Type u) [CommRing R] (G : Type u) [Group G] [Finite G] {H : Type u} [Group H] [Finite H] (A : Type u) [CommRing A] [Algebra R A] (f : G →* H) (p : WithConv (coordinateRing R G →ₐ[R] A)) : CategoryTheory.CategoryStruct.comp ((groupSchemePointMulEquiv R G A) p) (groupSchemeMap R f).hom.hom = (groupSchemePointMulEquiv R H A) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (CommHopfAlgCat.ofHom (coordinateBialgHom R G H f))).app ↧A)) p)

The scheme-valued point comparison is natural in the finite group: applying the group-scheme map induced by f is precomposition by pullback of coordinate functions.

instance TauCeti.ConstantGroup.isAffine_groupScheme (R : Type u) [CommRing R] (G : Type u) [Group G] [Finite G] : AlgebraicGeometry.IsAffine (groupScheme R G).X.left

The constant group scheme is affine.

instance TauCeti.ConstantGroup.isFinite_groupScheme (R : Type u) [CommRing R] (G : Type u) [Group G] [Finite G] : AlgebraicGeometry.IsFinite (groupScheme R G).X.hom

The structural morphism of a constant finite group scheme is finite.

instance TauCeti.ConstantGroup.etale_groupScheme (R : Type u) [CommRing R] (G : Type u) [Group G] [Finite G] : AlgebraicGeometry.Etale (groupScheme R G).X.hom

The structural morphism of a constant finite group scheme is étale.