Cocharacter lattices of groups of multiplicative type

For a group T of multiplicative type over a field k, a geometric cocharacter is a group-scheme morphism G_m → T after extension to the chosen algebraic closure. Contravariantly, it is a morphism of coordinate Hopf algebras

O(T_bar) → O(G_m).

The canonical group-like evaluation equivalence reconstructs the geometric fibre from its characters. Full faithfulness of the diagonalizable-group coordinate-ring functor then identifies these geometric morphisms with the integral dual of the geometric character lattice. This comparison, rather than the definition of cocharacters, supplies the evaluation pairing. The dual description is specific to groups of multiplicative type: a semisimple group can have trivial character group and nontrivial cocharacters. For tori, the character lattice is finite free and the pairing is perfect; those consequences are proved in the torus module.

The absolute Galois action on X_*(T) is the contragredient of its action on X*(T). The evaluation pairing is invariant under the diagonal action.

Main declarations

• TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterLattice: geometric group-scheme morphisms G_m → T_bar.
• TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterLatticeLinearEquivDual: the comparison between geometric cocharacters and the integral character dual.
• TauCeti.MultiplicativeTypeCommHopfAlgCat.geometricCharacterGroupSchemeMap: the group-scheme morphism attached to a geometric character.
• TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterGaloisRepresentation: its contragredient absolute Galois representation.
• TauCeti.MultiplicativeTypeCommHopfAlgCat.characterCocharacterPairing: the evaluation pairing between characters and cocharacters, intrinsically characterized by composition of their group-scheme morphisms.

Roadmap

This completes the lattice-and-pairing part of Layer 4, "Tori: split and non-split; the character lattice X*(T) and cocharacter lattice X_*(T) with their perfect pairing", in the reductive-groups roadmap. Continuity of the Galois actions and the descent classification of non-split tori remain separate steps.

References

See J. S. Milne, Algebraic Groups (2017), Definitions 12.14 and 12.17.

@[reducible, inline]

noncomputable abbrev TauCeti.MultiplicativeTypeCommHopfAlgCat.geometricFiberGroupScheme {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧(AlgebraicClosure k)))

The geometric fibre as an affine group scheme over the chosen algebraic closure.

Equations

• T.geometricFiberGroupScheme = (AlgebraicGeometry.hopfSpec ↧(AlgebraicClosure k)).obj (Opposite.op T.obj.baseChange.obj)

@[reducible, inline]

abbrev TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterLattice {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) : Type u

The geometric cocharacter lattice: group-scheme morphisms G_m → T_bar over the chosen algebraic closure.

Equations

• T.cocharacterLattice = (TauCeti.DiagonalizableGroup.multiplicativeGroupScheme (AlgebraicClosure k) ⟶ T.geometricFiberGroupScheme)

noncomputable def TauCeti.MultiplicativeTypeCommHopfAlgCat.geometricCharacterGroupSchemeMap {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) (x : CommHopfAlgCat.additiveCharacterGroup T.obj.obj) : T.geometricFiberGroupScheme ⟶ DiagonalizableGroup.multiplicativeGroupScheme (AlgebraicClosure k)

A geometric character, as the corresponding group-scheme morphism from the geometric fibre of the torus to the multiplicative group.

Equations

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

noncomputable def TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterLatticeEquivDual {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) : T.cocharacterLattice ≃ Module.Dual ℤ (CommHopfAlgCat.additiveCharacterGroup T.obj.obj)

Group-like reconstruction identifies geometric cocharacters with the integral dual of geometric characters. This equivalence transports the additive and module structures; the linear equivalence below is the canonical comparison for consumers.

Equations

• T.cocharacterLatticeEquivDual = (TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterLatticeEquivFG✝ T).trans (TauCeti.MultiplicativeTypeCommHopfAlgCat.characterHomDualEquiv✝ T)

@[instance_reducible]

noncomputable instance TauCeti.MultiplicativeTypeCommHopfAlgCat.instCocharacterLatticeAddCommGroup {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) : AddCommGroup T.cocharacterLattice

Equations

• T.instCocharacterLatticeAddCommGroup = T.cocharacterLatticeEquivDual.addCommGroup

@[instance_reducible]

