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: Groupoids - How are things the same but different?


view this post on Zulip Alex Kreitzberg (Oct 04 2025 at 23:15):

Trying to understand HoTT seems to have deeply clarified Groupoids for me, specifically that they can be thought of as a generalization of an equivalence relation.

Thinking back on many concepts I've been trying to formalize categorically, it seems like groupoids account for, or at least clarify, most of them. But I'm a bit confused how things are "the same" but "different". So I'm going to try and give examples of this, but also I'd like to just chat a bit about groupoids.

Awhile ago I was trying to understand accordions with category theory. The discussion can be summarized by saying it's useful to model musical concepts with G-Torsors, or "generalized musical intervals" in David Lewin's terminology. By thinking of G-Torsors as a translation groupoid - I could imagine musical concepts as objects, and the arrows transforming between them as given by group transformations. These symmetries could then be given a physical interpretation for how the musical objects would be played, via an accordion layout.

One aspect that bugged me about this, was that an actual accordion had a finite number of buttons, but Z2\mathbb{Z}^2-Torsors wanted an infinite number of buttons. Applying a translation to the highest note falls off the edge of the accordion.

The article "Groupoids: Unifying Internal and External Symmetry" illustrated how action groupoids (or transformation groupoids) restricted to a bounded set, allows one to define symmetrical features via automorphisms of the ambient space.

An infinite grid, its symmetries exist at intersections, and midpoints of lines:
Infinite tile grid

A finite grid requires groupoids to find more distinct sorts of symmetries:
image.png

For example, Its possible to detect the corners of a tiled rectangle, by noticing certain reflections preserve the corner edges.

This gives me ideas for exploring accordions, but maybe I should switch gears to something more familiar. I also wanted to model chess moves, which incidentally also requires the pieces move on a grid. Moving from and to either the corners, edges, or interior squares corresponds to very different familes of moves, which I would say are roughly indicated by the symmetries indicated on the finite rectangle.

However if I choose my isomorphisms to be knight moves of the would be groupoid, the knight can travel to any square. It's still a puzzle to ask which paths there are between two points on the board.

Very similar to this, Baez gave the 16 puzzle as an example of a groupoid, where all the positions of the game correspond to different objects, with moves between states given by isomorphisms. If a game can be won from a given position, it's usually thought of as "equivalent" to a winning position. Conway invented the Surreal numbers by carefully identifying positions of similar "winnability". So I suspect this groupoid perspective is "correct" in that a puzzle that hasn't been finished yet, is "the same" as a finished puzzle. This is a bit confusing to me.

Normally, when I think of something as the same, I think of a sort of congruence. If I know how to play a song on the accordion, and I shift my hands, it's still the same song. I'd even go so far as to suggest a path of transitions between various dance positions determines a dance, which different people can perform in different places by simply changing where they start.

Dancing over diagram

Regardless, in HoTT, I believe it's still meaningful to provide a solution to a 16 puzzle in an identity type, to show the puzzle is actually solvable. How should I think about "equivalance" in a context where it's important to provide a proof that things are equivalent, like in solutions to the 16 puzzles?

Context for a second question, I'm used to groups being defined as transformations which preserve certain structures or properties of a set we want to explore. With the classic groups being given by isometries. So interesting stuff doesn't happen until you have a symmetrical figure that maps to itself.

If we lift our perspective to groupoids, thinking of one specified triangle as having lengths (1,2,3)(1, 2, 3), then every isometry on this triangle will give an entire groupoids worth of triangles across the plane. Geometric operations on this triangle, like circumscribing with a circle, in a sense should circumscribe all the triangles at the same time. That is, we have a groupoids worth of circles under the same transformations, given by the previous geometric construction. All triangles with various possible side lengths, are connected components of their own groupoids, in general the groupoids will be contractible; however, the non-contractible groupoids correspond to the symmetrical triangles, baking in potential ambiguities.

Somehow it feels like there should be more to the story, than a groupoid of non-symmetrical triangles being contractible to a point. I'm assuming "the rest of the story" is clarified by generalizing to categories. Maps from the contractible groupoid of one triangle, should be different than maps from the triangle of a different contractible groupoid. But I'm not sure how to go about this.

So to restate my questions, what's happening that makes groupoids more natural than groups, even though they're equivalent? Why do the skeletons seem to be worse? How can things be "equal" but different?

Secondly, I have some narrative in my head of how Klein organized geometry around his Erlangen program. I think it's mostly right, but now I'm feeling there could be a real, or false but simpler, history that takes this narrative further. Is there a natural sequence of ideas to motivate classifying geometry by groupoids instead of groups - and then somehow by categories instead of groupoids? Assuming I really understand groupoids well, how do they fit into the story around the "Erlangen program"?

In any case, I have a much deeper feeling for how important groupoids are, and in what way they are "better than" sets with equality. So I'd appreciate any further discussions or suggestions to take this understanding further.

(I have this sense, "in mathematics", that there is a very well understood arrow "groupoids → categories" and a mostly understood arrow "groupoids → ∞-groupoids/HoTT", but that it's still an active research program to work out the "pushout" of "∞-categories" in a really nice way. But right now I'm still trying to sort out those first two arrows).

view this post on Zulip Chris Grossack (she/they) (Oct 04 2025 at 23:50):

As you say, you can think of a groupoid as being a bunch of things, some of which are the same and some of which aren't. I think two good examples to think about are

  1. The category of finite sets, with bijections
  2. The category of finite dimensional vector spaces, with invertible linear maps.
    Eg, the sets {1,2} and {a,b} aren't literally the same, but for many purposes they are, and this groupoid reflects that fact.

I would push back a little bit on saying that "groupoids are equivalent to groups". Every connected groupoid is equivalent to a group, but part of the fun is that groupoids don't have to be connected! For instance, example (1) is the disjoint union of all the symmetric groups SnS_n. This actually matters quite a lot! For instance, there's a new "parabolic induction" tensor product that you can only see if you look at representations of all the SnS_n simultaneously. This leads to a very pretty connection with braid diagrams (that gets even prettier if you work with example (2), over a finite field).

view this post on Zulip Mike Shulman (Oct 04 2025 at 23:53):

Arguably only pointed connected groupoids are equivalent to groups. Of course every connected groupoid can be made pointed somehow, but in general there's no canonical or unique choice of a point. An unpointed connected groupoid only determines a group "up to conjugacy".

view this post on Zulip Chris Grossack (she/they) (Oct 04 2025 at 23:54):

Yeah, that's an important clarification. Especially since "group up to conjugacy" is a useful way that groupoids naturally show up

view this post on Zulip Alex Kreitzberg (Oct 05 2025 at 04:11):

Could you say a little bit more about the "parabolic induction" tensor? I see how it's a dramatic demonstration of how useful all the connected components are.

