Results on elements of number fields and ideals

Stream: Is there code for X?

[Michael Stoll]

In the quest for formalizing the Mordell-Weil Theorem for elliptic curves over number fields, I have now reduced the proof of the Northcott property for a number field K (i.e., there are only finitely many elements of K whose height is below any given bound) to the following two statements (whose informal proofs are clear to me, but I don't feel at home yet with the relevant API).

import Mathlib.NumberTheory.NumberField.FinitePlaces

namespace NumberField

variable {K : Type*} [Field K] [NumberField K]

lemma absNorm_mul_finprod_nonarchAbsVal_eq_one {ι : Type*} [Finite ι] {x : ι → 𝓞 K} (hx : x ≠ 0) :
    (Ideal.span (Set.range x)).absNorm * ∏ᶠ (v : FinitePlace K), ⨆ i, v.val (x i : K) = 1 := by
  sorry

lemma exists_nat_ne_zero_exists_integer_mul_eq_and_absNorm_span_eq_pow (x : K) :
    ∃ n : ℕ, n ≠ 0 ∧ ∃ a : 𝓞 K, n * x = a ∧
      (Ideal.span {(n : 𝓞 K), a}).absNorm = n ^ (Module.finrank ℚ K - 1) := by
  sorry

What would be a good way to approach this? (In the second lemma, n is supposed to be the absolute norm of the "denominator ideal" of x. Is this ideal defined somewhere?)
@Fabrizio Barroero

[Fabrizio Barroero]

In the last few months I have been working on linking heights and Mahler Measures, for which we have Northcott already. This was the motivation for the definition of intMinpoly (see #mathlib4 > intMinpoly). One piece I am still missing, but I am working towards, would be the following

theorem leadingCoeff_eq_finprod {x : K} (hpol : ((intMinpoly x).map (algebraMap ℤ K)).Splits) :
    (intMinpoly x).leadingCoeff =  ∏ᶠ w : FinitePlace K, max 1 (w x) := by sorry

(there might be some exponent finrank ℚ K missing) which is probably very much related to your absNorm_mul_finprod_nonarchAbsVal_eq_one. Another thing needed is the invariance of the height with respect to finite extensions, but I guess you dealt with that already.

Unfortunately, because of personal and work reasons, this is proceeding very slowly.

In any case, for some other project I need what you call "denominator ideal" of x. I looked briefly in Mathlib but couldn't find anything.

[Michael Stoll]

To do it via Mahler measure, I think the cleanest way is to show that the height (docs#Height.mulHeight₁) is the same as the Mahler measure of the integral characteristic polynomial; otherwise one needs to jump through additional hoops for elements that live in a smaller field.

Of course, this can be dealt with when the relation between heights in extensions is available. I'm planning to add this (for general fields with an admissible family of absolute values) eventually, but decided to pivot to getting the basic stuff in first (you are welcome to review the relevant PRs; see #PR reviews > Heights). So for now, this is not yet available.

[Fabrizio Barroero]

I probably will have a have a look at your PRs on the weekend. I took a glance and it looks exciting. :grinning:

[Michael Stoll]

Fabrizio Barroero said:

which is probably very much related to your absNorm_mul_finprod_nonarchAbsVal_eq_one.

Yes, I think these are essentially the same (for the characteristic polynomial).

[Antoine Chambert-Loir]

You don't need an exact comparison with the Mahler measure. It would suffice, given an element of degree d and height <= H to bound the height of the d elementary symmetric functions of their conjugates, aka the height of the coefficient of its minimal polynomial. Those bounds follow from the general bounds for sums and products. Then one is reduced to rational numbers.

[Michael Stoll]

But note that this will still require the compatibility of the heights on $\mathbb Q$ and the number field in question.

[Michael Stoll]

... and also, to be able to write the coefficients as sums of products, one needs the field to be Galois, and one needs that the height is invariant under the Galois action. So one first has to extend to the Galois closure and also needs the compatibility of heights in finite extensions in general. It is not clear to me which path offers less resistance.

[Antoine Chambert-Loir]

My impression is that algebraic number theory, involving level of ring of integers etc., is an additional burden to this story which is intrinsically “adelic”.

[Michael Stoll]

I've been researching Mathlib for a bit today to figure out how to best set up a proof of the first of the two lemmas in the initial post. I learned that there are at least seven ways of expressing the multiplicity of a prime ideal p in the factorization of another (nonzero) ideal I in a Dedkind domain:

• factorization I p
• emultiplicity p I (but this is an ENat)
• multiplicity p I
• (UniqueFactorizationMonoid.normalizedFactors I).count p
• (UniqueFactorizationMonoid.normalizedFactors I).count (normalize p)
• (UniqueFactorizationMonoid.factors I).count p
• (UniqueFactorizationMonoid.factors I).count (normalize p)

The APIs for these are a bit disparate. There are lemmas relating some of these: docs#factorization_eq_count and docs#UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors (and, of course, one can relate docs#emultiplicity with docs#multiplicity and docs#UniqueFactorizationMonoid.normalizedFactors with docs#UniqueFactorizationMonoid.factors).

My feeling is that it would be good to standardize; my preference would be to use docs#factorization.

Any thoughts?

[Michael Stoll]

Side question: why do we have both docs#UniqueFactorizationMonoid.normalizedFactors and docs#UniqueFactorizationMonoid.factors? The latter is defined using choice, so we could as well also define a normalization map using choice and then use normalized factors. As it stands, there seems to be a lot of duplication.

[Xavier Roblot]

Yeah, I noticed too that there were many ways to express that multiplicity even though I didn't know about factorization. It would really be nice to standardize things as you suggested. My choices would go to multiplicity, but factorization would be okay too.

[Riccardo Brasca]

Note that there has been a refactor around multiplicity/emultiplicity and it is very likely not all declaration have been aligned to one style.

[Michael Stoll]

I can live with multiplicity (it is even one character shorter); emultiplicity is likely to cause pain from converting between ENat and Nat.

We should then have simp lemmas that convert the other ways of expressing this into multiplicity p I and extend the API for multiplicity suitably. I can try out this approach while working on my two lemmas.