Product formula for number fields

Stream: mathlib4

[Fabrizio Barroero]

About a month ago I posted here #mathlib4 > Product formula for the rationals saying that I proved the product formula for the rationals and that I would PR it into Mathlib.

I changed my mind and started working on the number field case. A few days ago I finished. Here is the theorem:

NumberField.product_formula {K : Type u_1} [Field K] [NumberField K] {x : K} (h_x_nezero : x ≠ 0) :
  (∏ w : InfinitePlace K, w x ^ w.mult) * ∏ᶠ (P : IsDedekindDomain.HeightOneSpectrum (𝓞 K)), PadicNorm P x = 1

where PadicNorm is the norm of P raised to the power IsDedekindDomain.HeightOneSpectrum.valuation P x.

I only had to prove the non-archimedean part of the formula, i.e.,

theorem product_formula_finite {x : K} (h_x_nezero : x ≠ 0) :
    ∏ᶠ P : IsDedekindDomain.HeightOneSpectrum (𝓞 K), PadicNorm P x = |(Algebra.norm ℚ) x|⁻¹

because the archimedean one is already in mathlib docs#NumberField.InfinitePlace.prod_eq_abs_norm.

I had a look at the NumberField.Embeddings file and I think it would be good to imitate what has been done with docs#NumberField.InfinitePlace. I defined

def NumberField.FinitePlace (K : Type*) [Field K] [NumberField K] := { w : AbsoluteValue K ℝ //
    ∃ (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)),
    ∃ φ : K →+* (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v), place φ = w }

and started proving some basic facts.

The hope is to translate what I've already done and obtain

NumberField.product_formula {K : Type u_1} [Field K] [NumberField K] {x : K} (h_x_nezero : x ≠ 0) :
  (∏ w : InfinitePlace K, w x ^ w.mult) * ∏ᶠ (w : FinitePlace K), w x = 1

[Fabrizio Barroero]

By the way, the end goal is to define Heights.

[Michael Stoll]

Fabrizio Barroero said:

The hope is to translate what I've already done and obtain

NumberField.product_formula {K : Type u_1} [Field K] [NumberField K] {x : K} (h_x_nezero : x ≠ 0) :
  (∏ w : InfinitePlace K, w x ^ w.mult) * ∏ᶠ (w : FinitePlace K), w x = 1

You could go a step further and define Place K as the sum type to finally obtain a version that is closer to what we usually write down.

[Kevin Buzzard]

Oh I just ran into this this morning when thinking about FLT! Please PR to mathlib! Many thanks!

[Fabrizio Barroero]

Michael Stoll said:

Fabrizio Barroero said:

The hope is to translate what I've already done and obtain

NumberField.product_formula {K : Type u_1} [Field K] [NumberField K] {x : K} (h_x_nezero : x ≠ 0) :
  (∏ w : InfinitePlace K, w x ^ w.mult) * ∏ᶠ (w : FinitePlace K), w x = 1

You could go a step further and define Place K as the sum type to finally obtain a version that is closer to what we usually write down.

In the same file we have docs#NumberField.place which is an absolute value coming from an embedding into a NormedDivisionRing.
I guess when we’ll have Ostrowski for number fields we are going to be able to say that a place is either finite or infinite.
On the other hand I wonder if we could just change the definition of docs#NumberField.place to what you are suggesting. I am not sure docs#NumberField.place is used anywhere else…

[Fabrizio Barroero]

Kevin Buzzard said:

Oh I just ran into this this morning when thinking about FLT! Please PR to mathlib! Many thanks!

I will!

[Fabrizio Barroero]

Yesterday I created #19667 with the definition of FinitePlace and some basic APIs.

[Fabrizio Barroero]

#20132 contains the product formula for number fields

[Riccardo Brasca]

Great! Can you request my review so I will not forget to have a look?

[Kevin Buzzard]

Fabrizio Barroero said:

#20132 contains the product formula for number fields

Great because I now need it for FLT! (see section 9.6)

[Johan Commelin]

Do we already have a spelling for all places of a number field, including both finite and infinite places?
If not, should we add that to mathlib?

[Fabrizio Barroero]

Johan Commelin said:

Do we already have a spelling for all places of a number field, including both finite and infinite places?
If not, should we add that to mathlib?

Yes, we have docs#NumberField.place and they are absolute values coming from embeddings into a NormedDivisionRing. I am not sure this is the most useful definition.

[Johan Commelin]

So we can't really use that for the product formula, because we don't know how those norms are normalized?

[Fabrizio Barroero]

Johan Commelin said:

So we can't really use that for the product formula, because we don't know how those norms are normalized?

Yes, and there's too many of them: two different equivalent absolute values give two different places...

[Kevin Buzzard]

Adeles are defined as the binary product of finite and infinite adeles. I see no point in unifying the theories at the finite and infinite places and it would probably be a real pain to do so. A prime ideal is a genuinely different object to a field embedding into $\mathbb{C}$ and in practice proofs treat both cases in different ways, even though we have a common abstraction for both

[Michael Stoll]

@Fabrizio Barroero I have set up a repository containing a first attempt at starting a formalization of heights at Heights. Please have a look and let me know what you think.
(I'll be away until this evening CET, so won't be able to react before that, though.)

[Fabrizio Barroero]

This is great! I'll have a closer look later. By the way, I also have started working on the formalisation of Heights but it's in a too messy state to show it around.
In any case, I mostly made progress on the definition of Mahler measure and some API.

noncomputable def MahlerMeasure (p : Polynomial ℂ) := ‖leadingCoeff p‖₊ *
    (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖₊) p.roots).prod

I am now going towards Northcott and Kronecker's Theorems. For the moment, I only have

theorem bdd_coeff_of_bdd_roots_and_lead {K : Type*} [NormedField K]
    [IsAlgClosed K] [CharZero K] {p : Polynomial K} {B : NNReal}
    (h_bdd : (Multiset.map (fun (a : K) ↦ ‖a‖₊) p.roots).sup ≤ B) (n : ℕ) :
    ‖p.coeff n‖₊ ≤ ‖p.leadingCoeff‖₊ * Nat.choose p.natDegree n * B ^ (p.natDegree - n)

[Junyan Xu]

cc @David Ang who opened a PR #15786 for heights on elliptic curves