Multiplicities of infinite places in an extension

Let L / K be an extension of number fields and v an infinite place of K. The multiplicities m_w ∈ {1, 2} of the infinite places w ∣ v of L add up to m_v [L : K]: above v the multiplicity is m_w = m_v [L_w : K_v] (NumberField.InfinitePlace.mult_mul_finrank), and the local degrees above v add up to [L : K] (NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank).

Grouping the infinite places of L by their restriction to K turns this into a product formula: for any function g on the infinite places of K, ∏_w g(w|_K) ^ m_w = ∏_v g(v) ^ (m_v [L : K]). This is the archimedean half of the comparison of heights computed over K and over L.

Main results

• NumberField.InfinitePlace.mem_placesOver: w ∈ v.placesOver L ↔ w.LiesOver v.
• NumberField.InfinitePlace.sum_mult_eq_mult_mul_finrank: ∑_{w ∣ v} m_w = m_v [L : K].
• NumberField.InfinitePlace.prod_comap_pow_mult: ∏_w g(w|_K) ^ m_w = ∏_v g(v) ^ (m_v [L : K]).

References

• X. Wu, Diophantine geometry, week 08: arithmetic heights (2023), §2, Lemma 2.2.

@[simp]

theorem NumberField.InfinitePlace.mem_placesOver {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} : w ∈ placesOver L v ↔ w.LiesOver v

An infinite place of L belongs to v.placesOver L exactly when it lies over v.

theorem NumberField.InfinitePlace.sum_mult_eq_mult_mul_finrank {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] (v : InfinitePlace K) : ∑ w ∈ (placesOver L v).toFinset, w.mult = v.mult * Module.finrank K L

The multiplicities of the infinite places of L above an infinite place v of K add up to the multiplicity of v times [L : K].

theorem NumberField.InfinitePlace.prod_comap_pow_mult {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] {M : Type u_3} [CommMonoid M] (g : InfinitePlace K → M) : ∏ w : InfinitePlace L, g (w.comap (algebraMap K L)) ^ w.mult = ∏ v : InfinitePlace K, g v ^ (v.mult * Module.finrank K L)

Grouping the infinite places of L by their restriction to K: a product over the infinite places w of L of g (w|_K) ^ m_w is the product over the infinite places v of K of g v ^ (m_v [L : K]).