done

Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean

@@ -18,42 +18,43 @@ topology on a space. In this file we are concerned in particular with the *discr
 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`).
 
-We begin by defining a metric on `ℕ` (see `dist_def`) that
-1. Induces the discrete topology, as proven in `TopIsDiscrete`;
-1. Is not the discrete metric, in particular because the identity is a Cauchy sequence, as proven
-in `idIsCauchy`
-
 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.
+general, along the lines of the above discussion. We explicitely produce a metric and a uniform
+structure on a space (on `ℕ`, actually) that are not discrete, yet induce the discrete topology.
 
-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 the principal filter `𝓟 {x}` (see `Filter.principal`) and for some `x : α`. This is
-the declaration `UniformSpace.DiscreteUnif.eq_const_of_cauchy` in Mathlib.
+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
 implicitely endowing `ℕ` with the metric inherited from `ℝ`, that induces the discrete uniformity
-on `ℕ`: on the other hand, the geometric intuition might suggest that a Cauchy sequence, whose
+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.
-
-## The question and the counterexample
-It is natural to wonder whether the assumption of `UniformSpace.DiscreteUnif.eq_const_of_cauchy`
-that the uniformity is discrete can be relaxed to assume that the *topology* is discrete. In other
-terms, is it true that every Cauchy sequence in a uniform space whose topology is discrete is
-eventually constant? In the language of filters: is it true that every Cauchy filter `ℱ` in a
-uniform space `α` whose induced topology `UniformSpace.toTopologicalSpace` is discrete, is of the
-form `ℱ = 𝓟 {x}` for some `x : α`?
-
-The goal of this file is to show that the answer is "no", by providing a counterexample. We
-construct a uniform structure on `ℕ`, showing that it induces the discrete topology on `ℕ` but
-such that the filter `Filter.atTop` (that can be of the form `𝓟 {x}` only when `x` is a top
-element, which is not the case if `α = ℕ`) is Cauchy. In particular, the identity sequence
-`fun x ↦ x : ℕ → ℕ` is a Cauchy sequence valued in the discrete topological space `ℕ`.
-
-## The construction of the uniformity
+*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, explicitely 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 set-point 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
@@ -72,7 +73,7 @@ This induces the discrete topology, as proven in `TopIsDiscrete` and the `atTop`
 
 ## 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`.
+inequality) to explicit subsets, many proofs are easily closed by `aesop` or `omega` or `linarith`.
 
 ### References
 * [N. Bourbaki, *General Topology*, Chapter II][bourbaki1966]