Artin L-functions

StructureArtin local datum#✓fully proved

For a finite group \(G\), an Artin local datum consists of a subgroup \(D \le G\) (the decomposition group), a normal subgroup \(I\) of \(D\) (the inertia group), and an element \(\sigma\) of the quotient group \(D/I\) (the Frobenius coset).

In the arithmetic application, \(L/\mathbb{Q}\) is a finite Galois extension with \(G = \mathrm{Gal}(L/\mathbb{Q})\), \(D\) is the decomposition group at a place \(w\) of \(L\) above a prime \(p\), \(I\) is its inertia group and \(\sigma\) is the Frobenius. A complex representation of \(G\) restricted to \(D\) then gives an action of \(D/I\) on the \(I\)-invariant vectors, on which \(\sigma\) acts as the local operator. The definition does not require the data to arise this way.

structure ArtinLocalDatum (G : Type u) [Group G] [Finite G] where
  decomposition : Subgroup G
  inertia : Subgroup decomposition
  [isNormal : inertia.Normal]
  frobenius : decomposition ⧸ inertia

Used by 8

Used byEuler product of Artin local factors · Artin local denominator · Artin local factor · Artin local factor of a one-dimensional trivial Frobenius action · Artin local factor when Frobenius acts trivially · Regularity of the Artin local factor · Convergent Artin Euler product · Nonzero convergent Artin Euler product

DefinitionArtin local denominator#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), let \(p\) be a prime, let \((D, I, \sigma)\) be an Artin local datum for \(G\), and let \(s \in \mathbb{C}\). Let \(V^{I}\) be the subspace of vectors fixed by \(\rho(I)\), on which \(D/I\) acts, and let \(\rho(\sigma)\) be the action of \(\sigma\) on \(V^{I}\). The Artin local denominator is

\[\det\left(\mathrm{id} - p^{-s}\,\rho(\sigma) \mid V^{I}\right).\]

noncomputable def artinLocalDenominator (ρ : Representation ℂ G V)
    [Module.Free ℂ V] [Module.Finite ℂ V] (p : Nat.Primes)
    (d : ArtinLocalDatum G) (s : ℂ) : ℂ :=
  LinearMap.det
    (LinearMap.id - ((p.1 : ℂ) ^ (-s)) •
      ((Representation.quotientToInvariants
        (ρ.comp d.decomposition.subtype : Representation ℂ d.decomposition V)
        d.inertia) d.frobenius))

Uses 1 · Used by 3

Statement usesArtin local datum

Used byArtin local factor · Artin local factor when Frobenius acts trivially · Regularity of the Artin local factor

DefinitionRegularity of the Artin local factor#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), let \(p\) be a prime, let \(d\) be an Artin local datum for \(G\), and let \(s \in \mathbb{C}\). The Artin local factor of \(\rho\) at \(p\), \(d\) is regular at \(s\) when the Artin local denominator of \(\rho\) at \(p\), \(d\) and \(s\) is nonzero, that is, when the local factor has no pole at \(s\).

def ArtinLocalFactorRegular (ρ : Representation ℂ G V)
    [Module.Free ℂ V] [Module.Finite ℂ V] (p : Nat.Primes)
    (d : ArtinLocalDatum G) (s : ℂ) : Prop :=
  artinLocalDenominator ρ p d s ≠ 0

Uses 2

Statement usesArtin local datum · Artin local denominator

DefinitionArtin local factor#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), let \(p\) be a prime, let \((D, I, \sigma)\) be an Artin local datum for \(G\), and let \(s \in \mathbb{C}\). Let \(V^{I}\) be the subspace of vectors fixed by \(\rho(I)\) and \(\rho(\sigma)\) the induced action of \(\sigma \in D/I\) on it. The Artin local factor is the inverse of the Artin local denominator,

\[\det\left(\mathrm{id} - p^{-s}\,\rho(\sigma) \mid V^{I}\right)^{-1},\]

with the value \(0\) when the denominator vanishes.

Where the denominator vanishes the true factor has a pole; the regularity condition picks out the \(s\) at which this value is a genuine finite Euler factor.

noncomputable def artinLocalFactorRaw (ρ : Representation ℂ G V)
    [Module.Free ℂ V] [Module.Finite ℂ V] (p : Nat.Primes)
    (d : ArtinLocalDatum G) (s : ℂ) : ℂ :=
  (artinLocalDenominator ρ p d s)⁻¹

Uses 2 · Used by 4

Statement usesArtin local datum · Artin local denominator

Used byEuler product of Artin local factors · Artin local factor of a one-dimensional trivial Frobenius action · Artin local factor when Frobenius acts trivially · Convergent Artin Euler product

DefinitionEuler product of Artin local factors#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), and suppose that for every prime \(p\) an Artin local datum \(d_p\) for \(G\) is given. For \(s \in \mathbb{C}\), this is the product over all primes \(p\) of the Artin local factors of \(\rho\) at \(p\), \(d_p\) and \(s\), taken as an unconditional infinite product (the limit of the products over finite sets of primes); when this product does not converge, the value is \(1\) by convention.

The data need not come from the places of a number field, and no independence of the choice of place above \(p\) is asserted.

