A (new?) proof of the Gelfand-Mazur Theorem

We provide a formalization of proofs of the following versions of the Gelfand-Mazur Theorem.

• NormedAlgebra.Complex.algEquivOfNormMul: if F is a nontrivial normed ℂ-algebra with multiplicative norm, then we obtain a ℂ-algebra equivalence with ℂ.

  This differs from NormedRing.algEquivComplexOfComplete in the assumptions: there,

  • F is assumed to be complete,
  • F is assumed to be a (nontrivial) division ring,
  • but the norm is only required to be submultiplicative.

• NormedAlgebra.Complex.nonempty_algEquiv: A nontrivial normed ℂ-algebra with multiplicative norm is isomorphic to ℂ as a ℂ-algebra.

• NormedAlgebra.Real.nonempty_algEquiv_or: if a field F is a normed ℝ-algebra, then F is isomorphic as an ℝ-algebra either to ℝ or to ℂ.

  With some additional work (TODO), this implies a Theorem of Ostrowski, which says that any field that is complete with respect to an archimedean absolute value is isomorphic to either ℝ or ℂ as a field with absolute value. The additional input needed for this is to show that any such field is in fact a normed ℝ-algebra.

The complex case

The proof we use here is a variant of a proof for the complex case (any normed ℂ-algebra is isomorphic to ℂ) that is originally due to Ostrowski A. Ostrowski, Über einige Lösungen der Funktionalgleichung φ(x)⋅φ(y)=φ(xy) (Section 7). See also the concise version provided by Peter Scholze on Math Overflow.

(In the following, we write a • 1 instead of algebraMap _ F a for easier reading. In the code, we use algebraMap.)

This proof goes as follows. Let x : F be arbitrary; we need to show that x = z • 1 for some z : ℂ. We consider the function z ↦ ‖x - z • 1‖. It has a minimum M, which it attains at some point z₀, which (upon replacing x by x - z₀ • 1) we can assume to be zero. If M = 0, we are done, so assume not. For n : ℕ, a primitive nth root of unity ζ : ℂ, and z : ℂ with |z| < M = ‖x‖ we then have that M ≤ ‖x - z • 1‖ = ‖x ^ n - z ^ n • 1‖ / ∏ 0 < k < n, ‖x - (ζ ^ k * z) • 1‖, which is bounded by (M ^ n + |z| ^ n) / M ^ (n - 1) = M * (1 + (|z| / M) ^ n). Letting n tend to infinity then shows that ‖x - z • 1‖ = M (see NormedAlgebra.norm_eq_of_isMinOn_of_forall_le). This implies that the set of z such that ‖x - z • 1‖ = M is closed and open (and nonempty), so it is all of ℂ, which contradicts ‖x - z • 1‖ ≥ |z| - M when |z| is sufficiently large.

The real case

The usual proof for the real case is "either F contains a square root of -1; then F is in fact a normed ℂ-algebra and we can use the result above, or else we adjoin a square root of -1 to F to obtain a normed ℂ-algebra F' and apply the result to F'". The difficulty with formalizing this is that (as of October 2025) Mathlib does not provide a normed ℂ-algebra instance for F' (neither for F' := AdjoinRoot (X ^ 2 + 1 : F[X]) nor for F' := TensorProduct ℝ ℂ F), and it is not so straight-forward to set this up. So we take inspiration from the proof sketched above for the complex case to obtain a direct proof. An additional benefit is that this approach minimizes imports.

Since irreducible polynomials over ℝ have degree at most 2, it must be the case that each element is annihilated by a monic polynomial of degree 2. We fix x : F in the following.

The space ℝ × ℝ of monic polynomials of degree 2 is complete and locally compact and hence ‖aeval x p‖ gets large when p has large coefficients. This is actually slightly subtle. It is certainly true for ‖x - r • 1‖ with r : ℝ. If the minimum of this is zero, then the minimum for monic polynomials of degree 2 will also be zero (and is attained on a one-dimensional subset). Otherwise, one can indeed show that a bound on ‖x ^ 2 - a • x + b • 1‖ implies bounds on |a| and |b|.

By the first sentence of the previous paragraph, there will be some p₀ such that ‖aeval x p₀‖ attains a minimum (see NormedAlgebra.Real.exists_isMinOn_norm_φ). We assume that this is positive and derive a contradiction. Let M := ‖aeval x p₀‖ > 0 be the minimal value. Since every monic polynomial f : ℝ[X] of even degree can be written as a product of monic polynomials of degree 2 (see Polynomial.IsMonicOfDegree.eq_isMonicOfDegree_two_mul_isMonicOfDegree), it follows that ‖aeval x f‖ ≥ M ^ (f.natDegree / 2).

