Alright, I'm finally getting somewhere with the theory of paths. I have a small HB hierarchy for defining paths and loops. I have a proof that path connectnedness is an equivalence relation. Still lots of polish work to do (linting, shortening the proofs, fixing notations) but I think the idea is on the right track. If you all have a chance to review, I'd appreciate it. Thanks!
I'm just learning the HB stuff, as well as the quotient stuff. So let me know if there are better ways to use these libraries.
So I've got a draft on my local branch of homotopies that defines reparametrization, proves it's an equivalence relation, and defines paths as a quotient space, Path
. I've also proved that the initial/final points are pimorphims of this quotient. However I'd like to define some mixins that control endpoints, like "IsLoop", "IsPathFrom x" , and "IsPathTo y". However, defining those mixins gives
HB: coercion not to Sortclass or Funclass not supported yet.
Which is an accurate error, because I'm trying to define HB mixins for points in Path
. In my previous attempt, paths were actually functions, so this didn't come up before. I'm not totally blocked on this, as I can do it without HB. A few questions though:
1: Is there a way around this error?
2: Do you plan on expanding HB to support this case?
3: Is there any timeline for this?
Zachary Stone said:
HB: coercion not to Sortclass or Funclass not supported yet.
2: Do you plan on expanding HB to support this case?
3: Is there any timeline for this?
The master
branch of HB got extended last month: https://github.com/mathcomp/hierarchybuilder/pull/311
Oh right, we should release then...
@Enrico Tassi should we?
fine, but the fix we talk about here seems to already be in 1.3.0
It's not... the release was in July and the PR from @Pierre Roux is from August.
Excellent, that's good news for me. I would definitely benefit from a release, then.
So... Cyril made the very reasonable request to define paths as a quotient for the homotopy work to yield improved algebraic properties. Turns out there's a wrinkle I did not anticipate. Best way to explain the problem is with a picture:
Finest quotients
 No Quotient: `{continuous [0,1] >> R}` : No identities, no associativity, no inverses

 Quotient by _injective_ reparametrization : only associativity

 Quotient by _monotonic_ reparametrization : identities + assocativity

 Quotient by homotopy : identities + associativity + inverses.
V
Coarsest Quotients
Doing _injective_ reparametrization is mostly straightforward, I have it mostly done. However, constant paths are _not_ the identity, which is not great. Doing things by monotonic reparametrization looks like the best choice... except that the proof of transitivity seems quite difficult. I have found only one paper that even talks about it from 2007. Almost every other source jumps straight to homotopy equivalence.
Unless someone else knows a proof, I'll probably stick with "injective" paths definition. Then I can define path components. Then I can define "f is homotopy equivalent to g" as "f and g are in the same path component of {continuous A >> B}
with the right topology (turns out compact convergence is the right one).
I've finally untangled all the homotopy stuff. It now has a suitable definition of paths (a quotient of injective reparameterizations). The proofs are antielegant, especially around piecewise definitions for linking paths. But QED is QED. Please take a look when you have a minute, I'd love to get another round of feedback on this.
Last updated: Jan 30 2023 at 11:03 UTC