noncomputable instance TauCeti.MultiplicativeTypeCommHopfAlgCat.instCocharacterLatticeModule {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) : Module ℤ T.cocharacterLattice

Equations

• T.instCocharacterLatticeModule = AddEquiv.module ℤ T.cocharacterLatticeEquivDual.addEquiv

noncomputable def TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterLatticeLinearEquivDual {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) : T.cocharacterLattice ≃ₗ[ℤ] Module.Dual ℤ (CommHopfAlgCat.additiveCharacterGroup T.obj.obj)

The canonical equivalence from geometric cocharacters to the character dual, as a linear equivalence.

Equations

• T.cocharacterLatticeLinearEquivDual = AddEquiv.linearEquiv ℤ T.cocharacterLatticeEquivDual.addEquiv

noncomputable def TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterGaloisRepresentation {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) : Representation ℤ (Field.absoluteGaloisGroup k) T.cocharacterLattice

The contragredient absolute-Galois representation on the cocharacter lattice. Thus a Galois element σ sends a cocharacter functional f to x ↦ f (σ⁻¹ • x).

Equations

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

@[simp]

theorem TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterGaloisRepresentation_apply_apply {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) (σ : Field.absoluteGaloisGroup k) (f : T.cocharacterLattice) (x : CommHopfAlgCat.additiveCharacterGroup T.obj.obj) : (T.cocharacterLatticeLinearEquivDual ((T.cocharacterGaloisRepresentation σ) f)) x = (T.cocharacterLatticeLinearEquivDual f) (σ⁻¹ • x)

The contragredient Galois representation evaluates by applying the inverse Galois element to the character.

noncomputable def TauCeti.MultiplicativeTypeCommHopfAlgCat.characterCocharacterPairing {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) : CommHopfAlgCat.additiveCharacterGroup T.obj.obj →ₗ[ℤ] T.cocharacterLattice →ₗ[ℤ] ℤ

The character--cocharacter pairing transported through the canonical dual comparison. It is evaluation of a functional in X_*(T) = Hom_ℤ(X*(T), ℤ) on a character.

Equations

• T.characterCocharacterPairing = (↑T.cocharacterLatticeLinearEquivDual).flip

@[simp]

theorem TauCeti.MultiplicativeTypeCommHopfAlgCat.characterCocharacterPairing_apply {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) (x : CommHopfAlgCat.additiveCharacterGroup T.obj.obj) (f : T.cocharacterLattice) : (T.characterCocharacterPairing x) f = (T.cocharacterLatticeLinearEquivDual f) x

The character--cocharacter pairing is evaluation.

@[simp]

theorem TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacter_comp_geometricCharacterGroupSchemeMap {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) (x : CommHopfAlgCat.additiveCharacterGroup T.obj.obj) (f : T.cocharacterLattice) : CategoryTheory.CategoryStruct.comp f (T.geometricCharacterGroupSchemeMap x) = DiagonalizableGroup.powEndGroupSchemeMap ((T.characterCocharacterPairing x) f)

Composing an intrinsic geometric cocharacter with an intrinsic geometric character is the multiplicative-group power map whose exponent is their character--cocharacter pairing.

theorem TauCeti.MultiplicativeTypeCommHopfAlgCat.characterCocharacterPairing_eq_iff_comp_eq_powEndGroupSchemeMap {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) (x : CommHopfAlgCat.additiveCharacterGroup T.obj.obj) (f : T.cocharacterLattice) (n : ℤ) : (T.characterCocharacterPairing x) f = n ↔ CategoryTheory.CategoryStruct.comp f (T.geometricCharacterGroupSchemeMap x) = DiagonalizableGroup.powEndGroupSchemeMap n

The pairing is the unique exponent whose power map is the composite of the corresponding geometric cocharacter and character.

theorem TauCeti.MultiplicativeTypeCommHopfAlgCat.characterCocharacterPairing_galois_invariant {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) (σ : Field.absoluteGaloisGroup k) (x : CommHopfAlgCat.additiveCharacterGroup T.obj.obj) (f : T.cocharacterLattice) : (T.characterCocharacterPairing (σ • x)) ((T.cocharacterGaloisRepresentation σ) f) = (T.characterCocharacterPairing x) f

The character--cocharacter pairing is invariant under the diagonal absolute-Galois action.