Documentation

TauCeti.Algebra.AlgebraicGroup.CommHopfAlgCat.CharacterLattice.Basic

Geometric character groups and their Galois action #

For a commutative Hopf algebra H over a field k, its geometric characters are the group-like elements of its coordinate algebra after extension to an algebraic closure:

X*(H) = GroupLike k̄ (k̄ ⊗[k] H).

The generic scalar action from TauCeti.Algebra.Bialgebra.GroupLike.ScalarAut specializes to the absolute Galois group and acts by σ • (a ⊗ h) = σ(a) ⊗ h. Its actions on the scalar extension, the group-like elements, and their additive form are available through the instances ScalarAut.instMulSemiringAction, ScalarAut.instGroupLikeDistribMulAction, and Additive.distribMulAction; this module supplies the instance bridges needed for the opaque Field.absoluteGaloisGroup definition.

Main declarations #

References #

For the torus character-module viewpoint motivating this construction, see J. S. Milne, Algebraic Groups (2017), §§12.14--12.17. The scalar-action lemmas themselves are generic bialgebra facts.

source
@[reducible, inline]
abbrev TauCeti.CommHopfAlgCat.geometricCharacterGroup {k : Type u} [Field k] (H : CommHopfAlgCat k) :
Type u

The geometric character group of a commutative Hopf algebra: the group-like elements of its coordinate algebra after extension to an algebraic closure. For a represented affine group, these are exactly its morphisms over k̄ to the multiplicative group.

Equations
Instances For
    source
    @[reducible, inline]
    noncomputable instance TauCeti.CommHopfAlgCat.instMulSemiringActionAlgebraicClosure {k : Type u} [Field k] :
    MulSemiringAction (Field.absoluteGaloisGroup k) (AlgebraicClosure k)

    Bridge the tautological action across the opaque Field.absoluteGaloisGroup definition.

    Equations
    source
    @[reducible, inline]
    noncomputable instance TauCeti.CommHopfAlgCat.instGaloisScalarMulSemiringAction {k : Type u} [Field k] {A : Type v} [Semiring A] [Algebra k A] :
    MulSemiringAction (Field.absoluteGaloisGroup k) (TensorProduct k (AlgebraicClosure k) A)

    Bridge the generic scalar action across the opaque Field.absoluteGaloisGroup definition.

    Equations
    source
    @[reducible, inline]
    noncomputable instance TauCeti.CommHopfAlgCat.instGeometricCharacterGroupGaloisAction {k : Type u} [Field k] {A : Type v} [Semiring A] [Bialgebra k A] :
    MulDistribMulAction (Field.absoluteGaloisGroup k) (GroupLike (AlgebraicClosure k) (TensorProduct k (AlgebraicClosure k) A))

    Bridge the generic group-like action across the opaque absolute-Galois-group definition.

    Equations
    source
    @[reducible, inline]
    abbrev TauCeti.CommHopfAlgCat.additiveCharacterGroup {k : Type u} [Field k] (H : CommHopfAlgCat k) :
    Type u

    The additive form of the geometric character group of a commutative Hopf algebra. For a torus its underlying additive group is free of finite rank.

    Equations
    Instances For
      source
      @[reducible, inline]
      noncomputable instance TauCeti.CommHopfAlgCat.instAdditiveCharacterGroupGaloisAction {k : Type u} [Field k] {A : Type v} [Semiring A] [Bialgebra k A] :
      DistribMulAction (Field.absoluteGaloisGroup k) (Additive (GroupLike (AlgebraicClosure k) (TensorProduct k (AlgebraicClosure k) A)))

      Bridge the generic additive action across the opaque absolute-Galois-group definition.

      Equations
      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.val_smul {k : Type u} [Field k] {A : Type v} [Semiring A] [Bialgebra k A] (sigma : Field.absoluteGaloisGroup k) (x : GroupLike (AlgebraicClosure k) (TensorProduct k (AlgebraicClosure k) A)) :
      ↑(sigma • x) = (have this := sigma; this) • ↑x

      The underlying value of the absolute-Galois action on a scalar-extended group-like element.

      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.toMul_smul {k : Type u} [Field k] {A : Type v} [Semiring A] [Bialgebra k A] (sigma : Field.absoluteGaloisGroup k) (x : Additive (GroupLike (AlgebraicClosure k) (TensorProduct k (AlgebraicClosure k) A))) :
      Additive.toMul (sigma • x) = sigma • Additive.toMul x

      Passing from additive to multiplicative group-like elements commutes with the absolute-Galois action.