The goal is now to show that when a and b achieve the minimum M of ‖x ^ 2 - a • x + b • 1‖ and M > 0, then we can find some neighborhood U of (a, b) in ℝ × ℝ such that ‖x ^ 2 - a' • x + b' • 1‖ = M for all (a', b') ∈ U Then the set S = {(a', b') | ‖x ^ 2 - a' • x + b' • 1‖ = M} must be all of ℝ × ℝ (as it is closed, open, and nonempty). (see NormedAlgebra.Real.norm_φ_eq_norm_φ_of_isMinOn). This will lead to a contradiction with the growth of ‖x ^ 2 - a • x‖ as |a| gets large.

To get there, the idea is, similarly to the complex case, to use the fact that X ^ 2 - a' * X + b' divides the difference (X ^ 2 - a * X + b) ^ n - ((a' - a) * X - (b' - b)) ^ n; this gives us a monic polynomial p of degree 2 * (n - 1) such that (X ^ 2 - a' * X + b') * p equals this difference. By the above, ‖aeval x p‖ ≥ M ^ (n - 1).

Since (a', b') ↦ x ^ 2 - a' • x + b' • 1 is continuous, there will be a neighborhood U of (a, b) such that ‖(a' - a) • x - (b' - b) • 1‖ = ‖(x ^ 2 - a • x + b • 1) - (x ^ 2 -a' • x + b' • 1)‖ is less than M for (a', b') ∈ U. For such (a', b'), it follows that ‖x ^ 2 - a' • x + b' • 1‖ ≤ ‖(x ^ 2 - a • x + b • 1) ^ n - ((a' - a) • x - (b' - b) • 1) ^ n‖ / ‖aeval x p‖, which is bounded by (M ^ n + c ^ n) / M ^ (n - 1) = M * (1 + (c / M) ^ n), where c = ‖(a' - a) • x - (b' - b) • 1‖ < M. So, letting n tend to infinity, we obtain that M ≤ ‖x ^ 2 - a' • x + b' • 1‖ ≤ M, as desired.

Auxiliary results used in both cases

theorem NormedAlgebra.exists_isMinOn_norm_sub_smul (𝕜 : Type u_1) {F : Type u_2} [NormedField 𝕜] [ProperSpace 𝕜] [SeminormedRing F] [NormedAlgebra 𝕜 F] [NormOneClass F] (x : F) : ∃ (z : 𝕜), IsMinOn (fun (x_1 : 𝕜) => ‖x - (algebraMap 𝕜 F) x_1‖) Set.univ z

In a normed algebra F over a normed field 𝕜 that is a proper space, the function z : 𝕜 ↦ ‖x - algebraMap 𝕜 F z‖ achieves a global minimum for every x : F.

The complex case

theorem NormedAlgebra.Complex.exists_norm_sub_smul_one_eq_zero {F : Type u_1} [NormedRing F] [NormOneClass F] [NormMulClass F] [NormedAlgebra ℂ F] (x : F) : ∃ (z : ℂ), ‖x - (algebraMap ℂ F) z‖ = 0

If F is a normed ℂ-algebra and x : F, then there is a complex number z such that ‖x - algebraMap ℂ F z‖ = 0 (whence x = algebraMap ℂ F z).

noncomputable def NormedAlgebra.Complex.algEquivOfNormMul (F : Type u_1) [NormedRing F] [NormOneClass F] [NormMulClass F] [NormedAlgebra ℂ F] [Nontrivial F] : ℂ ≃ₐ[ℂ] F

A version of the Gelfand-Mazur Theorem.

If F is a nontrivial normed ℂ-algebra with multiplicative norm, then we obtain a ℂ-algebra equivalence with ℂ.

Equations

• NormedAlgebra.Complex.algEquivOfNormMul F = AlgEquiv.ofBijective (Algebra.ofId ℂ F) ⋯

theorem NormedAlgebra.Complex.nonempty_algEquiv (F : Type u_1) [NormedRing F] [NormOneClass F] [NormMulClass F] [NormedAlgebra ℂ F] [Nontrivial F] : Nonempty (ℂ ≃ₐ[ℂ] F)

A version of the Gelfand-Mazur Theorem for nontrivial normed ℂ-algebras F with multiplicative norm: any such F is isomorphic to ℂ as a ℂ-algebra.

The real case

theorem NormedAlgebra.Real.exists_isMonicOfDegree_two_and_aeval_eq_zero {F : Type u_1} [NormedRing F] [NormedAlgebra ℝ F] [NormOneClass F] [NormMulClass F] (x : F) : ∃ (p : Polynomial ℝ), p.IsMonicOfDegree 2 ∧ (Polynomial.aeval x) p = 0

If F is a normed ℝ-algebra with a multiplicative norm (and such that ‖1‖ = 1), e.g., a normed division ring, then every x : F is the root of a monic quadratic polynomial with real coefficients.

theorem NormedAlgebra.Real.nonempty_algEquiv_or (F : Type u_2) [NormedField F] [NormedAlgebra ℝ F] : Nonempty (F ≃ₐ[ℝ] ℝ) ∨ Nonempty (F ≃ₐ[ℝ] ℂ)

A version of the Gelfand-Mazur Theorem over ℝ.

If a field F is a normed ℝ-algebra, then F is isomorphic as an ℝ-algebra either to ℝ or to ℂ.