Rings with a zero sequence of units

Henkel's open mapping theorem is stated for a topological ring carrying a zero sequence of units: a sequence of units converging to zero. This file isolates that hypothesis and proves the absorption property it exists for — every element is carried into every neighbourhood of zero by some term of the sequence, so the dilates of a neighbourhood cover the space acted on.

The class carries no continuity, and this file assumes no continuity instance either, so each result below takes an explicit hc : ContinuousAt (fun a : A ↦ a • x) 0 — continuity of the scalar action in the scalar alone, at zero, for the vector in question. Without it the statements are false for a MonoidWithZero with an arbitrary topology. ContinuousSMul A M would do but is joint continuity, strictly more than these proofs use.

Nothing here is Huber-specific, or even ring-specific. The hypothesis is about A, but the results act on a space M carrying a zero and a scalar multiplication by A — [Zero M], [TopologicalSpace M], and a scalar multiplication, with no additive structure on M required, so M is not assumed to be a module.

How much scalar multiplication is needed splits the file in two. The two pointwise absorption results ask for [SMul A M] and h0 : (0 : A) • x = 0 at the given vector. The covering theorem requires [MulAction A M] and h0 : ∀ x : M, (0 : A) • x = 0. Neither requires scalar multiplication to preserve zero in the vector argument.

That is the form Henkel's theorem needs, since his Baire argument covers the domain of the map rather than the base ring; taking M = A recovers the ring statements. The bridge to Huber theory — that the powers of a pseudouniformiser are such a sequence, so a Tate ring qualifies — is in TauCeti/RingTheory/Huber/ZeroSequenceOfUnits.lean.

The covering is the point, and it must be countable. Henkel's proof applies a Baire argument to the sets uₙ⁻¹ • U indexed by n : ℕ; a cover indexed by all of Aˣ would exhaust M just as well but could not start that argument. Both results are therefore stated for an arbitrary zero sequence, so that a caller holding a concrete one — the powers of a pseudouniformiser, say — keeps it rather than trading it for an opaque choice.

Main definitions

• TauCeti.HasZeroSequenceOfUnits: the ring admits a sequence of units tending to zero.

Main results

All three carry the continuity hypothesis described above; the covering needs it at every vector, the two pointwise results only at their own.

• TauCeti.exists_smul_mem_of_tendsto_zero: along any zero sequence of units, some term carries a given element of a space with [SMul A M] and 0 • x = 0 into a neighbourhood of zero.
• TauCeti.iUnion_inv_smul_eq_univ_of_tendsto_zero: its dilates uₙ⁻¹ • U cover M, indexed by ℕ. This needs [MulAction A M] and 0 • x = 0 for every vector.
• TauCeti.HasZeroSequenceOfUnits.exists_unit_smul_mem: the weaker unit-only form of absorption — it produces some v : Aˣ, with no sequence and no term index. Being an absorption result it too needs only [SMul A M] and 0 • x = 0 at the given vector.

References

• L. Henkel, An Open Mapping Theorem for rings which have a zero sequence of units, arXiv:1407.5647. The hypothesis formalised here, the terminology, and the results below are its setup.

class TauCeti.HasZeroSequenceOfUnits (A : Type u_1) [MonoidWithZero A] [TopologicalSpace A] : Prop

Henkel's hypothesis on the base ring: there is a sequence of units converging to zero.

A discrete ring has none unless it is trivial, and that is the intended exclusion: the theorem needs to shrink a neighbourhood by an invertible factor.

• exists_tendsto : ∃ (u : ℕ → Aˣ), Filter.Tendsto (fun (n : ℕ) => ↑(u n)) Filter.atTop (nhds 0)

  Some sequence of units converges to zero.

@[simp]

theorem TauCeti.hasZeroSequenceOfUnits_iff (A : Type u_1) [MonoidWithZero A] [TopologicalSpace A] : HasZeroSequenceOfUnits A ↔ ∃ (u : ℕ → Aˣ), Filter.Tendsto (fun (n : ℕ) => ↑(u n)) Filter.atTop (nhds 0)

The class unfolds to the existential it wraps. This is its @[simp] normal form; a proof already holding the instance normally reaches the sequence through the field directly, as ‹HasZeroSequenceOfUnits A›.exists_tendsto.

theorem TauCeti.exists_smul_mem_of_tendsto_zero {A : Type u_1} [MonoidWithZero A] [TopologicalSpace A] {M : Type u_2} [Zero M] [TopologicalSpace M] [SMul A M] {u : ℕ → Aˣ} (hu : Filter.Tendsto (fun (n : ℕ) => ↑(u n)) Filter.atTop (nhds 0)) (x : M) (h0 : 0 • x = 0) (hc : ContinuousAt (fun (a : A) => a • x) 0) {U : Set M} (hU : U ∈ nhds 0) : ∃ (n : ℕ), ↑(u n) • x ∈ U

Absorption. Along a zero sequence of units in A, every element of a space M carrying a scalar multiplication by A satisfying 0 • x = 0 is carried into every neighbourhood of zero by some term of the sequence.

Stated for an arbitrary such sequence rather than a chosen one, so a caller holding a concrete sequence — the powers of a pseudouniformiser, say — gets the conclusion for that sequence.

The hypothesis hc requires continuity of a ↦ a • x at 0 : A, with x fixed. This is weaker than the joint continuity required by ContinuousSMul A M. When M = A, (continuous_mul_const x).continuousAt supplies this hypothesis modulo smul_eq_mul.

theorem TauCeti.iUnion_inv_smul_eq_univ_of_tendsto_zero {A : Type u_1} [MonoidWithZero A] [TopologicalSpace A] {M : Type u_2} [Zero M] [TopologicalSpace M] [MulAction A M] {u : ℕ → Aˣ} (hu : Filter.Tendsto (fun (n : ℕ) => ↑(u n)) Filter.atTop (nhds 0)) (h0 : ∀ (x : M), 0 • x = 0) (hc : ∀ (x : M), ContinuousAt (fun (a : A) => a • x) 0) {U : Set M} (hU : U ∈ nhds 0) : ⋃ (n : ℕ), (u n)⁻¹ • U = Set.univ

The countable covering Henkel's Baire argument runs on: the dilates uₙ⁻¹ • U of a neighbourhood of zero exhaust M. The index is ℕ, which is what makes the cover usable in a Baire argument — a cover by all of Aˣ would exhaust M too but could not start that argument. Henkel needs this for the domain of the map, which is why M is not just the base ring.

theorem TauCeti.HasZeroSequenceOfUnits.exists_unit_smul_mem {A : Type u_1} [MonoidWithZero A] [TopologicalSpace A] {M : Type u_2} [Zero M] [TopologicalSpace M] [SMul A M] [HasZeroSequenceOfUnits A] (x : M) (h0 : 0 • x = 0) (hc : ContinuousAt (fun (a : A) => a • x) 0) {U : Set M} (hU : U ∈ nhds 0) : ∃ (v : Aˣ), ↑v • x ∈ U

Some unit of A carries a given element of M into a given neighbourhood of zero.

Deliberately not phrased with a sequence: quantifying over an unconstrained u : ℕ → Aˣ would say no more than this, since a constant sequence witnesses it. The sequence matters only for iUnion_inv_smul_eq_univ_of_tendsto_zero, which is stated for a given sequence carrying its own convergence hypothesis rather than restated at class level.