Bounded subsets of a topological ring

A subset S of a topological monoid with zero is bounded when every neighbourhood U of zero absorbs S: there is a neighbourhood V of zero with V * S ⊆ U. This is the notion of boundedness underlying Huber's theory of adic spaces (Wedhorn, Adic Spaces, Definition 5.27), where it is the condition cutting out the rings of definition of a Huber ring.

Provenance

IsBounded and the elementary calculus — IsBounded.subset, isBounded_empty, isBounded_singleton_zero, isBounded_pair_zero_one, IsBounded.union, IsBounded.mul, isBounded_singleton and isBounded_finite — follow William Coram's mathlib4#40013, as do several of their proofs. Everything else here is new: isBounded_iUnion, the nonarchimedean IsBounded.addSubgroupClosure, IsBounded.add and isBounded_sup, and the image and transport lemmas. The selection and ordering of results follows AINTLIB's Bounded.lean; its proofs were not used.

Main definitions

• TauCeti.Huber.IsBounded: S is bounded, i.e. every neighbourhood of zero absorbs S.

Main results

• TauCeti.Huber.isBounded_iff: unfolding lemma for IsBounded.
• TauCeti.Huber.isBounded_finsetProd: a finite pointwise product of bounded sets is bounded.
• TauCeti.Huber.isBounded_finite: finite sets are bounded.
• TauCeti.Huber.isBounded_of_isLinearTopology: in a linearly topologized commutative ring, such as an adic ring, every subset is bounded.
• TauCeti.Huber.IsBounded.union, TauCeti.Huber.IsBounded.mul: unions and pointwise products of bounded sets are bounded.
• TauCeti.Huber.IsBounded.add, TauCeti.Huber.IsBounded.addSubgroupClosure: over a ring with a nonarchimedean additive group, sums and the generated additive subgroup of bounded sets stay bounded.
• TauCeti.Huber.isBounded_sup: the join of two bounded subrings of a commutative ring is bounded — the boundedness input for joins of rings of definition.
• TauCeti.Huber.IsBounded.image: a morphism continuous at zero which is open at zero preserves boundedness, and TauCeti.Huber.isBounded_image_ringEquiv_iff transports boundedness along a topological ring isomorphism.

Implementation notes

This is not Mathlib's Bornology.IsVonNBounded. That predicate asks that every neighbourhood of zero absorb S after dilation by a norm-large scalar, so it needs a SeminormedRing of scalars to have a bornology to be cofinal in; a Huber ring such as ℤ_[p]⟦T⟧ with its (p, T)-adic topology carries no such norm. The two notions agree over a nontrivially normed field acting on itself, but neither the statement shape (∃ V ∈ 𝓝 0, V * S ⊆ U against ∀ᶠ a in cobounded, S ⊆ a • U) nor the hypotheses transfer.

Boundedness is not preserved by an arbitrary continuous homomorphism: giving ℚ_[p] the discrete topology makes every subset bounded, while the identity to the p-adic topology is continuous and ℚ_[p] is not bounded in itself. IsBounded.image therefore carries the extra hypothesis that the morphism maps neighbourhoods of zero to neighbourhoods of zero.

References

• Wedhorn, Adic Spaces, Definition 5.27 and Remark 5.28.
• William Coram, feat: define bounded sets and power bounded elements, mathlib4#40013.
• AINTLIB, branch dev/adic-spaces, projects/AdicSpaces/Adic spaces/Bounded.lean.

def TauCeti.Huber.IsBounded {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] (S : Set M) : Prop

A subset S of a topological monoid with zero is bounded if for every neighbourhood U of 0 there is a neighbourhood V of 0 with V * S ⊆ U.

Equations

• TauCeti.Huber.IsBounded S = ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, V * S ⊆ U

theorem TauCeti.Huber.isBounded_iff {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] {S : Set M} : IsBounded S ↔ ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, V * S ⊆ U

Unfolding lemma for TauCeti.Huber.IsBounded.

theorem TauCeti.Huber.IsBounded.exists_pow_mul_subset {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] {S U : Set M} {a : M} (hS : IsBounded S) (ha : IsTopologicallyNilpotent a) (hU : U ∈ nhds 0) : ∃ (n : ℕ), {a ^ n} * S ⊆ U

Some power of a topologically nilpotent element multiplies a bounded set into any neighbourhood of zero.

theorem TauCeti.Huber.IsBounded.subset {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] {S T : Set M} (hS : IsBounded S) (hTS : T ⊆ S) : IsBounded T

Subsets of bounded sets are bounded.

@[simp]

theorem TauCeti.Huber.isBounded_empty {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] : IsBounded ∅

The empty set is bounded.

@[simp]

theorem TauCeti.Huber.isBounded_singleton_zero {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] : IsBounded {0}

The singleton {0} is bounded.

@[simp]

theorem TauCeti.Huber.isBounded_pair_zero_one {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] : IsBounded {0, 1}

The pair {0, 1} is bounded.

theorem TauCeti.Huber.isBounded_iUnion {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] {ι : Sort u_2} [Finite ι] {S : ι → Set M} (hS : ∀ (i : ι), IsBounded (S i)) : IsBounded (⋃ (i : ι), S i)

A finite union of bounded sets is bounded.

@[simp]

theorem TauCeti.Huber.isBounded_iUnion_iff {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] {ι : Sort u_2} [Finite ι] {S : ι → Set M} : IsBounded (⋃ (i : ι), S i) ↔ ∀ (i : ι), IsBounded (S i)

