Evaluation of continuous functions is continuous

Stream: maths

[Eric Wieser]

Is there a generalization that unifies the typeclass assumptions of docs#continuous_map.continuous_ev and docs#continuous_map.continuous_eval?

[Anatole Dedecker]

Isn’t the first one strictly stronger than the second one ?

[Eric Wieser]

If it is then mathlib doesn't know

[Eric Wieser]

Apparently compact spaces are not always locally compact (https://math.stackexchange.com/q/1632637/1896)

[Eric Wieser]

Indeed, docs#locally_compact_of_compact says they're only locally compact in the presence of docs#t2_space, which seems to match that question

[Anatole Dedecker]

Yes I just realized that

[Eric Wieser]

Although it does seem strange that the former wouldn't cover the latter, given the docstring for docs#locally_compact_space:

There are various definitions of "locally compact space" in the literature, which agree for
Hausdorff spaces but not in general. This one is the precise condition on X needed for the
evaluation map C(X, Y) × X → Y to be continuous for all Y when C(X, Y) is given the
compact-open topology.

[Eric Wieser]

Is C(X, Y) getting a different topology in the two statements?

[Anatole Dedecker]

Then the question becomes : is the metric_space assumption in the compact case really necessary

[Eric Wieser]

I'm very out of my depth here; so for now I've just PR'd #12738 which makes the duplication obvious in the docstrings

[Reid Barton]

These are good questions. I would be prepared to believe that if X is compact but not Hausdorff, then since maps into a Hausdorff space (e.g. metric space) Y factor through the maximal Hausdorff quotient X -> X' of X, then maybe the induced map C(X', Y) -> C(X, Y) is a homeomorphism--though it's not obvious to me. Here I'm always giving C(-, -) the compact-open topology. If this is right then it would explain why there are these two theorems with conclusions of the same form.

Math-wise there is another question of whether the compact-open topology on C(X, Y) is the same as something coming from a metric when X is compact and Y a metric space. Based on a brief inspection, it looks like mathlib knows this is the case, but I don't have time to look at it further--I vaguely recall @Oliver Nash proving some statement like this, maybe this one?

[Reid Barton]

OK now I think that what I said in the first paragraph probably is in fact easy (compact subsets of X' are sufficiently closely related to compact subsets of X to see that the topologies are the same).

[Reid Barton]

Eric Wieser said:

Is C(X, Y) getting a different topology in the two statements?

This is also a good question--I hope the answer is yes

[Eric Wieser]

This is also a good question--I hope the answer is yes

I somewhat hope the answer is no, because otherwise there's probably a diamond at play here and we need some type aliases.

[Anatole Dedecker]

No it is the same topology (provably, but I think it has been setup carefully so it is definitional). Compact open topology is a generalization of the usual uniform convergence topology

[Reid Barton]

Oh whoops you said "different"! I meant I hope it has the same topology.

[Oliver Nash]

Reid Barton said:

Based on a brief inspection, it looks like mathlib knows this is the case, but I don't have time to look at it further--I vaguely recall Oliver Nash proving some statement like this, maybe this one?

Yes, that's right. For the sake of definiteness, the following works:

import topology.continuous_function.compact

example (X Y : Type*) [topological_space X] [compact_space X] [metric_space Y] :
  metric_space.to_uniform_space'.to_topological_space = @continuous_map.compact_open X Y _ _ :=
rfl

[Oliver Nash]

The actual math content is expressed in docs#continuous_map.compact_open_eq_compact_convergence and IIRC it was @Heather Macbeth who hooked this up to docs#continuous_map.metric_space

[Eric Wieser]

This one is the precise condition on X needed for the
evaluation map C(X, Y) × X → Y to be continuous for all Y when C(X, Y) is given the
compact-open topology.

Perhaps the way to understand this quote from the docs in the context of this topic is "in docs#continuous_map.continuous_eval we know more about Y so can get away with weaker assumptions on X".

[Eric Wieser]

The reason I started this topic is that I wonder which of the two lemmas #11261 should be using