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.
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 -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.
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 , 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).
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
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 . 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 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).
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".
Yeah, that's an important clarification. Especially since "group up to conjugacy" is a useful way that groupoids naturally show up
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?
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.
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.
Since Chris is talking about tensoring representations of different symmetric groups, I figure they must be talking about how , the groupoid of all finite sets and bijections, is symmetric monoidal under disjoint union. Thanks to this , the category of representations of the groupoid , gets a [[Day convolution]] symmetric monoidal structure.
is the coproduct of connected components, one for each . Call the th connected component , since it's equivalent to the one-object groupoid where the automorphisms of that object are the symmetric group :
Thus
and is usually called the category of representations of .
The Day convolution monoidal structure lets you tensor a representation of and one of and get one of . This is usually called 'induction', since you can define it an [[induced representation]].
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 of .
Also, I think, Chris, that another nice example of groupoid to have in mind, besides Path Groupoids, is the Action Groupoid , associated to any (non necessarily transitive) -set , used by Alain Connes among others. Its sets of objects is and its arrows are the triples where , and . This groupoid allows you to do "geometric induction", without choosing a fixed subgroup of , from a representation (quite often a linear character) of to . This is most useful to construct "Gelfand Models" for the linear complex representations of . More details in this arXiv preprint In the case of the relevant -set is the set of all involutions in on which acts by conjugacy. The action groupoid has an easy to guess nice linear character...
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 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.
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 and two Functors , the naturality condition gives . When become single object groupoids , the functors become homomorphisms , the arrow becomes an arbitrary , and the natural transformation is given by just one arrow, from . Which gives for all .
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 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 .
So I think, we have , or (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 , 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 arises in a natural way as the orbit equivalence relation of some groupoid over . Instead of dealing directly with the orbit space as an object in the category of sets and mappings, one should consider instead the groupoid itself as an object in the category 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.
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.
Nobody should ever say "groupoids as a member of Cat".
A moment of haste when writing can produce minutes of annoyed head-scratching for dozens of readers.
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.
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!"
Is that still ambiguous?
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.
Two things make the phrase "groupoids as a member of Cat" feel to me like fingernails rubbing on a blackboard:
Each one requires me to choose a way to correct the phrase, so I can get a phrase I can understand.
"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 gives a one-object groupoid , 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 for some group iff it's a pointed connected groupoid.
There are better things to say....
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.
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".
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!)
A pointed category is a category with one of its objects specified . The objects of are arrows in that start at . Given two objects and , an arrow between them in is an , making the implied triangle commute : .
When our pointed category is a groupoid, the objects determine the arrow, in the above we'd have .
This limits the natural transformations between our functors heavily. If I have two functors a potential natural transformation between them, is determined by their values on objects therefore if we have a natural transformation it's x component would be . 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 is the image of a groupoid . 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 what exactly is the "delooping" ? 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.
Thanks for straightening this out! I never really had.
The delooping of a group is the corresponding one-object groupoid: the groupoid with one object , one morphism for each , with composition of morphisms being multiplication in .
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.
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
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.
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.
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?
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?'
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 -category as an -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 -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 -groupoids is to learn Homotopy Type Theory then?
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?
What an adorable mascot!
(from: https://kerodon.net/)
Wiki-style textbooks about fields of math with cute mascots are the best nanogenre, there's also one with space cats!
Here's a relevant math.stackexchange question:
Textbooks on higher category theory
(Though I want to underscore I'm trying to understand -groupoids first, because I'm assuming they're easier to understand and more settled than arbitrary weak -categories)
Trying to understand -groupoids is approximately the same as trying to understand homotopy theory, since while -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:
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.
The first 40 pages are just category theory.
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 -groupoids (e.g. Kan complexes) for your purposes, since they're in a rush to get to -categories.
And for the third, the HoTT book is one obvious candidate.
I recently purchased the HoTT book, I'm impressed with Lulu's print quality!
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".
I think it's the opposite of gentle. It's like they left out the first few chapters.
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.
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.
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?
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 "up to congruence". I want to say and are simply "equal", but the story is complicated by the existence of symmetrical triangles like 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 , 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 - being a functor means it satisfies Leibniz's law:
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 -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 , we want to write 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 "isn't empty").
Am I getting this right, or are there critical details I'm messing up?
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.
Right, so if we establish that two categories and are equivalent, if we're very careful with what we mean by "=", then we can write understanding it implies for any 2-Functor 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 gives the same answer for isomorphic geometric configurations.
(I hope the following usage of core is right)
So maybe , could send a category to a set of connected components, with bijections as the default notion of "equality" for Set.
Then with "=" meaning "equivalence" would get mapped to with "=" meaning "bijection".
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.
Everything you said is right. Certainly the choice of equivalence affects the choice of bijection .
I think homotopy type theorists started out being rather gung-ho about saying to indicate that there is an equivalence from to , 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.
I'm curious what @Chris Grossack (she/they) or others think about my usage of equality in the above couple messages
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.
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.
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.
I'm also young enough to be very happy with writing to mean equivalence in any -category (this includes isomorphism in a -category as a special case), because I've internalized the idea that "equality on objects doesn't make sense" for (-)groupoids. So I'll add to the chorus of people who are happy with what you've written.
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
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 and to be "the same" if there's a transformation (read: function) (which will become an isomorphism) which moreover gives isomorphisms on all homotopy groups.
Now it turns out to be difficult to determine in advance if has this nice property, but there's a sufficient condition that happens to be necessary for nice enough spaces! In favorable cases, gives isomorphisms on all homotopy groups if and only if has a homotopy inverse ! 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 -category of -groupoids (read: homotopy types, anima, "spaces", etc.)
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"!
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.
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)
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 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!
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!
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!
John Baez said:
I think homotopy type theorists started out being rather gung-ho about saying to indicate that there is an equivalence from to , 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.
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:
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.
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.
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.
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.
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 needs vs how much power and data device 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.
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
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.
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.
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
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.
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.
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.
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".
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.
This nlab page seems to be about my question specifically:
[[Structure identity principle]]
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.
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.
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).
Can I say that sharply,
Adjunctions generalize the 2-categorical notion of equivalence.
is left adjoint to if
And is right adjoint to if
I want to convert the preorder into the preorder . I'd like an equivalence, but if I don't find one of those, maybe I can find an adjunction.
If has a right adjoint . What does that mean?
If and formed an equivalence, I could say the "preorders are the same". Additionally an arbitrary element in has a corresponding that acts "the same" in . This correspondence is identified by the maps or , with both logically equivalent as relations.
But instead we have an adjunction, so the story has more features. We still have the analogous relationship , so what do these say about how the elements and how the preorders are related?
Well with thought of as given, this defines which is the best lower bound of with an interpreted as an element of via . So for any , gives an optimal lower bound of via some through .
Because this is true for all in a natural way - I'd like to say therefore is a lower bound of , relative to and . Perhaps this motivates making adjunctions into arrows of a category.
An aside I want to leave here as a note.
If I have a , the closest I can get to it from via is . And because the arrow is left adjoint to - we have .
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.
I'm going to move on from this thread, as a note for the future the following readings were helpful:
and
As well as Mac lane's chapter on geometry from "Mathematics: Form and function". In particular the sections on groups.