A finite indexed union is bounded exactly when every piece is.

theorem TauCeti.Huber.IsBounded.union {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] {S T : Set M} (hS : IsBounded S) (hT : IsBounded T) : IsBounded (S ∪ T)

The union of two bounded sets is bounded.

@[simp]

theorem TauCeti.Huber.isBounded_union {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] {S T : Set M} : IsBounded (S ∪ T) ↔ IsBounded S ∧ IsBounded T

A union is bounded exactly when both parts are.

theorem TauCeti.Huber.IsBounded.mul {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] {S T : Set M} (hS : IsBounded S) (hT : IsBounded T) : IsBounded (S * T)

The pointwise product of two bounded sets is bounded.

theorem TauCeti.Huber.isBounded_of_discreteTopology {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] [DiscreteTopology M] (S : Set M) : IsBounded S

Every subset of a discrete monoid with zero is bounded.

@[simp]

theorem TauCeti.Huber.isBounded_singleton {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] [SeparatelyContinuousMul M] (a : M) : IsBounded {a}

Every singleton is bounded.

theorem TauCeti.Huber.isBounded_finite {M : Type u_1} [MonoidWithZero M] [TopologicalSpace M] [SeparatelyContinuousMul M] {S : Set M} (hS : S.Finite) : IsBounded S

Every finite subset is bounded.

theorem TauCeti.Huber.isBounded_finsetProd {M : Type u_1} [CommMonoidWithZero M] [TopologicalSpace M] {ι : Type u_2} (s : Finset ι) {S : ι → Set M} (hS : ∀ i ∈ s, IsBounded (S i)) : IsBounded (∏ i ∈ s, S i)

A finite pointwise product of bounded sets is bounded. Commutativity is what makes the Finset product of sets available in the first place, and no continuity is required.

theorem TauCeti.Huber.isBounded_of_isLinearTopology {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsLinearTopology A A] (S : Set A) : IsBounded S

Every subset of a linearly topologized commutative ring is bounded: a neighbourhood of zero contains an open ideal, which absorbs every subset. This covers the adic rings, such as ℤ_[p] or W(𝒪_F) with its (p, [ϖ])-adic topology, and in particular the discrete rings.

theorem TauCeti.Huber.IsBounded.addSubgroupClosure {A : Type u_1} [Ring A] [TopologicalSpace A] [NonarchimedeanAddGroup A] {S : Set A} (hS : IsBounded S) : IsBounded ↑(AddSubgroup.closure S)

The additive subgroup generated by a bounded set is bounded in a nonarchimedean ring (the key step of Wedhorn, Proposition 5.30).

theorem TauCeti.Huber.IsBounded.add {A : Type u_1} [Ring A] [TopologicalSpace A] [NonarchimedeanAddGroup A] {S T : Set A} (hS : IsBounded S) (hT : IsBounded T) : IsBounded (S + T)

The pointwise sum of two bounded sets is bounded in a nonarchimedean ring.

theorem TauCeti.Huber.isBounded_sup {A : Type u_2} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] (B₀ B₁ : Subring A) (hB₀ : IsBounded ↑B₀) (hB₁ : IsBounded ↑B₁) : IsBounded ↑(B₀ ⊔ B₁)

The join of two bounded subrings of a commutative ring is bounded.

theorem TauCeti.Huber.IsBounded.image {M : Type u_1} {N : Type u_2} [MonoidWithZero M] [MonoidWithZero N] [TopologicalSpace M] [TopologicalSpace N] {F : Type u_3} [FunLike F M N] [ZeroHomClass F M N] [MulHomClass F M N] {f : F} (hf : ContinuousAt (⇑f) 0) (hf₀ : ∀ V ∈ nhds 0, ⇑f '' V ∈ nhds 0) {S : Set M} (hS : IsBounded S) : IsBounded (⇑f '' S)

A morphism continuous at zero which carries neighbourhoods of zero to neighbourhoods of zero sends bounded sets to bounded sets.

Boundedness is a condition at zero only, so continuity away from zero is irrelevant; but continuity at zero alone is not enough, since refining the topology on the source only creates bounded sets.

theorem TauCeti.Huber.IsBounded.image_of_isOpenMap {M : Type u_1} {N : Type u_2} [MonoidWithZero M] [MonoidWithZero N] [TopologicalSpace M] [TopologicalSpace N] {F : Type u_3} [FunLike F M N] [ZeroHomClass F M N] [MulHomClass F M N] {f : F} (hf : ContinuousAt (⇑f) 0) (hf₀ : IsOpenMap ⇑f) {S : Set M} (hS : IsBounded S) : IsBounded (⇑f '' S)

An open morphism continuous at zero sends bounded sets to bounded sets.

theorem TauCeti.Huber.IsBounded.image_ringEquiv {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] [TopologicalSpace A] [TopologicalSpace B] (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) {S : Set A} (hS : IsBounded S) : IsBounded (⇑e '' S)

A topological ring isomorphism sends bounded sets to bounded sets.

theorem TauCeti.Huber.isBounded_image_ringEquiv_iff {A : Type u_1} {B : Type u_2} [Semiring A] [Semiring B] [TopologicalSpace A] [TopologicalSpace B] (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) {S : Set A} : IsBounded (⇑e '' S) ↔ IsBounded S

Boundedness transports along a topological ring isomorphism.