splitting function space topologies

[zstone1]

Motivation for this change

Three important changes here.

1. The topology.v file is huge, and kinda unpleasant for development. This splits all the function space topology stuff into a separate file. Note that prod_topology (not U * V, but forall i : U, K i is a function space. So all that stuff, including tychonoff's theorem, lives in function_spaces.v.
2. This removes the canonical topology on ->. It's a bit arbitrary to choose the topology of uniform convergence, and it was causing other bugs. Assigning topologies to aliases of -> like compact-open had to be done in modules to avoid some HB errors. This cleans all that up. It also introduces ArrowAsX modules that can locally assign a canonical topology to ->.
3. I also removed pointwise_fun, which was a layer of indirection that I believe is no longer serving a purpose. It was an alias for prod_topology (fun (_:U) => V). But should have all the same canonicals. Seems better to just use the dedicated notation {ptws, U -> V}.

A few other notes.

• The typeclass inference is slightly weaker outside topology.v. I've marked a couple places where I had to manually introduce a Filter F into the context. Not a big deal, but a little surprising. All the instances are Global, so I can't tell why the inference would be different. I don't consider this blocking, as it's a very minor inconvenience.
• I'm very grateful for the changelog tools. This was have been really annoying otherwise.
• I wrote up some documentation in function_spaces. And I think correctly removed references to function spaces from topology.v. Probably worth a quick scan to double check.

Checklist

• [x] added corresponding entries in CHANGELOG_UNRELEASED.md

• [x] added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

I made a first pass. A few things (doc) were not moved, a few removed things were not documented in the changelog, and I formatted a bit the documentation and suppressed a couple of parentheses here and there. I left a few comments mostly documentation that we'd better address now. Yet, a very welcome PR!

[affeldt-aist]

As a last check I mostly checked the doc for typos. It just needs a rebase before being merged I think.

[affeldt-aist]

I added two NBs and force-pushed to merge asap.