Isn't saying a groupoid is a group "up to conjugacy" the same thing as saying "No really think about the groupoid!"? How do you have a group up to conjugacy without just having all the objects of the groupoid?

view this post on Zulip Alex Kreitzberg (Oct 05 2025 at 05:03):

I spent a couple days trying to find compelling groupoid resources about games and just now found Dan Pipioni linked to a blog post (https://cornellmath.wordpress.com/2008/01/27/puzzles-groups-and-groupoids/) as a reply to this math overflow question (https://mathoverflow.net/questions/1114/whats-a-groupoid-whats-a-good-example-of-a-groupoid) :face_palm:

I didn't fully understand the significance of the 15 puzzle as a groupoid example. It was way more subtle than I gave it credit for. The blog gave a compelling way to think of different objects in the 15 puzzle groupoid as the same. I'll think about whether I can work this back to my knight move example as well as how this relates to conjugation.

view this post on Zulip Morgan Rogers (he/him) (Oct 05 2025 at 11:31):

Alex Kreitzberg said:

Could you say a little bit more about the "parabolic induction" tensor? I see how it's a dramatic demonstration of how useful all the connected components are.

I haven't heard the name "parabolic induction tensor" before (does that come from representation theory @Chris Grossack (she/they) ?), but there are a few tensor products on the groupoid of finite sets and bijections. Notably, the restrictions of products and coproducts of finite sets provide tensor products (note that these no longer have the respective universal properties!) which capture how some symmetries of a set can be constructed by decomposing the set and putting together symmetries of the parts.

view this post on Zulip John Baez (Oct 05 2025 at 12:33):

Since Chris is talking about tensoring representations of different symmetric groups, I figure they must be talking about how S\mathsf{S}, the groupoid of all finite sets and bijections, is symmetric monoidal under disjoint union. Thanks to this [S,Vect][\mathsf{S},\mathsf{Vect}], the category of representations of the groupoid S\mathsf{S}, gets a [[Day convolution]] symmetric monoidal structure.

S\mathsf{S} is the coproduct of connected components, one for each nNn \in \mathbb{N}. Call the nn th connected component BSnB S_n, since it's equivalent to the one-object groupoid where the automorphisms of that object are the symmetric group SnS_n:

SnNBSn \mathsf{S} \simeq \sum_{n \in \mathbb{N}} B S_n

Thus

[S,Vect]nN[BSn,Vect] [\mathsf{S}, \mathsf{Vect}] \simeq \prod_{n \in \mathbb{N}} [B S_n , \mathsf{Vect} ]

and [BSn,Vect][B S_n , \mathsf{Vect} ] is usually called the category of representations of SnS_n.

The Day convolution monoidal structure lets you tensor a representation of SnS_n and one of SmS_m and get one of Sn+mS_{n+m}. This is usually called 'induction', since you can define it an [[induced representation]].

view this post on Zulip Jorge Soto-Andrade (Oct 05 2025 at 16:11):

I would add that parabolic induction was discovered in the 70s by Andrey Zelevinsky and published in Zelevinsky. Representations of Finite Classical Groups (LNM0869, Springer, 1981), also for the case of the q-analogue GL(n,Fq)GL(n, \mathbb F_q) of SnS_n.
Also, I think, Chris, that another nice example of groupoid to have in mind, besides Path Groupoids, is the Action Groupoid A(X,G)A(X,G), associated to any (non necessarily transitive) GG-set XX , used by Alain Connes among others. Its sets of objects is XX and its arrows are the triples (x,g,y)(x,g,y) where x,yXx,y \in X, gGg\in G and g.x=yg.x=y. This groupoid allows you to do "geometric induction", without choosing a fixed subgroup HH of GG, from a representation (quite often a linear character) of A(X,G)A(X,G) to GG. This is most useful to construct "Gelfand Models" for the linear complex representations of GG. More details in this arXiv preprint In the case of G=SnG = S_n the relevant GG-set is the set of all involutions in SnS_n on which SnS_n acts by conjugacy. The action groupoid has an easy to guess nice linear character...

view this post on Zulip Mike Shulman (Oct 05 2025 at 17:21):

Alex Kreitzberg said:

How do you have a group up to conjugacy without just having all the objects of the groupoid?

Define the 2-category GrpConj of "groups up to conjugacy" as follows:

Though defined without any reference to groupoids, this 2-category is equivalent to the 2-category of (unpointed!) connected groupoids. Specifically, there is a 2-functor GrpConjGroupoid\mathrm{GrpConj} \to \mathrm{Groupoid} taking a group to its corresponding 1-object groupoid. The 2-cells in GrpConj are chosen exactly so as to make this 2-functor 2-fully-faithful (an isomorphism on hom-categories), so it is an equivalence onto its essential image, which is the 2-category of connected groupoids.

view this post on Zulip Alex Kreitzberg (Oct 06 2025 at 19:35):

I'm still processing all of this and relating it to my examples, I wanted to give a couple comments to indicate I'm listening.

In Shulman's explanation, Functors between groups as categories "are just" homomorphisms, and natural transformations "are just" conjugations (of homomorphisms). That latter part was new to me.

For any arrow f:xyf : x \rightarrow y and two Functors F,G:CDF, G : C \rightarrow D, the naturality condition gives αyFf=Gfαx\alpha_y \circ F f = G f \circ \alpha_x. When C,DC, D become single object groupoids G,HG, H, the functors F,GF, G become homomorphisms ϕ,ψ:GH\phi, \psi : G \rightarrow H, the arrow ff becomes an arbitrary g:GGg : G \rightarrow G, and the natural transformation is given by just one arrow, h:HHh: H \rightarrow H from HH. Which gives hϕ(g)=ψ(g)hh \cdot \phi(g) = \psi(g) \cdot h for all gGg \in G.

The point I missed, is instead of viewing groupoids as a member of Cat, I should view them as a member of 2-Cat the 2-category Cat.

So to relate this to a concrete example. If I have two congruent equilateral triangles in a plane, then I have D3D_3 choices of how to lay one on top of the other, which is encoded in a group homomorphism. But, even better, in the 2 Cat we can tell two homomorphisms are "the same" when they both express a reflection over some axis.

Baez's and Soto-Andrade's comments aren't the same but "rhyme". There's a lot I'm unpacking, but its clear I need to understand representations better. Here's a bit about how I'm thinking about this.

To understand the 15 puzzle - I'm imagining a 4 by 4 board, with a rook that can only move one square (Or like a character in an old zelda game). There is a (2) Functor from this board as a groupoid to 15 puzzles. Each position of the board, maps to the 15 puzzles with a gap in the same spot. The numbers get jumbled up based on how the gap moves, which then defines a permutation in S15S_{15}.

So I think, we have A(15-puzzle,gameboard)A(15\text{-puzzle},\text{gameboard}), or 15-puzzle:[gameboard,S]15\text{-puzzle} : [\text{gameboard}, S] (The former is like the category of elements for the later I think). Maybe it'd be cool to consider permutation linear transformations.

I can see the point of Andrade's discussion, that the action groupoid allows a definition of a process we call "induction" (that Baez also referenced) which doesn't require an arbitrary choice of subgroup.

The equivalence [nNBSn,Vect]nN[BSn,Vect][\sum_{n \in \mathbb{N}} B S_n, \mathsf{Vect}] \simeq \prod_{n \in \mathbb{N}} [B S_n , \mathsf{Vect} ], is also a nice way to see how infinite products and sums in groupoids are interesting.

I want to explicitly reference a "guiding principle" indicated in Alan Weinstein's paper "Groupoids: Unifying Internal and External Symmetry":

Almost every interesting equivalence relation on a space BB arises in a natural way as the orbit equivalence relation of some groupoid GG over BB. Instead of dealing directly with the orbit space B/GB/G as an object in the category SmapS_\text{map} of sets and mappings, one should consider instead the groupoid GG itself as an object in the category GhtpG_\text{htp} of groupoids and homotopy classes of morphisms.

My motivation for this thread is internalizing this perspective. I'm not sure what the best road is for doing this.

view this post on Zulip Mike Shulman (Oct 06 2025 at 21:30):

Alex Kreitzberg said:

instead of viewing groupoids as a member of Cat, I should view them as a member of 2-Cat.

No, I would say that rather than viewing groupoids as objects of the 1-category Cat, you should view them as objects of the 2-category Cat. 2-Cat is something different, its objects are 2-categories.

view this post on Zulip John Baez (Oct 07 2025 at 09:30):

Nobody should ever say "groupoids as a member of Cat".

  1. It's always dangerous to mix singular and plural - like groupoids as a member - because it promotes ambiguity, and the reader, trying to resolve this ambiguity, can reach for different solutions. Do you mean "the category of groupoids as a member of Cat" or "groupoids as members of Cat"?
  2. It's also not usual to say "members" for objects of a category or 2-category - for me at least it denotes elements of a set. So reading "groupoids as a member of Cat", I'm also imagining a set called Cat, but I have to discard this as an unlikely interpretation.

A moment of haste when writing can produce minutes of annoyed head-scratching for dozens of readers.

view this post on Zulip Alex Kreitzberg (Oct 07 2025 at 17:46):

The singular and plural mix seems to reflect my own confusion actually, good opportunity to fix my semantics by checking my syntax :sweat_smile:.

The "member of" in my mind was an attempt at "type of", but the later phrase feels weird to write informally. I don't think that fixes the sentence though.

Here's another attempt.

"A group is a single object groupoid" is actually a great definition, because groupoids should be read as having natural transformations.

So I'm trying to write in my own words "don't forget the 2-cells!" Maybe that's enough.

Using Shulman's writing as an example, keeping the spirit of my original sentence:

"A groupoid is not just an object of the 1-category Cat, it's even an object of the 2-category Cat!"

I think I wanted to say "A groupoid is a two category" or more obviously wrong "A category is a 2-category", but I didn't understand the error.

Something like "Don't forget the 2-cells!" Is the right way to say this.

view this post on Zulip Alex Kreitzberg (Oct 07 2025 at 17:56):

I want to assemble a "plural" of "groups" into a "singular" "category". In a sentence like

"A group is a single object groupoid; when assembling groups into a category, don't forget the 2-cells!"

view this post on Zulip Alex Kreitzberg (Oct 07 2025 at 17:56):

Is that still ambiguous?

view this post on Zulip Alex Kreitzberg (Oct 07 2025 at 18:26):

It's like "a murder of crows", but honestly I can still feel the risk because we don't usually talk about a "a crime of murders" or whatever. The towers of sorts in category theory should be written about with care. I'll keep this in mind.

I guess the real issue is the word "member", it made that sentence fall apart.

view this post on Zulip John Baez (Oct 08 2025 at 09:32):

Two things make the phrase "groupoids as a member of Cat" feel to me like fingernails rubbing on a blackboard:

  1. mixing singular and plural
  2. saying "member of Cat".

view this post on Zulip John Baez (Oct 08 2025 at 09:33):

Each one requires me to choose a way to correct the phrase, so I can get a phrase I can understand.

view this post on Zulip John Baez (Oct 08 2025 at 09:37):

"A group is a single object groupoid; when assembling groups into a category, don't forget the 2-cells!"

Is that still ambiguous?

No, that's not ambiguous. It's even true if you stretch the meaning of "is" a bit. To clarify this word "is" youcan say something like "any group GG gives a one-object groupoid BGBG, and conversely any one-object groupoid arises in this way up to isomorphism." One can polish this statement further.

But experts don't like to talk about the number of objects in a category since it violates the principal of equivalence. (That's the woke way to say it's evil.) So instead of talking about one-object groupoids they prefer to talk about pointed connected groupoids.

Theorem. A groupoid is equivalent to BGB G for some group GG iff it's a pointed connected groupoid.

view this post on Zulip John Baez (Oct 08 2025 at 09:38):

There are better things to say....

view this post on Zulip Alex Kreitzberg (Oct 08 2025 at 20:56):

I don't know if I'm able to express this correctly and tersely.

The 2-category with groups as objects, homomorphisms as 1-morphisms, and conjugations between homomorphisms as 2-morphisms

is equivalent to

the 2-category of connected groupoids.

I also want to say:

The category of groups is equivalent to the category of pointed connected groupoids

But I've been convinced my handle on the basic definitions is worse than I thought, so I looked up [[pointed connected groupoid]]. Happily, I found the book Symmetry by Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson.

This book seems like an extended answer to this thread topic from the point of view of HoTT - maybe that's what I want. For example it gives some nice context for pointed connected groupoids on the fifth page in the margin:

pointed connected groupoid motivation

I'd really like to understand groupoids from a "mathematical" lens before I understand them from a "computer science" lens, if that's practical.

view this post on Zulip John Baez (Oct 09 2025 at 12:01):

Alex Kreitzberg said:

I don't know if I'm able to express this correctly and tersely.

The 2-category with groups as objects, homomorphisms as 1-morphisms, and conjugations between homomorphisms as 2-morphisms

is equivalent to

the 2-category of connected groupoids.

Umm, either that's true or we need to stick the word "pointed" in "the 2-category of connected groupids".

view this post on Zulip John Baez (Oct 09 2025 at 12:03):

The category of groups is equivalent to the category of pointed connected groupoids.

Maybe I'll throw this one back at you before I think harder about it: what are you taking the morphisms to be in the category of pointed connected groupoids?

(I think there's a fairly obvious answer, but let's make sure we agree on it!)

view this post on Zulip Alex Kreitzberg (Oct 10 2025 at 05:21):

A pointed category is a category C\mathcal{C} with one of its objects specified (C,c)(\mathcal{C}, c). The objects of (C,c)(\mathcal{C}, c) are arrows in C\mathcal{C} that start at cc. Given two objects x:cXx : c \rightarrow X and y:cYy : c \rightarrow Y, an arrow between them in (C,c)(\mathcal{C}, c) is an f:XYf : X \rightarrow Y, making the implied triangle commute : y=fxy = f x.

When our pointed category is a groupoid, the objects determine the arrow, in the above we'd have f:=yx1f := yx^{-1}.

This limits the natural transformations between our functors heavily. If I have two functors F,G:(C,c)(D,d)F,G : (\mathcal{C}, c) \rightarrow (\mathcal{D}, d) a potential natural transformation between them, is determined by their values on objects F(x:cX)=Fx:dFX,G(x:cX)=Gx:dGXF (x : c \rightarrow X) = F x : d \rightarrow F X, G (x : c \rightarrow X) = G x : d \rightarrow G X therefore if we have a natural transformation α:FG\alpha : F \Rightarrow G it's x component would be αx:cX=Gx(Fx)1\alpha_{x : c \rightarrow X} = G x (F x)^{-1}. Also, because these are groupoids, this would have to be a natural isomorphism.

In particular, there's only an identity natural transformation from any functor to itself, and at most one natural isomorphism to any other functor. So the functors, or symmetries, form a set of contractible groupoids, or just a set.

So we have just a category of pointed groupoids. Then the category of pointed connected groupoids is equivalent to the category of groups. To define a functor from pointed connected groupoids to groups, just pick out the automorphisms of the specified object of our groupoid. The groupoid laws require these form a group; such a map is fully faithful by construction and essentially surjective, because any given group GG is the image of a groupoid BGBG. If I took a bit more time, I bet I could find a proof that doesn't need choice.

Shulman outlined a proof earlier finding an equivalence between connected groupoids and groups up to conjugation, though I believe his proof requires choice in an essential way. The moral I'm digesting are that groupoids are different than groups, you need to carefully choose what you mean by both, and what you mean by equivalence, to illustrate their equivalence. So "a group is a one object groupoid" is a risky definition because it's evil.

If I got all of that right. I saw some cool stuff trying to find the definition of a pointed category - like [[delooping]], or the [[delooping hypothesis]]. For a group GG what exactly is the "delooping" BGBG? I've been thinking of it as a dot to hold the group in its set, but it seems like there's a lot more to the story there.

view this post on Zulip John Baez (Oct 10 2025 at 09:11):

Thanks for straightening this out! I never really had.

The delooping BGB G of a group is the corresponding one-object groupoid: the groupoid with one object \ast, one morphism g:g : \ast \to \ast for each gGg \in G, with composition of morphisms being multiplication in GG.

view this post on Zulip John Baez (Oct 10 2025 at 09:12):

It has that funny name because it's analogous to a construction in topology that turns a loop space into a group. If you try to understand this you may be forced into understanding that groupoids are 'the same' as certain kinds of topological spaces - a baby warmup for the homotopy hypothesis. You may or may not want to go down this road now! It's fascinating and leads very far.

view this post on Zulip Alex Kreitzberg (Oct 15 2025 at 03:52):

Trying to digest a lot of stuff connected to this - at the moment the name "simplex", though appropriate, is feeling comically ironic.

Working through your website here:
https://math.ucr.edu/home/baez/calgary/homotopy.html

view this post on Zulip John Baez (Oct 15 2025 at 08:55):

Oh, great! I could improve those pages a lot, making them easier to understand and better organized - but the items with letters like A, B, C, ... are all really important.

view this post on Zulip Alex Kreitzberg (Oct 18 2025 at 06:27):

Still processing a ton of information, but I wanted to ask how up to date your article "categorification" from 1998 is?

It's describing a lot of cool context, it seems like you can come down from infinity groupoids to reconstruct a lot of the themes we've talked about and some we haven't - like categorification, delooping, stabilization, monoidal categories and associated ideas like simplicies, operads, geometric realization, etc.

I think what I'm reading is making sense, but it's a lot of work, so if there's "newer stuff" I should look at instead I wanted to double check.

view this post on Zulip John Baez (Oct 18 2025 at 10:35):

A vast amount of work on categorification and its relation to homotopy theory came after that 1998 article. The article is tough because you're trying to learn a huge amount of math at once. But most of the newer stuff will be more work to read, I think - for example, nowadays everyone feels compelled to read Lurie's 735-page book, or at least some summary of it.

You say you're asking for "newer stuff", but maybe what you want is a simpler introduction? Maybe someone here can recommend a good easy modern introduction to homotopy theory and higher categories?

view this post on Zulip Ryan Wisnesky (Oct 18 2025 at 18:13):

I'm reminded of a viral student quote, 'Professor, is it OK to cite sources from the late 20th century or are they too old?'

view this post on Zulip Alex Kreitzberg (Oct 18 2025 at 18:44):

I generally feel safe thinking of textbooks as "settled", but papers generally are often bleeding edge or have a very particular point of view. So I'm much more cautious when building an understanding around them, even when the researcher is very good. (So "newer" probably wasn't the best choice of words. Something like "in a recent, more settled context" or "introductory, but on the same material" would probably be better phrasings)

