Documentation

TauCeti.NumberTheory.DirichletCharacter.GaussSum

Primitive Dirichlet Gauss sums in characteristic zero #

This file extends the Gauss-sum API from finite fields to primitive Dirichlet characters of an arbitrary level. For a primitive character χ and a primitive additive character e of ZMod N, the product of the Gauss sums for (χ, e) and (χ⁻¹, e⁻¹) is N. For a quadratic character this gives the familiar square formula gaussSum χ e ^ 2 = χ (-1) * N.

The characteristic-zero specialization gaussSumOfPrimitiveRoot χ hζ uses the additive character defined by a primitive root of unity ζ. Its Galois action is χ⁻¹ applied to the cyclotomic character, so its stabilizer is the kernel of χ. This is the form needed to identify quadratic subfields of cyclotomic fields.

The Gauss-sum identities are classical; see K. Ireland and M. Rosen, A Classical Introduction to Modern Number Theory, Chapter 6.

Gauss sums of primitive Dirichlet characters #

source
theorem DirichletCharacter.gaussSum_mul_gaussSum_inv_eq_card_of_isPrimitive {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} [NeZero n] {χ : DirichletCharacter R n} (hχ : χ.IsPrimitive) {e : AddChar (ZMod n) R} (he : e.IsPrimitive) :
gaussSum χ e * gaussSum χ⁻¹ e⁻¹ = ↑(Fintype.card (ZMod n))

The Gauss sums of a primitive Dirichlet character and its inverse, taken against inverse additive characters, multiply to the level. This holds for composite levels, unlike the finite-field result gaussSum_mul_gaussSum_eq_card.

source
theorem DirichletCharacter.gaussSum_sq_of_isPrimitive_of_isQuadratic {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} [NeZero n] {χ : DirichletCharacter R n} (hχ : χ.IsPrimitive) (hquad : MulChar.IsQuadratic χ) {e : AddChar (ZMod n) R} (he : e.IsPrimitive) :
gaussSum χ e ^ 2 = χ (-1) * ↑(Fintype.card (ZMod n))

The square of the Gauss sum of a primitive quadratic Dirichlet character is its value at -1 times the level.

Galois action in characteristic zero #

source
noncomputable def DirichletCharacter.gaussSumOfPrimitiveRoot {L : Type u_1} [Field L] {N : ℕ} [NeZero N] (χ : DirichletCharacter ℤ N) {ζ : L} (hζ : IsPrimitiveRoot ζ N) :
L

The Gauss sum of an integer-valued Dirichlet character, formed with the additive character defined by a primitive root of unity in a characteristic-zero field.

Equations
Instances For
    source
    theorem DirichletCharacter.gaussSumOfPrimitiveRoot_def {L : Type u_1} [Field L] {N : ℕ} [NeZero N] (χ : DirichletCharacter ℤ N) {ζ : L} (hζ : IsPrimitiveRoot ζ N) :
    χ.gaussSumOfPrimitiveRoot hζ = gaussSum (MulChar.ringHomComp χ (Int.castRingHom L)) (AddChar.zmodChar N ⋯)

    Expresses gaussSumOfPrimitiveRoot using the underlying Dirichlet Gauss sum.

    source
    theorem DirichletCharacter.gaussSumOfPrimitiveRoot_sq {L : Type u_1} [Field L] [CharZero L] {N : ℕ} [NeZero N] (χ : DirichletCharacter ℤ N) (hχ : χ.IsPrimitive) (hquad : MulChar.IsQuadratic χ) {ζ : L} (hζ : IsPrimitiveRoot ζ N) :
    χ.gaussSumOfPrimitiveRoot hζ ^ 2 = (MulChar.ringHomComp χ (Int.castRingHom L)) (-1) * ↑(Fintype.card (ZMod N))

    The square formula for the Gauss sum formed from a primitive root of unity.

    source
    theorem DirichletCharacter.map_gaussSumOfPrimitiveRoot {L : Type u_1} [Field L] [CharZero L] {N : ℕ} [NeZero N] (χ : DirichletCharacter ℤ N) {ζ : L} (hζ : IsPrimitiveRoot ζ N) (σ : Gal(L/ℚ)) :
    σ (χ.gaussSumOfPrimitiveRoot hζ) = (MulChar.ringHomComp χ (Int.castRingHom L))⁻¹ ↑((IsPrimitiveRoot.autToPow ℚ hζ) σ) * χ.gaussSumOfPrimitiveRoot hζ

    A Galois automorphism acts on a Dirichlet Gauss sum through the inverse character evaluated at its cyclotomic character.

    source
    theorem DirichletCharacter.gaussSumOfPrimitiveRoot_ne_zero {L : Type u_1} [Field L] [CharZero L] {N : ℕ} [NeZero N] (χ : DirichletCharacter ℤ N) (hχ : χ.IsPrimitive) {ζ : L} (hζ : IsPrimitiveRoot ζ N) :
    χ.gaussSumOfPrimitiveRoot hζ ≠ 0

    The Gauss sum attached to a primitive integer-valued Dirichlet character does not vanish in a characteristic-zero field.

    source
    theorem DirichletCharacter.stabilizer_gaussSumOfPrimitiveRoot {L : Type u_1} [Field L] [CharZero L] {N : ℕ} [NeZero N] (χ : DirichletCharacter ℤ N) (hχ : χ.IsPrimitive) {ζ : L} (hζ : IsPrimitiveRoot ζ N) :
    MulAction.stabilizer Gal(L/ℚ) (χ.gaussSumOfPrimitiveRoot hζ) = ((MulChar.toUnitHom χ).comp (IsPrimitiveRoot.autToPow ℚ hζ)).ker

    The stabilizer of a primitive Dirichlet Gauss sum is the kernel of the character composed with the cyclotomic character.