Homotopies · math-comp analysis · Zulip Chat Archive

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.

Zachary Stone (Sep 26 2022 at 03:56):

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 pi-morphims 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?

Pierre Roux (Sep 26 2022 at 07:22):

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?

Cyril Cohen (Sep 26 2022 at 08:42):

Cyril Cohen (Sep 26 2022 at 08:43):

Enrico Tassi (Sep 26 2022 at 08:48):

Cyril Cohen (Sep 26 2022 at 09:02):

It's not... the release was in July and the PR from @Pierre Roux is from August.

Zachary Stone (Sep 26 2022 at 14:35):

Excellent, that's good news for me. I would definitely benefit from a release, then.

Zachary Stone (Oct 15 2022 at 04:05):

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).

Zachary Stone (Oct 20 2022 at 20:12):

I've finally untangled all the homotopy stuff. It now has a suitable definition of paths (a quotient of injective reparameterizations). The proofs are anti-elegant, 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.

Stream: math-comp analysis

Topic: Homotopies

Zachary Stone (Sep 15 2022 at 14:03):