refactor of adeles

Stream: mathlib4

[Kevin Buzzard]

In FLT I am proving theorems about adeles and adelic objects in the following way: we're mid-way through a proof that $\mathbb{A}_K\otimes_KL\cong\mathbb{A}_L$ (if people would like to join in then let me know), and this enables us to reduce certain results about adeles of a general number field to the adeles of $\mathbb{Q}$, which, unfortunately, is a PITA to work with currently because its definition uses $\mathcal{O}_{\mathbb{Q}}$ which isn't equal to $\mathbb{Z}$.

To give a concrete example of the issues this raises, I would like to prove, as part of a theorem about the adeles of the rationals, that a rational number $x$ which is a $p$-adic integer for all $p$, is actually an integer. I certainly fancy my chances doing this in one sitting if that were the actual statement of what I want. However the actual hypothesis right now with our current definition of adeles is

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

which I think is going to be a lot more fiddly.

There are several ways to proceed here. One way would be to establish the isomorphism 𝓞 ℚ = $\Z$ and just push everything along this isomorphism. To be honest I am unclear about whether this is something that we should be doing, even though I'm fairly confident that it should be possible, although it will be quite a slog.

Another approach, which is super-painless, is to simply redefine adeles by asking for a number field and for a second type whose field of fractions is the number field, exactly as we do for finite adeles. The reason this is so painless is that mathlib has adeles in a leaf file which is only 150 lines long. The PR #20500 does this. I'm aware of the work of @Salvatore Mercuri on adeles, but I am hoping that this change will be not that disruptive (and might even help). I suspect that this approach will also not disrupt the $\mathbb{A}_K\otimes_K L\cong\mathbb{A}_L$ work we have in FLT, because we have this robust "AKLB" set-up which should take care of everything.

Are there arguments for not merging #20500 and instead powering through with the substitution of 𝓞 ℚ with $\Z$ in e.g. the hypothesis I quoted above? Perhaps one argument for keeping things as they are is that actually if R is a Dedekind domain with field of fractions K then it might well be the case that an element of K which is v-integral for all height one primes of R is in R, and perhaps this is something we should have anyway. But this is just the first example I've run into, there could be more.

[Kevin Buzzard]

OK well it's been merged so I guess that's the end of the discussion :-)

[Michael Stoll]

Kevin Buzzard said:

One way would be to establish the isomorphism 𝓞 ℚ = Z

This exists: docs#Rat.ringOfIntegersEquiv .

[Ruben Van de Velde]

I think I used that, but it didn't get me anywhere

[Ruben Van de Velde]

(Could still have been a skill issue, of course :))

[Salvatore Mercuri]

There'll be minimal disruption for me I think! Most of the locally compact work is done for general R K and only switched to RingOfIntegers K at the last moment.

[Salvatore Mercuri]

I think it makes sense to allow for the R input in AdeleRing, especially as FiniteAdeleRing already allows for this. I'm now wondering why I even switched over to RingOfIntegers in the first place!

[Kevin Buzzard]

It's funny, because since I posted this I am thinking "what am I fussing about? Let's just make the right API". For example is this true?

import Mathlib

open NumberField DedekindDomain IsDedekindDomain

