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).

[Michael Stoll]

After a fairly long pause, I've come back to this. I realized that one of my problems was that the various proofs I was looking at (and the result in Mathlib) were requiring a normed algebra structure over $\mathbb C$. But in my case, I only have an absolute value whose restriction to $\mathbb C$ is equivalent to the standard one, so the normed algebra structure I would get would be over $\mathbb C$ with some power of the standard absolute value. So I looked more closely and found a useful result: if I have two fields $F$ and $F'$ such that $F'$ is an $F$-algebra, and I have absolute values $v$ on $F$ and $v'$ on $F'$ such that the restriction of $v'$ to $F$ is equivalent to $v$, then there is an equivalent absolute value $v''$ on $F'$ whosse restriction to $F$ is equal to $v$. I've formalized this and used it to deal with the complex case:

Complex.GelfandMazur {F : Type*} [Field F] [Algebra ℂ F] {v : AbsoluteValue F ℝ}
  (hv : restrict ℂ v ≈ NormedField.toAbsoluteValue ℂ) [CompleteSpace (WithAbs v)] :
  ∃ e, v.comap (e.toRingEquiv.trans (WithAbs.equiv v)).toRingHom ≈ NormedField.toAbsoluteValue ℂ := sorry

Now I need to deal with the real case. The argument in the literature is either "adjoin a square root of $-1$ (if not already present) to get a $\mathbb C$-algebra and thus reduce to the complex case" or (in one case) a rather complicated computation that looks like a pain to formalize.

So I would like to use the first approach. I think I'm OK in the case that my field F does contain a square root of $-1$. So let's assume this is not the case. I basically see two approaches.

1. F' := AdjoinRoot (X ^ 2 + 1 : Polynomial F)
2. F' := TensorProduct ℝ ℂ F

I need to show that F' is a field and that I can give it a structure as normed ℂ-algebra (that is compatible with the normed ℝ-algebra structure I have on F). I know how to get that F' is a field with the first approach (show that X ^ 2 + 1 is irreducible), but not with the second approach. And there seem to be no results in Mathlib that give me a docs#NormedAlgebra structure on either AdjoinRoot _ or TensorProduct ℝ ℂ F. The "obvious" way in the first approach would be to say "write $x = x_0 + x_1 i$ and define $\|x\| = \sqrt{\|x_0\|^2 + \|x_1\|^2}$" (where $i$ is a root of the polynomial in F'). But then I need to show that this norm is multiplicative and sub-additive etc., for which I think I'll need to know how (addition and) multiplication in F' works in terms of the F-basis $(1, i)$. I can define a linear equivalence with Fin 2 → F as

noncomputable
def xyz : AdjoinRoot (Polynomial.X ^ 2 + 1 : Polynomial F) ≃ₗ[F] Fin 2 → F := by
  letI p : Polynomial F := Polynomial.X ^ 2 + 1
  have hp₀ : p ≠ 0 := Polynomial.Monic.ne_zero <| by simp only [p]; monicity!
  letI pb := AdjoinRoot.powerBasis hp₀
  have hpb : pb.dim = 2 := by
    simp [pb, p]
    compute_degree!
  exact (hpb ▸ (AdjoinRoot.powerBasis hp₀).basis.repr).trans
    (Finsupp.linearEquivFunOnFinite F F (Fin 2))

but I'm failing miserably at

lemma xyz_mul (x y : AdjoinRoot (Polynomial.X ^ 2 + 1 : Polynomial F)) :
    xyz (x * y) = ![xyz x 0 * xyz y 0 - xyz x 1 * xyz y 1,
                    xyz x 0 * xyz y 1 + xyz x 1 * xyz y 0] := sorry

Is there any kind of API that helps with explicit computations in AdjoinRoot?
Or is there some reasonable way to get it done via tensor products?

[Johan Commelin]

@Anne Baanen @Alain Chavarri Villarello can't some of your methods/tactics help with computations in a basis of an algebra? Is that available in mathlib?

[Michael Stoll]

I should say that I've switched to plan C now, which is coming up with a variant of the proof given by Peter Scholze on MathOverflow that Johan linked to earlier that works over the reals, and formalizing that. This looks lilke it's more fun :smiley:, but I may run into other problems instead -- watch this place!

This being said, it would still be nice to have a convenient way of doing computations in rings obtained by docs#AdjoinRoot .

[Johan Commelin]

@Michael Stoll Didn't that one also assume complexes as base field?

[Michael Stoll]

I'm saying "a variant that works over the reals" :slight_smile:

[Johan Commelin]

/me should learn to read

[Michael Stoll]

Most of the fun was actually coming up with this variant (though I don't know if it's really new).

[Anne Baanen]

Johan Commelin said:

