Cubic residue symbol

DefinitionTotalized prime-ideal cubic symbol#✓fully proved

Let \(K\) be a number field that is the third cyclotomic extension of \(\mathbb{Q}\), with ring of integers \(\mathcal{O}_K\), let \(\zeta \in K\) be a primitive cube root of unity and let \(\omega\) be \(\zeta\) regarded as an element of \(\mathcal{O}_K\). For an ideal \(P\) of \(\mathcal{O}_K\) and \(a \in \mathcal{O}_K\): if \(P\) is a nonzero prime ideal whose absolute norm \(N(P)\) is coprime to \(3\), the value is \(0\) when \(a \in P\), and otherwise the unique \(c \in \{1, \omega, \omega^2\}\) with \(c \equiv a^{(N(P) - 1)/3} \pmod{P}\); for every other ideal \(P\) the value is \(1\).

public noncomputable def primeIdealCubicSymbolFactorRaw
    {zeta : K}
    (hZeta : IsPrimitiveRoot zeta 3)
    (P : Ideal (NumberField.RingOfIntegers K))
    (a : NumberField.RingOfIntegers K) : NumberField.RingOfIntegers K :=
  if hPprime : P.IsPrime then
    if hPbot : P ≠ ⊥ then
      if hCop : Nat.Coprime (Ideal.absNorm P) 3 then
        if ha : a ∈ P then 0
        else primeIdealValidCubicSymbol hZeta P a hPprime hPbot hCop ha
      else 1
    else 1
  else 1

Used by 2

Used byTotalized cubic residue symbol · Cubic residue symbol at a prime ideal

DefinitionTotalized cubic residue symbol#✓fully proved

Let \(K\) be a number field that is the third cyclotomic extension of \(\mathbb{Q}\), with ring of integers \(\mathcal{O}_K\), and let \(\zeta \in K\) be a primitive cube root of unity. For \(a, n \in \mathcal{O}_K\), the value is \(0\) if \(n = 0\); otherwise it is the product, over the prime ideals \(P\) in the factorization of the principal ideal \((n)\) counted with multiplicity, of the totalized prime-ideal cubic symbol of \(a\) at \(P\) (which is \(1\) unless \(P\) is a nonzero prime ideal whose absolute norm is coprime to \(3\)).

public noncomputable def cubicResidueSymbolRaw
    {zeta : K}
    (hZeta : IsPrimitiveRoot zeta 3)
    (a n : NumberField.RingOfIntegers K) : NumberField.RingOfIntegers K :=
  if n = 0 then 0
  else
    let I := Ideal.span ({n} : Set (NumberField.RingOfIntegers K))
    let facs := UniqueFactorizationMonoid.normalizedFactors I
    (facs.map (fun P => primeIdealCubicSymbolFactorRaw hZeta P a)).prod

Uses 1 · Used by 1

Statement usesTotalized prime-ideal cubic symbol

Used byCubic residue symbol modulo an element

DefinitionCubic residue symbol at a prime ideal#✓fully proved

Let \(K\) be a number field that is the third cyclotomic extension of \(\mathbb{Q}\), with ring of integers \(\mathcal{O}_K\), let \(\zeta \in K\) be a primitive cube root of unity and let \(\omega\) be \(\zeta\) regarded as an element of \(\mathcal{O}_K\). For a nonzero prime ideal \(P\) of \(\mathcal{O}_K\) whose absolute norm \(N(P)\) is coprime to \(3\) and for \(a \in \mathcal{O}_K\), the cubic residue symbol \((a/P)_3\) is \(0\) if \(a \in P\), and otherwise the unique \(c \in \{1, \omega, \omega^2\}\) with \(c \equiv a^{(N(P) - 1)/3} \pmod{P}\).

public noncomputable def primeIdealCubicSymbol
    {zeta : K}
    (hZeta : IsPrimitiveRoot zeta 3)
    (P : Ideal (NumberField.RingOfIntegers K))
    (a : NumberField.RingOfIntegers K)
    (_hPprime : P.IsPrime)
    (_hPbot : P ≠ ⊥)
    (_hNormCoprime : Nat.Coprime (Ideal.absNorm P) 3) :
    NumberField.RingOfIntegers K :=
  primeIdealCubicSymbolFactorRaw hZeta P a

Uses 1

Statement usesTotalized prime-ideal cubic symbol

DefinitionCubic residue denominators#✓fully proved

Let \(K\) be a number field that is the third cyclotomic extension of \(\mathbb{Q}\), with ring of integers \(\mathcal{O}_K\). An element \(n \in \mathcal{O}_K\) is a cubic residue denominator when \(n \neq 0\) and the absolute norm of the principal ideal \((n)\) is coprime to \(3\).

public def IsCubicResidueDenominator
    (n : NumberField.RingOfIntegers K) : Prop :=
  n ≠ 0 ∧ Nat.Coprime (Ideal.absNorm (Ideal.span {n})) 3

Used by 1

Used byCubic residue symbol modulo an element

DefinitionCubic residue symbol modulo an element#✓fully proved

Let \(K\) be a number field that is the third cyclotomic extension of \(\mathbb{Q}\), with ring of integers \(\mathcal{O}_K\), let \(\zeta \in K\) be a primitive cube root of unity and let \(\omega\) be \(\zeta\) regarded as an element of \(\mathcal{O}_K\). For \(a \in \mathcal{O}_K\) and a cubic residue denominator \(n\) (that is, \(n \neq 0\) and the absolute norm of the principal ideal \((n)\) is coprime to \(3\)), the cubic residue symbol \((a/n)_3\) is the product, over the prime ideals \(P\) in the factorization of \((n)\) counted with multiplicity, of the value that is \(0\) if \(a \in P\) and otherwise the unique \(c \in \{1, \omega, \omega^2\}\) with \(c \equiv a^{(N(P) - 1)/3} \pmod{P}\), where \(N(P)\) is the absolute norm of \(P\). Each such \(P\) is a nonzero prime ideal whose absolute norm is coprime to \(3\).

public noncomputable def cubicResidueSymbol
    {zeta : K}
    (hZeta : IsPrimitiveRoot zeta 3)
    (a n : NumberField.RingOfIntegers K)
    (_hValid : IsCubicResidueDenominator n) :
    NumberField.RingOfIntegers K :=
  cubicResidueSymbolRaw hZeta a n

Uses 2

Statement usesCubic residue denominators · Totalized cubic residue symbol

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.