homotopy - naming collision

Stream: maths

[Shing Tak Lam]

In #8947 I have defined a homotopy between functions, and I've called it homotopy. But the linter is not happy, since there is already docs#homotopy in the root namespace. So one of these will need to be renamed, but I'm not really sure which (if either) should be in the root namespace.

[Alex J. Best]

I'd vote for the more basic notion (the topological one) being called homotopy and the other one be renamed to something like chain_homotopy or namespaced?

[Johan Commelin]

I think @Scott Morrison once gave a reason why he liked the idea of keeping the current _root_.homotopy as it is. I don't remember what or where he wrote... :see_no_evil:

[Adam Topaz]

We really just need to have a general context (e.g. model categories) in which both of these are special cases...

[Scott Morrison]

I don't seem to have a strong opinion either way any more! :-)

In some sense both notions get packaged into the machinery not that long after they are introduced: there aren't a huge number of occasions where one explicitly constructs from scratch or even refers to individual homotopies. Instead you pass to working with equivalence classes, or ways of knowing homotopies do or don't exist without talking about individual ones. So in that sense it doesn't matter much if either or both are namespaces or renamed to something longer.

If we only want to rename one, I would think about how often one needs to refer to them, after the basic undergraduate material on each has been developed.

[Johan Commelin]

In topology we'll need several notions, right? path.homotopy, continuous_function.homotopy, etc...? So it might make sense to namespace those from the beginning.

[Yury G. Kudryashov]

Should we have a homotopy for continuous maps with "frozen sets" and get other cases from this definition?

[Yury G. Kudryashov]

No, sometimes we might need something else.

[Yury G. Kudryashov]

(e.g., homotopy inside the class of smooth maps)

[Johan Commelin]

@Yury G. Kudryashov what exactly did you mean with "frozen sets"?

[Yury G. Kudryashov]

I meant something like (untested)

structure homotopy (f g : X → Y) (s : set X) :=
(to_fun : X × Icc 0 1 → Y)
(cont' : continuous to_fun)
(val_0 : ∀ x, to_fun (x, 0) = f x)
(val_1 : ∀ x, to_fun (x, 1) = g x)
(val_s : ∀ (x ∈ s) t, to_fun (x, t) = f x)

[Yury G. Kudryashov]

This way homotopy between two paths is a homotopy with s = {0, 1}.

[Yury G. Kudryashov]

And free homotopy is a homotopy with s = empty.

[Yury G. Kudryashov]

I'm not sure that this will help, because we, e.g., include endpoints into the type signature of a path.

[Yury G. Kudryashov]

(deleted)

[Johan Commelin]

@Yury G. Kudryashov That's https://github.com/leanprover-community/mathlib/pull/9252/files#diff-b71ec57735e04e7b2087c1be08ab7c9e08cd841a1b77ac133c4bfe6699519b8aR193-R198

[Johan Commelin]

It's an open PR

[Yury G. Kudryashov]

/me should read defs from PR in question before writing comments.

[Reid Barton]

Homotopy rel s really has a key role in the whole theory--I wouldn't be surprised if you could prove somehow that you can't do homotopy theory without it.
Things like homotopy through smooth maps can be built on top of homotopy, since you have access to the to_fun. At worst, you would need to prove things again like the composition of homotopies through smooth maps is a homotopy through smooth maps. We could prove this in "unbundled form", i.e. say what it means for a homotopy to be "through maps of type P : C(X, Y) -> Prop" and show that this is preserved by refl (if the original map is of type P), symm, trans.

[Reid Barton]

Isotopy is another example.

[Reid Barton]

I guess if you want to talk about isotopies then you will want isotopy := homotopy_with function.injective and then you will want to copy over isotopy.symm, isotopy.trans to the new types anyways, so it doesn't matter whether they were actually bundled for you already. So maybe keeping them unbundled to start is more flexible.

[Shing Tak Lam]

Reid Barton said:

Homotopy rel s really has a key role in the whole theory--I wouldn't be surprised if you could prove somehow that you can't do homotopy theory without it.
Things like homotopy through smooth maps can be built on top of homotopy, since you have access to the to_fun. At worst, you would need to prove things again like the composition of homotopies through smooth maps is a homotopy through smooth maps. We could prove this in "unbundled form", i.e. say what it means for a homotopy to be "through maps of type P : C(X, Y) -> Prop" and show that this is preserved by refl (if the original map is of type P), symm, trans.

Yeah, this is my question in the PR (#9252), which is whether it makes sense to have consider P : C(X, Y) -> Prop and then have homotopy_rel be defined in terms of this. This is what is done in HOL-Analysis, and what I have previously used, since we can get homotopy_rel by using an appropriate P.

[Reid Barton]

I don't see how it makes much difference either way.

[Johan Commelin]

@Shing Tak Lam @Reid Barton The P : C(X, Y) -> Prop version is strictly more general than the "usual" homotopy rel definition, right? So I think it is a good idea to develop the basic API in that generality.

[Johan Commelin]

@Shing Tak Lam Do you want to refactor to use that approach?

[Shing Tak Lam]

Yeah, I have a lot of code already written in that generality in a different repo. Would it make sense for this version to extends homotopy, or would it make more sense to redefine homotopy in terms of this with P f = true?

[Johan Commelin]

Hmm... there are pros and cons to both directions, right?

[Johan Commelin]

If homotopy is defined using P f = true, does that cause much annoyance?

[Yaël Dillies]

You probably will just need a few more trivial

[Shing Tak Lam]

Yeah pretty much, it's just some \lambda f, trivials. Since I have code already written with homotopy f g := homotopy_with f g (\lambda f, true), I might just PR it like that, and then see if this causes any issues later, since a refactor to change it from one to the other shouldn't be too bad.

[Shing Tak Lam]

Alright done, I've just changed #9252 instead of making a new PR, since this basically replaces all of the content there anyways

[Johan Commelin]

@Shing Tak Lam Thanks a lot! I left some comments.