naming of sup of some norms

Stream: mathlib4

[Kevin Buzzard]

#23184 is an important step towards constructing a perfectoid space with one element :-) Given a nonarchimedean norm on a field K and a field L which is a finite extension L, the PR constructs a "canonical" norm on L which is compatible with the norm on K. I would be happy to merge it if I were happy with the name of the definition, which is currently

IsNonarchimedean.algNormOfAut.{u_1, u_2} {K : Type u_1} [NormedField K] {L : Type u_2} [Field L] [Algebra K L]
  (h_fin : FiniteDimensional K L) (hna : IsNonarchimedean norm) : AlgebraNorm K L

The actual definition is: use the axiom of choice to get a noncanonical extension which is a power-multiplicative norm (this is not at all easy and was the subject of earlier PRs) and then take the sup over the Galois conjugates of this norm. It turns out that this averaging process gives you an extension which is the unique one with some properties, so it's definitely worth a name. But I don't like Aut in the name because there's no automorphism in the type of the definition, automorphism just play a role in the definition of the underlying function. What would be a better name for this? Or should I stop fussing?

[Anatole Dedecker]

IsNonarchimedean.invariantExtension ?

[Kevin Buzzard]

@María Inés de Frutos Fernández what do you think? Have I got the details right? Sorry for holding this PR up.

[Michael Stoll]

IsNonarchimedean.algNormOfFiniteDimensional?

[Kevin Buzzard]

Ha ha I suggested that in the PR but it's kind of a long name for a fundamental thing (Maria Ines is extending the p-adic norm to a norm on any finite extension of Q_p and proving uniqueness, so we can have a norm on Q_p-bar and thus create C_p, giving us Spa(C_p) as a perfectoid space and also B_{HT} etc). Imagine having to call such a fundamental construction such a large name all the way through this theory.

[Andrew Yang]

Can it be called extend or extendScalars etc?

[Yakov Pechersky]

Can I please ask we use IsUltrametricDist instead of the explicit arg (h : IsNonarchimedean (norm : K → ℝ))?

[Kevin Buzzard]

I'd be happy with extend. Of course once we have that it's unique (which I think will need extra assumptions e.g. completeness) then we'll perhaps need some extension of this to algebraic extensions of nonarch normed fields and that will also be a candidate for extend.

[Yakov Pechersky]

extendFin then, with a later extend that shows extendFin = extend?

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

Kevin Buzzard said:

Of course once we have that it's unique (which I think will need extra assumptions e.g. completeness) then we'll perhaps need some extension of this to algebraic extensions of nonarch normed fields and that will also be a candidate for extend.

I have already PR'd the extension to algebraic extensions and the uniqueness theorem: see #23301 and #23333. There I use the name spectralNorm, following BGR.
For the norm in #23184, I like Anatole's suggestion (IsNonarchimedean.invariantExtension).