Gelfand-Mazur theorem

Stream: mathlib4

[Michael Stoll]

Do we have the following version of the Gelfand-Mazur theorem?

The only complete archimedean fields are (up to iso) $\mathbb R$ and $\mathbb C$.

This would be helpful in the next step of showing that absolute values on complete fields lift uniquely to finite extensions...

[Jireh Loreaux]

not that I know of, but we do have this version: docs#NormedRing.algEquivComplexOfComplete, which could help proving it.

[Michael Stoll]

Thanks. The missing step seems to be that a nontrivially archimedean normed complete field such that the canonical map from the reals into it is not surjective must actually be a ℂ-algebra. Is there anything I can use for that?
I'm looking at Theorem 6.2 in these notes. The proof says "... Using a little complex analysis, it is shown in Theorem 2.3 and Corollary 2.4 in Ch. XII in Lang’s Algebra (3rd ed.) that F must be $\mathbb R$-isomorphic to $\mathbb C$ as a field ...", which is not so helpful. I can look up Lang's Algebra, of course.

[Kevin Buzzard]

How are you ruling out some larger formally real field with infinitely big/small elements like some completion of $\mathbb{R}(\epsilon)$? Oh is the idea that the norm is $\R$-valued?

[Damiano Testa]

There is also an archimedean included in the conditions.

[Kevin Buzzard]

Maybe I don't know what that word means :-) (I recall some rant in Wikipedia about how it means several things)

[Kevin Buzzard]

In my courses I usually define "archimedean" to mean "not non-archimedean" (I am serious)

[Michael Stoll]

That's what it means here :smile:

[Kevin Buzzard]

Well |1+1|>|1| so the completion of $\R(\epsilon)$ looks archimedean to me :-/

[Kevin Buzzard]

Basically I'm saying that I would happily think about the question but I don't know what the question is.

[Michael Stoll]

The norms are indeed real-valued here.

[Michael Stoll]

One thing that seems necessary is the implication "positive characteristic ==> absolute value is nonarchimedean". I don't think this is in Mathlib (but would be delighted to learn otherwise). This can be done via
$\lim_{r \to \infty} (x^r + y^r)^{1/r} \le \max\{x,y\}$
(for real $x, y \ge 0$), but loogle does not come up with something useful along these lines:
@loogle ((?x ^ (?r : ℝ)) + (?y ^?r)) ^ _

[loogle]

:search: NNReal.rpow_add_rpow_le_add, ENNReal.rpow_add_rpow_le_add, and 7 more

[Michael Stoll]

These statements all do not contain limits..

[Yakov Pechersky]

I think I proved something related in #15077?

[Luigi Massacci]

Kevin Buzzard said:

Well |1+1|>|1| so the completion of $\R(\epsilon)$ looks archimedean to me :-/

But $\mathbb{Z}\cdot \epsilon$ is bounded (and it not being bounded is the definition I was given of archimedean)

[Kevin Buzzard]

Yes, that's another definition.

[Michael Stoll]

Yakov Pechersky said:

I think I proved something related in #15077?

