Finite-type diagonalizable groups

The diagonalizable group attached to a commutative group G has coordinate Hopf algebra R[G]. It is of finite type over R precisely when G is finitely generated (over a nontrivial base). This file packages the forward direction categorically: finitely generated commutative groups form FGCommGrpCat, and the group-algebra construction gives a functor from this category to finite-type commutative Hopf algebras.

On affine schemes the variance reverses once more under Spec, so this covariant coordinate ring functor is the algebraic side of the contravariant assignment G ↦ D(G). Its morphism part is MonoidAlgebra.mapDomainBialgHom; the DiagonalizableGroup.Functoriality module separately shows that the resulting map of represented groups acts by precomposition on characters. When the base ring has connected prime spectrum, every coordinate Hopf-algebra morphism arises uniquely from a character-group homomorphism, so the coordinate-ring functor is fully faithful.

This advances the reductive-groups roadmap Layer 4 target constructing the anti-equivalence between finitely generated abelian groups and diagonalizable groups. It supplies the finite-type source and the coordinate-algebra functor, which is full and faithful over a base with connected prime spectrum. It does not prove essential surjectivity, construct the scheme-side functor, or depend on the general Hopf-algebra/affine-group-scheme anti-equivalence.

Main declarations

• TauCeti.FGCommGrpCat: the category of finitely generated commutative groups.
• TauCeti.DiagonalizableGroup.coordinateRing: R[G] as a finite-type commutative Hopf algebra.
• TauCeti.DiagonalizableGroup.coordinateMap: the coordinate morphism induced by a group homomorphism.
• TauCeti.DiagonalizableGroup.mapPointsFunctor_coordinateMap_app: the induced map on points is precomposition of characters.
• TauCeti.DiagonalizableGroup.coordinateMap_surjective_of_surjective: a surjective character-group homomorphism induces a surjective coordinate morphism.
• TauCeti.DiagonalizableGroup.coordinateRingFunctor: the group-algebra functor from finitely generated commutative groups to finite-type commutative Hopf algebras.
• TauCeti.DiagonalizableGroup.coordinateMap_injective: coordinate maps remember their underlying group homomorphisms over a nontrivial base.
• TauCeti.DiagonalizableGroup.coordinateMapPreimage: recover the character-group homomorphism inducing a coordinate Hopf-algebra morphism over a base with connected prime spectrum.
• TauCeti.DiagonalizableGroup.coordinateMapPreimage_apply_eq_iff: characterize the recovered homomorphism without exposing its choice-based construction.
• TauCeti.DiagonalizableGroup.coordinateMap_surjective: every coordinate Hopf-algebra morphism over a base with connected prime spectrum comes from a character-group homomorphism.
• TauCeti.DiagonalizableGroup.coordinateRingFunctor_faithful: the coordinate-ring functor is faithful over a nontrivial base.
• TauCeti.DiagonalizableGroup.coordinateRingFunctor_full: the coordinate-ring functor is full over a base with connected prime spectrum.

References

The mathematical construction is the diagonalizable-group correspondence in Waterhouse, Introduction to Affine Group Schemes, Chapter 2. The finite-type input is Mathlib's MonoidAlgebra.finiteType_of_fg, and the Hopf morphism is Mathlib's MonoidAlgebra.mapDomainBialgHom.

@[reducible, inline]

noncomputable abbrev TauCeti.DiagonalizableGroup.coordinateRing (R : Type u) [CommRing R] (G : FGCommGrpCat) : FiniteTypeCommHopfAlgCat R

The coordinate Hopf algebra R[G] of the diagonalizable group D(G), bundled as a finite-type commutative Hopf algebra when G is finitely generated.

Equations

• TauCeti.DiagonalizableGroup.coordinateRing R G = TauCeti.FiniteTypeCommHopfAlgCat.of R (MonoidAlgebra R ↑G)

@[reducible, inline]

noncomputable abbrev TauCeti.DiagonalizableGroup.coordinateMap (R : Type u) [CommRing R] {G H : FGCommGrpCat} (φ : G ⟶ H) : coordinateRing R G ⟶ coordinateRing R H

A homomorphism G → G' induces the coordinate Hopf-algebra morphism R[G] → R[G'] between the corresponding finite-type diagonalizable groups.

Equations

• TauCeti.DiagonalizableGroup.coordinateMap R φ = TauCeti.FiniteTypeCommHopfAlgCat.ofHom (MonoidAlgebra.mapDomainBialgHom R (TauCeti.FGCommGrpCat.toMonoidHom φ))

@[simp]

theorem TauCeti.DiagonalizableGroup.toBialgHom_coordinateMap (R : Type u) [CommRing R] {G H : FGCommGrpCat} (φ : G ⟶ H) : FiniteTypeCommHopfAlgCat.toBialgHom (coordinateMap R φ) = MonoidAlgebra.mapDomainBialgHom R (FGCommGrpCat.toMonoidHom φ)

The bialgebra morphism underlying coordinateMap φ is the group-algebra map induced by the underlying group homomorphism.

theorem TauCeti.DiagonalizableGroup.mapPointsFunctor_coordinateMap_app (R : Type u) [CommRing R] {G H : FGCommGrpCat} (φ : G ⟶ H) (A : CommAlgCat R) (p : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (coordinateMap R φ).hom).app A)) p = (pointsMap (FGCommGrpCat.toMonoidHom φ)) p

The map on algebra-valued points induced by a diagonalizable-group coordinate morphism is the contravariant point map given by precomposition of characters.

theorem TauCeti.DiagonalizableGroup.coordinateMap_single (R : Type u) [CommRing R] {G H : FGCommGrpCat} (φ : G ⟶ H) (g : ↑G) (r : R) : (FiniteTypeCommHopfAlgCat.toBialgHom (coordinateMap R φ)) (MonoidAlgebra.single g r) = MonoidAlgebra.single ((FGCommGrpCat.toMonoidHom φ) g) r

