Documentation

TauCeti.Algebra.AlgebraicGroup.Torus.CharacterLattice.Functoriality

The character-lattice functor of tori #

The character group of a torus is a finite free ℤ-module with a continuous action of the absolute Galois group. Here continuity is expressed without choosing topology data on the underlying module: every vector has an open stabilizer, which is the standard criterion for an action on a discrete space.

These objects form the category GaloisLatticeCat k, defined in the generic representation-theory module TauCeti.RepresentationTheory.GaloisLattice.Basic. The functorial geometric-character construction restricts to a functor from coordinate Hopf algebras of tori to that category. Because coordinate rings are contravariant in affine group schemes, this is the contravariant character-lattice functor from tori themselves.

Main declarations #

References #

See J. S. Milne, Algebraic Groups (2017), Theorem 12.23 and Corollary 12.24.

source
noncomputable def TauCeti.TorusCommHopfAlgCat.characterLatticeFunctor {k : Type u} [Field k] :
CategoryTheory.Functor (TorusCommHopfAlgCat k) (GaloisLatticeCat k)

The character-lattice functor from coordinate Hopf algebras of tori to continuous integral Galois lattices. On the corresponding affine group schemes this functor is contravariant.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.TorusCommHopfAlgCat.characterLatticeFunctor_obj_obj {k : Type u} [Field k] (T : TorusCommHopfAlgCat k) :
    (characterLatticeFunctor.obj T).obj = CommHopfAlgCat.geometricCharacterRepresentation T.obj.obj

    The underlying integral representation of a torus's character lattice is its geometric character group with the absolute-Galois action.

    source
    @[simp]
    theorem TauCeti.TorusCommHopfAlgCat.characterLatticeFunctor_map_hom {k : Type u} [Field k] {S T : TorusCommHopfAlgCat k} (f : S ⟶ T) :
    (characterLatticeFunctor.map f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.geometricCharacterRepresentationMap f.hom.hom) (CategoryTheory.eqToHom ⋯))

    The morphism part of characterLatticeFunctor is the induced equivariant character map.