Anne Baanen Alain Chavarri Villarello can't some of your methods/tactics help with computations in a basis of an algebra? Is that available in mathlib?

We had quad_ring in Lean 3, a two-field structure which generalizes docs#Zsqrtd and can compute by simp; ring or decide. This never ended up being ported to Mathlib or Lean 4. We also have some representations of polynomials and algebra elements by lists in Lean 4: https://github.com/alainchmt/RingOfIntegersProject/blob/main/DedekindProject4/CertifyAdjoinRoot.lean#L376

[Michael Stoll]

The desire to have an implementation of quadratic rings (in the correct generality) seems to be a recurring theme. Somebody just has to do it ...

[Kenny Lau]

#Is there code for X? > Z[(1+sqrt(1+4k))/2]

[Michael Stoll]

After some more tinkering, I now have a complete formalization of the variant of Gelfand-Mazur I wanted:

GelfandMazur.nonempty_algEquiv_or {F : Type*} [NormedField F] [NormedAlgebra ℝ F] :
    Nonempty (F ≃ₐ[ℝ] ℝ) ∨ Nonempty (F ≃ₐ[ℝ] ℂ) := ...

See GelfandMazur.lean in my Heights repo.

Since I found it very convenient, I'm introducing a predicate Polynomial.IsMonicOfDegree p n that states that p is a monic polynomial of degree n, together with some API (in a separate file IsMonicOfDegree.lean). Modulo that and some further auxiliary lemmas, the proof of Gelfand-Mazur needs about 300 lines. For a comparison, I have also formalized the complex version; this is about 100 lines (in the same file).

Unless there are objections, I'm planning to first PR the material on IsMonicOfDegree and then the real version of G-M. (A stronger form of the complex version is already there, so this part was just for fun.)

[Michael Stoll]

I've found a considerable simplification of my proof that reduces the formalization (modulo API) from ~300 to ~200 lines. There's always more to learn...

[Antoine Chambert-Loir]

Michael Stoll said:

The desire to have an implementation of quadratic rings (in the correct generality) seems to be a recurring theme. Somebody just has to do it ...

I proposed something for the Lean 2025 conference at the Simons Foundation. Maybe I should go on. For the moment, it just defines quadratic algebras mimicking the first half of the file defining docs#ZSqrtd

[Michael Stoll]

After some more streamlining, I'm now quite satisfied.
#26507 is a first PR; it adds IsMonicOfDegree and API for it.

[Michael Stoll]

@Damiano Testa Assuming #26507 gets merged eventually, would it be possible to extend the monicity tactic to work on goals of the form IsMonicOfDegree _ _ without too much effort?

[Damiano Testa]

That would be really easy. Is there a lemma saying that IsMonivODegree follows from natDegree = ... and Monic ...? Once that is in, the tactic should simply be told that when the goal is IsMonicOfDegree, then it should apply this lemma and then compute_degree and monicity on the two branches.

[Michael Stoll]

There is

lemma isMonicOfDegree_iff {R : Type*} [Semiring R] [Nontrivial R] (p : R[X]) (n : ℕ) :
    IsMonicOfDegree p n ↔ p.natDegree ≤ n ∧ p.coeff n = 1 := by ...

and the definition:

/-- This says that `p` has `natDegree` `n` and is monic. -/
def IsMonicOfDegree {R : Type*} [Semiring R] (p : R[X]) (n : ℕ) : Prop :=
  p.natDegree = n ∧ p.Monic

Depending on what would be most convenient for the tactic, I can also add another characterization.

[Damiano Testa]

I had in mind the version below, but it can go in the in-tactic lemmas, since it is mostly to get the right goals, from the right shape.

lemma IsMonicOfDegree.of_natDegree_of_monic {R : Type*} [Semiring R] {p : R[X]} {n : ℕ}
    (hp : p.natDegree = n) (hm : p.Monic) :
    IsMonicOfDegree p n :=
  sorry

[Damiano Testa]

So, basically, once IsMonicOfDegree is in Mathlib, I would add the lemma above to the ComputeDegree tactic and the very small addition that will make the tactic aware of IsMonicOfDegree.

[Michael Stoll]

@Damiano Testa I realized that in order for this to work, I cannot import compute_degree and friends in the new file. So I'm making a PR that removes the import (and replaces the use of compute_degree with more pedestrian proofs): #26759 (and I have requested your review; I hope this is OK).

[Damiano Testa]

How about moving just the definition of IsMonicOfDegree to an earlier file and keeping the new file with the lemmas?

[Damiano Testa]

In any case, the tactic does not need to import IsMonicOfDegree to be able to discriminate based on it, although it would make sense if it did.

[Michael Stoll]

Spelling out the proofs is not so bad, actually.

[Damiano Testa]

