Draft: Paths

[zstone1]

Motivation for this change

Paths and loops are a critical feature of complex analysis. So we get started here with some basic definitions. Note this is still in draft stage: The linting is terrible, docs are missing, and notations are wrong. But the approach should hopefully be in the right direction.

The main result here is that "reparametrization" is an equivalence relation, and all the relevant features of paths are preserved by the quotient. Lots of details happening here.

1. I introduce some basic HB structures for continuity. Obviously these don't belong in this file long term. But for now they can live here while I work (and while the other major refactoring are happening the code).
2. I introduce an HB structure for a "parametrization of [0,1]". I prove that the injective parametrizations induce an equivalence relation. It turns out that "monotonic increasing" parametrizations also induce an equivalence relation that is way more useful (because constant loops form an actual identity element). But the only proof is too difficult to deal with for now.
3. A large amount of work proves that split_domain actually lets us link paths together. There's a ton of grueling interval arithmetic to do here.
4. I build a quotient of R -> T by "injective reparametrization" equivalence class. This part is easy, thanks to the existing quotient constructions
5. I prove a bunch of operators are compatible with the quotient: initial and final points, reversing paths, image of the path, linking paths, and continuity of paths.
6. I define a hierarchy of paths with explicit endpoints.

The next steps will be

• Provide some builders for making paths from functions [0,1] -> T
• proving path linking is associative (another grueling proof about intervals)
• proving path connectedness is an equivalence relation (just needs linking)
• Defining the f g : X -> Y are homotopic if they are "in the same path component of X->Y"
• Define the fundamental group as the quotient of {Loop in B at x} by path-components.

Note the topology of X->Y ought to be "the compact-open topology". But if Y is a uniform space, this is equivalent to compact-convergence. So I'll probably just start with that assumption, and then generalize later.

@CohenCyril, please let me know if this is closer to what you had intended.

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md
  (do not edit former entries, only append new ones, be careful:
  merge and rebase have a tendency to mess up CHANGELOG_UNRELEASED.md)
• added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[zstone1]

Closing in favor of a much nicer approach in #1350