Constant finite groups

Let G be a finite group and R a commutative ring. The coordinate ring of the constant R-group associated to G is the function algebra G → R. We construct it intrinsically as the finite Hopf dual of the group algebra R[G]. This supplies its Hopf structure without making choices and proves that its underlying algebra is finite étale over R.

The formulas below identify multiplication, comultiplication, counit, and antipode with the usual pointwise product, group multiplication, identity, and inversion. Evaluation at a group element is then an algebra point, and these evaluations multiply exactly as the elements of G do.

Main declarations

• TauCeti.ConstantGroup.coordinateRing: the Hopf algebra of functions on a finite group.
• TauCeti.ConstantGroup.functionAlgEquiv: its canonical equivalence with G → R.
• TauCeti.ConstantGroup.eval: evaluation at a group element as an algebra homomorphism.
• TauCeti.ConstantGroup.toPoints: the group homomorphism from G to its algebra points.
• TauCeti.ConstantGroup.coordinateBialgHom: contravariant pullback along a group homomorphism.

References

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

@[reducible, inline]

abbrev TauCeti.ConstantGroup.coordinateRing (R : Type u) [CommRing R] (G : Type v) : Type (max v u)

The coordinate ring of the constant group attached to a finite group G over R.

It is defined as the finite Hopf dual of the group algebra.

Equations

• TauCeti.ConstantGroup.coordinateRing R G = TauCeti.ConvolutionDual R (MonoidAlgebra R G)

noncomputable def TauCeti.ConstantGroup.functionLinearEquiv (R : Type u) [CommRing R] (G : Type v) [Finite G] : coordinateRing R G ≃ₗ[R] G → R

The underlying linear equivalence between the coordinate ring and the algebra of functions on G.

Equations

• TauCeti.ConstantGroup.functionLinearEquiv R G = (WithConv.linearEquiv R (Module.Dual R (MonoidAlgebra R G))).trans (MonoidAlgebra.basis G R).dualBasis.equivFun

@[simp]

theorem TauCeti.ConstantGroup.functionLinearEquiv_apply (R : Type u) [CommRing R] (G : Type v) [Finite G] (f : coordinateRing R G) (g : G) : (functionLinearEquiv R G) f g = f.ofConv (MonoidAlgebra.single g 1)

noncomputable def TauCeti.ConstantGroup.functionAlgEquiv (R : Type u) [CommRing R] (G : Type v) [Finite G] : coordinateRing R G ≃ₐ[R] G → R

The coordinate ring of a finite constant group is canonically the function algebra G → R.

Equations

• TauCeti.ConstantGroup.functionAlgEquiv R G = AlgEquiv.ofLinearEquiv (TauCeti.ConstantGroup.functionLinearEquiv R G) ⋯ ⋯

@[simp]

theorem TauCeti.ConstantGroup.functionAlgEquiv_apply (R : Type u) [CommRing R] (G : Type v) [Finite G] (f : coordinateRing R G) (g : G) : (functionAlgEquiv R G) f g = f.ofConv (MonoidAlgebra.single g 1)

instance TauCeti.ConstantGroup.instEtale (R : Type u) [CommRing R] (G : Type v) [Finite G] : Algebra.Etale R (coordinateRing R G)

The coordinate ring of a finite constant group is finite étale over the base ring.

noncomputable def TauCeti.ConstantGroup.eval (R : Type u) [CommRing R] (G : Type v) [Finite G] (g : G) : coordinateRing R G →ₐ[R] R

Evaluation at a group element, regarded as an algebra point of the constant group.

Equations

• TauCeti.ConstantGroup.eval R G g = (Pi.evalAlgHom R (fun (x : G) => R) g).comp ↑(TauCeti.ConstantGroup.functionAlgEquiv R G)

@[simp]

theorem TauCeti.ConstantGroup.eval_apply (R : Type u) [CommRing R] (G : Type v) [Finite G] (g : G) (f : coordinateRing R G) : (eval R G g) f = (functionAlgEquiv R G) f g

theorem TauCeti.ConstantGroup.comul_apply (R : Type u) [CommRing R] (G : Type v) [Finite G] [Group G] (f : coordinateRing R G) (g h : G) : ((ConvolutionDual.dualDistribEquiv R (MonoidAlgebra R G)) (CoalgebraStruct.comul f)) (MonoidAlgebra.single g 1 ⊗ₜ[R] MonoidAlgebra.single h 1) = (functionAlgEquiv R G) f (g * h)

Comultiplication on the coordinate ring is dual to multiplication in G.

theorem TauCeti.ConstantGroup.counit_apply (R : Type u) [CommRing R] (G : Type v) [Finite G] [Group G] (f : coordinateRing R G) : CoalgebraStruct.counit f = (functionAlgEquiv R G) f 1

The counit of the coordinate ring is evaluation at the identity of G.

