The normed-field structure of a nonarchimedean local field

A nonarchimedean local field K is presented in Mathlib by a valuative relation together with a topology (IsNonarchimedeanLocalField K), whereas the analytic library (power series, the spectral norm, Krasner's lemma) consumes a NormedField. This file supplies the bridge: the normalized absolute value ‖x‖_K = q ^ (-v_K(x)) of TauCeti.normalizedAbsoluteValue makes K a normed field, and the topology of that norm is the topology K already carries.

The structures are named definitions rather than global instances, so that installing them is always local and a field already carrying a norm acquires no diamond. They are meant to be used as letI := normalizedNormedField K; the theorems below are stated in that form.

Main definitions

• TauCeti.normalizedNormedField: the normed-field structure on K given by the normalized absolute value.
• TauCeti.normalizedNormedFieldTopology: the topology of that norm.
• TauCeti.normalizedNontriviallyNormedField: the same norm, as a nontrivially normed field.

Main results

• TauCeti.normalizedNormedField_topology_eq: the norm topology is the given topology of K.
• TauCeti.normalizedNormedField_isUltrametricDist: the norm is ultrametric.
• TauCeti.normalizedNormedField_completeSpace: K is complete for the norm.

References

• J.-P. Serre, Corps Locaux, Chapter II, §1.
• J. Neukirch, Algebraic Number Theory, Chapter II, §§3–4.

@[implicit_reducible]

noncomputable def TauCeti.normalizedNormedField (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : NormedField K

The normed-field structure on a nonarchimedean local field K whose norm is the normalized absolute value ‖x‖_K = q ^ (-v_K(x)), where q is the cardinality of the residue field.

Equations

• TauCeti.normalizedNormedField K = { toFun := fun (x : K) => ↑((TauCeti.normalizedAbsoluteValue K) x), map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }.toNormedField

theorem TauCeti.normalizedNormedField_norm_def {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : K) : ‖x‖ = ↑((normalizedAbsoluteValue K) x)

The norm of normalizedNormedField K is the normalized absolute value.

@[implicit_reducible]

noncomputable def TauCeti.normalizedNormedFieldTopology (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : TopologicalSpace K

The topology on K induced by the norm of normalizedNormedField K. It is kept as a separate definition because it agrees with the given topology of K only propositionally, by normalizedNormedField_topology_eq.

Equations

• TauCeti.normalizedNormedFieldTopology K = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

theorem TauCeti.normalizedNormedField_topology_eq (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : normalizedNormedFieldTopology K = inst✝

The topology induced by the normalized absolute value is the given topology of a nonarchimedean local field.

theorem TauCeti.normalizedNormedField_isUltrametricDist (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsUltrametricDist K

The normalized absolute value is ultrametric.

theorem TauCeti.normalizedNormedField_completeSpace (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : CompleteSpace K

A nonarchimedean local field is complete for its normalized absolute value.

@[implicit_reducible]

noncomputable def TauCeti.normalizedNontriviallyNormedField (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : NontriviallyNormedField K

The normalized absolute value of a nonarchimedean local field K, as a nontrivially normed field structure on K. Its underlying normed field is normalizedNormedField K.

Equations

• TauCeti.normalizedNontriviallyNormedField K = { toNormedField := TauCeti.normalizedNormedField K, non_trivial := ⋯ }