Metrisability of compact-open topology

Stream: maths

[Oliver Nash]

Here's a basic fact that I believe we have yet to teach Mathlib.

If X is a compact topological space and Y is a metric space then the compact-open topology on C(X, Y) is metrisable with distance function dist f g = supr (λ x, dist (f x) (g x)).

[Oliver Nash]

We do have the compact-open topology docs#continuous_map.compact_open, (which arguably should be a def rather than an instance) and we do have the metric space structure docs#continuous_map.metric_space, but I believe we do not have this result.

[Oliver Nash]

I may want this result in the near future so I want to check I understand how to formalise it in such a way that the topology induced from the metric space structure is defeq to the compact-open topology. In other words, I'd like the following to work:

import topology.continuous_function.compact
import topology.compact_open

variables (X Y : Type*) [topological_space X] [compact_space X] [metric_space Y]

example : (continuous_map.compact_open : topological_space C(X, Y)) =
          metric_space.to_uniform_space'.to_topological_space := rfl -- Fails

[Oliver Nash]

Looking at the definition of docs#pseudo_metric_space, I see its constructor cleverly contains a redundant argument to_uniform_space which allows you to specify the topology manually and then I suppose uniformity_dist becomes the actual mathematical fact about metrisability. I think I recall watching a talk about this being invented to make the topology on the product of metrics spaces defeq to the product topology.

Have I got that right?

[Oliver Nash]

(In fact the situation is slightly more complicated because of the fact that we define the metric space structure on C(X, Y) via the bounded continuous functions but this is an independent complication.)

[Patrick Massot]

docs#continuous_map.metric_space assumes the target is a normed group

[Patrick Massot]

Otherwise you got the picture mostly right, except there are actually three layers, not two: metric, uniform structure, topology.

[Oliver Nash]

Patrick Massot said:

docs#continuous_map.metric_space assumes the target is a normed group

Ha, I thought #8717 would land before anyone read this. I think we're minutes away from what I said being literally true.

[Oliver Nash]

Patrick Massot said:

Otherwise you got the picture mostly right, except there are actually three layers, not two: metric, uniform structure, topology.

Right, thanks. I am aware that there is a uniform structure sitting in between the topology and metric space structures and was ignoring it to simplify but of course, it does matter. Thanks for highlighting it.

[Patrick Massot]

It seems we don't really have a nice API to do that, but you can still wrestle through it to get to the crucial point (which is left as an exercise of course):

import topology.continuous_function.compact
import topology.compact_open

noncomputable theory

open continuous_map filter set
open_locale filter

variables (X Y : Type*) [topological_space X] [compact_space X] [metric_space Y]

/- the following function is extacted from `uniform_space_of_dist` -/

def uniform_space.core_of_dist {α : Type*} (dist : α → α → ℝ)
  (dist_self : ∀ x : α, dist x x = 0)
  (dist_comm : ∀ x y : α, dist x y = dist y x)
  (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z) : uniform_space.core α :=
{ uniformity := (⨅ ε>0, 𝓟 {p:α×α | dist p.1 p.2 < ε}),
  refl       := le_infi $ assume ε, le_infi $
    by simp [set.subset_def, id_rel, dist_self, (>)] {contextual := tt},
  comp       := le_infi $ assume ε, le_infi $ assume h, lift'_le
    (mem_infi_of_mem (ε / 2) $ mem_infi_of_mem (div_pos h zero_lt_two) (subset.refl _)) $
    have ∀ (a b c : α), dist a c < ε / 2 → dist c b < ε / 2 → dist a b < ε,
      from assume a b c hac hcb,
      calc dist a b ≤ dist a c + dist c b : dist_triangle _ _ _
        ... < ε / 2 + ε / 2 : add_lt_add hac hcb
        ... = ε : by rw [div_add_div_same, add_self_div_two],
    by simpa [comp_rel],
  symm       := tendsto_infi.2 $ assume ε, tendsto_infi.2 $ assume h,
    tendsto_infi' ε $ tendsto_infi' h $ tendsto_principal_principal.2 $ by simp [dist_comm] }

def better_metric : metric_space C(X,Y) :=
{ dist := λ x y, dist (equiv_bounded_of_compact X Y x) (equiv_bounded_of_compact X Y y),
  dist_self := λ x, dist_self _,
  dist_comm := λ x y, dist_comm _ _,
  dist_triangle := λ x y z, dist_triangle _ _  _,
  edist := λ x y, edist (equiv_bounded_of_compact X Y x) (equiv_bounded_of_compact X Y y),
  edist_dist := λ x y, edist_dist _ _,
  to_uniform_space := { is_open_uniformity := begin
      dsimp only [uniform_space.core_of_dist],
      sorry
    end,
    ..uniform_space.core_of_dist dist dist_self dist_comm dist_triangle},
  uniformity_dist := rfl,
  eq_of_dist_eq_zero := begin
    intros x y h,
    exact (equiv_bounded_of_compact X Y).injective (eq_of_dist_eq_zero h)
  end }

