Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: definition of "path" and principle of equivalence

David Egolf (May 06 2023 at 17:58):

I learned a little about the principle of equivalence recently, and in that context I was thinking about the definition of a path. I'm hoping to understand better, through this example, when picking a specific object among isomorphic objects is fine, and when we'd prefer to not make such a choice.

We might define "a path in $X$" to be a continuous function $f: I \to X$, where $I = [0,1]$ has the usual subspace topology and $X$ is some topological space. Accepting this definition, the following sentence $P(I)$ is a true statement about $I$: "A continuous function from $I$ to $X$ is a path in $X$".

Now, let $J$ be some topological space that is isomorphic (homeomorphic) to $I$ in $\mathsf{Top}$, with $J \neq I$. Using the definition above, the following sentence $P(J)$ about $J$ is false: "A continuous function from $J$ to $X$ is a path in $X$".

So, we have $I \cong J$, but the truth values of $P(I)$ and $P(J)$ are not equal or even isomorphic in some appropriate partially ordered set of truth values. Does this violate the principle of equivalence?

Motivated by this, I am wondering if it would be more in the spirit of the principle of equivalence to define "a path in $X$" like this: a path in $X$ is a continuous function $f: J \to X$, where $J$ is some topological space isomorphic to the unit interval $I$. Is this an approach that people sometimes take?

Any thoughts on these specific questions, or more generally on the topic of selecting a specific object when isomorphic alternatives exist, would be most welcome.

John Baez (May 06 2023 at 23:59):

David Egolf said:

So, we have $I \cong J$, but the truth values of $P(I)$ and $P(J)$ are not equal or even isomorphic in some appropriate partially ordered set of truth values. Does this violate the principle of equivalence?

Yes. More objectively - since "principles" are not the same as mathematical facts, and it's often nice to state facts - we can say that you have defined a map $P$ from the class of topological spaces to the set of truth values, but this does not extend to a functor from the category of topological spaces to the poset of truth values, since it maps isomorphic topological spaces to nonisomorphic topological spaces.

John Baez (May 07 2023 at 00:01):

There are various ways to "fix" this. But the most popular, in math and especially computer science, is simply to avoid talking about this sort of map $P$. What do you plan to do with it, anyway?

John Baez (May 07 2023 at 00:03):

Does anyone ever want to say "If $A$ is a space such that a map from $A$ to any space $X$ is a path in $X$, then..."?

John Baez (May 07 2023 at 00:03):

I never need, or even desire, to say such things.

John Baez (May 07 2023 at 00:04):

After all, this is a long-winded way of saying "If $A = I$, then..."

John Baez (May 07 2023 at 00:05):

So in fact I think we should focus on the statement $A = I$, or for that matter any statement of equality between objects.

John Baez (May 07 2023 at 00:06):

In category-influenced mathematics we avoid such statements when they are used as a [[propositional equality]]. Note this is different from a [[definitional equality]]. For example it's fine to we say

Let $B = [0,1] \times [0,1] \times [0,1]$...

when we want a short name for something.

John Baez (May 07 2023 at 00:13):

David Egolf said:

Motivated by this, I am wondering if it would be more in the spirit of the principle of equivalence to define "a path in $X$" like this: a path in $X$ is a continuous function $f: J \to X$, where $J$ is some topological space isomorphic to the unit interval $I$. Is this an approach that people sometimes take?

This is an interesting idea, but I think if you try using it for something you'll see it's not very useful.

Suppose I have such a path in $X$: that is, a continuous function from some unknown space that is isomorphic to the unit interval to $X$. What can I do with it? Not much!

It's like saying "You have $1,000,000 in some mailbox, somewhere in the universe". Try spending it.

Verity Scheel (May 07 2023 at 00:13):

It depends on what you mean by “is” and $=$. There are a bunch of angles to tackle this question.

For instance, in HoTT, there simply is not any $J$ that is isomorphic to $I$ but is not equal to $I$, since equality and homeomorphism coincide for topological spaces.

Additionally, if you take “is” to mean $=$ in HoTT, the proposition “A continuous function from $I$ to $X$ is a path in $X$” is true for all spaces homeomorphic to $I$ as well. But I generally think that you want definitions to be something stricter than propositional equality (pardon the Type Theory jargon) ...

