Classification of tori by cocharacter lattices

The cocharacter-lattice functor is naturally isomorphic to the integral dual of the character-lattice functor. Over a perfect field it is therefore an equivalence: continuous integral Galois lattices classify tori covariantly, or their coordinate Hopf algebras contravariantly. The comparison of functors itself holds over every field.

References

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

noncomputable def TauCeti.TorusCommHopfAlgCat.cocharacterLatticeFunctorIsoDual {k : Type u} [Field k] : cocharacterLatticeFunctor ≅ characterLatticeFunctor.op.comp GaloisLatticeCat.dualFunctor

The cocharacter-lattice functor is the contragredient dual of the character-lattice functor. This identifies the intrinsic geometric cocharacters with integral character functionals.

Equations

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

@[simp]

theorem TauCeti.TorusCommHopfAlgCat.cocharacterLatticeFunctorIsoDual_hom_app_apply {k : Type u} [Field k] (T : TorusCommHopfAlgCat k) (y : T.toMultiplicativeTypeCommHopfAlgCat.cocharacterLattice) (x : CommHopfAlgCat.additiveCharacterGroup T.obj.obj) : ((Rep.Hom.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom (cocharacterLatticeFunctorIsoDual.hom.app (Opposite.op T)).hom) ((Rep.Hom.hom (CategoryTheory.eqToHom ⋯)) y))) x = (T.toMultiplicativeTypeCommHopfAlgCat.cocharacterLatticeLinearEquivDual y) x

The comparison with the dual character functor evaluates a cocharacter on a character.

instance TauCeti.TorusCommHopfAlgCat.cocharacterLatticeFunctor_isEquivalence {k : Type u} [Field k] [PerfectField k] : cocharacterLatticeFunctor.IsEquivalence

Over a perfect field, the geometric cocharacter-lattice functor classifies tori. Its variance is contravariant here because the source consists of coordinate Hopf algebras.