The coordinate map sends a group-algebra basis element to the basis element indexed by its image under the underlying group homomorphism.

This is deliberately not a simp lemma: FiniteTypeCommHopfAlgCat.toBialgHom_ofHom already rewrites the left-hand side to MonoidAlgebra.mapDomainBialgHom, so simp would never see this form.

theorem TauCeti.DiagonalizableGroup.coordinateMap_surjective_of_surjective (R : Type u) [CommRing R] {G H : FGCommGrpCat} (φ : G ⟶ H) (hφ : Function.Surjective ⇑(FGCommGrpCat.toMonoidHom φ)) : Function.Surjective ⇑(FiniteTypeCommHopfAlgCat.toBialgHom (coordinateMap R φ))

A surjective homomorphism of character groups induces a surjective morphism of their coordinate Hopf algebras.

noncomputable def TauCeti.DiagonalizableGroup.coordinateMapPreimage (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {G H : FGCommGrpCat} (F : coordinateRing R G ⟶ coordinateRing R H) : G ⟶ H

Recover the character-group homomorphism that induces a morphism between coordinate Hopf algebras of finite-type diagonalizable groups over a base with connected prime spectrum.

Equations

• TauCeti.DiagonalizableGroup.coordinateMapPreimage R F = TauCeti.FGCommGrpCat.ofHom (TauCeti.MonoidAlgebra.mapDomainBialgHomPreimage R (TauCeti.FiniteTypeCommHopfAlgCat.toBialgHom F))

theorem TauCeti.DiagonalizableGroup.coordinateMapPreimage_apply_eq_iff (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {G H : FGCommGrpCat} (F : coordinateRing R G ⟶ coordinateRing R H) (g : ↑G) (h : ↑H) : (FGCommGrpCat.toMonoidHom (coordinateMapPreimage R F)) g = h ↔ (FiniteTypeCommHopfAlgCat.toBialgHom F) (MonoidAlgebra.single g 1) = MonoidAlgebra.single h 1

The recovered character-group homomorphism takes g to h exactly when the coordinate Hopf-algebra morphism takes the corresponding standard basis element to the standard basis element indexed by h.

@[simp]

theorem TauCeti.DiagonalizableGroup.coordinateMapPreimage_single (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {G H : FGCommGrpCat} (F : coordinateRing R G ⟶ coordinateRing R H) (g : ↑G) : (FiniteTypeCommHopfAlgCat.toBialgHom F) (MonoidAlgebra.single g 1) = MonoidAlgebra.single ((FGCommGrpCat.toMonoidHom (coordinateMapPreimage R F)) g) 1

The recovered character-group homomorphism is characterized by the image of each standard basis element under the coordinate Hopf-algebra morphism.

@[simp]

theorem TauCeti.DiagonalizableGroup.coordinateMap_coordinateMapPreimage (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {G H : FGCommGrpCat} (F : coordinateRing R G ⟶ coordinateRing R H) : coordinateMap R (coordinateMapPreimage R F) = F

Applying the coordinate-map construction to the recovered character-group homomorphism gives the original coordinate Hopf-algebra morphism.

theorem TauCeti.DiagonalizableGroup.coordinateMap_surjective (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {G H : FGCommGrpCat} : Function.Surjective (coordinateMap R)

Every morphism between coordinate Hopf algebras of finite-type diagonalizable groups over a base with connected prime spectrum is induced by a character-group homomorphism.

theorem TauCeti.DiagonalizableGroup.coordinateMap_injective (R : Type u) [CommRing R] [Nontrivial R] {G H : FGCommGrpCat} : Function.Injective (coordinateMap R)

Over a nontrivial base ring, the coordinate morphism remembers the group homomorphism that induced it.

@[simp]

theorem TauCeti.DiagonalizableGroup.coordinateMapPreimage_coordinateMap (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {G H : FGCommGrpCat} (φ : G ⟶ H) : coordinateMapPreimage R (coordinateMap R φ) = φ

Recovering a character-group homomorphism from its coordinate map returns the original homomorphism.

noncomputable def TauCeti.DiagonalizableGroup.coordinateRingFunctor (R : Type u) [CommRing R] : CategoryTheory.Functor FGCommGrpCat (FiniteTypeCommHopfAlgCat R)

The coordinate-ring construction for finite-type diagonalizable groups.

It is covariant on coordinate Hopf algebras. After applying the contravariant spectrum functor, it becomes the usual contravariant assignment G ↦ D(G).

Equations

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

@[simp]

theorem TauCeti.DiagonalizableGroup.coordinateRingFunctor_obj (R : Type u) [CommRing R] (G : FGCommGrpCat) : (coordinateRingFunctor R).obj G = coordinateRing R G

The coordinate-ring functor sends a finitely generated commutative group to its coordinate Hopf algebra.

@[simp]

theorem TauCeti.DiagonalizableGroup.coordinateRingFunctor_map (R : Type u) [CommRing R] {G H : FGCommGrpCat} (φ : G ⟶ H) : (coordinateRingFunctor R).map φ = coordinateMap R φ

The coordinate-ring functor sends a group homomorphism to the induced coordinate Hopf-algebra morphism.

instance TauCeti.DiagonalizableGroup.coordinateRingFunctor_faithful (R : Type u) [CommRing R] [Nontrivial R] : (coordinateRingFunctor R).Faithful

The coordinate-ring functor of finite-type diagonalizable groups is faithful over a nontrivial base ring.

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

The coordinate-ring functor of finite-type diagonalizable groups is full over a base with connected prime spectrum.