Documentation

TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.CharacterLattice

Character groups of diagonalizable groups #

The intrinsic geometric character group of a diagonalizable coordinate ring recovers the finitely generated commutative group used to construct it. Its absolute-Galois action is trivial.

Main declarations #

References #

See J. S. Milne, Algebraic Groups (2017), Definition 12.7 and Theorems 12.8--12.9.

source
noncomputable def TauCeti.CommHopfAlgCat.geometricCharacterGroupEquivOfIso (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (G : FGCommGrpCat) (i : DiagonalizableGroup.coordinateRing (AlgebraicClosure k) G ≅ H.baseChange) :
geometricCharacterGroup H.obj ≃* ↑G

If the base change of a finite-type commutative Hopf algebra is a diagonalizable coordinate ring, its geometric character group is the group indexing that coordinate ring.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.geometricCharacterGroupEquivOfIso_apply_eq_iff (k : Type u) [Field k] (H : FiniteTypeCommHopfAlgCat k) (G : FGCommGrpCat) (i : DiagonalizableGroup.coordinateRing (AlgebraicClosure k) G ≅ H.baseChange) (x : geometricCharacterGroup H.obj) (g : ↑G) :
    (geometricCharacterGroupEquivOfIso k H G i) x = g ↔ (CategoryTheory.ConcreteCategory.hom i.inv.hom) ↑x = MonoidAlgebra.single g 1

    Characterization of the character corresponding to an index under geometricCharacterGroupEquivOfIso.

    source
    noncomputable def TauCeti.DiagonalizableGroup.geometricCharacterGroupEquiv (k : Type u) [Field k] (G : FGCommGrpCat) :
    CommHopfAlgCat.geometricCharacterGroup (coordinateRing k G).obj ≃* ↑G

    The intrinsic geometric character group of a diagonalizable coordinate ring is the finitely generated commutative group used to construct it.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.DiagonalizableGroup.geometricCharacterGroupEquiv_apply_eq_iff (k : Type u) [Field k] (G : FGCommGrpCat) (x : CommHopfAlgCat.geometricCharacterGroup (coordinateRing k G).obj) (g : ↑G) :
      (geometricCharacterGroupEquiv k G) x = g ↔ (MonoidAlgebra.scalarTensorBialgEquiv k (AlgebraicClosure k)) ↑x = MonoidAlgebra.single g 1

      A geometric character corresponds to g exactly when base change identifies its underlying group-like element with the standard monomial indexed by g.

      source
      @[simp]
      theorem TauCeti.DiagonalizableGroup.geometricCharacterGroupEquiv_symm_apply_val (k : Type u) [Field k] (G : FGCommGrpCat) (g : ↑G) :
      ↑((geometricCharacterGroupEquiv k G).symm g) = 1 ⊗ₜ[k] MonoidAlgebra.single g 1

      The inverse character corresponding to g is the standard monomial indexed by g, viewed in the scalar-extended coordinate ring.

      source
      @[simp]
      theorem TauCeti.DiagonalizableGroup.smul_geometricCharacterGroup_eq_self (k : Type u) [Field k] (G : FGCommGrpCat) (σ : Field.absoluteGaloisGroup k) (x : CommHopfAlgCat.geometricCharacterGroup (coordinateRing k G).obj) :
      σ • x = x

      The absolute Galois action on the geometric character group of a diagonalizable coordinate ring is trivial.