Diagonalizable group schemes

For a commutative ring R and a finitely generated commutative group G, the group algebra R[G] is a finite-type commutative Hopf algebra. Applying relative spectrum gives the affine group scheme

D(G) = Spec R[G]

over Spec R. A homomorphism G ⟶ H induces the coordinate morphism R[G] ⟶ R[H], so relative spectrum reverses its direction and gives D(H) ⟶ D(G). This file packages that assignment as a functor from the opposite of FGCommGrpCat to group objects in schemes over Spec R.

Every resulting group scheme is affine and locally of finite type over the base. The functor is faithful over a nontrivial base and full when the prime spectrum of the base is connected; these facts are transported from the corresponding coordinate-ring results through the full subcategory inclusion and Mathlib's fully faithful hopfSpec functor. In particular, it is fully faithful over a base with connected prime spectrum.

The pinned hopfSpec construction requires its base ring and Hopf-algebra carrier to lie in the same universe, so the scheme-level construction here uses FGCommGrpCat.{u} over a base ring in Type u.

Main declarations

• TauCeti.DiagonalizableGroup.groupScheme: the affine group scheme D(G) = Spec R[G].
• TauCeti.DiagonalizableGroup.groupScheme_one_left, TauCeti.DiagonalizableGroup.groupScheme_mul_left, and TauCeti.DiagonalizableGroup.groupScheme_inv_left: the underlying scheme maps of its group operations.
• TauCeti.DiagonalizableGroup.groupSchemeMap: the contravariant group-scheme morphism induced by a homomorphism of finitely generated commutative groups.
• TauCeti.DiagonalizableGroup.schemeFunctor: the functor FGCommGrpCatᵒᵖ ⟶ Grp (Over (Spec R)).
• TauCeti.DiagonalizableGroup.schemeFunctorIsoHopfSpec: its factorization through the coordinate-ring functor and relative spectrum.
• TauCeti.DiagonalizableGroup.isAffine_groupScheme: D(G) is affine.
• TauCeti.DiagonalizableGroup.locallyOfFiniteType_groupScheme: D(G) ⟶ Spec R is locally of finite type.
• TauCeti.DiagonalizableGroup.finiteTypeGroupScheme: D(G) bundled as a finite-type affine group scheme.
• TauCeti.DiagonalizableGroup.finiteTypeGroupSchemeIso: its comparison with the object produced by the finite-type Hopf/group-scheme anti-equivalence.
• TauCeti.DiagonalizableGroup.schemeFunctor_faithful and TauCeti.DiagonalizableGroup.schemeFunctor_full: faithfulness over a nontrivial base and fullness over a base with connected prime spectrum.
• TauCeti.DiagonalizableGroup.fullyFaithfulSchemeFunctor: the resulting fully faithful embedding over a base with connected prime spectrum.

References

Milne, Algebraic Groups, Definition 12.7 and Theorems 12.8--12.9, describes diagonalizable groups and their character groups. The affine group-scheme construction and its full faithfulness use Mathlib's AlgebraicGeometry.hopfSpec; finite generation and the coordinate-ring fullness and faithfulness are supplied by TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.FiniteType.

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

The affine group scheme D(G) = Spec R[G] represented by the group algebra of a finitely generated commutative group G.

The same-universe restriction is imposed by Mathlib's current hopfSpec construction.

Equations

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

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

The diagonalizable group scheme is obtained by applying relative spectrum to its coordinate Hopf algebra.

@[simp]

theorem TauCeti.DiagonalizableGroup.groupScheme_X_left (R : Type u) [CommRing R] (G : FGCommGrpCat) : (groupScheme R G).X.left = AlgebraicGeometry.Spec ↧(MonoidAlgebra R ↑G)

The scheme underlying D(G) is the spectrum of the group algebra R[G].

@[simp]

theorem TauCeti.DiagonalizableGroup.groupScheme_X_hom (R : Type u) [CommRing R] (G : FGCommGrpCat) : (groupScheme R G).X.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (MonoidAlgebra R ↑G))))

After identifying its source with Spec R[G], the structural morphism of D(G) is induced by the group-algebra structure map.

@[simp]

theorem TauCeti.DiagonalizableGroup.groupScheme_tensor_X_left (R : Type u) [CommRing R] (G : FGCommGrpCat) : (CategoryTheory.MonoidalCategoryStruct.tensorObj (groupScheme R G).X (groupScheme R G).X).left = CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (MonoidAlgebra R ↑G)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (MonoidAlgebra R ↑G))))