example : (continuous_map.compact_open : topological_space C(X, Y)) =
  (@metric_space.to_uniform_space' _ (better_metric X Y).to_pseudo_metric_space).to_topological_space :=
rfl

[Patrick Massot]

Note the @ in the example is only there because mathlib currently has the wrong metric space instance. Once you'll have replace this wrong instance with the better one you'll be able to state the example as you originally did.

[Oliver Nash]

Thank you so much for this!

[Oliver Nash]

My secret reason for originally wanting this was to eliminate this lemma because of docs#continuous_map.continuous_const'

[Patrick Massot]

@Oliver Nash I felt guilty for leaving you in such a mess so I came back and wrote an API:

import topology.continuous_function.compact
import topology.compact_open

noncomputable theory

open continuous_map filter set
open_locale filter

variables (X Y : Type*) [topological_space X] [compact_space X] [metric_space Y]

/- the following function is extacted from `uniform_space_of_dist` -/

def uniform_space.core_of_dist {α : Type*} (dist : α → α → ℝ)
  (dist_self : ∀ x : α, dist x x = 0)
  (dist_comm : ∀ x y : α, dist x y = dist y x)
  (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z) : uniform_space.core α :=
{ uniformity := (⨅ ε>0, 𝓟 {p:α×α | dist p.1 p.2 < ε}),
  refl       := le_infi $ assume ε, le_infi $
    by simp [set.subset_def, id_rel, dist_self, (>)] {contextual := tt},
  comp       := le_infi $ assume ε, le_infi $ assume h, lift'_le
    (mem_infi_of_mem (ε / 2) $ mem_infi_of_mem (div_pos h zero_lt_two) (subset.refl _)) $
    have ∀ (a b c : α), dist a c < ε / 2 → dist c b < ε / 2 → dist a b < ε,
      from assume a b c hac hcb,
      calc dist a b ≤ dist a c + dist c b : dist_triangle _ _ _
        ... < ε / 2 + ε / 2 : add_lt_add hac hcb
        ... = ε : by rw [div_add_div_same, add_self_div_two],
    by simpa [comp_rel],
  symm       := tendsto_infi.2 $ assume ε, tendsto_infi.2 $ assume h,
    tendsto_infi' ε $ tendsto_infi' h $ tendsto_principal_principal.2 $ by simp [dist_comm] }

def pseudo_metric_space.of_metrizable {X : Type*} [topological_space X] (dist : X → X → ℝ)
  (dist_self : ∀ x : X, dist x x = 0)
  (dist_comm : ∀ x y : X, dist x y = dist y x)
  (dist_triangle : ∀ x y z : X, dist x z ≤ dist x y + dist y z)
  (H : ∀ s : set X, is_open s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ y, dist x y < ε → y ∈ s) :
pseudo_metric_space X :=
{ dist := dist,
  dist_self := λ x, dist_self _,
  dist_comm := λ x y, dist_comm _ _,
  dist_triangle := λ x y z, dist_triangle _ _  _,
  to_uniform_space := { is_open_uniformity := begin
    dsimp only [uniform_space.core_of_dist],
    intros s,
    change is_open s ↔ _,
    rw H s,
    apply forall_congr, intro x,
    apply forall_congr, intro x_in,
    erw (has_basis_binfi_principal _ nonempty_Ioi).mem_iff,
    { apply exists_congr, intros ε,
      apply exists_congr, intros ε_pos,
      simp only [prod.forall, set_of_subset_set_of],
      split,
      { rintros h _ y H rfl,
        exact h y H },
      { intros h y hxy,
        exact h _ _ hxy rfl } },
      { exact λ r (hr : 0 < r) p (hp : 0 < p), ⟨min r p, lt_min hr hp,
        λ x (hx : dist _ _ < _), lt_of_lt_of_le hx (min_le_left r p),
        λ x (hx : dist _ _ < _), lt_of_lt_of_le hx (min_le_right r p)⟩ },
      { apply_instance }
    end,
    ..uniform_space.core_of_dist dist dist_self dist_comm dist_triangle },
  uniformity_dist := rfl }


def better_metric : metric_space C(X,Y) :=
{ eq_of_dist_eq_zero := begin
    intros x y h,
    exact (equiv_bounded_of_compact X Y).injective (eq_of_dist_eq_zero h)
  end,
  ..pseudo_metric_space.of_metrizable (λ x y, dist (equiv_bounded_of_compact X Y x)
    (equiv_bounded_of_compact X Y y)) (λ x, dist_self _) (λ x y, dist_comm _ _)
    (λ x y z, dist_triangle _ _ _) begin

      sorry
    end }

example : (continuous_map.compact_open : topological_space C(X, Y)) =
  (@metric_space.to_uniform_space' _ (better_metric X Y).to_pseudo_metric_space).to_topological_space :=
rfl

[Patrick Massot]

Note that the actual content about the compact open topology is still sorry but the goal is no longer a big mess.

[Oliver Nash]

Yes I see that. This is marvellous!

[Patrick Massot]

Now it's independent from the internals of our implementation of uniform and metric spaces.

[Oliver Nash]

Right.

[Oliver Nash]

From a quick scan it looks like uniform_space.core_of_dist and pseudo_metric_space.of_metrizable deserve to be PR'd on their own, right?

[Patrick Massot]

Sure. The first one needs to be put right above docs#uniform_space_of_dist and used there

[Patrick Massot]

I'll PR that right away

[Oliver Nash]

Excellent! I'll resume learning about convexity for now :-)

[Patrick Massot]

#8759

[Oliver Nash]

I returned to this yesterday. Despite the fact that you made it easy to establish the metrisability while ignoring the uniform space structure, I decided I wanted to prove the uniform structure was also compatible (and keep everything defeq).

[Oliver Nash]

I started like this:

import topology.compact_open

open_locale filter uniformity

variables {α β : Type*} [topological_space α] [uniform_space β]

instance : uniform_space C(α, β) :=
{ uniformity := ⨅ (K : set α) (hK : is_compact K) (V ∈ 𝓤 β),
                  𝓟 { p : C(α, β) × C(α, β) | ∀ (x : α), (p.1 x, p.2 x) ∈ V },
  refl := sorry, -- trivial
  symm := sorry, -- trivial
  comp := sorry, -- trivial
  is_open_uniformity := sorry, /- some work needed -/ }

(which hopefully is correct) and then decided the key to is_open_uniformity was a corollary of the Lebesgue number lemma so I've created #8963 .

[Oliver Nash]

I only wanted to give this a day at most so I'm going to pause again and resume in a week or so.

[Heather Macbeth]

Can this uniform space structure be expressed as the Sup or Inf (I'm not sure which way the order goes) of a family of uniform space structures, one for each compact set K in α, which are respectively the pullbacks to C(α, β) from α → β of a uniform space structure on α → β? Maybe the pi-type uniform structure,

def uniform_convergence_on (s : set α) : uniform_space (α → β) :=
uniform_space.of_core (⨅ a ∈ s, uniform_space.comap (λ f : (α → β), f a) _i).to_core

(edit: or on second thoughts maybe some other uniform structure, but the point remains)

[Heather Macbeth]

By definition if one takes K = set.univ this is really the pi uniform space structure.

example :
  (uniform_convergence_on set.univ : uniform_space (α → β)) = Pi.uniform_space (λ a : α, β) :=
rfl

[Heather Macbeth]

Also, is there a theorem somewhere in mathlib relating the compact-open topology to tendsto_locally_uniformly? Something like this, though maybe I'm missing some conditions:

import topology.uniform_space.uniform_convergence
import topology.compact_open

open_locale topological_space

variables {ι α β : Type*} [topological_space α] [uniform_space β]

example (F : ι → C(α, β)) (f : C(α, β)) (p : filter ι) :
  tendsto_locally_uniformly (λ i, F i) f p ↔ filter.tendsto F p (𝓝 f) :=
sorry

[Kevin Buzzard]

[just a comment on the ordering: to turn a poset into a category one turns a<=b into a map a -> b and this is the "philosophy" in general; by which I mean that for two uniform structures U1 and U2 on a type X, it's set up so that U1 <= U2 iff id : (X, U1) -> (X,U2) is continuous. I think this is the logic; it's how I remember the ordering for topological spaces.

import topology.uniform_space.basic

example {α : Type*} {u₁ u₂ : uniform_space α} : u₁ ≤ u₂ ↔ @uniform_continuous α α u₁ u₂ id :=
begin
  rw [uniform_continuous_iff, uniform_space_comap_id],
  refl,
end

]

[Heather Macbeth]

To reframe my main question more succinctly:

• is there a family of topologies uniform_convergence_on K on C(α, β), parametrized by the compact sets K of α, such that the compact-open topology is the infimum of these topologies?
• if so, and if moreover β is a uniform space, does the topology uniform_convergence_on K come from some natural uniform structure?

[Kevin Buzzard]

Dumb questions: does the functor from uniform spaces to topological spaces preserve Infs or Sups? I'm assuming the compact open topology isn't in general coming from a compact open uniformity

[Heather Macbeth]

I have no idea, thinking about uniform spaces makes my head hurt, but I thought that this

Kevin Buzzard said:

the compact open topology ... coming from a compact open uniformity

is what Oliver was doing here.

[Kevin Buzzard]

Aah -- so we are assuming that the target is a uniform space and not just a topological space?

[Heather Macbeth]

I am more interested in the uniform-space-target case. But maybe this part

Heather Macbeth said:

• is there a family of topologies uniform_convergence_on K on C(α, β), parametrized by the compact sets K of α, such that the compact-open topology is the infimum of these topologies?

is true even if the target is just a topological space?

[Kevin Buzzard]

[Another irrelevant point: my understanding is that for general topological spaces the compact open topology isn't quite as nice as one would help, i.e. it doesn't give a good "internal hom" structure on the category of topological spaces (in contrast to the category of abelian groups, where Hom(A,B) is naturally an abelian group and this abelian structure plays well with everything) and this was perhaps one of the things which motivates the study of condensed sets instead.]

[Kevin Buzzard]

[now back at Lean] docs#to_topological_space_Inf says that Infs for uniform spaces and topological spaces agree.

[Kevin Buzzard]

I think it is formally true (i.e. true by definition, at least by Wikipedia's definition) that for K compact in X, if T(K) is the coarsest topology on C(X,Y) such that for all U in Y open, the set of f in C(X,Y) such that f(K) \subseteq U is open, then the compact open topology on C(X,Y) is the topology generated by all of the T(K) as K varies, i.e. the Inf of these topologies in the mathlib sense. The reason is simply that the compact open topology on C(X,Y) is, if my understanding is correct, the coarsest topology (fewest open sets) such that V(K,U) is open for all K compact and U open, where V(K,U) is the f such that f(K) \subseteq U.

[Kevin Buzzard]

Heather Macbeth said:

Also, is there a theorem somewhere in mathlib relating the compact-open topology to tendsto_locally_uniformly? Something like this, though maybe I'm missing some conditions:

import topology.uniform_space.uniform_convergence
import topology.compact_open

open_locale topological_space

variables {ι α β : Type*} [topological_space α] [uniform_space β]

example (F : ι → C(α, β)) (f : C(α, β)) (p : filter ι) :
  tendsto_locally_uniformly (λ i, F i) f p ↔ filter.tendsto F p (𝓝 f) :=
sorry

This seems to be pretty much the content of the second paragraph of the Wikipedia page on the compact open topology (and there's also the implicit claim that if beta is not assumed to be a uniform space then this is false -- edit: actually I guess if beta isn't a uniform space the claim doesn't even make sense).

[Heather Macbeth]

Kevin Buzzard said:

This seems to be pretty much the content of the second paragraph of the Wikipedia page on the compact open topology (and there's also the implicit claim that if beta is not assumed to be a uniform space then this is false -- edit: actually I guess if beta isn't a uniform space the claim doesn't even make sense).

But it's not in mathlib -- is that right?

[Oliver Nash]

Correct, this is not in Mathlib. Indeed a regex search for import.*compact_open shows nothing imports topology/compact_open.lean so the only things Mathlib knows about the CO topology are in this file.

[Oliver Nash]

Heather Macbeth said:

I am more interested in the uniform-space-target case. But maybe this part

Heather Macbeth said:

• is there a family of topologies uniform_convergence_on K on C(α, β), parametrized by the compact sets K of α, such that the compact-open topology is the infimum of these topologies?

is true even if the target is just a topological space?

I think I must be parsing this paragraph incorrectly because I cannot make sense of uniform_convergence_on K without assuming β carries a uniform space structure: haven't you defineduniform_convergence_on using uniform_space.comap?

[Oliver Nash]

In any case I can well imagine that once we start developing the CO topology / uniform space structure further, we will find it useful provide these characterisations of them (e.g., the coarsest structure such that property X holds). For now I just want to actually get the definition of the uniform structure on C(α, β) in place (when β is uniform).

[Oliver Nash]

With regard to the connection with Pi types, the compact open topology can be defined on the space of all maps α → β and then CO topology on C(α, β) arises as the subspace topology. Mathematically it seems a bit ridiculous to topologise α → β but I can imagine it __might__ be useful to define the compact open topology on C(α, β) this way because it might allow a bit more flexibility when formalising. (E.g., if we have a subset of maps α → β that are continuous but not definitionally a subset of C(α, β).)

[Oliver Nash]

Anyway, none of the above answers your interesting questions but I claim the first thing to do is to fill in the proof of is_open_uniformity here and I claim the first thing to do for that is to merge #8963

[Oliver Nash]

Depending on how much progress I make with my primary goal this week, I'll try to return to this toward the end of the week.

[Heather Macbeth]

Oliver Nash said:

Mathematically it seems a bit ridiculous to topologise α → β

In fact, it already bears a topology, right? The topology of pointwise convergence, docs#Pi.topological_space. I was fighting against this before in a couple of experiments.

[Heather Macbeth]

Oliver Nash said:

I think I must be parsing this paragraph incorrectly because I cannot make sense of uniform_convergence_on K without assuming β carries a uniform space structure: haven't you defineduniform_convergence_on using uniform_space.comap?

Indeed I had a second idea here, different from the comap stuff, which I didn't write out explicitly. I was wondering if, by analogy with src#compact_open, we could define a family of topologies which I will temporarily call uniform_convergence_on K (but this is a bad name since it doesn't require a uniform structure):

def uniform_convergence_on (s : set α) : topological_space C(α, β) :=
topological_space.generate_from
  {m | ∃ (u : set β) (hu : is_open u), m = compact_open.gen s u}

[Heather Macbeth]

And if, then, it would be true that

example : (continuous_map.compact_open : topological_space C(α, β))
  = ⨅ (s : set α) (hs : is_compact s), uniform_convergence_on β s :=
sorry

[Heather Macbeth]

Kevin Buzzard said:

I think it is formally true (i.e. true by definition, at least by Wikipedia's definition) that for K compact in X, if T(K) is the coarsest topology on C(X,Y) such that for all U in Y open, the set of f in C(X,Y) such that f(K) \subseteq U is open, then the compact open topology on C(X,Y) is the topology generated by all of the T(K) as K varies, i.e. the Inf of these topologies in the mathlib sense

This is effectively defining uniform_convergence_on K as the topology T(K) described here by Kevin.

[Heather Macbeth]

Then, instead of uniformizing compact_open directly, it would suffice for you to uniformize each of the individual topologies uniform_convergence_on K.

[Oliver Nash]

Heather Macbeth said:

And if, then, it would be true that

example : (continuous_map.compact_open : topological_space C(α, β))
  = ⨅ (s : set α) (hs : is_compact s), uniform_convergence_on β s :=
sorry

Right I understand now. Yes, I agree that will probably be useful quite soon once one starts proving things with the compact-open topology.

[Heather Macbeth]

For me, the motivation is that I would like to relate the topology compact_open to the family of pseudo-metric space structures

def sup_metric_on (s : set α) : has_dist C(α, β) :=
⟨λf g, Inf {C | 0 ≤ C ∧ ∀ x ∈ s, dist (f x) (g x) ≤ C}⟩

(pseudo-metric because functions which agree on s are at distance 0 from each other). I was hoping that it would be true that compact_open is the Inf over all compact K of the topologies associated to sup_metric_on.

[Oliver Nash]

If I manage to get to this later in the week, I'll consider this approach.

[Oliver Nash]

Heather Macbeth said:

For me, the motivation is that I would like to relate the topology compact_open to the family of pseudo-metric space structures

def sup_metric_on (s : set α) : has_dist C(α, β) :=
⟨λf g, Inf {C | 0 ≤ C ∧ ∀ x ∈ s, dist (f x) (g x) ≤ C}⟩

Do you want α (or s) to be compact here? Don't you also have the problem that functions which are unboundedly far away from each other will be distance 0 with this definition?

[Heather Macbeth]

You're right, I was thinking s should be compact.

[Oliver Nash]

OK so in that case you essentially want the exact thing that caused me to start this thread, except that you also want the _on version because you have s.

[Oliver Nash]

I mean we have docs#continuous_map.metric_space already and it's metric is (indirectly) what you have defined because it comes from docs#bounded_continuous_function.has_dist

[Heather Macbeth]

Yes! Although I don't care about putting a literal (somewhat arbitrary) metric compatible with the compact-open topology for a general (not necessarily compact) domain, instead I care about connecting it (maybe as the Inf) to a certain family of canonical pseudo-metrics.

[Heather Macbeth]

And indeed, if this all works out, we probably want to refactor docs#continuous_map.metric_space to be a special case of this construction, the case when the whole space α is compact.

[Oliver Nash]

Heather Macbeth said:

And indeed, if this all works out, we probably want to refactor docs#continuous_map.metric_space to be a special case of this construction, the case when the whole space α is compact.

I plan to do this. I don't think it would be hard; it's just prioritised behind a bunch of other stuff. Maybe you'll get there before me ;-)

[Heather Macbeth]

This is all in the service of outlining what should replace @Chris Birkbeck's version of the Weierstrass M-test ... maybe I got a bit distracted :)

[Oliver Nash]

Likewise I was lead here from a distant land. I think I understand your point of view now. I think it's totally achievable and just requires a couple of solid days.

[Chris Birkbeck]

Heather Macbeth said:

This is all in the service of outlining what should replace Chris Birkbeck's version of the Weierstrass M-test ... maybe I got a bit distracted :)

Hmm yes, maybe it's best I wait a bit :)

[Heather Macbeth]

@Oliver Nash I've made #9046, expressing the compact-open topology as an Inf of topologies. The statement looks like

/-- The compact-open topology is equal to the infimum, as `s` varies over the compact subsets of
`α`, of the topologies of uniform convergence on `s`. -/
lemma compact_open_eq_Inf_uniform_on :
  continuous_map.compact_open = ⨅ (s : set α) (hs : is_compact s), uniform_on β s :=

Let me solicit opinions on two points:

• a better name for what I have called uniform on β s, i.e. a certain family of topologies on C(α, β), parametrized by s : set α ... if β is a uniform space and s is compact then this topology should be the topology of uniform convergence on s, but uniform_on seems like a bad name because it doesn't require a uniform structure on β
• should I actually redefine compact_open to this Inf definition, or keep the old definition?

[Heather Macbeth]

Maybe @Reid Barton is the right person to ask.

[Oliver Nash]

Oh wow, thanks @Heather Macbeth , really nice work. I'll comment on the PR and thanks!

[Oliver Nash]

@Heather Macbeth I finally came back to the problem of proving that the topology of compact convergence (when the target is a uniform space) is the same as the compact-open topology.

[Oliver Nash]

Don't celebrate too soon because I'm not done yet but I did get this far:

[Oliver Nash]

import topology.compact_open
import topology.uniform_space.basic

universes u₁ u₂

open_locale filter uniformity topological_space
open uniform_space set

variables {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β]
variables (K : set α) (V : set (β × β)) (f : C(α, β))

/-- A subbase for the topology of compact convergence. -/
def uniform_gen : set C(α, β) := {g | ∀ (x ∈ K), (f x, g x) ∈ V }

/-- The topology of compact convergence. I claim this topology is induced by a uniform structure,
defined below. -/
def compact_convergence_topology : topological_space C(α, β) :=
topological_space.generate_from
  {m | ∃ (K : set α) (hK : is_compact K) (V ∈ 𝓤 β) (f : C(α, β)), m = uniform_gen K V f }

lemma mem_uniform_gen_self (hV : V ∈ 𝓤 β) : f ∈ uniform_gen K V f := λ x hx, refl_mem_uniformity hV

/-- This should be sufficient to show we actually have a neighbourhood basis. -/
lemma uniform_gen_nhd_basis {g₁ g₂ : C(α, β)}
  (h₁ : g₁ ∈ uniform_gen K V f) (h₂ : g₂ ∈ uniform_gen K V g₁) :
  g₂ ∈ uniform_gen K (V ○ V) f :=
λ x hx, ⟨g₁ x, h₁ x hx, h₂ x hx⟩

/-- Any point of `compact_open.gen K U` is also an interior point wrt the topology of compact
convergence.

The topology of compact convergence is thus at least as fine as the compact-open topology. -/
lemma uniform_gen_subset_compact_open (hK : is_compact K) {U : set β} (hU : is_open U)
  (hf : f ∈ continuous_map.compact_open.gen K U) :
  ∃ (V ∈ 𝓤 β), uniform_gen K V f ⊆ continuous_map.compact_open.gen K U :=
begin
  obtain ⟨V, hV₁, hV₂, hV₃⟩ := lebesgue_number_of_compact_open (hK.image f.continuous) hU hf,
  refine ⟨V, hV₁, _⟩,
  rintros g hg - ⟨x, hx, rfl⟩,
  exact hV₃ (f x) ⟨x, hx, rfl⟩ (hg x hx),
end

/-- The point `f` in `uniform_gen K V f` is also an interior point wrt the compact-open topology.

From this it should follow that the compact-open topology is at least as fine as the topology of
compact convergence. -/
lemma Inter_compact_open_gen_subset_uniform_gen (hK : is_compact K) (hV : V ∈ 𝓤 β) :
  ∃ (ι : Sort (u₁ + 1)) [fintype ι]
  (C : ι → set α) (hC : ∀ i, is_compact (C i))
  (U : ι → set β) (hU : ∀ i, is_open (U i)),
  (f ∈ ⋂ i, continuous_map.compact_open.gen (C i) (U i)) ∧
  (⋂ i, continuous_map.compact_open.gen (C i) (U i)) ⊆ uniform_gen K V f :=
begin
  -- Below needs https://github.com/leanprover-community/mathlib/pull/9981
  obtain ⟨W, hW₁, hW₄, hW₂, hW₃⟩ := comp_open_symm_mem_uniformity_sets hV,
  obtain ⟨Z, hZ₁, hZ₄, hZ₂, hZ₃⟩ := comp_open_symm_mem_uniformity_sets hW₁,
  let U : α → set α := λ x, f⁻¹' (ball (f x) Z),
  have hU : ∀ x, is_open (U x) := λ x, f.continuous.is_open_preimage _ (is_open_ball _ hZ₄),
  have hUK : K ⊆ ⋃ (x : K), U (x : K),
  { intros x hx,
    simp only [exists_prop, mem_Union, Union_coe_set, mem_preimage],
    use (⟨x, hx⟩ : K),
    simp [hx, mem_ball_self (f x) hZ₁], },
  obtain ⟨t, ht⟩ := hK.elim_finite_subcover _ (λ (x : K), hU x.val) hUK,
  let C : t → set α := λ i, K ∩ closure (U ((i : K) : α)),
  have hC : K ⊆ ⋃ i, C i,
  { rw [← K.inter_Union, subset_inter_iff],
    refine ⟨rfl.subset, ht.trans _⟩,
    simp only [set_coe.forall, subtype.coe_mk, Union_subset_iff],
    intros x hx₁ hx₂,
    apply subset_subset_Union (⟨_, hx₂⟩ : t),
    simp [subset_closure], },
  have hfC : ∀ (i : t), f '' C i ⊆ ball (f ((i : K) : α)) W,
  { rintros ⟨⟨x, hx₁⟩, hx₂⟩,
    calc f '' (K ∩ closure (U x))
          ⊆ f '' (closure (U x)) : by { mono, simp only [inter_subset_right], }
      ... ⊆ closure (f '' (U x)) : continuous_on.image_closure f.continuous.continuous_on
      ... ⊆ closure (ball (f x) Z) : by { mono, simp, }
      ... ⊆ ball (f x) W : by { intros y hy,
                                obtain ⟨z, hz₁,hz₂⟩ := uniform_space.mem_closure_iff_ball.mp hy hZ₁,
                                rw mem_ball_symmetry hZ₂ at hz₁,
                                exact ball_mono hZ₃ _ (mem_ball_comp hz₂ hz₁), }, },
  refine ⟨t,
          t.fintype_coe_sort,
          C,
          λ i, hK.inter_right is_closed_closure,
          λ i, ball (f ((i : K) : α)) W,
          λ i, is_open_ball _ hW₄,
          by simp [continuous_map.compact_open.gen, hfC, -image_subset_iff],
          _⟩,
  intros g hg x hx,
  apply hW₃,
  replace hx := mem_Union.mp (hC hx),
  obtain ⟨y, hy⟩ := hx,
  rw mem_comp_rel,
  use f y,
  simp only [mem_Inter, continuous_map.compact_open.gen, mem_set_of_eq, image_subset_iff] at hg,
  refine ⟨_, mem_preimage.mp (hg y hy)⟩,
  simp only [image_subset_iff, mem_preimage] at hfC,
  specialize hfC y hy,
  rw [ball_eq_of_symmetry hW₂] at hfC,
  exact hfC,
end

/-- This should follow from the various lemmas above. -/
lemma compact_open_eq_uniform :
  (compact_convergence_topology : topological_space C(α, β)) = continuous_map.compact_open :=
sorry

/-- I believe the topology this induces is `compact_convergence_topology`. -/
instance : uniform_space C(α, β) :=
{ uniformity := ⨅ (K : set α) (hK : is_compact K) (V ∈ 𝓤 β),
                  𝓟 { p : C(α, β) × C(α, β) | ∀ (x : α), (p.1 x, p.2 x) ∈ V },
  refl := sorry, -- trivial
  symm := sorry, -- trivial
  comp := sorry, -- trivial
  is_open_uniformity := sorry, /- Should be easily reduced to `compact_open_eq_uniform` -/ }

[Oliver Nash]

I really want to switch back to sort out another lemma in the Sphere Eversion project now but I think the above takes care of the mathematical content of what we need.

[Oliver Nash]

I'll push this through to the end in a week or two.

[Heather Macbeth]

This is more than you initially planned, right? You were initially going to do just the fact that if α is compact then compact-open is the uniform topology.

[Oliver Nash]

I always planned to do it for any topological space α (not just compact).

[Oliver Nash]

Though I may well have communicated my intentions poorly!

[Heather Macbeth]

Does it, in the end, route through the theorem docs#continuous_map.exists_tendsto_compact_open_iff_forall which I had proved? Or is this theorem now a corollary of your bigger result?

[Heather Macbeth]

(I need to hop on the subway but I'll think more about this later. Thanks for working on this!)

[Oliver Nash]

It does not actually use that result.

[Oliver Nash]

I'm not sure if it would be better if it did but either way I'm glad we have that result.

[Chris Birkbeck]

Hello, I just wanted to follow up on the status of this. If I remember correctly, Heather mentioned that using some of the things here one could show that "on a compact space , the compact-open topology is the same as the topology induced by the sup-norm".

Do we have this result now?

[Oliver Nash]

We don't but we're close. I have it on one of my lists to get back to this but it would be great if someone else took up the baton.

[Oliver Nash]

Part of the reason it is a bit of work is that we want to factor it through the result that when the codomain is a uniform space, the compact open topology is the same as the topology of compact convergence.

[Oliver Nash]

I basically proved this here https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Metrisability.20of.20compact-open.20topology/near/259114393 but some details still need to be filled in.

[Chris Birkbeck]

Ah ok, well I'm happy to try and help removing some sorries. Where can I find the repo for this?

[Oliver Nash]

Great! There's no repo or branch, just the snippet above.

[Oliver Nash]

It's a MWE if you open it against master in Mathlib.

[Oliver Nash]

I do actually have proofs of the sorrys marked trivial but my proofs are so disgusting I didn't censored them.

[Chris Birkbeck]

Ah ok cool. Let me play around with it a bit and see what I can do. I'll need to think about how one goes from this to the sup-norm statement, I expect its easy, but I need to parse all the different things here first :)

[Oliver Nash]

Chris Birkbeck said:

I'll need to think about how one goes from this to the sup-norm statement

Putting aside the issue that the distance is the norm of the difference, this should come down to proving docs#pseudo_metric_space.uniformity_dist

[Oliver Nash]

The setup is all very clever but if you're seeing it for the first time, it might be a bit opaque.

[Chris Birkbeck]

Hmm yeah I've not really been that exposed to this part of the mathlib, so I need to spend some time getting up to speed :)

[Chris Birkbeck]

So I made a start on this and made a draft PR here: #10439. Haven't really got that far yet.

[Oliver Nash]

Thanks for doing this @Chris Birkbeck What you have so far looks like a good start!

[Oliver Nash]

I finally returned to this earlier this week and have removed all sorrys from #10439

[Oliver Nash]

The code needs about a day's work till I have something that I can put out for review but I am at least confident that the definitions are correct in view of:

lemma correct_entourages (X : set (C(α, β) × C(α, β))) :
  X ∈ 𝓤 C(α, β) ↔ ∃ (K : set α) (V : set (β × β)) (hK : is_compact K) (hV : V ∈ 𝓤 β),
    { fg : C(α, β) × C(α, β) | ∀ (x : α), x ∈ K → (fg.1 x, fg.2 x) ∈ V } ⊆ X :=
mem_compact_convergence_uniformity X

lemma correct_topology_even_defeq :
  @uniform_space.to_topological_space C(α, β) _ = continuous_map.compact_open :=
rfl

(here α is a topological_space and β is a uniform_space).

[Oliver Nash]

In summary when α is a topological_space and β is a uniform_space, we'll be able to speak of uniform convergence in the space of continuous maps C(α, β) and furthermore, we'll know that the underlying topology is the compact-open topology.

[Heather Macbeth]

Fantastic!

[Chris Birkbeck]

Awesome!

[Oliver Nash]

I finally have a version of this work ready for review: #10967

[Oliver Nash]

@Chris Birkbeck I accidentally dropped you as a co-author when creating the tidied-up PR. I've just added you back!

[Chris Birkbeck]

Oh don't worry, I really don't think I did much! You did all the work really

[Oliver Nash]

Incidentally the Bourbaki proof of the main result in this PR uses some non-trivial results so that they can say:
image.png

[Oliver Nash]

and I could never see where they use these assumptions in what follows. Now that I've formalised this, I don't think they do use them.

[Kevin Buzzard]

It was to make the arguments fit in their head better

[Patrick Massot]

In the end, is there a lemma where you can say: this is exactly lemma X from Bourbaki except that we removed assumption Y?

[Oliver Nash]

Patrick Massot said:

In the end, is there a lemma where you can say: this is exactly lemma X from Bourbaki except that we removed assumption Y?

Oh dear, I seem to have given the wrong impression; I love beating Bourbaki but that's not what happened here. Bourbaki establish their result in full generality but they do so by reducing to the case where they're looking at maps from a compact space to a Hausdorff space. What I meant in my remark above was that if you look at the proof they then give for the case to which they reduce, I couldn't see where they used the assumptions of compactness and Hausdorffness.

[Oliver Nash]

It's hardly worth all these words but to be precise, I wondered:
(a) am I missing something and they really do need the assumptions of compactness and Hausdorffness?
(b) is it necessary to set things up this way or can one just prove the result directly?

I'm still not sure about (a) because I didn't chase down the precise generality in which they proved the various lemmata that they invoke but I am now absolutely sure about (b) because I have convinced Lean using a direct argument.

[Patrick Massot]

I played a bit with the code in this PR. I feel bad because I'm responsible for some of the mess here. We have a nice API around docs#filter.has_basis, some connection with docs#filter_basis but not connection with docs#topological_space.is_topological_basis. The main issue is probably that we need a parametrized version of docs#topological_space.is_topological_basis (ie an API for talking about maps whose image is a topological basis, probably using also a predicate on the source type as in docs#filter.has_basis). And then we would need a lot of stupid small lemmas. Anyway, I pushed some new branch hinting at how we could use docs#filter.has_basis in that file. I'm not sure it's worth pursuing and I exhausted my time budget. The current state is somehow stuck between two worlds hence features extremely nasty unpacking and packing as in has_basis_nhds_compact_open (note for expert tactic writers: this is really the kind of proof that is driving me crazy).

[Oliver Nash]

Don't feel bad! The very few rough corners around is_topological_basis were more than compensated for by the awesomeness of what is in place. I'll take a look at your branch this afternoon and see if I can easily incorporate its ideas.

[Oliver Nash]

In the end, I didn't get a chance to look at this today but I expect to have time for it tomorrow morning.