Point-set topology of a nonarchimedean local field

A nonarchimedean local field K is Hausdorff (Mathlib's IsValuativeTopology.instT2Space) and locally compact (part of IsNonarchimedeanLocalField K). This file adds that it is second countable, and records that it is totally disconnected: its valuative topology is nonarchimedean (TauCeti.instNonarchimedeanRingOfIsValuativeTopology), so Mathlib's NonarchimedeanAddGroup.instTotallySeparated applies.

These four properties are what the point topology on the rational points of an affine group over K inherits (TauCeti/Topology/Algebra/PointTopology/Separation.lean).

Second countability is proved through the normalized absolute value (TauCeti.normalizedNontriviallyNormedField): a locally compact nontrivially normed field is a proper metric space, and proper metric spaces are second countable.

Main declarations

• TauCeti.instSecondCountableTopologyOfIsNonarchimedeanLocalField: a nonarchimedean local field is second countable.

instance TauCeti.instSecondCountableTopologyOfIsNonarchimedeanLocalField {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : SecondCountableTopology K

A nonarchimedean local field is second countable.