Gelfand-Tornheim theorem

In this file the Gelfand-Tornheim theorem (AbsoluteValue.exists_ringHom_complex_of_not_isNonarchimedean) is proved, that is, if a field K has an infinite place, then there exists an embedding K →+* ℂ such that the absolute value is equivalent to the usual absolute value | | on ℂ.

theorem AbsoluteValue.exists_ringHom_complex_of_not_isNonarchimedean_of_isNormalized {K : Type u_1} [Field K] [CharZero K] (v : AbsoluteValue K ℝ) (h : ¬IsNonarchimedean ⇑v) [v.IsNormalized] : ∃ (φ : K →+* ℂ), NumberField.place φ = v

Gelfand-Tornheim theorem: if a field K has a normalized archimedean absolute value, then there exists an embedding K →+* ℂ such that the absolute value is equal to the usual absolute value | | on ℂ.

theorem AbsoluteValue.exists_ringHom_complex_of_not_isNonarchimedean {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) (h : ¬IsNonarchimedean ⇑v) : ∃ (φ : K →+* ℂ), NumberField.place φ ≈ v

Gelfand-Tornheim theorem: if a field K has an infinite place, then there exists an embedding K →+* ℂ such that the absolute value is equivalent to the usual absolute value | | on ℂ. Note that it is not necessary equal to | | as it is in fact equal to | | ^ c for some 0 < c ≤ 1.

theorem AbsoluteValue.exists_equiv_and_liesOver_of_comp_equiv {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) (w : AbsoluteValue F ℝ) (h : v.comp ⋯ ≈ w) : ∃ (v' : AbsoluteValue K ℝ), v' ≈ v ∧ v'.LiesOver w

Let K / F be a field extension, v and w are absolute values on K and F, respectively, such that the restriction of v on F is equivalent to w, then there exists v' equivalent to v, and which lies over w.