theorem is_integral (R K : Type*) [CommRing R] [Field K]
  [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (x : K)
      (h2 :
      ∀ (v : HeightOneSpectrum R),
        ((algebraMap K (FiniteAdeleRing R K)) x) v ∈
          HeightOneSpectrum.adicCompletionIntegers K v) :
    ∃ (y : R), algebraMap R K y = x := by
  sorry

Probably the sorry which inspired this PR follows easily from this.

[Kevin Buzzard]

Indeed the sorry I want follows from the above theorem and

import Mathlib

open NumberField

example (z : 𝓞 ℚ) : (Rat.ringOfIntegersEquiv z : ℚ) = algebraMap (𝓞 ℚ) ℚ z := sorry

(which I can't immediately do)

[Junyan Xu]

I think this is what I did in Lean 3 here.

[Kevin Buzzard]

import Mathlib

open NumberField

open DedekindDomain IsDedekindDomain

open HeightOneSpectrum

variable (R K : Type*) [CommRing R] [Field K] [IsDedekindDomain R] [Algebra R K]
    [IsFractionRing R K]
theorem heightOneSpectrum.mem_integers_of_valuation_le_one (x : K)
    (h : ∀ v : HeightOneSpectrum R, v.valuation x ≤ 1) : x ∈ (algebraMap R K).range := by
  obtain ⟨⟨x', y, hy⟩, hy1⟩ := IsLocalization.surj (nonZeroDivisors R) x
  dsimp at hy1
  obtain rfl : x = IsLocalization.mk' K x' ⟨y, hy⟩ := IsLocalization.eq_mk'_iff_mul_eq.mpr hy1
  have hy' := nonZeroDivisors.ne_zero hy
  obtain rfl | hx' := eq_or_ne x' 0
  · simp_all
  suffices Ideal.span {y} ∣ (Ideal.span {x'} : Ideal R) by
    obtain ⟨z, rfl⟩ := Ideal.span_singleton_le_span_singleton.1 (Ideal.le_of_dvd this)
    use z
    rw [map_mul, mul_comm,mul_eq_mul_left_iff] at hy1
    cases' hy1 with h h
    · exact h.symm
    · simp [hy'] at h
  classical
  rw [← Associates.mk_le_mk_iff_dvd, ← Associates.factors_le]
  have ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥ := λ {r} hr => mt Ideal.span_singleton_eq_bot.mp hr
  rw [Associates.factors_mk _ (ine hx'), Associates.factors_mk _ (ine hy')]
  rw [WithTop.coe_le_coe, Multiset.le_iff_count]
  rintro ⟨v, hv⟩
  obtain ⟨v, rfl⟩ := Associates.mk_surjective v
  have hv' := hv
  rw [Associates.irreducible_mk, irreducible_iff_prime] at hv
  specialize h ⟨v, Ideal.isPrime_of_prime hv, hv.ne_zero⟩
  rw [valuation_of_mk', intValuation, ← Valuation.toFun_eq_coe] at h
  dsimp only [Subtype.coe_mk] at h
  rw [intValuationDef_if_neg _ hx', intValuationDef_if_neg _ hy'] at h
  rw [← WithZero.coe_div, ← WithZero.coe_one, WithZero.coe_le_coe, ← ofAdd_sub, ← ofAdd_zero] at h
  simp at h
  rw [Associates.factors_mk _ (ine hx'), Associates.factors_mk _ (ine hy')] at h
  simp_rw [Associates.count_some hv'] at h
  exact h

[Kevin Buzzard]

(a lot of it was ChatGPT 3.5)

[Kevin Buzzard]

OK so modulo the `Rat.ringOfIntegersEquiv sorry I've managed to fill in the sorry in the FLT repo without the adele refactor (I can't bump mathlib right now anyway, because the cache system is currently broken for all non-mathlib projects; this is a known issue). I've left the ringOfIntegers sorry as an issue on the FLT repo: FLT#307 . If anyone is interested in filling it in (it's

import Mathlib.NumberTheory.NumberField.Basic

open scoped NumberField

theorem Rat.ringOfIntegersEquiv_eq_algebraMap (z : 𝓞 ℚ) :
    (Rat.ringOfIntegersEquiv z : ℚ) = algebraMap (𝓞 ℚ) ℚ z := by
  sorry -- #307

then they should feel free to go to the issue and post a message saying

claim

When they've filled in the sorry, they should open a PR from a fork in the usual github way.

[Andrew Yang]

import Mathlib.NumberTheory.NumberField.Basic

open scoped NumberField

theorem Rat.ringOfIntegersEquiv_eq_algebraMap (z : 𝓞 ℚ) :
    (Rat.ringOfIntegersEquiv z : ℚ) = algebraMap (𝓞 ℚ) ℚ z := by
  obtain ⟨z, rfl⟩ := Rat.ringOfIntegersEquiv.symm.surjective z
  simp

[Yakov Pechersky]

Perhaps for the adicCompletionIntegers, there is missing API that uses the proposition docs#Valuation.Integers ?