Neglecting HoTT for a moment, what do we care about in the choice of $I = [0,1]$? I think you would agree that we don't care about the specific numbers: $[-1, 1]$ would work just as well, $[-42, 132.516]$ too. But I think being _merely_ isomorphic is too weak: we do want to be able to work with the endpoints, to say that a path starts at a known point and ends at a known point. If you don't know what the isomorphism is, you cannot say which point is the start and which the end, so I might suggest a tweak to your second definition that makes it remember the end points at least.

You can make my last point more formal by talking about path induction and stuff in HoTT, but I don't want to type out the details at the moment. It's the difference between $\Sigma J, (J = I) \wedge P(J)$ (which is provably equal to $P(I)$) and $\Sigma J, \| J = I \| \wedge P(J)$ (which is not, due to the propositional truncation of the equality).

Verity Scheel (May 07 2023 at 00:39):

If you want “is” to mean a definitional equality, my first comment would be that it's customary to write the thing you are defining on the left: “A path in $X$ is a continuous function from $I$ to $X$”.

From that point of view, it is true that if you define path that way, then other equalities fail to hold definitionally, like “A path in $X$ is a continuous function from $[-42, 132.516]$ to $X$” fails to hold, since $I$ is not definitionally equal to $[-42, 132.516]$.

But that is at the meta-theoretic level: within the logic you are working in, you cannot observe a “lack of definitional equality”. It just doesn't make sense to ask that. (Such as for the reason that we know that definitional equality is an under-approximation of equality in the theory.) This is the difference between “judgment” and “proposition”, where that distinction makes sense. Propositions can be negated, judgments cannot (except at a meta-theoretic level).

David Egolf (May 07 2023 at 00:59):

John Baez said:

David Egolf said:

Motivated by this, I am wondering if it would be more in the spirit of the principle of equivalence to define "a path in $X$" like this: a path in $X$ is a continuous function $f: J \to X$, where $J$ is some topological space isomorphic to the unit interval $I$. Is this an approach that people sometimes take?

This is an interesting idea, but I think if you try using it for something you'll see it's not very useful.

Suppose I have such a path in $X$: that is, a continuous function from some unknown space that is isomorphic to the unit interval to $X$. What can I do with it? Not much!

It's like saying "You have $1,000,000 in some mailbox, somewhere in the universe". Try spending it.

Maybe I didn't say it right, but I think what I wanted to say was this: To specify a path in $X$ according to my proposed definition, you must specify a space $J$ and a continuous function $f: J \to X$, where $J$ is isomorphic to $I$. One way to specify $J$ could be by providing an isomorphism to it from $I$. (But the idea is that you don't have to pick $J=I$, you can pick a $J$ different from $I$ as long as it is isomorphic to $I$).

Hmmm. This is tricky to think about. I suppose we talk about an arbitrary path $f: I \to X$ without actually specifying $f$. Maybe I shouldn't be asking for specification of the $f: J \to X$, but only require a specification of $J$? I don't feel like I have a clear way of thinking about this kind of thing yet.

Verity Scheel also brings up the good point that we want to be able to talk about the "endpoints" of $J$. I'd have to think about ways to manage that. If we require a specified isomorphism from $I$ to $J$, that could provide a way to talk about endpoints, for example.

David Egolf (May 07 2023 at 01:07):

And thank-you both for sharing the concepts of "propositional equality" and "definitional" equality". Those seem like interesting and important concepts to absorb!

David Egolf (May 07 2023 at 01:13):

I also wonder if it could be interesting to define a path in $X$ as an isomorphism class of continuous maps to $X$, such that the isomorphism class contains a continuous map from $I$ to $X$. (Drawing inspiration from the definition of subobject). Although I'm not sure how to evaluate if this is "better" than the above proposed definition.

Verity Scheel (May 07 2023 at 01:14):

I think if you don't have the isomorphism specified between $I$ and your $J$ specified, you can still work with some topological notions like path-connected (where the specific path and even the choice of endpoints does not matter), but not other uses of paths.

Verity Scheel (May 07 2023 at 01:38):

