Project idea: Power residue symbols

Stream: LFTCM 2024

[Chris Birkbeck]

The idea is to define power residue symbols see the definition here. For this we might need to first define residue fields for rings of integers (or maybe more generally Dedekind domains). Then its "just" playing around with roots of unity

[Chris Birkbeck]

Here is a mess of ideas on how to start this that you can just copy-paste:

import Mathlib.NumberTheory.Cyclotomic.Basic
import Mathlib.RingTheory.Ideal.Norm

open scoped NumberField BigOperators

variable {F : Type*} [Field F] [NumberField F] (ζ : 𝓞 F) (n : ℕ) (h : IsPrimitiveRoot ζ n)

/--The residue field of a number field (specifically the ring of intergers) at a prime-/
def ResidueFieldAtPrime (p : Ideal (𝓞 F)) (hp : Ideal.IsPrime p) :=
  LocalRing.ResidueField (Localization.AtPrime p)

/--The residue field of a number field (specifically the ring of intergers) at a prime-/
def ResidueFieldAtPrime2 (p : Ideal (𝓞 F)) (hp : Ideal.IsPrime p) :=  𝓞 F ⧸ p

variable (p : Ideal (𝓞 F)) (hp : Ideal.IsPrime p)

noncomputable instance : Field (ResidueFieldAtPrime p hp) := by
  apply LocalRing.ResidueField.field

noncomputable instance (hp2 : p ≠ ⊥) : Field (ResidueFieldAtPrime2 p hp) := by
  have h : Ideal.IsMaximal p := by
    apply Ideal.IsPrime.isMaximal hp hp2
  apply Ideal.Quotient.field

def residue_map : 𝓞 F →+* (ResidueFieldAtPrime p hp) :=
  (LocalRing.residue (Localization.AtPrime p)).comp (algebraMap (𝓞 F) (Localization.AtPrime p))

instance inst1 (hp2: p ≠ ⊥) : Fintype (ResidueFieldAtPrime2 p hp) := by
  sorry

lemma norm_div_lemmas (p : Ideal (𝓞 F)) (hp : Ideal.IsPrime p)
      (hpn : p ⊔ Ideal.span ({(n : (𝓞 F))} : Set (𝓞 F)) = ⊤) : n  ∣ ((Ideal.absNorm p) - 1) := by
    sorry

lemma exits_pth_root (a : 𝓞 F) (p : Ideal (𝓞 F)) (hp : Ideal.IsPrime p)
    (hpn : p ⊔ Ideal.span ({(n * a : (𝓞 F))} : Set (𝓞 F)) = ⊤) :
  ∃! (i : ℕ), (a ^ (((Ideal.absNorm p) - 1) / n)) -  ζ^i ∈ p := by sorry

[Edgar Costa]

@Chris Birkbeck are ideals computable in mathlib?

[Chris Birkbeck]

When you say computable, which sense do you mean?

[Edgar Costa]

I mean, in the practical sense, given two ideals defined by its generators $I_1, I_2$, can one for example compute $I_1 I_2$?

I am just curious if one would be able to apply the residue map to a concrete ideal, or it will be totally theoretical.

[Johan Commelin]

It will be theoretical, but you can prove a lemma for ideals generated by explicit elements that will "compute" for you

[Johan Commelin]

If you label it with @[simp] then the simp tactic will use it automatically

[Chris Birkbeck]

Actually computing something can be quite difficult! I expect we have results that describe the product of two ideals in terms of the generators of each one. But if it lets you say (2)(3)=(6), I'm don't know if that works (but maybe I'm wrong!)

[Edgar Costa]

Sure, maybe the right approach would not be having lean to compute it, but have a tactic that calls a CAS to express both generators in terms of the other, and thus establish equality

[Chris Birkbeck]

Ok I've made a repository for this: If you follow these instructions it should download it for you:

https://github.com/CBirkbeck/power_residue_symbols
cd power_residue_symbols
lake exe cache get
lake build

[Chris Birkbeck]

I propose we meet up after Amelia's talk this afternoon and we can chat about how to approach this!

[Chris Birkbeck]

I'll be near the front of the lecture theatre, so we can group there and organise ourselves!

[Ramla ABDELLATIF]

Chris Birkbeck said:

I'll be near the front of the lecture theatre, so we can group there and organise ourselves!

I gather my stuffs and I join you!

[Chris Birkbeck]

This might be useful for proving that the roots are distinct modulo p: Polynomial.X_pow_sub_one_separable_iff

[Edgar Costa]

I was thinking of IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic, so that
$\zeta - 1 \in P$ that relates $\operatorname{Nm} P$ with $\phi_n(1) = \operatorname{Nm}(\zeta - 1) =$ 1 or $q$ if $n = q^k$

[Sandra Rozensztajn]

We can probably do a proof like this:

• show that n is not zero in the quotient ring
• define P(X) = (X^n-1)/(X-1), so that (in characteristic 0) P(1) = n and P(\zeta^i) = 0 if n does not divide i.
• assuming that 1 and \zeta^i are congruent modulo p, obtain a contradiction if n does not divide i

So we avoid working with the norm of \zeta - 1, or separabilty.

[Chris Birkbeck]

ok I added a proof that the reduction mod p of the primitive root is still a primitive root: primitivemodp'. The key is to use the link to cyclotomic polynomials and roots under ring homs. it still has one sorry asking that n is not zero in the residue field, but that should be easy.