theorem TauCeti.ConstantGroup.antipode_apply (R : Type u) [CommRing R] (G : Type v) [Finite G] [Group G] (f : coordinateRing R G) (g : G) : (functionAlgEquiv R G) ((HopfAlgebraStruct.antipode R) f) g = (functionAlgEquiv R G) f g⁻¹

The antipode of the coordinate ring sends a function f to g ↦ f (g⁻¹).

theorem TauCeti.ConstantGroup.eval_mul (R : Type u) [CommRing R] (G : Type v) [Finite G] [Group G] (g h : G) : WithConv.toConv (eval R G (g * h)) = WithConv.toConv (eval R G g) * WithConv.toConv (eval R G h)

Evaluation points multiply according to multiplication in G.

theorem TauCeti.ConstantGroup.eval_one (R : Type u) [CommRing R] (G : Type v) [Finite G] [Group G] : WithConv.toConv (eval R G 1) = 1

Evaluation at the identity is the identity element among algebra points.

noncomputable def TauCeti.ConstantGroup.toPoints (R : Type u) [CommRing R] (G : Type v) [Finite G] [Group G] : G →* WithConv (coordinateRing R G →ₐ[R] R)

A finite group maps canonically to the group of algebra points of its constant group.

Equations

• TauCeti.ConstantGroup.toPoints R G = { toFun := fun (g : G) => WithConv.toConv (TauCeti.ConstantGroup.eval R G g), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.ConstantGroup.toPoints_apply (R : Type u) [CommRing R] (G : Type v) [Finite G] [Group G] (g : G) : ((toPoints R G) g).ofConv = eval R G g

theorem TauCeti.ConstantGroup.toPoints_injective (R : Type u) [CommRing R] (G : Type v) [Finite G] [Group G] [Nontrivial R] : Function.Injective ⇑(toPoints R G)

Over a nontrivial base ring, evaluation distinguishes the elements of the constant group.

noncomputable def TauCeti.ConstantGroup.coordinateBialgHom (R : Type u) [CommRing R] (G : Type v) [Finite G] [Group G] (H : Type w) [Group H] [Finite H] (f : G →* H) : coordinateRing R H →ₐc[R] coordinateRing R G

A group homomorphism induces a contravariant bialgebra morphism of constant-group coordinate rings.

Equations

• TauCeti.ConstantGroup.coordinateBialgHom R G H f = TauCeti.ConvolutionDual.map R (MonoidAlgebra.mapDomainBialgHom R f)

noncomputable def TauCeti.ConstantGroup.coordinateMap (R : Type u) [CommRing R] (G : Type v) [Finite G] [Group G] (H : Type w) [Group H] [Finite H] (f : G →* H) : coordinateRing R H →ₐ[R] coordinateRing R G

The underlying algebra homomorphism of coordinateBialgHom.

Equations

• TauCeti.ConstantGroup.coordinateMap R G H f = ↑(TauCeti.ConstantGroup.coordinateBialgHom R G H f)

@[simp]

theorem TauCeti.ConstantGroup.coordinateBialgHom_toAlgHom (R : Type u) [CommRing R] (G : Type v) [Finite G] [Group G] (H : Type w) [Group H] [Finite H] (f : G →* H) : ↑(coordinateBialgHom R G H f) = coordinateMap R G H f

The algebra homomorphism underlying coordinateBialgHom is coordinateMap.

theorem TauCeti.ConstantGroup.functionAlgEquiv_coordinateMap_apply (R : Type u) [CommRing R] (G : Type v) [Finite G] [Group G] (H : Type w) [Group H] [Finite H] (f : G →* H) (a : coordinateRing R H) (g : G) : (functionAlgEquiv R G) ((coordinateMap R G H f) a) g = (functionAlgEquiv R H) a (f g)

Under functionAlgEquiv, the coordinate map is precomposition by the group homomorphism.

@[simp]

theorem TauCeti.ConstantGroup.coordinateMap_id (R : Type u) [CommRing R] (G : Type v) [Finite G] [Group G] : coordinateMap R G G (MonoidHom.id G) = AlgHom.id R (coordinateRing R G)

The coordinate map induced by the identity group homomorphism is the identity.

@[simp]

theorem TauCeti.ConstantGroup.coordinateMap_comp (R : Type u) [CommRing R] (G : Type v) [Finite G] [Group G] (H : Type w) [Group H] [Finite H] (K : Type u_1) [Group K] [Finite K] (f : G →* H) (q : H →* K) : coordinateMap R G K (q.comp f) = (coordinateMap R G H f).comp (coordinateMap R H K q)

Coordinate maps reverse composition of group homomorphisms.

@[simp]

theorem TauCeti.ConstantGroup.eval_comp_coordinateMap (R : Type u) [CommRing R] (G : Type v) [Finite G] [Group G] (H : Type w) [Group H] [Finite H] (f : G →* H) (g : G) : (eval R G g).comp (coordinateMap R G H f) = eval R H (f g)

Evaluation is natural with respect to the coordinate map induced by a group homomorphism.