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: Can it be safe to think of objects in two different categ...

Alex Kreitzberg (Sep 19 2024 at 17:54):

This question was inspired by "Resolving CT typing issues" (https://categorytheory.zulipchat.com/#narrow/stream/229136-theory.3A-category-theory/topic/Resolving.20CT's.20Typing.20Issues)

Broadly I want to work against the "types get in the way" feeling, so I'm trying to ask answerable questions. But if you get what I'm really trying to ask feel free to change the question.

When can we, if ever, think of objects in distinct categories as "About the same thing"?

Say I have a glass cup, I can move it around, rotate it, translate it, look at it in a mirror, generally I can do "rigid transformations. But if I get the glass really hot, now I can deform it, and explore homotopies of the cup. And points on the original cup can be seen as continuously mapped to points on the resulting deformed cup.

I want to relate these two ways of working with the same cup.

Do I model this with a forgetful functor from the category of metric spaces into continuous maps? Do I imagine the cup living in a more complicated category that keeps track of what happens under temperature change? Or to restate that last question, does sameness of objects really only make sense to ask in a category?

There are many categories with Natural numbers as objects (ordinals, matrices, divisibility, etc.), is it dangerous to think of the Natural numbers in these various settings as "the same"?

Alex Kreitzberg (Sep 19 2024 at 18:07):

@John Baez answered essentially this question in the above channel just after I posted this question. I reposted his answer here.

Alex Kreitzberg said:

It's just weird to think of one conceptual object as existing in multiple categories.

Baez said:

No, it's not weird. This is how math works. First, "the sphere" is NOT one conceptual object in any sort of precise sense. There are many spheres:

There's the 'metric space sphere' where we can measure distances between points. In fact there are at least 2 really important metric space spheres: one where we measure distances along the surface of there sphere, and one where we measure distances in the ambient $\mathbb{R}^3$. This sphere has a 3-dimensional Lie group of symmetries.

There's the 'topological space sphere' where we only equip the sphere with a topology, not a metric. This sphere has a huge infinite-dimensional topological group of symmetries.

There's the 'smooth manifold sphere' where we make the sphere into a manifold. This sphere has a infinite-dimensional Frechet Lie group of symmetries, which is huge - but tiny compared to the symmetry group of the topological space sphere.

There's the 'set sphere' where we treat the sphere as a set. This has an even larger symmetry group, of cardinality greater than the continuum, consisting of all permutation of points on the sphere.

There's the 'complex analytic sphere' where we treat the sphere as a complex analytic manifold of complex dimension 1. This has a 6-dimensional real Lie group of symmetries (which is a 3-dimensional complex Lie group).

And so on: you need to separately learn theorems about each of these objects.

Alex Kreitzberg (Sep 19 2024 at 18:13):

As you guessed, all these different objects in different categories are related by functors between those different categories.

Math does not operate solely within one category at a time! Except for very limited tasks, we need to be working with a bunch of categories , and functors between them, and natural transformations between those. When we study 'the sphere' or 'the integers' or 'the real numbers', we are looking at not a single object, but multiple objects, in different categories, that are mapped to each other by functors.

Most mathematicians do this naturally and almost unconsciously, saying things like "the sphere has a 3d real Lie group of symmetries that preserve its metric, but a 3d complex Lie group of symmetries that preserve its complex structure".

One of the jobs of the category theorist is to formalize what's going on here - but not scold the mathematicians who do all this naturally. That would be like scolding a dolphin for not having taken swimming lessons.

Kevin Carlson (Sep 19 2024 at 18:21):

I think this is basically the standard right response mathematically, refusing to agree that “the sphere” is a well-defined concept. But psychologically it clearly is such a concept; I think probably “the sphere” is psychologically an amalgam of various categories in which you habitually picture the sphere.

Madeleine Birchfield (Sep 19 2024 at 18:24):

There was a discussion over the various notions of "the real numbers" in #theory: category theory > One universe as a foundation & friends, and the same things that John Baez said about the spheres also applies here.

Mike Shulman (Sep 19 2024 at 18:30):

One non-psychological reason this question is interesting is when you try to formalize mathematics in a proof assistant. The user will naturally expect to be able to write "$S^2$" or "$\mathbb{R}$" in any of these contexts and have the system realize which is meant. To do that "realizing" people introduce various fairly complicated mechanisms like "typeclass inference" and "canonical structures". I don't think a really perfect solution has emerged yet. Part of the problem is "bundling", e.g. how precisely is the ring structure on $\mathbb{R}$ related to its two underlying monoid structures? Which is similar to asking which functors should be considered "forgetful", and which should be functors or [[displayed categories]].

Alex Kreitzberg (Sep 19 2024 at 19:18):

If the real solution is "actually $S^2$ with no qualifiers really doesn't make sense" then I would love programming tools to make managing this easier and more explicit.

Having to reconcile competing definitions in libraries is one of my least favorite parts about programming.

Madeleine Birchfield (Sep 19 2024 at 19:28):

That's why in proof assistants formulated in dependent type theory, every type $A$ has to be some element of a type universe, $A:U$.

If we are considering $\mathbb{S}^2$ as a set then one would consider the element $\mathbb{S}^2:\mathrm{Set}$, which by definition of $\mathrm{Set}$ is really a pair consisting of a type $\mathbb{S}^2:U$ and an element $p:\mathrm{isSet}(\mathbb{S}^2)$ which says that the equalities in $\mathbb{S}^2$ are propositions.

For $\mathbb{S}^2$ as an metric space, one would consider the element $\mathbb{S}^2:\mathrm{Met}$, which by definition of $\mathrm{Met}$ is really a tuple consisting of a type $\mathbb{S}^2:U$ and additional elements which represent the structure and properties of the metric on $\mathbb{S}^2$.

Alex Kreitzberg (Sep 19 2024 at 19:30):

In that example do $\mathbb{S}^2 : U$ and $\mathbb{S}^2 : Met$ both use the same name $\mathbb{S}^2$ by convention then?

Alex Kreitzberg (Sep 19 2024 at 19:35):

(That's fine if they do, that feature is really interesting, I'm just making sure I understand)

Madeleine Birchfield (Sep 19 2024 at 19:37):

Informally, one would tend to identify $\mathbb{S}^2$ with its underlying type, but I think that in proof assistants they all have to have a different name, because there are multiple possible metric space structures on $\mathbb{S}^2$, such as the discrete metric or the Euclidean metric or etc, and $\mathbb{S}^2$ with the discrete metric is a different element of $\mathrm{Met}$ than $\mathbb{S}^2$ with the Euclidean metric.

Alex Kreitzberg (Sep 19 2024 at 19:39):

That makes sense, thank you

Mike Shulman (Sep 19 2024 at 19:40):

Actually $\rm Set$ and $\rm Met$ are not type universes, as the term is usually used, because their elements are not types simpliciter, but tuples or records that bundle a type with structure on it.

Alex Kreitzberg (Sep 19 2024 at 19:42):

Well there's a hierarchy of types and you have to say where they live on this hierarchy right?

I interpreted that answer as saying that was enough to disambiguate most, or even all, cases.

Mike Shulman (Sep 19 2024 at 19:43):

Everything has to belong to a type, yes. I'm just saying that the phrase "type universe" refers to a type whose elements are just types, rather than a type like Set or Met whose elements are types bundled with other stuff.

Mike Shulman (Sep 19 2024 at 19:43):

Just a terminological point.

Mike Shulman (Sep 19 2024 at 19:45):

The techniques such as typeclass inference and canonical structures that I mentioned are precisely a way to give the "same name" to elements of different types in this desired way. With typeclasses (which I'm more familiar with, and I think are more "modern"), there is one type $S^2$, but you could register an "instance" of this type as a metric space, and another "instance" of this type as a manifold. Then when you write "$S^2$" in a context where a type with a metric space structure is expected, the proof assistant goes to the database of instances and finds the metric space structure on $S^2$ automatically, so you don't need to name it.

Mike Shulman (Sep 19 2024 at 19:46):

Of course this only works if there is a unique or canonical such structure. As Madeleine said, since $S^2$ has multiple metrics, you'd have to either pick one to be the canonical instance and name all the others differently when you want to refer to them, or have no instances and name them all explicitly.

Mike Shulman (Sep 19 2024 at 19:47):

However, another feature of proof assistants that's sometimes underappreciated by mathematicians is that, like any programming language, they have namespace management. So you can have two different $S^2$'s in different libraries, and according to which library you "import" into your code, when you write $S^2$ it might mean different things. So if your paper is going to consistently use only, say, the Euclidean metric on $S^2$, you don't need to worry about multiple names but can just import that library into your namespace.

Alex Kreitzberg (Sep 19 2024 at 19:55):

That makes sense!

I don't really have anything clever to add. In my own Haskell code I think I noticed this naming issue with typeclasses but didn't know if it was essential, or reflected poor theory. It sounds like the issue is essential?

Avoiding typeclasses can make the code twice as long. So I get the pragmatics shouldn't be ignored carelessly. But it's good to know if they "at best" make referencing definitions easier.

John Baez (Sep 19 2024 at 20:04):

Kevin Carlson said:

I think this is basically the standard right response mathematically, refusing to agree that “the sphere” is a well-defined concept.

I wasn't trying to say that - I wasn't trying to talk about "concepts". I was only trying to say that in category theory, we treat 'the sphere' as shorthand for a bunch of pointed categories related by pointed functors - that is, different categories $C_1, C_2, \dots$, containing different objects $c_1 \in C_1, c_2 \in C_2, \dots$, but related by various functors $F: C_i \to C_j$ with $F(c_i) \cong c_j$.

In these terms, the 'concept of the sphere' is the whole diagram of pointed categories.

But elsewhere I said something like this:

Mathematics is like the land, while category theory and other formalisms are like the street systems and artificial boundaries that we impose on the land in an attempt to organize it and make it easy to travel across it. The land came first, and it may outlive the particular roads and boundaries we now use.

John Baez (Sep 19 2024 at 20:06):

The 'concept of the sphere' came long before set theory or category theory. We may someday get a better formalism for mathematics, which comes closer to capturing the concept of the sphere, and how it connects the numerous ways we refine and embellish this concept. Or maybe not!

John Baez (Sep 19 2024 at 20:08):

But my massive digression on the homotopy groups of the sphere and Brunnian braid arose because I find it frustrating to talk about 'the concept of the sphere' without actually saying anything really surprising or interesting about the sphere. It's like staring in the display window of a candy shop but not actually eating any candy... just talking about 'the concept of candy'. :upside_down:

Alex Kreitzberg (Sep 19 2024 at 20:21):

I love math! I wasn't trying to hide your interesting digression. I was just trying to move my questions out of somebody else's thread, and the snippet of your quote I grabbed was a natural unit.

Alex Kreitzberg (Sep 19 2024 at 20:22):

Shulman really hit the nail on the head with how I've struggled with my intuition of working with definitions and how it actually felt using definitions in practice, when programming for example.

I really wasn't trying to get too philosophical

Alex Kreitzberg (Sep 19 2024 at 20:33):

It's like for 7 year old Alex a circle was what a compass made.

But then for 20 year old Alex, a circle could be a subclass of an ellipse, or a predicate, or a quotient, or whatever, and I got unironically confused what I was doing.

If I had to add "circle" to a personal software library, I wouldn't know which one to pick, or what their interface should be.

Whereas if I stopped programming and only let myself use a compass and straight edge, I could calm down and get back to doing stuff with circles XD

It's almost more of a mental health thing with me, than a philosophical problem exactly.

Alex Kreitzberg (Sep 19 2024 at 20:34):

But this discussion helped!

Alex Kreitzberg (Sep 19 2024 at 22:38):

I think Thales's theorem is really cool.

Mike Shulman (Sep 19 2024 at 22:43):

Alex Kreitzberg said:

In my own Haskell code I think I noticed this naming issue with typeclasses but didn't know if it was essential, or reflected poor theory. It sounds like the issue is essential?

Hmm, specifically what issue are you referring to? The fact that if there's more than one possible instance you can only make one of them an official instance?

Alex Kreitzberg (Sep 19 2024 at 22:46):

Right, a number is a monoid in a few ways. So I end up feeling tempted to make typeclasses like "addable", "multipliable" etc. which sorta defeats the purpose.

Mike Shulman (Sep 19 2024 at 22:47):

Well, I believe Lean does that, so you're not alone!

Alex Kreitzberg (Sep 19 2024 at 22:48):

I remember seeing a dependent typing feature where "Monoid" was a type, and multiple monoids could be elements of that type, and I thought "ahh this fixes it!", but you explained very well how this doesn't actually fix the issue

Mike Shulman (Sep 19 2024 at 22:48):

Yeah, it just bundles things differently; it's basically the same as explicitly saying which monoid you want to talk about.

Mike Shulman (Sep 19 2024 at 22:52):

My own feeling is that these issues should be helped by proper namespacing of everything, including instances and notations. I should be able to say that the integers, for instance, have two underlying monoid structures, and declare them both as typeclass instances in two different namespaces. Then if someone wants to talk about the additive monoid, they can import the monoid instance for plus, and if they want to talk about the multiplicative monoid, they can import the monoid instance for times, both separately from importing all the theorems about integers that involve both addition and multiplication. Similarly for notation: someone proving general facts about a monoid should be able to say "I want to use * for the product in my monoid", and then I should be able to import all of his theorems but not his notation and specialize them to the additive monoid of the integers for which I'm using the notation +.

Mike Shulman (Sep 19 2024 at 22:54):

I'm trying to build this sort of flexibility into my proof assistant Narya. It doesn't have typeclasses yet, but it does have notations, and they have namespaces and import control like this.

Alex Kreitzberg (Sep 19 2024 at 22:54):

That makes a lot of sense, and would be better. Thank you for your thoughts. I think my question is answered.

Paolo Perrone (Sep 20 2024 at 14:42):

One thing that one could try to model is a specific category where

• Objects are particular pointed categories and pointed functors between them, following John's idea. (Each object is a collection of categories with a distinguished object, and different objects may have different underlying collections.)
• Morphisms are partial collections of morphisms which change the base point.

One could construct this category to make precise how we usually think of "the sphere", etc.

Partial because: consider the circle and the plane. They are sets, metric spaces, manifolds, Lie groups, etc.
Now the canonical embedding S^1 -> R^2 is continuous, smooth, etc, but not a morphism of groups.

John Baez (Sep 20 2024 at 20:03):

This sounds fun! Thanks, @Paolo Perrone!

Paolo Perrone (Sep 21 2024 at 00:17):

By the way, perhaps oversimplifying, this may be similar to how the categories of philosophy work. One object lives simultaneously in several of them, like 'aspects' of that object that one can study.

Alex Kreitzberg (Sep 23 2024 at 16:03):

Tom Leinster's notes were very fortuitous.

If I replace my sphere example with the number 2, then his discussion is on exactly my question as I understand it.

It's much more intuitive to me how $2 \in Z_3$ shouldn't have an equivalence with $2 \in Z_5$, and at the same time how serious of a notational problem this is if you're trying to design a programming language. Which is part of the reason I asked this question (but couldn't articulate as such)

From there it isn't hard to understand how objects have more complicated versions of the same problem.

I've been trying to think through Paolo's category, and as I understand it better, it's also clear how difficult it is to think that way as a habit. If you can clearly articulate the relevant categories, your job gets much easier.

I think it's worth mentioning, many programming languages see it as a feature to obscure the types, so I don't think types are intuitive for everyone necessarily. Lienster referencing the joke from "mathematics made difficult":

Is the number 48 on this page a natural number or an integer?

is a perfect example of how weird or pedantic this situation can seem. And I definitely fell into the trap implied by the book (the poor programmer, has to give an answer to that question. JavaScript automatically makes it a float!)

Thank you for the discussion, this was really helpful.

John Baez (Sep 23 2024 at 16:15):

I've been trying to think through Paolo's category, and as I understand it better, it's also clear how difficult it is to think that way as a habit.

I guess it's difficult just like playing the piano well, but like playing the piano well a lot of people do it. I think most pure mathematicians, particularly algebraists and topologists, think this way routinely in a somewhat relaxed way. E.g. they will say "the sphere, regarded as a manifold" and then say "its underlying topological space", and they know exactly what they're allowed to do with each of these things, and how they're related.

Alex Kreitzberg (Sep 23 2024 at 16:42):

I guess I don't (usually) get tripped up by the various different 2s XD.

Alex Kreitzberg (Sep 23 2024 at 16:54):

But it can still be worth saying when it's an integer or a real number to communicate which relationships you want to draw attention to.

Alex Kreitzberg (Sep 23 2024 at 16:56):

Rather than fighting to maintain "2" as a concept that exists above all of its versions.

Alex Kreitzberg (Sep 23 2024 at 17:01):

Like I was doing

Kevin Carlson (Sep 23 2024 at 17:04):

It's not just about fuzzy stuff like "communicating relationships", of course; whether $2$ is in $\mathbb Z/3$ or $\mathbb Z/5$ affects the computation of $2+2$!

Alex Kreitzberg (Sep 23 2024 at 17:07):

Right exactly, I was avoiding the "what does 2+2 mean?" Framing, maybe unnecessarily XD

But I think this issue might connect with people taking that expression too seriously, that it is ambiguous if you aren't careful

Alex Kreitzberg (Sep 23 2024 at 17:10):

Or you need something like Paolo's construction to make it make sense.