A rational which is a p-adic integer for all p is an integer.

[kbuzzard]

Sounds easy, but when I say "p-adic integer for all p" I unfortunately actually mean

 ∀ (v : IsDedekindDomain.HeightOneSpectrum (𝓞 ℚ)),
  ↑((algebraMap ℚ (FiniteAdeleRing (𝓞 ℚ) ℚ)) x) v ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v

so that adds a bit of a twist. Probably one should start by proving that for all such v, there's a prime p : Nat such that v=(p), and then show that ↑((algebraMap ℚ (FiniteAdeleRing (𝓞 ℚ) ℚ)) x) v ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v is an interesting way of saying that p doesn't divide the denominator of v.

[Ruben-VandeVelde]

claim

at least for a little bit

[Ruben-VandeVelde]

claim

[kbuzzard]

I wonder whether we shouldn't be wasting our time with this and should refactor adeles so that they allow us to supply a Dedekind domain (like for finite adeles), meaning that we can just replace all this nonsense with \Z.

[Ruben-VandeVelde]

disclaim

[Ruben-VandeVelde]

Sorry for keeping this claimed - I started with

        intro p hp hpdvd
        let p' : IsDedekindDomain.HeightOneSpectrum (𝓞 ℚ) := {
          asIdeal := Ideal.span {(p : 𝓞 ℚ)}
          isPrime := by
            rw [Ideal.span_singleton_prime (by simp [hp.ne_zero])]
            have := map_prime Rat.ringOfIntegersEquiv.symm (Nat.prime_iff_prime_int.mp hp)
            simpa
          ne_bot := by simp [hp.ne_zero]
        }

but didn't get anywhere and didn't have time to look further