Also, I'm pretty sure that in set-theoretic foundations, if you specify both your space $J$ and the isomorphism between $J$ and $I$ you get way too much data in there. Why would your usage of the path care about the particular topological space the path uses? (HoTT solves this, via path induction, but maybe you don't want to commit to that as a foundation, and I'm not sure how it could be handled in set theory exactly.)

David Egolf (May 07 2023 at 01:46):

Verity Scheel said:

Also, I'm pretty sure that in set-theoretic foundations, if you specify both your space $J$ and the isomorphism between $J$ and $I$ you get way too much data in there. Why would your usage of the path care about the particular topological space the path uses? (HoTT solves this, via path induction, but maybe you don't want to commit to that as a foundation, and I'm not sure how it could be handled in set theory exactly.)

I'm trying to understand what you are saying. Is the idea that we could pick $J$, or pick $J'$, and - as long as both are given with a specified isomorphism to $I$ - we should be able to work with the resulting path just as well? If that is so, it does seem undesirable to have this additional data of specifying a specific $J$ as our choice of space the path is mapping from.

If we instead define a path in $X$ to be an isomorphism class of continuous functions to $X$ - so we specify one continuous function from each $J$ isomorphic to $I$ - maybe we can avoid singling out a particular $J$ in this way.

Regarding homotopy type theory, it always intrigues me whenever it comes up, but it sounds like a lot of work to learn!

Verity Scheel (May 07 2023 at 02:27):

Yeah, I guess the right kind of quotient could work, but you need to be more careful about how you state it.

Verity Scheel (May 07 2023 at 02:27):

And at the end of the day, your isomorphism class is going to have a canonical representative, namely the standard definition of paths.

Verity Scheel (May 07 2023 at 16:33):

Returning to this:

Fix a topological space $X$. Consider the set of triples $(J, h, p)$ where $J$ is a topological space, $h : I \cong J$ is a specified homeomorphism between $J$ and $I$, and $p : J \to X$ is a continuous function from $J$ to $X$.

If you want to recover something that is equivalent to the usual definition of path you can do this: Define an equivalence relation on this set by $(J_1, h_1, p_1) \sim (J_2, h_2, p_2)$ iff $p_1 \circ h_1 = p_2 \circ h_2$. This is quite literally saying that the only thing that matters is the view of these paths via the usual definition $I \to X$.

You can have finer or coarser equivalence relations as well.

David Egolf (May 07 2023 at 16:40):

That makes sense! I think that condition implies that $(J_1, h_1, p_1)$ and $(J_2, h_2, p_2)$ both induce the same continuous function from $I$ to $X$. So, it sounds reasonable to me to intuitively view them as essentially describing the same path.

It's interesting to note how this situation is different from the definition of a subobject in terms of equivalence classes. I hadn't fully appreciated that for each $J$ we don't just have a morphism from $J$ to $X$; we have a morphism from $J$ to $X$ together with a specified isomorphism from $I$ to $J$, and that makes things a bit different. Thanks for helping to clarify that!

Mike Shulman (May 08 2023 at 04:40):

One nice thing about allowing different isomorphs of $[0,1]$ is that you can sometimes get stricter behavior. For instance, a Moore path in $X$ is a continuous map $[0,r] \to X$ for some real number $r\ge 0$. Then if $p:[0,r] \to X$ and $q:[0,s] \to X$ are Moore paths with $p(r) = q(0)$, we define their concatenation $t:[0,r+s] \to X$ by $t(x)=p(x)$ if $x\le r$ and $t(x) = q(x-r)$ if $x\ge r$. This concatenation operation is then strictly associative and unital, with units being 0-length constant paths $[0,0] \to X$.

Morgan Rogers (he/him) (May 08 2023 at 07:28):

Mike Shulman said:

This concatenation operation is then strictly associative and unital, with units being 0-length constant paths $[0,0] \to X$.

Hang on, $[0,0]$ isn't isomorphic to $[0,1]$! So a Moore path is a smidge more general than the definition @David Egolf suggested.

Mike Shulman (May 08 2023 at 13:47):

Hah, yes, that's true. But you still get a strictly associative composition if you leave that one out.

Mike Shulman (May 08 2023 at 14:49):

You may also be interested in https://mathoverflow.net/q/92206/49.