Going from a place of Q to a natural prime which generates i

Stream: Is there code for X?

[Stepan Nesterov]

Is there a function which takesv : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ) and returns a p :Nat.Prime, such that v is the p-adic valuation?

[Kenny Lau]

@Stepan Nesterov Submodule.IsPrincipal.generator followed with Int.natAbs would work

(well, after you map it using Rat.ringOfIntegersEquiv)

[Yakov Pechersky]

docs#Ideal.isPrime_int_iff

[Yakov Pechersky]

docs#Rat.ringOfIntegersEquiv

[Yakov Pechersky]

docs#Ideal.IsPrime.comap

[Stepan Nesterov]

Thank you @Kenny Lau @Yakov Pechersky !!
Does this code look good or are there obvious inefficiencies that I should fix?

noncomputable def toNatPrime
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)) :
  {p : ℕ // Nat.Prime p} :=
by
  let e : NumberField.RingOfIntegers ℚ ≃+* ℤ := Rat.ringOfIntegersEquiv
  let I : Ideal ℤ := Ideal.comap e.symm.toRingHom v.asIdeal
  have I_def : I = Ideal.comap e.symm.toRingHom v.asIdeal := rfl
  have vprime := v.isPrime
  have vnebot := v.ne_bot
  have Iprime : I.IsPrime := by
    rw[I_def]
    exact Ideal.comap_isPrime e.symm.toRingHom v.asIdeal
  rw[Ideal.isPrime_int_iff] at Iprime
  have hIne : I ≠ ⊥ := by
    rw[I_def]
    have hsurj := RingEquiv.surjective e.symm
    have := Ideal.map_comap_of_surjective e.symm.toRingHom hsurj v.asIdeal
    intro hyp
    rw[hyp] at this
    simp at this
    symm at this
    exact vnebot this
  have Iprime' := Or.resolve_left Iprime hIne
  use Classical.choose Iprime'
  exact (Classical.choose_spec Iprime').1

[Xavier Roblot]

import Mathlib

noncomputable def toNatPrime
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)) :
  {p : ℕ // Nat.Prime p} := by
  refine ⟨Ideal.absNorm (Ideal.under ℤ v.asIdeal), ?_⟩
  have vnezero : NeZero v.asIdeal := ⟨v.ne_bot⟩
  apply Nat.absNorm_under_prime

[Yakov Pechersky]

Which lends itself to an equiv easier?

[Xavier Roblot]

I guess it depends on what you want to do with it. I don't think it's difficult to make this def into an equiv but then it will be given by v ↦ Ideal.absNorm (Ideal.under ℤ v.asIdeal) which might or might not be easy to use depending on the application. Note that there is some API for it, for example the result docs#Int.absNorm_under_eq_sInf that says that this is the smallest positive integer contained in v.asIdeal.