noncomputable def artinEulerProductOfLocalData (ρ : Representation ℂ G V)
    [Module.Free ℂ V] [Module.Finite ℂ V]
    (localData : Nat.Primes → ArtinLocalDatum G) (s : ℂ) : ℂ :=
  ∏' p, artinLocalFactorRaw ρ p (localData p) s

Uses 2

Statement usesArtin local datum · Artin local factor

DefinitionConvergent Artin Euler product#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), let \(d_p\) be an Artin local datum for \(G\) for every prime \(p\), and let \(s, z \in \mathbb{C}\). The Artin Euler product of \(\rho\) and \((d_p)\) has value \(z\) at \(s\) when the products of the Artin local factors of \(\rho\) at \(p\), \(d_p\) and \(s\) over finite sets of primes \(p\) converge to \(z\) as the finite set grows to all primes (unconditional convergence). The value \(z = 0\) is allowed.

def HasArtinEulerProduct (ρ : Representation ℂ G V)
    [Module.Free ℂ V] [Module.Finite ℂ V]
    (localData : Nat.Primes → ArtinLocalDatum G) (s z : ℂ) : Prop :=
  HasProd (fun p => artinLocalFactorRaw ρ p (localData p) s) z

Uses 2 · Used by 1

Statement usesArtin local datum · Artin local factor

Used byNonzero convergent Artin Euler product

DefinitionNonzero convergent Artin Euler product#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), let \(d_p\) be an Artin local datum for \(G\) for every prime \(p\), and let \(s, z \in \mathbb{C}\). The Artin Euler product of \(\rho\) and \((d_p)\) has nonzero value \(z\) at \(s\) when it has value \(z\) at \(s\) and \(z \ne 0\).

In particular every local factor is then regular at \(s\): a factor whose denominator vanishes has value \(0\) and would force the product to be \(0\), so this describes a genuine finite Euler-product value rather than a pole.

def HasNonzeroArtinEulerProduct (ρ : Representation ℂ G V)
    [Module.Free ℂ V] [Module.Finite ℂ V]
    (localData : Nat.Primes → ArtinLocalDatum G) (s z : ℂ) : Prop :=
  HasArtinEulerProduct ρ localData s z ∧ z ≠ 0

Uses 2

Statement usesArtin local datum · Convergent Artin Euler product

TheoremArtin local factor when Frobenius acts trivially#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), let \(p\) be a prime, let \((D, I, \sigma)\) be an Artin local datum for \(G\), and let \(s \in \mathbb{C}\). Let \(V^{I}\) be the subspace of vectors fixed by \(\rho(I)\) and \(n = \dim V^{I}\). If \(\sigma\) acts as the identity on \(V^{I}\), then the Artin local factor of \(\rho\) at \(p\), \((D, I, \sigma)\) and \(s\) equals \(\left((1 - p^{-s})^{n}\right)^{-1}\), where the inverse of \(0\) is read as \(0\).

theorem artinLocalFactorRaw_of_action_eq_id_general (ρ : Representation ℂ G V)
    [Module.Free ℂ V] [Module.Finite ℂ V] (p : Nat.Primes)
    (d : ArtinLocalDatum G) (s : ℂ)
    (hact : (Representation.quotientToInvariants
      (ρ.comp d.decomposition.subtype : Representation ℂ d.decomposition V)
      d.inertia) d.frobenius = LinearMap.id) :
    artinLocalFactorRaw ρ p d s =
      ((1 - (p.1 : ℂ) ^ (-s)) ^ Module.finrank ℂ (invariants
      ((ρ.comp d.decomposition.subtype : Representation ℂ d.decomposition V).comp
        d.inertia.subtype)))⁻¹

Uses 3 · Used by 1

Statement usesArtin local datum · Artin local factor

Proof usesArtin local denominator

Used byArtin local factor of a one-dimensional trivial Frobenius action

TheoremArtin local factor of a one-dimensional trivial Frobenius action#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), let \(p\) be a prime, let \((D, I, \sigma)\) be an Artin local datum for \(G\), and let \(s \in \mathbb{C}\). Let \(V^{I}\) be the subspace of vectors fixed by \(\rho(I)\). If \(\sigma\) acts as the identity on \(V^{I}\) and \(V^{I}\) is one-dimensional, then the Artin local factor of \(\rho\) at \(p\), \((D, I, \sigma)\) and \(s\) equals \((1 - p^{-s})^{-1}\), where the inverse of \(0\) is read as \(0\).

This is the unramified trivial-character case, which gives the local factor of the Riemann zeta function.

theorem artinLocalFactorRaw_of_action_eq_id (ρ : Representation ℂ G V)
    [Module.Free ℂ V] [Module.Finite ℂ V] (p : Nat.Primes)
    (d : ArtinLocalDatum G) (s : ℂ)
    (hact : (Representation.quotientToInvariants
      (ρ.comp d.decomposition.subtype : Representation ℂ d.decomposition V)
      d.inertia) d.frobenius = LinearMap.id)
    (hdim : Module.finrank ℂ (invariants
      ((ρ.comp d.decomposition.subtype : Representation ℂ d.decomposition V).comp
        d.inertia.subtype)) = 1) :
    artinLocalFactorRaw ρ p d s = (1 - (p.1 : ℂ) ^ (-s))⁻¹

Uses 3

Statement usesArtin local datum · Artin local factor

Proof usesArtin local factor when Frobenius acts trivially

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.