Ok, I may not make the tactic import that file either, just to avoid adding unnecessary imports to the compute_degree tactic (and I prefer to have all these tactics in the same file, for simplicity).

[Damiano Testa]

Given how this is evolving, I am wondering if compute_degree and monicity should be merged into a single tactic, since the internal logic is essentially the same.

[Michael Stoll]

That sounds like a good idea. The question is, what should this single tactic be called? :smile:

[Damiano Testa]

Yes, I also think that right now that is the hardest step in the process.

[Aaron Liu]

just merge them and have compute_degree_monotonicity

[Michael Stoll]

poly_prop?

[Damiano Testa]

aesopoly? :lol:

[Damiano Testa]

Maybe poly_simp or simp_poly could work?

[Damiano Testa]

(Although the tactic is nothing like simp internally.)

[Ruben Van de Velde]

Just poly

[Yaël Dillies]

What about making them simprocs? Then no new tactic needed

[Damiano Testa]

I am not familiar enough with simprocs to know if they replace compute_degree.

[Damiano Testa]

How would a simproc know to compute the degree of X + 1?

[Damiano Testa]

(Right now, compute_degree reduces this to computing the max of the degree of X and of 1 and similarly for all ring operations.)

[Aaron Liu]

I imagine it would rewrite degree (X + 1) into max (degree X) (degree 1)

[Yaël Dillies]

You can plug any metaprogram into a simproc, so long as the metaprogram produces an equality of terms

[Aaron Liu]

oh I guess that works too

[Aaron Liu]

it feels like everything is turning into a simproc

[Yaël Dillies]

I personally believe that everything* that rewrites should be turned into a simproc

*unless it loops or has a very generic LHS

[Michael Stoll]

Coming back to the orignal topic: I have made #26766, which adds some convenience lemmas related to bounded sets.

[Michael Stoll]

Two more small PRs with convenience lemmas:

• #29214 adds two lemmas on (x ± r • 1)^2

[Michael Stoll]

• #29218 adds one lemma on ‖x • 1‖.

[Michael Stoll]

Coming back to docs#IsMonicOfDegree :
I would like to add two results (on factorization of monic polynomials over algebraically closed fields and over the reals), which need heavier imports, so they shouldn't go into the current file Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree. So a new file seems to be required. Should this be something like Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegreeFactorization, or is it better to add a subdirectory Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree, move the original file to ...Basic and have another file ...Factorization in there?

[Michael Stoll]

In any case, I get the warning

warning: Mathlib/Algebra/Polynomial/Degree/IsMonicOfDegreeFactorization.lean:9:0:
   Modules starting with Mathlib.Algebra are not allowed to import modules starting with Mathlib.Geometry.
   This module depends on Mathlib.Geometry.Convex.Cone.Basic
which is imported by Mathlib.Analysis.Convex.Cone.Extension,
which is imported by Mathlib.Analysis.NormedSpace.HahnBanach.Extension,
which is imported by Mathlib.Analysis.Normed.Module.Dual,
which is imported by Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus,
which is imported by Mathlib.Analysis.SpecialFunctions.NonIntegrable,
which is imported by Mathlib.MeasureTheory.Integral.CircleIntegral,
which is imported by Mathlib.Analysis.Complex.CauchyIntegral,
which is imported by Mathlib.Analysis.Complex.Liouville,
which is imported by Mathlib.Analysis.Complex.Polynomial.Basic,
which is imported by this module. (Exceptions can be added to `overrideAllowedImportDirs`.)

Should I add an exception? Or should the material go under Analysis somewhere?

[Michael Stoll]

FWIW, I added the line

set_option linter.directoryDependency false

suggested by the warning message to the file, but it still produces the same warning.
So how can I silence the linter without modifying the exceptions file?

[Michael Stoll]

For the time being, I have moved the file to Analysis.Polynomial.Factorization. See #29249 .

The first result is purely algebraic (but needs algebraically closed fields), whereas the second one needs the fact that irreducible polynomials over the reals have degree at most two, which comes down to the fact that $\mathbb C$ is algebraically closed and thus uses analysis.

[Damiano Testa]

Does the silencing work if you write

set_option linter.style.header false
set_option linter.directoryDependency false

between the last import and the first module doc?

[Damiano Testa]

I wonder if the directoryDependency linter should adopt some mechanism to only emit its warning on the first non-module-doc command, unless that command is set_option linter.directoryDependency false.

[Michael Stoll]

I had it after the module docstring. I didn't try to move it to right after the imports (before them would not work, I think, because of some other linter).

If a consensus emerges to move the file back into Algebra, I can try your suggestion.

[Damiano Testa]

Before the imports would not work, since there cannot be an import command after a non-import command.

[Michael Stoll]

#29649 now adds my versions of Gelfand-Mazur (~250 LOC plus docstrings). Reviews welcome!