A first-countable nonarchimedean group has a decreasing basis of open subgroups

Henkel's open mapping theorem runs a successive-approximation argument down a sequence of neighbourhoods of zero, each one absorbing the previous error. Two properties of that sequence are used and neither comes for free: its terms must be subgroups, so that a sum of errors drawn from one term stays inside it, and it must be decreasing, so that the tail of the construction stays inside the neighbourhood it started in.

Nonarchimedean gives the first, countable generation of 𝓝 0 the second, and this file combines them. Neither hypothesis alone suffices — a nonarchimedean group has open subgroups arbitrarily close to zero but possibly uncountably many with no cofinal sequence among them, and a first-countable group has a decreasing countable basis whose terms need not be subgroups.

Main results

• NonarchimedeanAddGroup.exists_antitone_basis_openAddSubgroup: the neighbourhoods of zero admit an antitone basis consisting of open subgroups, indexed by ℕ.

References

• L. Henkel, An Open Mapping Theorem for rings which have a zero sequence of units, arXiv:1407.5647, whose approximation argument needs such a sequence.

theorem NonarchimedeanAddGroup.exists_antitone_basis_openAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] [(nhds 0).IsCountablyGenerated] [NonarchimedeanAddGroup G] : ∃ (V : ℕ → OpenAddSubgroup G), (nhds 0).HasAntitoneBasis fun (n : ℕ) => ↑(V n)

A first-countable nonarchimedean additive group has an antitone basis of open subgroups at zero.

Both hypotheses are used, and only where stated: nonarchimedean makes the open subgroups a basis of 𝓝 0 at all, and countable generation of 𝓝 0 is what extracts an antitone sequence from that basis.

Countable generation of 𝓝 0 and FirstCountableTopology G are in fact equivalent under these hypotheses, since NonarchimedeanAddGroup extends IsTopologicalAddGroup: TauCeti.SeparatelyContinuousAdd.toFirstCountableTopology gives one direction and FirstCountableTopology.nhds_generated_countable the other. The 𝓝 0 form is stated because it is the one the proof consumes.