Appropriate base for the RankOne hom instance for K((X))

Stream: new members

[Yakov Pechersky]

Since my PR on nonarchimedean local fields is almost complete (#16733), I thought about making sure that the results can be applied for the enumeration of such fields (finite extensions of Q_p and F_q((T))). To even start down this route, I found that NontriviallyNormedField K((X)) does not yet exist. We do have Valued K⸨X⸩ ℤₘ₀.

Apparently, the only thing that was missing for Valued.toNormedField to fir e is a Valuation.RankOne instance. We only have 2 such instances in mathlib, one of which I added myself (the obvious NormedField.toValued one). I haven't grokked the API set up of Valued and Valuation.RankOne entirely, especially with way that Valued carries data and can be "noncanonical" since the codomain is an outparam.

Here is my attempt to generate a NontriviallyNormedField K⸨X⸩. You'll note that I used e := 2 for the base of the Zm0 -> NNReal hom. What is the "proper" value to use here? Does it even matter (?), since the RankOne nature is only used for the nontrivial aspect. cc @Jiang Jiedong @María Inés de Frutos Fernández as contributors to Valued.to(Nontrivially)NormedField.

import Mathlib

variable {K : Type*} [Field K]

noncomputable
instance : Valuation.RankOne (Valued.v (R := LaurentSeries K)) where
  hom := WithZeroMulInt.toNNReal two_ne_zero
  strictMono' := WithZeroMulInt.toNNReal_strictMono one_lt_two
  nontrivial' := by
    refine ⟨HahnSeries.single 2 1, ?_⟩
    simp only [LaurentSeries.valuation_single_zpow, ofAdd_neg, WithZero.coe_inv, ne_eq, inv_eq_one]
    simp [← WithZero.coe_one]

open scoped Valued in
noncomputable instance : NontriviallyNormedField (LaurentSeries K) := inferInstance

instance : IsUltrametricDist (LaurentSeries K) := inferInstance

[Kevin Buzzard]

There's no canonical value in general. If K were finite then its size would be a nice choice because then $K((x))$ is locally compact and you've chosen the factor that additive haar measure is being scaled by (see the Haar character project in the FLT blueprint) but I imagine that it's not in general in your situation (yet) so anything bigger than 1 works

[Kevin Buzzard]

The argument for using 37 instead of 2 is that it indicates that it's random

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

In our work on local fields, given a valued field K (not necessarily a field of Laurent series), @Filippo A. E. Nuccio and I take e to be the size of the residue field ofK if it is finite, and otherwise e := 6 (a random non-prime power). You could do an analogous choice here.

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

We call this Valuation.base.

[Michael Stoll]

There is an instance WithAbs.nontriviallynormedField in Heights.Equivalence. (This circumvents the "base" problem by forcing you to specify the absolute value.)