continuity of `coe_fn : C(α, β) → (α → β)`

Stream: Is there code for X?

[Eric Wieser]

Do we have a way to prove the following sorry? Is it even true, or is docs#continuous_map.compact_open sufficently different from docs#Pi.topological_space for it not to be?

def coe_fn_continuous_map {α β : Type*} [topological_space α] [topological_space β] :
  C(C(α, β), α → β) :=
⟨coe_fn, sorry⟩

[Kevin Buzzard]

There is more than one way to put a topology on the type of continuous functions between two topological spaces -- I am quite surprised that compact_open is an instance. If one is doing duals of topological vector spaces this might not be the topology one wants.

[Kevin Buzzard]

I think this map is continuous. Here's an attempt at a mathematical proof. A basis for the Pi.topological_space topology on alpha -> beta is indexed by pairs (a,U) with a : alpha and U in beta an open set, the corresponding open set of functions being the f such that f(a) is an element of U. It suffices to prove that the preimage of this basis element is open in the compact open topology. However a singleton {a} is compact, so in fact the preimage of (a,U) is one of the generators for the compact open topology.

[Kevin Buzzard]

Hmm, if one is doing duals of topological vector spaces then one will be looking at continuous linear maps, not continuous maps, so as long as there are not enough instances available to force the subspace topology on you, it should be OK.