Documentation

TauCeti.Algebra.AlgebraicGroup.Torus.CharacterLattice.Basic

The character lattice of a torus #

The geometric characters of a torus are the group-like elements of its coordinate algebra after extension to an algebraic closure. The generic construction and its absolute-Galois action are in TauCeti.Algebra.AlgebraicGroup.CommHopfAlgCat.CharacterLattice.Basic.

The defining splitting over the algebraic closure identifies the underlying additive character group, noncanonically, with a finite-rank free abelian group. The absolute-Galois action and its continuity for the discrete topology are constructed in the generic character-group modules. An equivariant classification of non-split tori is not formalized here.

Main declarations #

References #

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

source
theorem TauCeti.exists_characterLattice_addEquiv_of_torus (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (hH : torusCommHopfAlgProperty k H) :
∃ (n : ℕ), Nonempty (CommHopfAlgCat.additiveCharacterGroup H.obj ≃+ (Fin n →₀ ℤ))

The character lattice of a torus is a finite-rank free abelian group. The equivalence is noncanonical: it uses the splitting over the chosen algebraic closure from the torus predicate.

source
theorem TauCeti.characterLattice_module_free_of_torus (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (hH : torusCommHopfAlgProperty k H) :
Module.Free ℤ (CommHopfAlgCat.additiveCharacterGroup H.obj)

The character lattice of a torus is a free ℤ-module.

source
theorem TauCeti.characterLattice_module_finite_of_torus (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (hH : torusCommHopfAlgProperty k H) :
Module.Finite ℤ (CommHopfAlgCat.additiveCharacterGroup H.obj)

The character lattice of a torus is a finite ℤ-module.