I was caught off guard by the observation many folks read Lurie to resolve my question. After thumbing through it, I saw the definition of \infty-category as an (,1)(\infty, 1)-category, and that the whole book was about this special case. I didn't realize "near state of the art" was only one step above \infty-groupoids. That's kinda funny, it's sorta like how categories are one step above sets.

I guess reprising the theme of this thread. Maybe the most direct way to learn about \infty-groupoids is to learn Homotopy Type Theory then?

view this post on Zulip Elisha Goldman (Oct 18 2025 at 19:02):

Maybe someone here can recommend a good easy modern introduction to homotopy theory and higher categories?

How about Higher Categories, Higher Operads? It doesn't go into homotopy theory but it does put effort into making higher categories intuitive. Maybe Kerodon for more focused homotopy theory?

view this post on Zulip Alex Kreitzberg (Oct 18 2025 at 19:14):

What an adorable mascot!

Guinea Pig!

(from: https://kerodon.net/)

view this post on Zulip Elisha Goldman (Oct 18 2025 at 19:18):

Wiki-style textbooks about fields of math with cute mascots are the best nanogenre, there's also one with space cats!

view this post on Zulip Alex Kreitzberg (Oct 18 2025 at 22:04):

Here's a relevant math.stackexchange question:

Textbooks on higher category theory

(Though I want to underscore I'm trying to understand \infty-groupoids first, because I'm assuming they're easier to understand and more settled than arbitrary weak nn-categories)

view this post on Zulip John Baez (Oct 18 2025 at 22:50):

Trying to understand \infty-groupoids is approximately the same as trying to understand homotopy theory, since while \infty-groupoids and homotopy types can each be defined in many (equivalent) ways, they are equivalent to each other.

There are many ways to start trying to understand them, but the most standard are:

view this post on Zulip John Baez (Oct 18 2025 at 22:54):

The table of contents of Strom's book Modern Classical Homotopy Theory looks like a good intro to the first approach. The first 200 pages would be enough for your purposes.

view this post on Zulip John Baez (Oct 18 2025 at 22:57):

The first 40 pages are just category theory.

view this post on Zulip John Baez (Oct 18 2025 at 23:13):

Someone like @Mike Shulman might know a good gentle introduction to the big picture of simplicial homotopy theory, which is the second of the three approaches I listed. The Foundations section of Kerodon covers a lot of the right stuff, but not enough on \infty-groupoids (e.g. Kan complexes) for your purposes, since they're in a rush to get to (,1)(\infty,1)-categories.

And for the third, the HoTT book is one obvious candidate.

view this post on Zulip Alex Kreitzberg (Oct 18 2025 at 23:23):

I recently purchased the HoTT book, I'm impressed with Lulu's print quality!

view this post on Zulip Mike Shulman (Oct 19 2025 at 15:45):

I suppose the canonical introduction to pure simplicial homotopy theory is Goerss and Jardine's book Simplicial homotopy theory, although I don't know that I'd call it "gentle".

view this post on Zulip John Baez (Oct 19 2025 at 19:20):

I think it's the opposite of gentle. It's like they left out the first few chapters.

view this post on Zulip Mike Shulman (Oct 23 2025 at 21:46):

This may be a gap in the literature? Surely it should be possible to write a gentle introduction to simplicial homotopy theory, but I can't think of one.

view this post on Zulip John Baez (Oct 23 2025 at 22:26):

Your advisor's book Simplicial Objects in Algebraic Topology while very far from gentle, is much more introductory than Goerss and Jardine's. I found it pretty useful. And while we're talking about introductions to homotopy theory, I feel like adding his book A Concise Course in Algebraic Topology. But then I should add Hatcher's Algebraic Topology, and the list may keep growing and becoming more diffuse. The latter two books at least have the advantage of being free (and legal) in LaTeX form.

view this post on Zulip daniel gratzer (Oct 25 2025 at 08:03):

While they're a bit old, Curtis Edward's notes "Simplicial Homotopy Theory" (Advances in Mathematics, 1971) are pretty good. However, they're too terse to be an introduction on their own. There are also notes by Joyal and Tierney "Notes on simplicial homotopy theory" which are gentler and might be an on-ramp to some of the other resources mentioned?

view this post on Zulip Alex Kreitzberg (Oct 25 2025 at 17:56):

Thank you for the book references, I'll chip away at those over time.

I think I was able to focus my question into definite statements. Are the following correct?

A groupoid with at most one arrow in each homset, is an equivalence relation; and the delooping of a group is a one object groupoid - therefore a groupoid is a generalization of both "equalities" and "symmetries".

In many proof assistants/logics, one internalizes definitional equality into an equality type, which in HoTT is then "widened" by the univalence axiom.

I've called isomorphic objects "samey" in the past, because I was afraid to use the word "equals"; so I like the precision and tension the univalence axiom touches on. I wanted to "guess" what this amounts to before getting into HoTT's details.

Here's my best guess so far.

In euclidean geometry, a configuration of lines in the euclidean plane are "congruent" to another, if there is an isometry that overlaps one configuration over the other. Some theorems let us show there is only one triangle with side lengths (1,2,3)(1, 2, 3) "up to congruence". I want to say (1,2,3)(1, 2, 3) and (3,1,2)(3, 1, 2) are simply "equal", but the story is complicated by the existence of symmetrical triangles like (1,1,1)(1, 1, 1) which would then need to be equal in "more than one way".

But lets say that's okay.

One way I might try to make this more definite, is by letting figures be functions taking values in homogenous spaces, in the style of [[Klein geometry]]. I haven't fully thought through the details, but I'm assuming lifting a group action on a homogenous space, to figures in that space, forms a groupoid.

Real numbers having a notion of equality, an equivalence relation, makes the Reals into a groupoid.

So if I define a function area:FiguresR\text{area} : \text{Figures} \rightarrow \mathbb{R}, for finding the area of such triangles, I'm permitted to think of it as a functor between groupoids. That is, it doesn't exist in just a geometric, or numeric category - area\text{area} being a functor means it satisfies Leibniz's law:

x=y    area(x)=area(y)x = y \implies \text{area}(x) = \text{area}(y)

Isomorphic figures should map to isomorphic (or equal) areas, which we write as equal elements mapping to equal outputs.

All of these statements can be translated into statements about paths and homotopies, because groupoids are just \infty-groupoids, which are just homotopy types.

Awhile ago, I asked what exactly "the principle of equivalence" was, assuming I'd be given some answer intrinsic to the details or facts of category theory, but instead I was told "it's the definition of what we care about".

Our chosen notion of "sameyness" for a set, determines "what it is we care about".

So in Euclidean geometry, the important details are whatever gets captured by isometries, rotations, translations and reflections. But in projective geometry, we get to keep whatever details are captured by projective transformations. The point is, if I define a function from some set, with a specified underlying notion of "equality" it's implicit that the function should give "the same" answer for "equal" inputs, but these notions are relative to the space and problem under consideration.

A much more low brow version of this process is related to quotient constructions. For any set you can establish an equivalence relation (or a groupoid) by giving it a function, and sorting the elements of the domain by what they map to. In some cases, like when defining fractions, you require functions be "well defined" by ensuring they give the same answer when evaluated on data that is "supposed to be the same". So if we have (a,b)(ca,cb)(a, b) \mapsto (ca, cb), we want to write ab=cacb\frac{a}{b} = \frac{ca}{cb} and therefore define all our functions from these in such a way that the equality is respected (which means the equality in the mapped to set f(ab)=f(cacb)f(\frac{a}{b}) = f(\frac{ca}{cb}) "isn't empty").

Am I getting this right, or are there critical details I'm messing up?

view this post on Zulip John Baez (Oct 25 2025 at 20:52):

Awhile ago, I asked what exactly "the principle of equivalence" was, assuming I'd be given some answer intrinsic to the details or facts of category theory, but instead I was told "it's the definition of what we care about".

But I guess you know that it says we count equivalent categories as the same, so we're mainly interested in properties of categories that are preserved by equivalence, and structures on categories that can be transported along equivalences.

view this post on Zulip Alex Kreitzberg (Oct 25 2025 at 21:17):

Right, so if we establish that two categories CC and DD are equivalent, if we're very careful with what we mean by "=", then we can write C=DC = D understanding it implies F(C)=F(D)F(C) = F(D) for any 2-Functor FF between 2-groupoids (I hope I got the levels right).

So 2-functoriality is a form of Leibniz's law, or "indiscernibility of identicals". Which is how we define properties, or structures, common to equivalent categories.

Just like how area\text{area} gives the same answer for isomorphic geometric configurations.

(I hope the following usage of core is right)

So maybe Conn:core(Cat)core(Set)\text{Conn} :\text{core}(\text{Cat}) \rightarrow \text{core}(\text{Set}), could send a category to a set of connected components, with bijections as the default notion of "equality" for Set.

Then C=DC = D with "=" meaning "equivalence" would get mapped to Conn(C)=Conn(D)\text{Conn}(C) = \text{Conn}(D) with "=" meaning "bijection".

view this post on Zulip Alex Kreitzberg (Oct 25 2025 at 21:19):

I guess there's one extra subtlety sneaking through, that presumably the choice of equivalence would be part of the data used to calculate the resulting bijection. Which maybe is the point of your clarification.

view this post on Zulip John Baez (Oct 25 2025 at 21:44):

Everything you said is right. Certainly the choice of equivalence f:CDf: C \cong D affects the choice of bijection Conn(f):Conn(C)Conn(D)\text{Conn}(f): \text{Conn}(C) \to \text{Conn}(D).

I think homotopy type theorists started out being rather gung-ho about saying C=DC = D to indicate that there is an equivalence from CC to DD, based on the univalence axiom, but then attitudes changed. I'm not sure - I'm not a homotopy type theorist, so I'm probably getting the details wrong. But personally I don't write == for equivalence.

view this post on Zulip Alex Kreitzberg (Oct 26 2025 at 01:09):

I'm curious what @Chris Grossack (she/they) or others think about my usage of equality in the above couple messages

view this post on Zulip James Deikun (Oct 26 2025 at 01:46):

I personally am completely comfortable with uses of equality like that. I often use different symbols for bijection or categorical equivalence or weak homotopy equivalence, but that is primarily because there are multiple notions of "equality" in play (e.g. judgmental equality in a type theory) or to help prevent level slips.

view this post on Zulip John Baez (Oct 26 2025 at 10:15):

Btw, I don't care what symbols people use as long as I understand what they mean. I'm just old-fashioned: I date to the era where distinguishing between equality, isomorphism and equivalence of categories was an important moral message. Youngsters for whom it's obvious that equivalence is all you'd ever talk about don't need to do this. They do however need to distinguish the existence of an equivalence from a chosen equivalence.

view this post on Zulip Alex Kreitzberg (Oct 26 2025 at 15:02):

Existence vs chosen existence is definitely confusing me in more places than just here.

Regarding using the equality everywhere, I think the issue is somewhat confused by HoTT being a sort of programming language, and the way it "reuses" the equality symbol is fancy. On a computer the type system could enforce correct usage and tell the user which type the equality belonged to. In common situations on paper, it's easy to write the various possibilities and they help a reader.

But there was also a more subtle technical observation. The univalence axiom says something like "every abstract usage of the internalized equality, can be safely substituted with whatever notion of equivalence you prefer." Which is something that can be false. But if it were true, now theorems for logic's take on equality generalize to equivalence.

So part of my excitement was noticing the intuitive phrase "the same" being sharpened into a formal/logical "equality" which rigorously subsumed "equivalence". The stage was set for "equality" to be more than a proposition, and univalence made it happen.

It sounds like my informal explanation was honest to this technical slight of hand, and that it'd be safe for me to work through more technical proofs.

view this post on Zulip Chris Grossack (she/they) (Oct 26 2025 at 16:10):

I'm also young enough to be very happy with writing == to mean equivalence in any \infty-category (this includes isomorphism in a 11-category as a special case), because I've internalized the idea that "equality on objects doesn't make sense" for (\infty-)groupoids. So I'll add to the chorus of people who are happy with what you've written.

view this post on Zulip Chris Grossack (she/they) (Oct 26 2025 at 16:12):

I also agree that our notion of "sameness" affects what we care about for exactly the reason you mentioned, going back to Klein's Erlangenprogram. I would say moreover (and possibly you said this and I missed it) that you can go the other way! Once you've decided on some important invariants, you might look for a notion of "sameness" that is compatible with those invariants

view this post on Zulip Chris Grossack (she/they) (Oct 26 2025 at 16:15):

For example, one family of very important invariants for a topological space are its homotopy groups. These are so central that you might imagine wanting to define "sameness" to mean "has the same homotopy groups". This turns out to be a bad idea for the same reason we don't say two triangles are congruent if they have the same area! We need some transformation that compares the two triangles. Similarly, we end up wanting two spaces XX and YY to be "the same" if there's a transformation (read: function) f:XYf : X \to Y (which will become an isomorphism) which moreover gives isomorphisms on all homotopy groups.

view this post on Zulip Chris Grossack (she/they) (Oct 26 2025 at 16:24):

Now it turns out to be difficult to determine in advance if ff has this nice property, but there's a sufficient condition that happens to be necessary for nice enough spaces! In favorable cases, f:XYf : X \to Y gives isomorphisms on all homotopy groups if and only if ff has a homotopy inverse g:YXg : Y \to X! This is fantastic, and simplifies the story dramatically. So if we restrict attention to "nice" spaces and (in a slightly subtle way) quotient out by the equivalence relation "homotopic maps should be equal", then we get exactly the \infty-category of \infty-groupoids (read: homotopy types, anima, "spaces", etc.)

view this post on Zulip Chris Grossack (she/they) (Oct 26 2025 at 16:25):

This turns out to be a very very useful notion, and the whole of homotopy theory is named after it. Moreover, this is where the story connects back to the question of "equality", "isomorphism", and "equivalence"!

view this post on Zulip Chris Grossack (she/they) (Oct 26 2025 at 16:29):

In a very precise way (see: [[nerve]]) we can show that

and just like many of the most useful invariants of topological spaces can be defined on their homotopy class, we see that many of the most useful invariants of categories can be defined at the level of equivalence.

view this post on Zulip Chris Grossack (she/they) (Oct 26 2025 at 16:32):

There are still reasons to consider "strict categories", which have a notion of equality on objects and whose correct notion of "sameness" is isomorphism, but experience shows that working up to equivalence is usually what we want to do. For one, this lets us prove theorems that match our intuition (eg. the categories of matrices and of linear maps between finite dimensional vector spaces are equivalent)

view this post on Zulip Chris Grossack (she/they) (Oct 26 2025 at 16:38):

One price we pay is that we can't talk about the underlying set of objects of a category, or ask questions about which objects are "equal" -- when working up to homotopy this doesn't make sense for the same reason that R\mathbb{R} is homotopy equivalent to a point, so their underlying sets are very very different... But this "price" turns out to be a benefit in disguise! By only knowing the underlying groupoid (considered up to homotopy) of objects, the "[[generalized the]]" is made precise. After all, there might be multiple terminal objects (etc.) but we're only supposed to talk about the groupoid of such things, and if that groupoid is equivalent to the terminal groupoid with one object and only the identity arrow, then we might as well say there's only one terminal object!

view this post on Zulip Chris Grossack (she/they) (Oct 26 2025 at 16:39):

Hopefully this was helpful! I have some things to say about "an equivalence existing" vs "choosing an equivalence", but my parents are visiting and I should hang out with them. I'll say more soon if nobody beats me to it!

view this post on Zulip Alex Kreitzberg (Oct 26 2025 at 16:48):

Thank you! Enjoy the time with your parents.

I appreciate you clarifying that using the equality notation for equivalence amounts to insisting I won't use said notation for propositional equality when "it doesn't make sense".

Which is an easy mistake to make because we're so used to thinking of categories strictly.

Your proof sketch about homotopy group preservation being equivalent to homotopy invertibility also reminded me of arguments showing that maps which preserve distance must be invertible. I hadn't internalized that as defining automorphisms by the properties they preserve.

Thank you for your detailed answer, it seems to make sense to me, and interacts with all the various pieces I was trying to understand above. I'll spend a bit of time thinking about it, again thank you!

view this post on Zulip Mike Shulman (Oct 27 2025 at 05:41):

John Baez said:

I think homotopy type theorists started out being rather gung-ho about saying C=DC = D to indicate that there is an equivalence from CC to DD, based on the univalence axiom, but then attitudes changed.

This is interesting. It does seem to me also that even homotopy type theorists rarely write == to mean equivalence. Personally, I think the main reason for that is that up until now, they've been using formal systems that basically force you to distinguish equality of types from equivalence of types, despite the univalence axiom.

Specifically, in Book HoTT and in Cubical Type Theory, while you can make an equivalence of types into an equality of types, the resulting equality only remembers the equivalence you started from up to homotopy. This is seriously annoying, so people working in those systems tend to stick with equivalences of types and only make them into equalities when they're forced to apply univalence for some specific purpose.

Improving this situation is one of the motivations behind Higher Observational Type Theory. This system has what I call "definitional univalence": if you make an equivalence into an equality of types, the equality remembers exactly at least the two functions underlying the equivalence, not just up to homotopy. I hope and conjecture that when using H.O.T.T. it should be more feasible to actually use equalities of types everywhere instead of equivalences, and as this becomes more common, homotopy type theorists will get more comfortable writing "=" for equivalences.

view this post on Zulip Alex Kreitzberg (Oct 27 2025 at 06:03):

My takeaway is the axiom is deeper than just a notational convenience, because it can be essential. And that my understanding was the intended goal but, like Baez said, there's some technical fuss in the way of that dream.

So I was backwards. At least for the moment, equality everywhere is easier on paper :relieved:

view this post on Zulip John Baez (Oct 27 2025 at 17:08):

I didn't say any of this stuff was "technical fuss". I'd say we're talking about important conceptual stuff here: questions about words like "is" and "the same". I say something is "technical fuss" if it's the equivalent of trying to find the right kind of USB port to stick into something - boring, but you have to do it correctly or you get in trouble. What we're talking about here is more like philosophy, but incarnated in mathematics.

view this post on Zulip Alex Kreitzberg (Oct 27 2025 at 17:18):

Sorry! You're right I misrepresented what you said.

I was just trying to acknowledge you were right to suspect Homotopy Type theorists weren't blanketly using equality for equivalence.

I internalized Shulman's point to be that it was still the goal to make it possible for Homotopy type theorists to use equality everywhere, but it didn't quite work today for what sounded like (to me) fussy reasons.

This is an aside, but I'm shocked to what extent programming language issues are analogous to philosophical problems. Equality in normal software is a mess, HoTT's general approach feels much better than what's typical.

view this post on Zulip Alex Kreitzberg (Oct 27 2025 at 17:47):

You know, I might go so far as to suggest your USB example might have some connection to this conversation.

I've argued to folks we're being too careless, because we're treating different usb devices as if they were "the same" by making our ports too permissive.

view this post on Zulip Kevin Carlson (Oct 27 2025 at 18:13):

Well, it would hardly work to have different ports for every possible device! A USB port is an interface; the whole idea is that many different kinds of systems can have the same interface. Without that principle, you can't have any modularity in your engineering; every system has to be grown as an organic whole.

view this post on Zulip Alex Kreitzberg (Oct 27 2025 at 18:22):

I don't want to get too hung up on this in this thread. But I have a drawing tablet with a USB-C port on the tablet that expands into 4 distinct out ports, so you still have to buy a dedicated cable which defeats the point there. Apple's lightning USB-C cables are off standard I believe? I had to navigate whether they borked preamps I was considering buying.

Somehow there's tension between how much power the cable should support, and how much data. That has to be balanced against the power and data device AA needs vs how much power and data device BB can supply, or vice versa.

Of course you need some standard, I'm not against standards, what I'm saying is I've playfully thought about "static type disciplines" for ports. And now that Baez brought it up as a point of comparison, I wonder how much this question amounts to deciding when two ports should be considered isomorphic.

view this post on Zulip Alex Kreitzberg (Oct 27 2025 at 18:29):

It's funny when I tried to explain my intuition about this to a friend they trolled me with this video:

(Replace everything with USB-C)
https://youtu.be/At0KjsYMsi0?si=49ZTMJZ6MuvWpKx1

view this post on Zulip Alex Kreitzberg (Oct 27 2025 at 18:31):

It'd be like if in the "cooperative design" paper that uses Profunctors, if everywhere they used power they replaced it with "USB-C" and put "?" for the weight.

view this post on Zulip Alex Kreitzberg (Oct 27 2025 at 23:40):

I watched this lecture by Shulman: https://youtu.be/xx9Y3-WJs4Y?si=mPbkGWJrPj4-0lxi

It clarified to me that "Book HoTT" doesn't have canonicity and in particular doesn't have a computational interpretation, and that Cubical HoTT, although it has canonicity it does so at the price of manually adding higher combinatorial structure. Motivating Shulman's work on Higher Observational Type Theory. Which hopefully will keep convenient uses of univalence and still have a computational interpretation.

So what I referred to as a "fussy inconvenience" is a pretty serious issue in this setting.

view this post on Zulip Alex Kreitzberg (Nov 08 2025 at 00:44):

This seems to be related to the same ideas, but I don't think it's exploring the groupoidal aspects I was curious about here:

Invariance Under Isomorphism and Definability - Per Martin-Löf:
https://youtu.be/VDreWuWDUu0?si=u4wZuWML5KaAGWUG

view this post on Zulip Alex Kreitzberg (Nov 08 2025 at 01:15):

I guess this is specific to the details of Martin Lof Type Theory, and in particular the ideas of the argument would have to be translated to see how they would relate to Homotopy Type Theory. These ideas are probably discussed at length in the HoTT Book or elsewhere

I don't think I fully appreciated how much of a logical question "the same but different" was.

So at the moment my impression is, to understand the relationship between groupoids, and precise discussions of "the same", HoTT is the thing to understand.

view this post on Zulip John Baez (Nov 08 2025 at 10:17):

HoTT takes one approach to these questions, and there are others - but it's the most popular and well-developed approach, so it's good to understand.

view this post on Zulip Alex Kreitzberg (Nov 08 2025 at 18:26):

I've been consistently confused by understanding categorical ideas "up to equivalence", I don't think I noticed that I somehow asked the same question but from the point of view of groupoids.

So, I guess adjunctions are interesting because, unlike equivalences, you can translate or convert structures that aren't "the same", but in an optimal way?

But then when you make that jump we're no longer talking about homotopical structures in a classical sense.

view this post on Zulip Alex Kreitzberg (Nov 08 2025 at 20:07):

I guess back to the main theme

It's undecidable to determine whether two groups are isomorphic, so they are different with respect to their definitions. I have to specify an isomorphism to see they're "the same", both because it could be hard for a computer to find, and because there could be more than one choice.

After specifying such an isomorphism, because of stuff I've and Grossack already said, there's at least one story for how to treat this isomorphism like equality. In particular definitional equality is the basic one, from which isomorphic equality depends. This clarifies in what way "isomorphic" can be thought of as "the same".

view this post on Zulip Alex Kreitzberg (Nov 08 2025 at 21:25):

Okay!

So what's neat about a universal property, is given any two objects that satisfy such, it tells you how to find a unique isomorphism between them.

Just like how in geometry, if two triangles have the same lengths for three sides, then one can find an isometry that carries one over to the other. In both cases constructions done on one, can be automatically carried over to the other. Though in geometry, this criterion can be "worse" than for universal properties, because some triangles are symmetrical, making the isometry chosen ambiguous.

It's strange how something so beautiful "symmetry" is sort of annoying depending on your point of view.

view this post on Zulip Alex Kreitzberg (Nov 09 2025 at 04:00):

This nlab page seems to be about my question specifically:
[[Structure identity principle]]

view this post on Zulip John Baez (Nov 09 2025 at 14:12):

So, I guess adjunctions are interesting because, unlike equivalences, you can translate or convert structures that aren't "the same", but in an optimal way?

In two different optimal ways: the "best approximation from above" and the "best approximation from below". I suggest trying my explanation of adjunctions in lectures 4 and 5 of my applied category theory course. I'm only talking about adjunctions between preorders, which are sometimes called "Galois connections", but the morals apply much more generally to all adjunctions. The punchline:

Okay: I've told you what a Galois connection is. But now it's time to explain why they matter. This will take much longer - and be much more fun.

Galois connections do something really cool: they tell you the best possible way to recover data that can't be recovered.

More precisely, they tell you the best approximation to reversing a computation that can't be reversed.

Someone hands you the output of some computation, and asks you what the input was. Sometimes there's a unique right answer. But sometimes there's more than one answer, or none! That's when your job gets hard. In fact, impossible! But don't let that stop you.

THE DIFFICULT WE DO IMMEDIATELY.
THE IMPOSSIBLE TAKES A LITTLE LONGER.

view this post on Zulip Alex Kreitzberg (Nov 10 2025 at 05:29):

I reviewed your notes, and I believe I'm understanding them better than the first time I read them sevenish years ago. I may as well read the rest on adjunctions while I'm at it.

I think my question/thought was inspired by the database discussion from that course. If you had an isomorphism between databases you'd just carry the results of your transforms across the isomorphism.

But adjunctions let one convert databases between distinct schemas, so they're a bit more magical.

view this post on Zulip John Baez (Nov 10 2025 at 10:26):

Right. There's no perfect way to do it, but there are two ways to do your best, which are analogous to "best approximation from above" and "best approximation from below" (terminology that makes sense for adjunctions between preorders).

view this post on Zulip Alex Kreitzberg (Nov 10 2025 at 21:24):

Can I say that sharply,

Adjunctions generalize the 2-categorical notion of equivalence.

ff is left adjoint to gg if

f(a)bag(b)f(a) \leq b \Leftrightarrow a \leq g(b)

And ff is right adjoint to gg if

g(b)abf(a)g(b) \leq a \Leftrightarrow b \leq f(a)

I want to convert the preorder A\mathcal{A} into the preorder B\mathcal{B}. I'd like an equivalence, but if I don't find one of those, maybe I can find an adjunction.

If f:ABf : \mathcal{A} \rightarrow \mathcal{B} has a right adjoint g:BAg : \mathcal{B} \rightarrow \mathcal{A}. What does that mean?

If ff and gg formed an equivalence, I could say the "preorders are the same". Additionally an arbitrary element aa in A\mathcal{A} has a corresponding bb that acts "the same" in B\mathcal{B}. This correspondence is identified by the maps f(a)=bf(a) = b or a=g(b)a = g(b), with both logically equivalent as relations.

But instead we have an adjunction, so the story has more features. We still have the analogous relationship f(a)bag(b)f(a) \leq b \Leftrightarrow a \leq g(b), so what do these say about how the elements and how the preorders are related?

Well with ff thought of as given, this defines g(b)=sup{a:f(a)b}g(b) = \textrm{sup}\{ a : f(a) \leq b\} which is the best lower bound of bb with an aa interpreted as an element of B\mathcal{B} via ff. So for any bb, g(b)g(b) gives an optimal lower bound of bb via some aa through ff.

Because this is true for all bb in a natural way - I'd like to say therefore A\mathcal{A} is a lower bound of B\mathcal{B}, relative to ff and gg. Perhaps this motivates making adjunctions into arrows of a category.

An aside I want to leave here as a note.

If I have a bb, the closest I can get to it from A\mathcal{A} via ff is f(g(b))f(g(b)). And because the arrow f:ABf : \mathcal{A} \rightarrow \mathcal{B} is left adjoint to gg - we have f(g(b))bf(g(b)) \leq b.

Functors convert objects, but also categories if they're nice enough, somehow I'm confusing these with isomorphisms within one category, which are pairs of inequalities in preorders. I'm still getting levels confused.

view this post on Zulip Alex Kreitzberg (Nov 11 2025 at 20:36):

I'm going to move on from this thread, as a note for the future the following readings were helpful:

[[Homogenous space]]

[[Klein geometry]]

and

[[Erlangen program]]

As well as Mac lane's chapter on geometry from "Mathematics: Form and function". In particular the sections on groups.