The source scheme of multiplication on D(G) is the fibre product of two copies of Spec R[G] over Spec R.

@[simp]

theorem TauCeti.DiagonalizableGroup.groupScheme_one_left (R : Type u) [CommRing R] (G : FGCommGrpCat) : CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(Bialgebra.counitAlgHom R (MonoidAlgebra R ↑G)))) (CategoryTheory.eqToHom ⋯)

The unit of D(G) is induced by the counit of the group algebra.

@[simp]

theorem TauCeti.DiagonalizableGroup.groupScheme_mul_left (R : Type u) [CommRing R] (G : FGCommGrpCat) : CategoryTheory.Over.Hom.left CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R (MonoidAlgebra R ↑G) (MonoidAlgebra R ↑G)).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(Bialgebra.comulAlgHom R (MonoidAlgebra R ↑G)))) (CategoryTheory.eqToHom ⋯)))

Multiplication on D(G) is induced by the comultiplication of the group algebra. The first transport identifies its opaque product source with the standard affine fibre product.

@[simp]

theorem TauCeti.DiagonalizableGroup.groupScheme_inv_left (R : Type u) [CommRing R] (G : FGCommGrpCat) : CategoryTheory.Over.Hom.left CategoryTheory.GrpObj.inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(HopfAlgebra.antipodeAlgHom R (MonoidAlgebra R ↑G)))) (CategoryTheory.eqToHom ⋯))

Inversion on D(G) is induced by the antipode of the group algebra.

noncomputable def TauCeti.DiagonalizableGroup.groupSchemeMap (R : Type u) [CommRing R] {G H : FGCommGrpCat} (f : G ⟶ H) : groupScheme R H ⟶ groupScheme R G

A homomorphism G ⟶ H induces the contravariant group-scheme morphism D(H) ⟶ D(G).

Equations

• TauCeti.DiagonalizableGroup.groupSchemeMap R f = (AlgebraicGeometry.hopfSpec ↧R).map (TauCeti.DiagonalizableGroup.coordinateMap R f).hom.op

theorem TauCeti.DiagonalizableGroup.groupSchemeMap_def (R : Type u) [CommRing R] {G H : FGCommGrpCat} (f : G ⟶ H) : groupSchemeMap R f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧R).map (coordinateMap R f).hom.op) (CategoryTheory.eqToHom ⋯))

The morphism of diagonalizable group schemes is obtained by applying relative spectrum to the coordinate Hopf-algebra morphism.

@[simp]

theorem TauCeti.DiagonalizableGroup.groupSchemeMap_hom_left (R : Type u) [CommRing R] {G H : FGCommGrpCat} (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 ↑↑(FiniteTypeCommHopfAlgCat.toBialgHom (coordinateMap R f)))) (CategoryTheory.eqToHom ⋯))

Under the identifications of its source and target with spectra, the scheme morphism underlying groupSchemeMap f is induced by the coordinate Hopf-algebra morphism R[G] ⟶ R[H].

@[simp]

theorem TauCeti.DiagonalizableGroup.groupSchemeMap_id (R : Type u) [CommRing R] (G : FGCommGrpCat) : groupSchemeMap R (CategoryTheory.CategoryStruct.id G) = CategoryTheory.CategoryStruct.id (groupScheme R G)

The group-scheme morphism induced by the identity homomorphism is the identity.

@[simp]

theorem TauCeti.DiagonalizableGroup.groupSchemeMap_comp (R : Type u) [CommRing R] {G H K : FGCommGrpCat} (f : G ⟶ H) (g : H ⟶ K) : groupSchemeMap R (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (groupSchemeMap R g) (groupSchemeMap R f)

Composition of group homomorphisms becomes composition in the reverse order on their diagonalizable group schemes.

noncomputable def TauCeti.DiagonalizableGroup.schemeFunctor (R : Type u) [CommRing R] : CategoryTheory.Functor FGCommGrpCatᵒᵖ (CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R)))

The diagonalizable group-scheme functor. It is contravariant in finitely generated commutative groups and covariant on their opposite category.

Equations

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

noncomputable def TauCeti.DiagonalizableGroup.schemeFunctorIsoHopfSpec (R : Type u) [CommRing R] : schemeFunctor R ≅ (coordinateRingFunctor R).op.comp ((CategoryTheory.forget₂ (FiniteTypeCommHopfAlgCat R) (CommHopfAlgCat R)).op.comp (AlgebraicGeometry.hopfSpec ↧R))

The diagonalizable group-scheme functor is the composite of the opposite coordinate-ring functor, the inclusion from finite-type to unrestricted commutative Hopf algebras, and relative spectrum. This is the categorical interface for factoring schemeFunctor without unfolding its implementation.