Thanks, this helps!
(Nit: The second isUltrametricDist in docs#IsUltrametricDist.isUltrametricDist_iff_isNonarchimedean_norm etc. seems to be unnecessary.)

[Michael Stoll]

Here is an approach:

import Mathlib

variable {F : Type*} [Field F] {v : AbsoluteValue F ℝ}

open IsUltrametricDist in
lemma charZero_of_archimedean (h : ¬ IsNonarchimedean v) : CharZero F := by
  contrapose! h
  let p := ringChar F
  have : CharP (WithAbs v) p := ringChar.charP F
  have : NeZero p := ⟨mt (CharP.ringChar_zero_iff_CharZero _).mp h⟩
  have H (n : ℕ) : ‖(n : WithAbs v)‖ ≤ 1 := by
    let φ := ZMod.castHom (m := p) dvd_rfl (WithAbs v)
    obtain ⟨B, hB⟩ : ∃ B, ∀ a : ZMod p, ‖φ a‖ ≤ B := Finite.exists_le _
    refine le_of_forall_pos_le_add fun ε hε ↦ ?_
    obtain ⟨m, hm⟩ := pow_unbounded_of_one_lt B <| lt_add_of_pos_right 1 hε
    refine (pow_le_pow_iff_left₀ (norm_nonneg _) (by linarith) m.zero_ne_add_one.symm).mp ?_
    rw [← norm_pow, pow_succ (1 + ε), ← Nat.cast_pow, ← map_natCast φ, ← mul_one (‖_‖)]
    have hε' := lt_add_of_pos_right 1 hε -- for `gcongr` below
    gcongr
    exact (hB _).trans hm.le
  exact isUltrametricDist_iff_isNonarchimedean_norm.mp <|
    isUltrametricDist_of_forall_norm_natCast_le_one H

[Artie Khovanov]

Kevin Buzzard said:

In my courses I usually define "archimedean" to mean "not non-archimedean" (I am serious)

Aren't the definitions equivalent (for normed fields)?
R(ϵ) doesn't have an R-valued norm.

[Kevin Buzzard]

It wouldn't surprise me. I was just very confused above

[Artie Khovanov]

image.png

[Michael Stoll]

I'm going to add that.

[Michael Stoll]

I'm running into the following problem.

import Mathlib

open Rat.AbsoluteValue
-- `real` is the standard absolute value on `ℚ`

#synth Field (real.Completion) -- fails :-(
-- The relevant instance is
/-
instance UniformSpace.Completion.instField {K : Type u_1} [Field K] [UniformSpace K]
    [TopologicalDivisionRing K] [CompletableTopField K] [UniformAddGroup K] :
    Field (UniformSpace.Completion K)
-/

#synth Field (WithAbs real) -- OK
#synth UniformSpace (WithAbs real) -- OK
#synth TopologicalDivisionRing (WithAbs real) -- OK
#synth CompletableTopField (WithAbs real) -- fails :-(
#synth UniformAddGroup (WithAbs real) -- OK

/-
class CompletableTopField (K : Type u_1) [Field K] [UniformSpace K] extends T0Space K :
Prop

A topological field is completable if it is separated and the image under the mapping x ↦ x⁻¹ of every Cauchy filter (with respect to the additive uniform structure) which does not have a cluster point at 0 is a Cauchy filter (with respect to the additive uniform structure). This ensures the completion is a field.

    t0 ⦃x y : K⦄ : Inseparable x y → x = y
    nice (F : Filter K) : Cauchy F → nhds 0 ⊓ F = ⊥ → Cauchy (Filter.map (fun (x : K) => x⁻¹) F)
-/
-- the only relevant instance is
/-
@[instance 100]
instance Valued.completable {K : Type u_1} [Field K] {Γ₀ : Type u_2}
    [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] :
    CompletableTopField K
-/
-- but
/-
class Valued (R : Type u) [Ring R] (Γ₀ : outParam (Type v))
    [LinearOrderedCommGroupWithZero Γ₀] extends UniformSpace R, UniformAddGroup R where
  v : Valuation R Γ₀
  is_topological_valuation : ∀ s, s ∈ 𝓝 (0 : R) ↔ ∃ γ : Γ₀ˣ, { x : R | v x < γ } ⊆ s

structure Valuation extends R →*₀ Γ₀ where
  /-- The valuation of a a sum is less that the sum of the valuations -/
  map_add_le_max' : ∀ x y, toFun (x + y) ≤ max (toFun x) (toFun y)
-/

Note that the docstring is wrong: it should say "less than the max of"

Anyway, this prevents the Field instance to fire when the valuation is archimedean. (There is also the added complication that ℝ is not a docs#LinearOrderedCommGroupWithZero .)

So my question is: How can I fill in the sorry below?

import Mathlib

variable {F : Type*} [Field F] {v : AbsoluteValue F ℝ}

instance : CompletableTopField (WithAbs v) where
  t0 := (inferInstanceAs <| T0Space _).t0
  nice f hc hn := by sorry

Unfortunately, I have next to no idea how to work with Cauchy filters and uniformities...

[Artie Khovanov]

Artie Khovanov said:

image.png

should I bother sourcing stuff like this btw
or does it not matter bc it's folklore

[Michael Stoll]

Is there something like a "topological ring isomorphism" in Mathlib? It doesn't look like it:
@loogle RingEquiv, Homeomorph

[loogle]

:search: LocallyConstant.congrLeftRingEquiv, LocallyConstant.congrLeftRingEquiv_apply_apply, and 1 more

[Michael Stoll]

These are not what I was hoping to see...

[Michael Stoll]

#xy: I would like to show that the completions of a field F w.r.t. two equivalent absolute values are isomorphic as topological fields (for the fact that they are fields I need the sorry above) and I'm trying to figure out how to write down the statement.

[Michael Stoll]

Michael Stoll said:

I'm going to add that.

There is now

variable {R : Type*} [Ring R] {v : AbsoluteValue R ℝ}

lemma le_one_on_nat_of_isNonarchimedean [Nontrivial R] (h : IsNonarchimedean v) (n : ℕ) : v n ≤ 1 := by ...

lemma le_one_on_nat_of_bounded [Nontrivial R] {B : ℝ} (h : ∀ n : ℕ, v n ≤ B) (n : ℕ) : v n ≤ 1 := by ...

variable {F : Type*} [Field F] {v : AbsoluteValue F ℝ}

lemma isNonarchimedean_of_le_one_on_nat (h : ∀ n : ℕ, v n ≤ 1) : IsNonarchimedean v := ...

lemma isNonarchimedean_of_bounded_on_nat {B : ℝ} (h : ∀ n : ℕ, v n ≤ B) : IsNonarchimedean v := ...

/-- An absolute value on a field is nonarchimedean if and only if it is bounded by `1`
on the image of `ℕ`. -/
lemma isNonarchimedean_iff_le_one_on_nat : IsNonarchimedean v ↔ ∀ n : ℕ, v n ≤ 1 := ...

in Heights.Auxiliary .

[Fabrizio Barroero]

Michael Stoll said:

#xy: I would like to show that the completions of a field F w.r.t. two equivalent absolute values are isomorphic as topological fields (for the fact that they are fields I need the sorry above) and I'm trying to figure out how to write down the statement.

I got stuck on the same problem last summer when I was working on Ostrowski for number fields. Then, I stumbled upon #16483 which I thought could be helpful but it was under review and constantly changing so I decided to wait for it to settle and be merged.

[Fabrizio Barroero]

Michael Stoll said:

Is there something like a "topological ring isomorphism" in Mathlib? It doesn't look like it:
loogle RingEquiv, Homeomorph

I think it would be helpful to have something like that...

This was my attempt for MulRingNorm

structure NormHom {R S : Type*} [NonAssocRing R] (f : MulRingNorm R) [NonAssocRing S] (g : MulRingNorm S) where
  toFun : R → S
  map_norm : g ∘ toFun = f

structure MulRingNormHom {R S : Type*} [NonAssocRing R] (f : MulRingNorm R) [NonAssocRing S] (g : MulRingNorm S) extends
  R →+* S, NormHom f g

structure MulRingNormIso {R S : Type*} [NonAssocRing R] (f : MulRingNorm R) [NonAssocRing S] (g : MulRingNorm S) extends
  R ≃+* S, NormHom f g

structure NormHomEquiv {R S : Type*} [NonAssocRing R] (f : MulRingNorm R) [NonAssocRing S] (g : MulRingNorm S) where
  toFun : R → S
  map_norm : ∃ (c : ℝ), 0 < c ∧ (g ∘ toFun) ^ c = f

structure MulRingNormHomEquiv {R S : Type*} [NonAssocRing R] (f : MulRingNorm R) [NonAssocRing S] (g : MulRingNorm S) extends
  R →+* S, NormHomEquiv f g

structure MulRingNormIsoEquiv {R S : Type*} [NonAssocRing R] (f : MulRingNorm R) [NonAssocRing S] (g : MulRingNorm S) extends
  R ≃+* S, NormHomEquiv f g

[Michael Stoll]

The problem with that (i.e., #16483) is that a docs#NumberField.InfinitePlace comes already packaged with a homomorphism into a normed field (the complex numbers), which is then used to get the docs#CompletableTopField instance. In the general setting I am in, we don't know a priori that such a target field exists.

[Michael Stoll]

Your NormHom etc. is too rigid (the norms are not necessarily the same, but the induced topologies are).

[Michael Stoll]

But of course one could just bundle docs#RingEquiv and docs#Homeomorph together.

[Michael Stoll]

But this would entail writing a bunch of API lemmas...

[Michael Stoll]

So I was hoping that something like that already exists.

[Fabrizio Barroero]

Michael Stoll said:

So I was hoping that something like that already exists.

Indeed, it is quite surprising there's nothing like that in Mathlib

[Michael Stoll]

Michael Stoll said:

So my question is: How can I fill in the sorry below?

Here is a solution (that goes back to $\varepsilon$ s and $\delta$ s):

import Mathlib

variable {F : Type*} [Field F] {v : AbsoluteValue F ℝ}

instance : CompletableTopField (WithAbs v) where
  t0 := (inferInstanceAs <| T0Space _).t0
  nice f hc hn := by
    rw [Metric.cauchy_iff] at hc ⊢
    obtain ⟨hf₁, hf₂⟩ := hc
    refine ⟨Filter.map_neBot, ?_⟩
    obtain ⟨U, hU, V, hV, hUV⟩ := Filter.inf_eq_bot_iff.mp hn
    obtain ⟨ε, hε₀, hε⟩ := Metric.mem_nhds_iff.mp hU
    intro δ hδ₀
    obtain ⟨t, ht₁, ht₂⟩ := hf₂ (δ * ε ^ 2) (by positivity)
    let t' := t ∩ V
    have h : ∀ x ∈ t', ∀ y ∈ t', dist x y < δ * ε ^ 2 :=
      fun x hx y hy ↦
        ht₂ x (Set.mem_of_mem_inter_left hx) y (Set.mem_of_mem_inter_left hy)
    simp_rw [Filter.mem_map]
    refine ⟨(· ⁻¹) ⁻¹' t', by simpa only [Set.inv_preimage, inv_inv] using Filter.inter_mem ht₁ hV,
      fun x hx y hy ↦ ?_⟩
    simp only [Set.inv_preimage, Set.mem_inv] at hx hy
    specialize h x⁻¹ hx y⁻¹ hy
    rw [dist_eq_norm_sub] at h ⊢
    have h₀ {z : WithAbs v} (hz : z⁻¹ ∈ t') : z ≠ 0 := by
      rintro rfl
      simp only [inv_zero] at hz
      exact (Set.mem_empty_iff_false _).mp <|
        hUV ▸ Set.mem_inter (hε <| Metric.mem_ball_self hε₀) (Set.mem_of_mem_inter_right hz)
    have Hε {z : WithAbs v} (hz : z⁻¹ ∈ t') : ‖z‖ ≤ ε⁻¹ := by
      have : z⁻¹ ∉ Metric.ball 0 ε :=
        fun H ↦ (Set.mem_empty_iff_false _).mp <|
          hUV ▸ Set.mem_inter (hε H) (Set.mem_of_mem_inter_right hz)
      simp only [Metric.mem_ball, dist_zero_right, norm_inv, not_lt] at this
      exact le_inv_of_le_inv₀ hε₀ this
    have hx₀ := h₀ hx
    have hy₀ := h₀ hy
    have hxε := Hε hx
    have hyε := Hε hy
    rw [show x⁻¹ - y⁻¹ = (y - x) / (x * y) by field_simp, norm_div, norm_mul, norm_sub_rev,
      div_lt_iff₀ (by simp [hx₀, hy₀])] at h
    refine h.trans_le ?_
    rw [mul_assoc]
    conv_rhs => rw [← mul_one δ]
    gcongr
    rw [sq]
    calc ε * ε * (‖x‖ * ‖y‖)
    _ ≤ ε * ε * (ε⁻¹ * ε⁻¹) := by gcongr
    _ = 1 := by field_simp

I invite our docs#Filter aficionados to improve on that :smile:

[Michael Stoll]

(The idea is clear: if x and y are uniformly close and away from zero, then their inverses are also uniformly close. But the proof feels a bit clumsy.)

[Yakov Pechersky]

Can you use docs#IsUniformInducing.completableTopField with the absolute value?

[Yakov Pechersky]

Ah, that presupposes Field already.

[Michael Stoll]

This is not the problem; rather, the problem is that the absolute value is not a ring homomorphism.

[Michael Stoll]

In any case, my proof above works with [NormedField F] for F in place of WithAbs v.

I think that NormedField.toCompletableTopField is a missing instance in Mathlib and should be added. I'd just like to have a more idiomatic proof...

Note that the following loogle query does not turn up something like that:
@loogle ⊢ CompletableTopField _

[loogle]

:search: completableTopField_of_complete, Subfield.completableTopField, and 3 more

[Michael Stoll]

(The other three are docs#CompletableTopField.mk, docs#IsUniformInducing.completableTopField mentioned by Yakov above, and docs#Valued.completable mentioned by me earlier.)

[Michael Stoll]

#20686 adds the missing instance.

[Antoine Chambert-Loir]

It's not the topic here, but I'd like to point out an elementary proof (three, in fact) of Gelfand Mazur that avoids a lot of stuff. They might be easier to formalize.

[Antoine Chambert-Loir]

https://projecteuclid.org/journalArticle/Download?urlid=10.1307%2Fmmj%2F1028998012

[Antoine Chambert-Loir]

https://www.jstage.jst.go.jp/article/jmath1948/4/1/4_1_96/_pdf

[Antoine Chambert-Loir]

https://projecteuclid.org/journals/michigan-mathematical-journal/volume-1/issue-1/Normed-fields-over-the-real-and-complex-fields/10.1307/mmj/1028989727.full

[Yakov Pechersky]

Does docs#uniformContinuous_div_const' help at all?

[Yakov Pechersky]

Or not, since you have to vary both x and y simultaneously?

[Michael Stoll]

That has a fixed denominator, so it is basically multiplication by a constant...

[Michael Stoll]

You'd need x ↦ x⁻¹ to be uniformly continuous on the complement of any given neighborhood of zero.

[Michael Stoll]

@loogle ⊢ UniformContinuous .., ?x⁻¹

[loogle]

:search: uniformContinuous_inv, UniformContinuous.inv, and 1 more

[Michael Stoll]

docs#Real.uniformContinuous_inv is the last one; it has something like the correct statement for the reals. Perhaps one can use that one via pulling back...?

[Johan Commelin]

@Michael Stoll What is the Lean statement of Gelfand-Mazur that you are going for? There is also the short proof https://mathoverflow.net/a/420803 that seems quite similar to one of the proofs Antoine linked to. (But maybe even a bit more streamlined.)

[Michael Stoll]

Something along the lines of the following.

import Mathlib

variable {F R S : Type*} [Field F] [Semiring R] [Nontrivial R] [Algebra F R] [OrderedSemiring S]

variable (F) in
/-- The restriction to a field `F` of an absolute value on an `F`-algebra `R`. -/
def AbsoluteValue.restrict (v : AbsoluteValue R S) : AbsoluteValue F S :=
  v.comp (RingHom.injective (algebraMap F R))

theorem gelfand_mazur {v : AbsoluteValue F ℝ} [CompleteSpace (WithAbs v)]
    (hv : ¬ IsNonarchimedean v) :
    (∃ f : ℝ ≃+* F, letI alg := f.toRingHom.toAlgebra; v.restrict ℝ ≈ AbsoluteValue.abs) ∨
      ∃ f : ℂ ≃+* F, letI alg := f.toRingHom.toAlgebra; v.restrict ℂ ≈ Complex.abs := by
  sorry

(AbsoluteValue.restrict is in Heights.)
The most convenient way of writing it will depend on how I can use it to show that if L/K is a (finite) extension of fields with K complete w.r.t. an archimedean absolute value v, then v can be extended to L (which the theorem would reduce to basically three cases).

[Kevin Buzzard]

@María Inés de Frutos Fernández did your work on the nonarchimedean version of this cover this case?

[María Inés de Frutos Fernández]

I formalized that if K is a field complete with respect to a nonarchimedean real-valued norm, and L/K is an algebraic field extension, then there is a unique norm on L extending the given norm on K, but the proof I followed (from BGR) would not apply in the archimedean case. At the time where I formalized this I thought about whether it was possibly to unify the proofs in the archimedean and nonarchimedean cases, but there is a step of the proof that I formalized that uses the nonarchimedean property in a way that I did not see how to avoid.

[Michael Stoll]

Is this available somewhere? I will need this (plus the archimedean counterpart and then the classification of extensions of the absolute value in a general finite field extension) to show that an family of absolute values with product formula can be extended to a finite extension, so it would be good to have it available in Mathlib.

This is likely closely related to showing that ${\mathbb A}_K \otimes_K L \cong {\mathbb A}_L$, so maybe I should look at the FLT project. Pointers appreciated!

[Michael Stoll]

@María Inés de Frutos Fernández There is docs#ContinuousAlgHom (which, I think, you introduced), but apparently the corrsesponding notion of "topological algebra equivalence" is missing. Are there plans to add it?

This would be very convenient in order to state that the completions of a field F w.r.t. two equivalent absolute values are isomorphic as topological algebras over F .

[Kevin Buzzard]

#20609 (this was a coincidence, not a response to this conversation; I needed it for FLT)

[Michael Stoll]

I'll have a :eyes: tomorrow (it is getting late and there is snooker again...).

[Michael Stoll]

Do we know that docs#UniformSpace.Completion.mapRingHom is compatible with compositions (i.e., that docs#UniformSpace.Completion is a functor)?

[María Inés de Frutos Fernández]

Michael Stoll said:

Is this available somewhere?

You can find it here. I am working on PRing this to Mathlib, but it is going a slowly (and I am currently at a conference, so I have not been able to update my open PRs in the last few days).

[Michael Stoll]

@María Inés de Frutos Fernández I see that you use docs#MulRingNorm. Did you see this recent thread? The consensus there was to discourage use of MulRingNorm R in favor of AbsoluteValue R Real, to avoid duplicating stuff.

In any case, thanks for the pointer!

[María Inés de Frutos Fernández]

Yes, I saw that thread, but I have not updated the code yet (I finished this in 2022).