A Tate ring has a zero sequence of units

Henkel's open mapping theorem is stated for a topological ring carrying a zero sequence of units. That hypothesis and the absorption property it exists for are generic, and live in TauCeti/Topology/Algebra/ZeroSequenceOfUnits.lean; this file supplies the bridge from Huber theory, namely that the powers of a pseudouniformiser are such a sequence.

This is where the Tate condition enters Henkel's theorem: a Huber ring that is not Tate need not admit such a sequence, ℤ_[p] being the example.

Main results

• TauCeti.Huber.IsPseudoUniformizer.tendsto_pow_unit: the powers of a pseudouniformiser converge to zero, as units. This is the concrete sequence, kept nameable so a caller holding ϖ can feed it to the generic results instead of destructing an existential.
• TauCeti.Huber.IsPseudoUniformizer.hasZeroSequenceOfUnits and TauCeti.Huber.IsTateRing.hasZeroSequenceOfUnits: a pseudouniformiser — hence a Tate ring, by instance search — satisfies the hypothesis.

References

• L. Henkel, An Open Mapping Theorem for rings which have a zero sequence of units, arXiv:1407.5647, whose hypothesis this discharges.
• Wedhorn, Adic Spaces, Theorem 6.16 and Propositions 6.17–6.18, which are proved from Henkel's theorem; downstream context for this file rather than its source.

theorem TauCeti.Huber.IsPseudoUniformizer.tendsto_pow_unit {A : Type u_1} [MonoidWithZero A] [TopologicalSpace A] {a : A} (ha : IsPseudoUniformizer a) : Filter.Tendsto (fun (n : ℕ) => ↑(⋯.unit ^ n)) Filter.atTop (nhds 0)

The powers of a pseudouniformiser converge to zero, as units. This is the concrete zero sequence, kept nameable so a caller holding ϖ can feed it to the absorption and covering results instead of destructing an existential.

theorem TauCeti.Huber.IsPseudoUniformizer.hasZeroSequenceOfUnits {A : Type u_1} [MonoidWithZero A] [TopologicalSpace A] {a : A} (ha : IsPseudoUniformizer a) : HasZeroSequenceOfUnits A

A pseudouniformiser makes the ring admit a zero sequence of units. No Huber or Tate hypothesis is needed: a topologically nilpotent unit supplies the class, through its powers. It is sufficient, not equivalent — the class asks only for some sequence of units tending to zero, and such a sequence need not consist of the powers of a single unit. The witness here is TauCeti.Huber.IsPseudoUniformizer.tendsto_pow_unit, which a caller wanting the powers themselves should use instead.

instance TauCeti.Huber.IsTateRing.hasZeroSequenceOfUnits {A : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsTateRing A] : HasZeroSequenceOfUnits A

A Tate ring satisfies Henkel's hypothesis on the base ring, via the powers of a pseudouniformiser.

This is where the Tate condition enters Henkel's theorem: a Huber ring that is not Tate need not admit such a sequence, ℤ_[p] being the example.