lemmastandard

Weighted product formula for number fields

Lemma·ht:product·§4.1 A weighted product formula

Statement (paper)

There is a countable collection of absolute-value entries

v

\mathcal N

, each of weight

1/d_{\mathcal N}

, with the following properties. Its archimedean entries are

|u|_v=|\sigma(u)|

for the

d_{\mathcal N}

embeddings

\sigma:\mathcal N\to\C

, so their total weight is one. All other entries are nonarchimedean. For each nonzero

u\in\mathcal N

, only finitely many nonarchimedean entries have

|u|_v\ne1

, and

\sum_v^*\log|u|_v=0.

Here and below a star denotes the sum with the stated weights.

In plain English

The number field

\mathcal N

carries a countable family of absolute values

v

, each of weight

1/d_{\mathcal N}

, consisting of the

d_{\mathcal N}

archimedean embeddings

|u|_v=|\sigma(u)|

and nonarchimedean entries. For each nonzero

u\in\mathcal N

, only finitely many nonarchimedean entries have

|u|_v\ne 1

, and the weighted sum

\sum_v^*\log|u|_v

equals

0

Why it's here

This is the standard product formula, rewritten with weights that make the archimedean total weight equal to one. It is the foundation for the height

h(u)

and its basic inequalities, and it supplies the cancellation used in later arguments that sum

\log|u|_v

over all entries.

Classified standard:

The product formula for number fields (e.g. Bombieri–Gubler, Heights in Diophantine Geometry, 2006), here normalized so that each place is repeated according to its local degree and weighted by 1/d.

Uses

Nothing else in the paper

Used by

lemBasic properties of the heightlemNegligible-height elements form an algebraically closed subfieldclaimCentral-window excess and product-formula cancellation

Sources

PaperOpen

Section: §4.1 A weighted product formula
Page: —
Label: ht:product
Line: sections/03-heights.tex:33

Leannot aligned

Phase 2 aligns this node to a Lean declaration.