Equations

• TauCeti.DiagonalizableGroup.schemeFunctorIsoHopfSpec R = CategoryTheory.Iso.refl (TauCeti.DiagonalizableGroup.schemeFunctor R)

@[simp]

theorem TauCeti.DiagonalizableGroup.schemeFunctor_obj (R : Type u) [CommRing R] (G : FGCommGrpCatᵒᵖ) : (schemeFunctor R).obj G = groupScheme R (Opposite.unop G)

On objects, the diagonalizable group-scheme functor is G ↦ Spec R[G].

@[simp]

theorem TauCeti.DiagonalizableGroup.schemeFunctor_map (R : Type u) [CommRing R] {G H : FGCommGrpCatᵒᵖ} (f : G ⟶ H) : (schemeFunctor R).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (groupSchemeMap R f.unop) (CategoryTheory.eqToHom ⋯))

On morphisms, the diagonalizable group-scheme functor applies relative spectrum to the coordinate map, reversing its direction. The object equalities transport the map between the public descriptions of its source and target.

instance TauCeti.DiagonalizableGroup.isAffine_groupScheme (R : Type u) [CommRing R] (G : FGCommGrpCat) : AlgebraicGeometry.IsAffine (groupScheme R G).X.left

Every diagonalizable group scheme D(G) constructed here is affine.

instance TauCeti.DiagonalizableGroup.locallyOfFiniteType_groupScheme (R : Type u) [CommRing R] (G : FGCommGrpCat) : AlgebraicGeometry.LocallyOfFiniteType (groupScheme R G).X.hom

The structural morphism D(G) ⟶ Spec R is locally of finite type.

noncomputable def TauCeti.DiagonalizableGroup.finiteTypeGroupScheme (R : Type u) [CommRing R] (G : FGCommGrpCat) : FiniteTypeAffineGroupSchemeCat ↧R

The diagonalizable group scheme D(G) bundled as a finite-type affine group scheme.

Equations

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

@[simp]

theorem TauCeti.DiagonalizableGroup.finiteTypeGroupScheme_obj_obj (R : Type u) [CommRing R] (G : FGCommGrpCat) : (finiteTypeGroupScheme R G).obj.obj = groupScheme R G

The underlying group scheme of the bundled finite-type D(G) is groupScheme R G.

noncomputable def TauCeti.DiagonalizableGroup.finiteTypeGroupSchemeIso (R : Type u) [CommRing R] (G : FGCommGrpCat) : (finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat R).functor.obj (Opposite.op (coordinateRing R G)) ≅ finiteTypeGroupScheme R G

The finite-type Hopf/group-scheme anti-equivalence sends the coordinate ring R[G] to the bundled diagonalizable group scheme D(G).

Equations

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

instance TauCeti.DiagonalizableGroup.isAffine_schemeFunctor_obj (R : Type u) [CommRing R] (G : FGCommGrpCatᵒᵖ) : AlgebraicGeometry.IsAffine ((schemeFunctor R).obj G).X.left

Every object produced by the diagonalizable group-scheme functor is affine.

instance TauCeti.DiagonalizableGroup.locallyOfFiniteType_schemeFunctor_obj (R : Type u) [CommRing R] (G : FGCommGrpCatᵒᵖ) : AlgebraicGeometry.LocallyOfFiniteType ((schemeFunctor R).obj G).X.hom

Every structural morphism produced by the diagonalizable group-scheme functor is locally of finite type.

instance TauCeti.DiagonalizableGroup.schemeFunctor_faithful (R : Type u) [CommRing R] [Nontrivial R] : (schemeFunctor R).Faithful

The diagonalizable group-scheme functor is faithful over a nontrivial base ring.

instance TauCeti.DiagonalizableGroup.schemeFunctor_full (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] : (schemeFunctor R).Full

The diagonalizable group-scheme functor is full when the prime spectrum of the base is connected.

noncomputable def TauCeti.DiagonalizableGroup.fullyFaithfulSchemeFunctor (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] : (schemeFunctor R).FullyFaithful

Over a base with connected prime spectrum, the diagonalizable group-scheme functor is fully faithful. Connectedness includes nonemptiness, hence supplies the nontriviality needed for faithfulness.

Equations

• TauCeti.DiagonalizableGroup.fullyFaithfulSchemeFunctor R = CategoryTheory.Functor.FullyFaithful.ofFullyFaithful (TauCeti.DiagonalizableGroup.schemeFunctor R)