Tori over a field

A finite-type affine group over a field is a torus when it becomes a finite-rank split torus after extending scalars to an algebraic closure. On coordinate Hopf algebras, the rank-n split torus has coordinate ring

k[Multiplicative (Fin n →₀ ℤ)].

This file records both the split and geometric forms of that definition as object properties on finite-type commutative Hopf algebras. Keeping them as properties, rather than building them into the ambient category, leaves finite, non-smooth groups such as μ_p in the general theory.

Every split torus is a torus: after base change, the standard coordinate-ring comparison identifies K ⊗[k] k[ℤⁿ] with K[ℤⁿ]. Every torus is of multiplicative type, since its base change is a diagonalizable coordinate Hopf algebra. Thus this definition extends the existing multiplicative-type theory while imposing the free finite-rank character lattice that distinguishes tori from general groups of multiplicative type.

Main declarations

• TauCeti.splitTorusCommHopfAlgProperty: finite-type coordinate Hopf algebras isomorphic over the base ring to the coordinate ring of a finite-rank split torus.
• TauCeti.torusCommHopfAlgProperty: finite-type coordinate Hopf algebras that become a finite-rank split torus over AlgebraicClosure k.
• TauCeti.splitTorusCommHopfAlgProperty.torus: every split torus is a torus.
• TauCeti.torusCommHopfAlgProperty.multiplicativeType: every torus is of multiplicative type.
• TauCeti.torusCommHopfAlgProperty.isCocomm: the coordinate Hopf algebra of a torus is cocommutative.
• TauCeti.SplitTorus.splitTorus_coordinateRing: the standard finite-rank split tori satisfy the split predicate.
• TauCeti.rankZeroSplitTorusIso: the rank-zero split torus is the trivial affine group.
• TauCeti.splitTorusCommHopfAlgProperty_trivial: the trivial affine group is the rank-zero split torus.

References

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

This is the coordinate-algebra definition required by Layer 4, "Tori: split and non-split", of the ReductiveGroups roadmap. Smoothness and geometric connectedness are proved in TauCeti.Algebra.AlgebraicGroup.Torus.SmoothConnected; the next step is the character lattice with its Galois action.

def TauCeti.splitTorusCommHopfAlgProperty (k : Type u) [CommRing k] : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat k)

The object property selecting finite-type commutative Hopf algebras that are coordinate rings of split tori of finite rank.

The witness n is the rank. The finite index type is universe-lifted so that its character group lives in the same universe as k; this does not change the represented rank-n torus.

Equations

• TauCeti.splitTorusCommHopfAlgProperty k H = ∃ (n : ℕ), Nonempty (TauCeti.DiagonalizableGroup.coordinateRing k (TauCeti.SplitTorus.characterGroup (ULift.{?u.1, 0} (Fin n))) ≅ H)

@[simp]

theorem TauCeti.splitTorusCommHopfAlgProperty_iff (k : Type u) [CommRing k] (H : FiniteTypeCommHopfAlgCat k) : splitTorusCommHopfAlgProperty k H ↔ ∃ (n : ℕ), Nonempty (DiagonalizableGroup.coordinateRing k (SplitTorus.characterGroup (ULift.{u, 0} (Fin n))) ≅ H)

Membership in the split-torus property means being isomorphic to the coordinate Hopf algebra of a finite-rank split torus.

instance TauCeti.instIsClosedUnderIsomorphismsFiniteTypeCommHopfAlgCatSplitTorusCommHopfAlgProperty (k : Type u) [CommRing k] : (splitTorusCommHopfAlgProperty k).IsClosedUnderIsomorphisms

Being a split torus is invariant under isomorphisms of finite-type commutative Hopf algebras.

@[reducible, inline]

abbrev TauCeti.SplitTorusCommHopfAlgCat (k : Type u) [CommRing k] : Type (u + 1)

The category of finite-type split-torus coordinate Hopf algebras over a commutative ring.

Equations

• TauCeti.SplitTorusCommHopfAlgCat k = (TauCeti.splitTorusCommHopfAlgProperty k).FullSubcategory

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

The object property selecting finite-type commutative Hopf algebras that become coordinate rings of split tori of finite rank after base change to an algebraic closure.

This is the coordinate-Hopf-algebra definition of a not-necessarily-split torus over k.

Equations

• TauCeti.torusCommHopfAlgProperty k = (TauCeti.splitTorusCommHopfAlgProperty (AlgebraicClosure k)).inverseImage TauCeti.FiniteTypeCommHopfAlgCat.baseChangeFunctor

@[simp]

theorem TauCeti.torusCommHopfAlgProperty_iff (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) : torusCommHopfAlgProperty k H ↔ ∃ (n : ℕ), Nonempty (DiagonalizableGroup.coordinateRing (AlgebraicClosure k) (SplitTorus.characterGroup (ULift.{u, 0} (Fin n))) ≅ H.baseChange)

Membership in the torus property means becoming a finite-rank split torus after base change to an algebraic closure.

instance TauCeti.instIsClosedUnderIsomorphismsFiniteTypeCommHopfAlgCatTorusCommHopfAlgProperty (k : Type u) [Field k] : (torusCommHopfAlgProperty k).IsClosedUnderIsomorphisms

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

theorem TauCeti.torusCommHopfAlgProperty.isCocomm (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (hH : torusCommHopfAlgProperty k H) : Coalgebra.IsCocomm k ↑H.obj

The coordinate Hopf algebra of a torus is cocommutative.

@[reducible, inline]

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

The category of finite-type torus coordinate Hopf algebras over a field.

Objects need not be split over the base field; they become split after extension to an algebraic closure.

Equations

• TauCeti.TorusCommHopfAlgCat k = (TauCeti.torusCommHopfAlgProperty k).FullSubcategory

theorem TauCeti.splitTorusCommHopfAlgProperty.torus (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (hH : splitTorusCommHopfAlgProperty k H) : torusCommHopfAlgProperty k H

Every split torus is a torus.

theorem TauCeti.torusCommHopfAlgProperty.multiplicativeType (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (hH : torusCommHopfAlgProperty k H) : multiplicativeTypeCommHopfAlgProperty k H

Every torus is a group of multiplicative type.

theorem TauCeti.SplitTorus.splitTorus_coordinateRing (k : Type u) [CommRing k] (σ : Type u) [Finite σ] : splitTorusCommHopfAlgProperty k (DiagonalizableGroup.coordinateRing k (characterGroup σ))

The coordinate Hopf algebra of a finite-rank split torus satisfies the split-torus property.

noncomputable def TauCeti.rankZeroSplitTorusIso (k : Type u) [CommRing k] : DiagonalizableGroup.coordinateRing k (SplitTorus.characterGroup (ULift.{u, 0} (Fin 0))) ≅ FiniteTypeCommHopfAlgCat.of k k

The rank-zero split torus is the trivial affine group: the group algebra of the trivial character group is the base field.

Equations

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

@[simp]

theorem TauCeti.rankZeroSplitTorusIso_hom_apply (k : Type u) [CommRing k] (x : ↑(DiagonalizableGroup.coordinateRing k (SplitTorus.characterGroup (ULift.{u, 0} (Fin 0)))).obj) : (CategoryTheory.ConcreteCategory.hom (rankZeroSplitTorusIso k).hom) x = CoalgebraStruct.counit x

The rank-zero split-torus isomorphism is the counit on its coordinate ring.

theorem TauCeti.splitTorusCommHopfAlgProperty_trivial (k : Type u) [CommRing k] : splitTorusCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.of k k)

The trivial affine group is the split torus of rank zero.