The cocharacter-lattice functor of tori #

A morphism of coordinate Hopf algebras sends geometric characters forward. Precomposition with that character map sends integral duals backward, and hence gives the contravariant map on geometric cocharacters. This file proves that these maps are equivariant for the contragredient absolute-Galois actions and assembles them into a functor from the opposite of the category of torus coordinate rings to integral Galois lattices.

The character--cocharacter pairing is natural for these two variance conventions. Thus the two lattice functors supply the functorial perfect pairing needed to form root data from a split pair.

Main declarations #

TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterMap: the contravariant map on geometric cocharacters induced by a coordinate Hopf-algebra morphism.
TauCeti.TorusCommHopfAlgCat.cocharacterLatticeFunctor: the cocharacter-lattice functor from the opposite category of torus coordinate rings to integral Galois lattices.
TauCeti.MultiplicativeTypeCommHopfAlgCat.characterCocharacterPairing_map: naturality of the perfect character--cocharacter pairing.

References #

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

source

noncomputable def TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterMap {k : Type u} [Field k] {S T : MultiplicativeTypeCommHopfAlgCat k} (f : S ⟶ T) :

T.cocharacterLattice →ₗ[ℤ ] S.cocharacterLattice

The contravariant map on geometric cocharacters induced by a morphism of coordinate Hopf algebras. Under X_*(T) ≃ Hom_ℤ(X^*(T), ℤ), it is precomposition with the covariant map on geometric characters.

Equations

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

Instances For

source

@[simp]

theorem TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterLatticeLinearEquivDual_cocharacterMap_apply {k : Type u} [Field k] {S T : MultiplicativeTypeCommHopfAlgCat k} (f : S ⟶ T) (y : T.cocharacterLattice) (x : CommHopfAlgCat.additiveCharacterGroup S.obj.obj) :

(S.cocharacterLatticeLinearEquivDual ((cocharacterMap f) y)) x = (T.cocharacterLatticeLinearEquivDual y) ((CommHopfAlgCat.additiveCharacterMap f.hom.hom) x)

Mapping a cocharacter means precomposing its corresponding character functional with the map on characters.

source

@[simp]

theorem TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterMap_id {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) :

cocharacterMap (CategoryTheory.CategoryStruct.id T) = LinearMap.id

The identity coordinate morphism induces the identity on cocharacters.

source

@[simp]

theorem TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterMap_comp {k : Type u} [Field k] {S T U : MultiplicativeTypeCommHopfAlgCat k} (f : S ⟶ T) (g : T ⟶ U) :

cocharacterMap (CategoryTheory.CategoryStruct.comp f g) = cocharacterMap f ∘ₗ cocharacterMap g

Cocharacter maps reverse composition of coordinate morphisms.

source

@[simp]

theorem TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterMap_smul {k : Type u} [Field k] {S T : MultiplicativeTypeCommHopfAlgCat k} (f : S ⟶ T) (σ : Field.absoluteGaloisGroup k) (y : T.cocharacterLattice) :

(cocharacterMap f) ((T.cocharacterGaloisRepresentation σ) y) = (S.cocharacterGaloisRepresentation σ) ((cocharacterMap f) y)

The map on cocharacters is equivariant for the contragredient absolute-Galois actions.

source

theorem TauCeti.MultiplicativeTypeCommHopfAlgCat.characterCocharacterPairing_map {k : Type u} [Field k] {S T : MultiplicativeTypeCommHopfAlgCat k} (f : S ⟶ T) (x : CommHopfAlgCat.additiveCharacterGroup S.obj.obj) (y : T.cocharacterLattice) :

(T.characterCocharacterPairing ((CommHopfAlgCat.additiveCharacterMap f.hom.hom) x)) y = (S.characterCocharacterPairing x) ((cocharacterMap f) y)

The character--cocharacter pairing is natural: mapping a character covariantly or mapping a cocharacter contravariantly gives the same integer.

source

@[reducible, inline]

noncomputable abbrev TauCeti.TorusCommHopfAlgCat.toMultiplicativeTypeMap {k : Type u} [Field k] {S T : TorusCommHopfAlgCat k} (f : S ⟶ T) :

S.toMultiplicativeTypeCommHopfAlgCat ⟶ T.toMultiplicativeTypeCommHopfAlgCat

A morphism of torus coordinate rings, regarded as a morphism of coordinate rings of groups of multiplicative type.

Equations

TauCeti.TorusCommHopfAlgCat.toMultiplicativeTypeMap f = CategoryTheory.ObjectProperty.homMk f.hom

Instances For

source

@[reducible, inline]

noncomputable abbrev TauCeti.TorusCommHopfAlgCat.cocharacterLatticeRepresentation {k : Type u} [Field k] (T : TorusCommHopfAlgCat k) :

Rep ℤ (Field.absoluteGaloisGroup k)

The geometric cocharacter lattice of a torus with its contragredient absolute-Galois representation.

Equations

T.cocharacterLatticeRepresentation = Rep.of T.toMultiplicativeTypeCommHopfAlgCat.cocharacterGaloisRepresentation

Instances For

source

noncomputable def TauCeti.TorusCommHopfAlgCat.cocharacterLatticeRepresentationMap {k : Type u} [Field k] {S T : TorusCommHopfAlgCat k} (f : S ⟶ T) :

T.cocharacterLatticeRepresentation ⟶ S.cocharacterLatticeRepresentation

The equivariant map from the cocharacter representation of the target torus to that of the source torus.

Equations

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

Instances For

source

@[simp]

theorem TauCeti.TorusCommHopfAlgCat.cocharacterLatticeRepresentationMap_hom_apply {k : Type u} [Field k] {S T : TorusCommHopfAlgCat k} (f : S ⟶ T) (y : T.toMultiplicativeTypeCommHopfAlgCat.cocharacterLattice) :

(Rep.Hom.hom (cocharacterLatticeRepresentationMap f)) y = (MultiplicativeTypeCommHopfAlgCat.cocharacterMap (toMultiplicativeTypeMap f)) y

Evaluation of the equivariant morphism induced on geometric cocharacters.

source

noncomputable def TauCeti.TorusCommHopfAlgCat.cocharacterLatticeFunctor {k : Type u} [Field k] :

CategoryTheory.Functor (TorusCommHopfAlgCat k)ᵒᵖ (GaloisLatticeCat k)

The cocharacter-lattice functor from coordinate Hopf algebras of tori, contravariant as a functor on coordinate rings, to continuous integral Galois lattices.

Equations