Discrete uniformities and discrete topology

Exactly as different metrics can induce equivalent topologies on a space, it is possible that different uniform structures (a notion that generalises that of a metric structure) induce the same topology on a space. In this file we are concerned in particular with the discrete topology, formalised using the class DiscreteTopology, and the discrete uniformity, that is the bottom element of the lattice of uniformities on a type (see bot_uniformity).

The theorem discreteTopology_of_discrete_uniformity shows that the topology induced by the discrete uniformity is the discrete one, but it is well-known that the converse might not hold in general, along the lines of the above discussion. We explicitly produce a metric and a uniform structure on a space (on ℕ, actually) that are not discrete, yet induce the discrete topology.

To check that a certain uniformity is not discrete, recall that once a type α is endowed with a uniformity, it is possible to speak about Cauchy filters on a and it is quite easy to see that if the uniformity on a is the discrete one, a filter is Cauchy if and only if it coincides with the principal filter 𝓟 {x} (see Filter.principal) for some x : α. This is the declaration UniformSpace.DiscreteUnif.eq_const_of_cauchy in Mathlib.

A special case of this result is the intuitive observation that a sequence a : ℕ → ℕ can be a Cauchy sequence if and only if it is eventually constant: when claiming this equivalence, one is implicitly endowing ℕ with the metric inherited from ℝ, that induces the discrete uniformity on ℕ. Hence, the intuition suggesting that a Cauchy sequence, whose terms are "closer and closer to each other", valued in ℕ must be eventually constant for topological reasons, namely the fact that ℕ is a discrete topological space, is wrong in the sense that the reason is intrinsically "metric". In particular, if a non-constant sequence (like the identity id : ℕ → ℕ is Cauchy, then the uniformity is certainly not discrete.

The counterexamples

We produce two counterexamples: in the first section Metric we construct a metric and in the second section SetPointUniformity we construct a uniformity, explicitly as a filter on ℕ × ℕ. They basically coincide, and the difference of the examples lies in their flavours.

The metric

We begin by defining a metric on ℕ (see dist_def) that

1. Induces the discrete topology, as proven in TopIsDiscrete;
2. Is not the discrete metric, in particular because the identity is a Cauchy sequence, as proven in idIsCauchy

The definition is simply dist m n = |2 ^ (- n : ℤ) - 2 ^ (- m : ℤ)|, and I am grateful to Anatole Dedecker for his suggestion.

The point-set-theoretic uniformity

A uniformity on ℕ is a filter on ℕ × ℕ satisfying some properties: we define a sequence of subsets fundamentalEntourage n : (Set ℕ × ℕ) (indexed by n : ℕ) and we observe it satisfies the condition needed to be a basis of a filter: moreover, the filter generated by this basis satisfies the condition for being a uniformity, and this is the uniformity we put on ℕ.

For each n, the set fundamentalEntourage n : Set (ℕ × ℕ) consists of the n+1 points {(0,0),(1,1)...(n,n)} on the diagonal; together with the half plane {(x,y) | n ≤ x ∧ n ≤ y}

That this collection can be used as a filter basis is proven in the definition counterBasis and that the filter counterBasis.filterBasis is a uniformity is proven in the definition counterCoreUniformity.

This induces the discrete topology, as proven in TopIsDiscrete and the atTop filter is Cauchy (see atTopIsCauchy): that this specializes to the statement that the identity sequence id : ℕ → ℕ is Cauchy is proven in idIsCauchy.

Implementation details

Since most of the statements evolve around membership of explicit natural numbers (framed by some inequality) to explicit subsets, many proofs are easily closed by aesop or omega or linarith.

References

• N. Bourbaki, General Topology, Chapter II

noncomputable def instPseudoMetricSpaceNat_counterexamples : PseudoMetricSpace ℕ

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem dist_def {n m : ℕ} : dist n m = |2 ^ (-↑n) - 2 ^ (-↑m)|

theorem Int.eq_of_pow_sub_le {d : ℕ} {m n : ℤ} (hd1 : 1 < d) (h : |↑d ^ (-m) - ↑d ^ (-n)| < ↑d ^ (-n - 1)) : m = n

theorem ball_eq_singleton {n : ℕ} : Metric.ball n (2 ^ (-↑n - 1)) = {n}

theorem TopIsDiscrete : DiscreteTopology ℕ

theorem idIsCauchy : CauchySeq id

def fundamentalEntourage (n : ℕ) : Set (ℕ × ℕ)

The fundamental entourages (index by n : ℕ) used to construct a basis of the uniformity: for each n, the set fundamentalEntourage n : Set (ℕ × ℕ) consists of the n+1 points {(0,0),(1,1)...(n,n)} on the diagonal; together with the half plane {(x,y) | n ≤ x ∧ n ≤ y}.

Equations

• fundamentalEntourage n = (⋃ (i : ↑(Set.Icc 0 n)), {(↑i, ↑i)}) ∪ Set.Ici (n, n)

@[simp]

theorem fundamentalEntourage_ext (t : ℕ) (T : Set (ℕ × ℕ)) : fundamentalEntourage t = T ↔ T = (⋃ (i : ↑(Set.Icc 0 t)), {(↑i, ↑i)}) ∪ Set.Ici (t, t)

theorem mem_range_fundamentalEntourage (S : Set (ℕ × ℕ)) : S ∈ Set.range fundamentalEntourage ↔ ∃ (n : ℕ), fundamentalEntourage n = S

theorem mem_fundamentalEntourage (n : ℕ) (P : ℕ × ℕ) : P ∈ fundamentalEntourage n ↔ n ≤ P.1 ∧ n ≤ P.2 ∨ P.1 = P.2

def counterBasis : FilterBasis (ℕ × ℕ)

The collection fundamentalEntourage satisfies the axioms to be a basis for a filter on ℕ × ℕ and gives rise to a term in the relevant type.

Equations

• counterBasis = { sets := Set.range fundamentalEntourage, nonempty := counterBasis._proof_1, inter_sets := @counterBasis._proof_2 }

@[simp]

theorem mem_counterBasis_iff (S : Set (ℕ × ℕ)) : S ∈ counterBasis ↔ S ∈ Set.range fundamentalEntourage

def counterCoreUniformity : UniformSpace.Core ℕ

The "crude" uniform structure, without topology, simply as a the filter generated by Basis and satisfying the axioms for being a uniformity. We later extract the topology counterTopology generated by it and bundle counterCoreUniformity and counterTopology in a uniform structure on ℕ, proving in passing that counterTopology = ⊥.

Equations

• counterCoreUniformity = UniformSpace.Core.mkOfBasis counterBasis counterCoreUniformity._proof_1 counterCoreUniformity._proof_2 counterCoreUniformity._proof_3

instance counterTopology : TopologicalSpace ℕ

The topology on ℕ induced by the "crude" uniformity

Equations

• counterTopology = counterCoreUniformity.toTopologicalSpace

instance counterUniformity : UniformSpace ℕ

The uniform structure on ℕ bundling together the "crude" uniformity and the topology

Equations

• counterUniformity = UniformSpace.ofCore counterCoreUniformity

theorem HasBasis_counterUniformity : (uniformity ℕ).HasBasis (fun (x : ℕ) => True) fundamentalEntourage

theorem TopIsDiscrete' : DiscreteTopology ℕ

A proof that the topology on ℕ induced by the "crude" uniformity counterCoreUniformity (or by counterUniformity tout-court, since they are defeq) is discrete

theorem atTopIsCauchy : Cauchy Filter.atTop

theorem idIsCauchy' : CauchySeq id

We find the same result about the identity map found in idIsCauchy, without using any metric structure.