Cartier duals of finite constant and diagonalizable groups

For a finite commutative group G over a commutative ring R, the constant group and the diagonalizable group D(G) are Cartier dual. The constant coordinate algebra is already the finite convolution dual of R[G]; double-dual evaluation therefore supplies the comparison in the other direction. These identifications concern the existing group schemes, with their group laws, and hold without invertibility assumptions on the order of G.

For G = Multiplicative (ZMod N), with positive N, D(G) is the group scheme μ_N. Thus the two isomorphisms specialize to the duality of the constant cyclic group and μ_N.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 2.
• SGA 3, Exposé VIIA, §3.3.

The coordinate construction is ConstantGroup.coordinateRing; biduality is ConvolutionDual.evalBialgEquiv. The group-scheme comparisons use the transported FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDuality and the existing constant and diagonalizable groupScheme constructions.

noncomputable def TauCeti.DiagonalizableGroup.finiteLocallyFreeGroupScheme (R : Type u) [CommRing R] (G : FGCommGrpCat) [Finite ↑G] : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R

The finite diagonalizable group scheme bundled as a finite locally free commutative affine group scheme.

Equations

• TauCeti.DiagonalizableGroup.finiteLocallyFreeGroupScheme R G = { obj := { obj := TauCeti.DiagonalizableGroup.groupScheme R G, property := ⋯ }, property := ⋯ }

@[simp]

theorem TauCeti.DiagonalizableGroup.finiteLocallyFreeGroupScheme_obj_obj (R : Type u) [CommRing R] (G : FGCommGrpCat) [Finite ↑G] : (finiteLocallyFreeGroupScheme R G).obj.obj = groupScheme R G

Forgetting finite local freeness recovers the existing diagonalizable group scheme.

noncomputable def TauCeti.DiagonalizableGroup.finiteLocallyFreeGroupSchemeIso (R : Type u) [CommRing R] (G : FGCommGrpCat) [Finite ↑G] : (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).functor.obj (Opposite.op (FiniteLocallyFreeBicommutativeHopfAlgCat.of R (MonoidAlgebra R ↑G))) ≅ finiteLocallyFreeGroupScheme R G

The Hopf--spectrum anti-equivalence sends the group algebra to the finite diagonalizable group scheme.

Equations

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

noncomputable def TauCeti.ConstantGroup.finiteLocallyFreeGroupScheme (R : Type u) [CommRing R] (G : Type u) [CommGroup G] [Finite G] : FiniteLocallyFreeCommAffineGroupSchemeCat ↧R

The finite constant group scheme bundled as a finite locally free commutative affine group scheme.

Equations

• TauCeti.ConstantGroup.finiteLocallyFreeGroupScheme R G = { obj := { obj := TauCeti.ConstantGroup.groupScheme R G, property := ⋯ }, property := ⋯ }

@[simp]

theorem TauCeti.ConstantGroup.finiteLocallyFreeGroupScheme_obj_obj (R : Type u) [CommRing R] (G : Type u) [CommGroup G] [Finite G] : (finiteLocallyFreeGroupScheme R G).obj.obj = groupScheme R G

Forgetting finite local freeness recovers the existing constant group scheme.

noncomputable def TauCeti.ConstantGroup.finiteLocallyFreeGroupSchemeIso (R : Type u) [CommRing R] (G : Type u) [CommGroup G] [Finite G] : (finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).functor.obj (Opposite.op (FiniteLocallyFreeBicommutativeHopfAlgCat.of R (coordinateRing R G))) ≅ finiteLocallyFreeGroupScheme R G

The Hopf--spectrum anti-equivalence sends the finite dual of the group algebra to the finite constant group scheme.

Equations

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

noncomputable def TauCeti.DiagonalizableGroup.cartierDualIso (R : Type u) [CommRing R] (G : FGCommGrpCat) [Finite ↑G] : FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDual R (finiteLocallyFreeGroupScheme R G) ≅ ConstantGroup.finiteLocallyFreeGroupScheme R ↑G

The Cartier dual of a finite diagonalizable group is its constant character group.

Equations

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

theorem TauCeti.DiagonalizableGroup.cartierDualIso_hom (R : Type u) [CommRing R] (G : FGCommGrpCat) [Finite ↑G] : (cartierDualIso R G).hom = CategoryTheory.CategoryStruct.comp ((FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualFunctor R).map (finiteLocallyFreeGroupSchemeIso R G).op.hom) (CategoryTheory.CategoryStruct.comp (FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualHopfSpecIso R (FiniteLocallyFreeBicommutativeHopfAlgCat.of R (MonoidAlgebra R ↑G))).hom (ConstantGroup.finiteLocallyFreeGroupSchemeIso R ↑G).hom)

The duality comparison for a diagonalizable group is finite dualization followed by the constant-group coordinate presentation. This equation characterizes the comparison without unfolding its definition.

noncomputable def TauCeti.ConstantGroup.cartierDualIso (R : Type u) [CommRing R] (G : FGCommGrpCat) [Finite ↑G] : FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDual R (finiteLocallyFreeGroupScheme R ↑G) ≅ DiagonalizableGroup.finiteLocallyFreeGroupScheme R G

The Cartier dual of a finite commutative constant group is the diagonalizable group with that character group.

Equations

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

theorem TauCeti.ConstantGroup.cartierDualIso_hom (R : Type u) [CommRing R] (G : FGCommGrpCat) [Finite ↑G] : (cartierDualIso R G).hom = CategoryTheory.CategoryStruct.comp ((FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualFunctor R).map (finiteLocallyFreeGroupSchemeIso R ↑G).op.hom) (CategoryTheory.CategoryStruct.comp (FiniteLocallyFreeCommAffineGroupSchemeCat.cartierDualHopfSpecIso R (FiniteLocallyFreeBicommutativeHopfAlgCat.of R (coordinateRing R ↑G))).hom (CategoryTheory.CategoryStruct.comp ((finiteLocallyFreeBicommutativeHopfAlgCatOpEquivFiniteLocallyFreeCommAffineGroupSchemeCat R).functor.map (FiniteLocallyFreeBicommutativeHopfAlgCat.of R (MonoidAlgebra R ↑G)).evalIso.op.hom) (DiagonalizableGroup.finiteLocallyFreeGroupSchemeIso R G).hom))

The duality comparison for a constant group is induced by double-dual evaluation on its group algebra, through the Hopf--spectrum anti-equivalence.