Groups of multiplicative type

A finite-type affine group over a field is of multiplicative type when it becomes diagonalizable after extending scalars to an algebraic closure. On coordinate Hopf algebras, diagonalizability is the intrinsic condition that the group-like elements span the algebra. Thus a finite-type commutative Hopf algebra H over k is of multiplicative type exactly when the group-like elements span AlgebraicClosure k ⊗[k] H.

The essential-image characterization of diagonalizable coordinate rings identifies this intrinsic definition with the usual one: after base change, the Hopf algebra is isomorphic to k̄[M] for a finitely generated commutative group M. In particular, every coordinate ring arising from FGCommGrpCat is of multiplicative type.

Main declarations

• TauCeti.multiplicativeTypeCommHopfAlgProperty: the multiplicative-type object property on finite-type commutative Hopf algebras over a field.
• TauCeti.multiplicativeTypeCommHopfAlgProperty_iff_exists_iso_coordinateRing: the characterization by becoming a diagonalizable coordinate ring over an algebraic closure.
• TauCeti.DiagonalizableGroup.multiplicativeType_coordinateRing: every finite-type diagonalizable coordinate Hopf algebra is of multiplicative type.
• TauCeti.MultiplicativeTypeCommHopfAlgCat: the full subcategory of coordinate Hopf algebras of multiplicative-type groups.

References

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

This is the coordinate-algebra foundation for Layer 4, "Diagonalizable groups and groups of multiplicative type", of the ReductiveGroups roadmap. Non-split tori will add smoothness and geometric connectedness to this property and equip the resulting character lattice with its Galois action.

def TauCeti.multiplicativeTypeCommHopfAlgProperty (k : Type u) [Field k] : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat k)

The object property selecting finite-type commutative Hopf algebras that become diagonalizable after base change to an algebraic closure.

Diagonalizability is expressed intrinsically by the group-like elements spanning the base-changed coordinate algebra.

Equations

• TauCeti.multiplicativeTypeCommHopfAlgProperty k = (TauCeti.DiagonalizableGroup.groupLikeSpannedProperty (AlgebraicClosure k)).inverseImage TauCeti.FiniteTypeCommHopfAlgCat.baseChangeFunctor

@[simp]

theorem TauCeti.multiplicativeTypeCommHopfAlgProperty_iff (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) : multiplicativeTypeCommHopfAlgProperty k H ↔ DiagonalizableGroup.groupLikeSpannedProperty (AlgebraicClosure k) H.baseChange

Membership in the multiplicative-type property means that the base-changed Hopf algebra is spanned by its group-like elements.

instance TauCeti.instIsClosedUnderIsomorphismsFiniteTypeCommHopfAlgCatMultiplicativeTypeCommHopfAlgProperty (k : Type u) [Field k] : (multiplicativeTypeCommHopfAlgProperty k).IsClosedUnderIsomorphisms

Being of multiplicative type is invariant under isomorphisms of finite-type commutative Hopf algebras.

theorem TauCeti.multiplicativeTypeCommHopfAlgProperty_iff_exists_iso_coordinateRing (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) : multiplicativeTypeCommHopfAlgProperty k H ↔ ∃ (G : FGCommGrpCat), Nonempty (DiagonalizableGroup.coordinateRing (AlgebraicClosure k) G ≅ H.baseChange)

A finite-type commutative Hopf algebra is of multiplicative type exactly when its base change to an algebraic closure is the coordinate Hopf algebra of a diagonalizable group.

theorem TauCeti.DiagonalizableGroup.multiplicativeType_coordinateRing (k : Type u) [Field k] (G : FGCommGrpCat) : multiplicativeTypeCommHopfAlgProperty k (coordinateRing k G)

Every finite-type diagonalizable coordinate Hopf algebra is of multiplicative type.

@[reducible, inline]

abbrev TauCeti.MultiplicativeTypeCommHopfAlgCat (k : Type u) [Field k] : Type (u + 1)

The category of finite-type commutative Hopf algebras of multiplicative type over a field.

Objects are not required to be split over the base field; they become diagonalizable after base change to an algebraic closure.

Equations

• TauCeti.MultiplicativeTypeCommHopfAlgCat k = (TauCeti.multiplicativeTypeCommHopfAlgProperty k).FullSubcategory