Documentation

TauCeti.Algebra.AlgebraicGroup.GroupAlgebra.Galois.Torus

Galois descent produces a torus #

Let L / k be a finite Galois extension and let M be a lattice, that is, a torsion-free finitely generated abelian group, carrying an integral representation of Gal(L/k). The invariants of the simultaneous semilinear action on L[M] form a finite-type commutative Hopf algebra over k whose scalar extension to L is L[M] again. This file bundles the resulting affine group as an object of the finite-type coordinate category and proves that it is a torus, split by L.

This is the existence half of the Galois-descent classification of tori: every integral representation of a finite Galois group on a lattice is realised by a torus over the base field, split by the extension the representation is taken over. Identifying the geometric character lattice of that torus with the given Galois module is a separate step. Nothing here restricts the characteristic, and the action of Gal(L/k) on the lattice is arbitrary; a split torus is the case of the trivial action.

Main declarations #

References #

source
noncomputable def TauCeti.GaloisDescent.exponentGroup {M : Type u} [AddCommGroup M] [Module.Finite ℤ M] :
FGCommGrpCat

The exponent group of the split group algebra, written multiplicatively and bundled as a finitely generated commutative group.

This is the exponent group used to present the split base change; finite generation supplies the bundling.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.GaloisDescent.exponentGroup_obj {M : Type u} [AddCommGroup M] [Module.Finite ℤ M] :
    exponentGroup.obj = ↧(Multiplicative M)

    The underlying commutative group of the exponent group is M written multiplicatively.

    source
    instance TauCeti.GaloisDescent.instIsMulTorsionFreeExponentGroup {M : Type u} [AddCommGroup M] [Module.Finite ℤ M] [IsAddTorsionFree M] :
    IsMulTorsionFree ↑exponentGroup

    The exponent group of a torsion-free lattice is torsion-free.

    source
    noncomputable def TauCeti.GaloisDescent.descendedCoordinateRing {k L M : Type u} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] [Module.Finite ℤ M] (rho : Representation ℤ Gal(L/k) M) :
    FiniteTypeCommHopfAlgCat k

    The affine group descended from the diagonalizable group D(M) along a finite Galois extension, as an object of the category of finite-type commutative Hopf algebras.

    Its coordinate algebra is the invariant subalgebra (L[M])^{Gal(L/k)} for the action twisting both the coefficients and the exponents.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.GaloisDescent.descendedCoordinateRing_obj {k L M : Type u} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] [Module.Finite ℤ M] (rho : Representation ℤ Gal(L/k) M) :
      (descendedCoordinateRing rho).obj = ↧↥(groupAlgebraInvariants rho)

      The underlying Hopf algebra of the descended coordinate ring is the invariant group algebra.

      source
      noncomputable def TauCeti.GaloisDescent.descendedBaseChangeIso {k L M : Type u} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] [Module.Finite ℤ M] (rho : Representation ℤ Gal(L/k) M) :
      (descendedCoordinateRing rho).baseChange ≅ DiagonalizableGroup.coordinateRing L exponentGroup

      The descended group becomes the diagonalizable group D(M) over L.

      This is groupAlgebraInvariantsBaseChangeBialgEquiv bundled as an isomorphism of finite-type coordinate Hopf algebras over the splitting field.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.GaloisDescent.descendedBaseChangeIso_hom_apply {k L M : Type u} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] [Module.Finite ℤ M] (rho : Representation ℤ Gal(L/k) M) (x : TensorProduct k L ↥(groupAlgebraInvariants rho)) :
        (CategoryTheory.ConcreteCategory.hom (descendedBaseChangeIso rho).hom.hom) x = (groupAlgebraInvariantsBaseChangeBialgEquiv rho) x

        The forward descended splitting is the group-algebra base-change equivalence.

        source
        @[simp]
        theorem TauCeti.GaloisDescent.descendedBaseChangeIso_inv_apply {k L M : Type u} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] [Module.Finite ℤ M] (rho : Representation ℤ Gal(L/k) M) (x : MonoidAlgebra L (Multiplicative M)) :
        (CategoryTheory.ConcreteCategory.hom (descendedBaseChangeIso rho).inv.hom) x = (groupAlgebraInvariantsBaseChangeBialgEquiv rho).symm x

        The inverse descended splitting is the inverse group-algebra base-change equivalence.

        source
        theorem TauCeti.GaloisDescent.torusCommHopfAlgProperty_descendedCoordinateRing {k L M : Type u} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] [Module.Finite ℤ M] (rho : Representation ℤ Gal(L/k) M) [IsAddTorsionFree M] :
        torusCommHopfAlgProperty k (descendedCoordinateRing rho)

        The affine group descended from a Galois lattice is a torus.

        Torsion freeness of the lattice is what rules out the finite groups of multiplicative type such as μ_n; no hypothesis is placed on the characteristic of k or on the action of Gal(L/k) on the lattice.

        source
        theorem TauCeti.GaloisDescent.splitTorusCommHopfAlgProperty_baseChange_descendedCoordinateRing {k L M : Type u} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] [Module.Finite ℤ M] (rho : Representation ℤ Gal(L/k) M) [IsAddTorsionFree M] :
        splitTorusCommHopfAlgProperty L (descendedCoordinateRing rho).baseChange

        The descended torus is split by the Galois extension it was descended along.