Absorption of fixed elements in a nonarchimedean ring

In a nonarchimedean ring multiplication by a fixed element a is continuous, so every neighbourhood V of zero absorbs a: some open additive subgroup Z satisfies a * Z ⊆ V. That single-element fact is Mathlib's NonarchimedeanRing.left_mul_subset. This file adds the one thing Mathlib does not have: the finite-family form, that one open subgroup absorbs each of finitely many fixed elements into its own target.

It mentions no weight family, power series or Huber ring, so it is stated here rather than alongside the theory that uses it.

Main results

• NonarchimedeanRing.exists_openAddSubgroup_forall_mul_subset: finitely many fixed elements are absorbed into their own targets by a single open subgroup.

References

• Mathlib's Mathlib/Topology/Algebra/Nonarchimedean/Basic.lean, whose NonarchimedeanRing.left_mul_subset the proof below runs on.

theorem NonarchimedeanRing.exists_openAddSubgroup_forall_mul_subset {A : Type u_1} [Ring A] [TopologicalSpace A] [NonarchimedeanRing A] {ι : Type u_2} (s : Finset ι) (a : ι → A) (V : ι → AddSubgroup A) (hV : ∀ i ∈ s, ↑(V i) ∈ nhds 0) : ∃ (Z : OpenAddSubgroup A), ∀ i ∈ s, ∀ z ∈ Z, a i * z ∈ V i

The finite-family absorption lemma: one open subgroup absorbs each of finitely many fixed elements into its own target.

The single-element case is Mathlib's NonarchimedeanRing.left_mul_subset, used directly in the induction below; only the target has to be unbundled, since a subgroup that is a neighbourhood of zero is open.