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: Adjunction between sets and groupoids

Jade Master (Feb 18 2021 at 17:38):

Over in #values @Ben Sprott asked about the adjunction between sets and groupoids whose left adjoint sends a set to the groupoid whose objects are elements of that sets and whose morphisms are only identities. Is there something specific you would like to find out or compute about this adjunction?

Ben Sprott (Feb 18 2021 at 18:20):

Hi @Jade Master Thanks for starting this question. I would like to go through it in detail. In fact, I was interested in a functor that takes a set and maps it into Groupoid by turning every element in a given set into an object of a category and adds exactly one isomorphism between every pair of elements seen as objects in the category. We need to confirm that this is a well known example.

Let's start with how to compute the endofunctor on Set. Let's set up the question a bit.

$G : Set \rightarrow Groupoid$ takes a set and creates a groupoid where the objects are the elements of the set and for each pair of set elements we add one isomorphism between that pair of elements of the set considered as objects of the category.
$F: Groupoid \rightarrow Set$ takes a groupoid and returns a set by turning each object in the category into an element of a set. This is me guessing.

Next, we need some natural tranformations, but lets just confirm these basics.

John Baez (Feb 18 2021 at 18:22):

Jade Master said:

Over in #values Ben Sprott asked about the adjunction between sets and groupoids whose left adjoint sends a set to the groupoid whose objects are elements of that sets and whose morphisms are only identities.

That's a very important adjunction, but actually Ben had asked about the other famous adjunction between sets and groupoids. He wrote:

I am now more interested in the adjunction between Set and Groupoid where the functor takes a set, treats every element as an object, and returns a groupoid with exactly one iso between each object. I was told that this is one of two classic ways to have an adjunction between Set and Groupoid.

In this one the functor from sets to groupoids is the right adjoint.

Both adjunctions are important, and it's fun to compare them....

Jade Master (Feb 18 2021 at 18:26):

Oh whoops, yeah I misread.

John Baez (Feb 18 2021 at 18:28):

F means "free" which is often good way to think about a left adjoint; its partner is "U" for "underlying" which is often a good way to think about a right adjoint.

Jade Master (Feb 18 2021 at 18:28):

I think your two functors are correct. However yeah F is usually a left adjoint but in this case I'm pretty sure it's a right adjoint

Jade Master (Feb 18 2021 at 18:28):

Yeah what John said

John Baez (Feb 18 2021 at 18:29):

Hmm, Ben deleted his comment....

Ben Sprott (Feb 18 2021 at 18:29):

@Jade Master I think John's comment suggests that I have to change F , from set to groupoid, to the letter G, since F is reserved for the left adjoint. Is that right?

Jade Master (Feb 18 2021 at 18:30):

Yes sounds good. Not strictly necessary but it will make things clearer.

Ben Sprott (Feb 18 2021 at 18:30):

@John Baez Hi, sorry John, I am going fix my setup to address your point. Thank you!!

John Baez (Feb 18 2021 at 18:30):

Anyway, the adjunction between sets and groupoids that Ben proposes to investigate is a funny one, in that his particular functor from groupoids to sets does not feel "free", and its right adjoint from sets to groupoids does not feel underlying.

John Baez (Feb 18 2021 at 18:31):

However, if someone doesn't have a strong feel for "free" and "underlying", this doesn't matter.

Jade Master (Feb 18 2021 at 18:31):

It's true this is kind of a weird example. But it's still a fine one.

John Baez (Feb 18 2021 at 18:32):

More neutral commonly used letters for left and right adjoint are L and R. I don't think you can possibly beat that.

John Baez (Feb 18 2021 at 18:33):

Anyway, I'll try to stay out of this for a while!

Ben Sprott (Feb 18 2021 at 18:35):

So, we agree on the functors. We might want to explicitly state why they are adjoint.

In order to compute the monad, we need to compute the endofunctor on Groupoid which is
$F \cdot G : Set \rightarrow Set$

We may also want to consider the comonad on Groupoid:

$G \cdot F: Groupoid \rightarrow Groupoid$

John Baez (Feb 18 2021 at 18:36):

I can't resist interrupting yet again and saying: that's the hard way to show these functors are adjoint.

John Baez (Feb 18 2021 at 18:36):

It's fine to do it that way, but I wouldn't say "we need to" go this way.

John Baez (Feb 18 2021 at 18:37):

(I'm finding it irresistible to comment on this thread even though I want to let Jade take charge! I guess I just have strong opinions on all these things.)

Ben Sprott (Feb 18 2021 at 18:37):

@John Baez Sorry for my sloppy language. I meant as just a side note that we might want to explain why they are adjoint. Then on top of this, we want to compute the endofunctor. I didn't mean to say they were related.

John Baez (Feb 18 2021 at 18:38):

One way to show two functors F and G are adjoint are to think about FG and GF and their "unit" and "counit", and prove some stuff about these.

Another way is to show hom(Fx,y) is naturally isomorphic to hom(x,Gy).

John Baez (Feb 18 2021 at 18:39):

I find that 9 times out of 10, the second is easier if you have concrete descriptions of F and G.

John Baez (Feb 18 2021 at 18:42):

However, once you know F and G are adjoint, it's often interesting to think about the monad GF and the comonad FG, even if you didn't use those endofunctors to prove F and G are adjoint.

Jade Master (Feb 18 2021 at 18:42):

It's fine if you answer John, I'm a bit preoccupied right now.

Ben Sprott (Feb 18 2021 at 18:45):

I am not sure where the unit and co unit come from or how to get them. I will write them down with symbols:

$\epsilon : FG \rightarrow 1_{Groupoid}$
$\eta : 1_{Set} \rightarrow GF$

So, these are natural transformations that are defined by their components .

Jade Master (Feb 18 2021 at 18:49):

Yes, all correct so far.

Ben Sprott (Feb 18 2021 at 18:50):

At this point I need help. I have never understood natural transformations and have even convinced myself their presentation in Set is a problem and too complicated (though I know its just me).

Also, what is the definition of "Naturally Isomorphic"?

How am I going to prove that hom(Fx,y) is nat-iso to hom(x,Gy)? Do I find a natural iso?

Sorry if this sounds irritated. Thanks for all your help @John Baez @Jade Master

John Baez (Feb 18 2021 at 19:04):

I'm trying desperately to let Jade run this, but:

How am I going to prove that hom(Fx,y) is nat-iso to hom(x,Gy)? Do I find a natural iso?

My favorite general strategy:

First figure out what these sets hom(Fx,y) and hom(x,Gy) are. Then convince yourself that they're isomorphic. The isomorphism you discover will then, 98% of the time, be natural.

John Baez (Feb 18 2021 at 19:04):

This isomorphism will then give you the unit and counit you seek... but don't rush into that yet, that's another story.

Ben Sprott (Feb 18 2021 at 19:18):

$hom(Fx,y)$ is the set of morphisms between $Fx$ and $y$. $Fx$ is a set made from a groupoid as described and $y$ is any set. $hom(x,Gy)$ is the set of morphisms from $x$ to $Gy$. $Gy$ is a groupoid made from a Set as described. So we are talking about a homobject in Groupoid and a homobject in Set, but really, we are defaulting to the idea that the theory of categories is presented in Set so everything is just sets and functions, so they are both homsets. To know what a set is, amounts, I think, and especially when talking bout whether there is an iso between two them, to knowing what the cardinality of each set is. So, am I trying to calculate the cardinality of each of these homsets? Is there another way to know something about a homset?

Morgan Rogers (he/him) (Feb 18 2021 at 19:23):

You don't just want to know how many they are, you want to know what they are. A "morphism between $Fx$ and $y$" is just a function, whereas a morphism from $x$ to $Gy$ is a groupoid homomorphism (equivalently, a functor).

Morgan Rogers (he/him) (Feb 18 2021 at 19:24):

To find the isomorphism, you need to work out how to turn any function $Fx \to y$ into a functor $x \to Gy$, and vice versa.

Ben Sprott (Feb 18 2021 at 19:31):

This, sort of, forces you to define, or forces you to use the definition of how the functors act on morphisms....which I haven't spoken about yet.

Nick Hu (Feb 18 2021 at 19:31):

The most common definition of natural transformation I reach for in this instance is a family of morphisms.
That is, given functors $F, G\colon\mathscr{C} \to \mathscr{D}$, a natural transformation $\alpha\colon F \Longrightarrow G$ is given by a family of $\mathscr{D}$-morphisms parametrised by $\mathscr{C}$-objects: $\alpha_c\colon F c \to G c$ subject to a naturality constraint. A lot of the time you only need to think about the first part, and the second part turns out to be true anyway.

When a natural transformation admits an inverse, it is called a natural isomorphism. In this case, asking for those sets to be 'naturally isomorphic' means asking for the bijection on Hom-sets to be sufficiently nice (natural, i.e. making no arbitrary choices). For instance, every (finite dimensional) vector space $V$ is isomorphic to its dual, but not naturally so because you have to choose a basis (however, every finite dimensional vector space is naturally isomorphic to its double dual). A 'natural isomorphism' between sets is a bit vague; really, it's encoding some statement of natural isomorphism between functors, but that's a technical detail that isn't very elucidating.

Amar Hadzihasanovic (Feb 18 2021 at 19:37):

John Baez said:

I find that 9 times out of 10, the second is easier if you have concrete descriptions of F and G.

It's interesting to hear that! My own experience is different -- I guess it goes to show that we all have our personal approach to doing things.

I find the $\mathrm{Hom}(Fx,y) \simeq \mathrm{Hom}(x,Gy)$ approach really useful when I know one of the functors and have to figure out the other; like, if I know $G$, I will try to think what $F$ could be on some simple objects $x$ so that morphisms from $Fx$ to $y$ correspond to morphisms from $x$ to $Gy$.
But if I already have two functors $F$ and $G$, and suspect that they may be adjoint, then I will always try to see if there is a natural choice of morphism $FGx \to x$ or $x \to FGx$... that has the advantage of involving only one arbitrary object $x$ in a single category, rather than two arbitrary objects in two categories; and most of the time, if there is a natural choice of unit or counit then there will also be a natural paired counit or unit.

Nick Hu (Feb 18 2021 at 19:38):

I too find the unit/counit approach much easier to think about (in general) than natural bijections between Hom-sets - maybe not so surprising as Amar was my first teacher in category theory!

Morgan Rogers (he/him) (Feb 18 2021 at 19:53):

But the composite functor $FG$ is typically more complicated (by virtue of being a composite) than the individual functors. Each perspective has its uses. In this case either approach works well.

John Baez (Feb 18 2021 at 19:55):

Ben Sprott said:

So, am I trying to calculate the cardinality of each of these homsets?

No, you're trying to say very clearly and simply what an element of each homset actually is. You should start with a general abstract description of the homsets, as you've done, but then make it more and more explicit using all the facts you have in hand, until you see what their elements "really are".

That's often how calculations in category theory work. In this case the final answers are very simple.

John Baez (Feb 18 2021 at 19:56):

When you get the final answers, you'll know it, because you'll have the feeling "oh - so that's all it is???"

John Baez (Feb 18 2021 at 19:58):

So tell me: if $X$ is a groupoid and $Y$ is set, what are elements of $\mathrm{hom}(F X, Y)$?

John Baez (Feb 18 2021 at 19:59):

(I'm gonna makes $X$ and $Y$ be upper-case so we can call an element of $Y$ something like $y$, etc.)

Nick Hu (Feb 18 2021 at 20:00):

I think someone also ought to point out that there is a third 'flavour' of adjunction that is commonly used: the presentation in terms of universal morphisms (initial objects in some comma category). This one has a more traditional math-y style (so I'm told), but I always found it rather meaty. There's a nice article here which relates the three approaches: https://www.hedonisticlearning.com/posts/styles-of-category-theory.html

Ben Sprott (Feb 18 2021 at 20:05):

So tell me: if $X$ is a groupoid and $Y$ is set, what are elements of $\mathrm{hom}(F X, Y)$?

These are functions. I need to think a bit to say exactly what these functions are....are they isomorphisms?

John Baez (Feb 18 2021 at 20:09):

Yes, they are functions. But then:

First of all, functions from what to what? Saying they're functions is not good enough if you don't say from what to what.

John Baez (Feb 18 2021 at 20:09):

Second of all, are they required to be isomorphisms?

John Baez (Feb 18 2021 at 20:10):

The trick is to spell out everything in perfect detail. Exactly what are the elements of $\mathrm{hom}(F X, Y)$? You need to say it so clearly that we can look at anything in the universe and tell if it's an element of $\mathrm{hom}(F X, Y)$ or not.

Ben Sprott (Feb 18 2021 at 20:15):

I don't know what exactly "we" know about $\mathrm{hom}(F X, Y)$. To me, it just looks like two sets and so the homset is just all functions between two sets. What is the extra information I am missing? $FX$ is a set which we got by taking a groupoid $X$ and treating every object like a set element. $FX$ is the object-set of the groupoid X, in the sense that we present categories as a set of objects and a set of morphisms.

John Baez (Feb 18 2021 at 20:15):

Okay, you've told me what the set X is: it's the set of objects of the groupoid X. Good!

John Baez (Feb 18 2021 at 20:15):

That is half the answer to my question "functions from what to what?"

Ben Sprott (Feb 18 2021 at 20:16):

$Y$ is just a placeholder for any set, isn't it?

John Baez (Feb 18 2021 at 20:16):

This sort of math doesn't require sneaky tricks, just a lot of patience and the willingness to accept the fact that everything you need to know is right in front of you.

Nick Hu (Feb 18 2021 at 20:16):

John Baez said:

Okay, you've told me what the set X is: it's the set of objects of the groupoid X. Good!

I think you mean 'the set $F X$'

John Baez (Feb 18 2021 at 20:17):

Right, I meant the set F(X).

John Baez (Feb 18 2021 at 20:17):

Okay, so this was the answer to my first question, Ben:

$\mathrm{hom}(FX, Y)$ is the set of functions from the set of objects of the groupoid $X$ to the set $Y$.

John Baez (Feb 18 2021 at 20:18):

That is the answer I was looking for; you need to get in the habit of patiently writing sentences like that (or at least thinking them).

Ben Sprott (Feb 18 2021 at 20:18):

@John Baez Thanks for your patience!

John Baez (Feb 18 2021 at 20:19):

Sure: I'm trying to teach you patience.

Oh, but wait - my second question! You suggested that maybe $\mathrm{hom}(F(X), Y)$ consists only of isomorphisms from the set of objects of the groupoid $X$ to the set $Y$. Is that true?

John Baez (Feb 18 2021 at 20:20):

Ben Sprott said:

So tell me: if $X$ is a groupoid and $Y$ is set, what are elements of $\mathrm{hom}(F X, Y)$?

These are functions. I need to think a bit to say exactly what these functions are....are they isomorphisms?

Ben Sprott (Feb 18 2021 at 20:28):

Oh, but wait - my second question! You suggested that maybe $\mathrm{hom}(F(X), Y)$ consists only of isomorphisms from the set of objects of the groupoid $X$ to the set $Y$. Is that true?

I think not. We don't have any restrictions on these homsets as far as I can tell. It was just a guess.

John Baez (Feb 18 2021 at 20:28):

Right, there's no such restriction.

John Baez (Feb 18 2021 at 20:28):

Just checking. :upside_down:

John Baez (Feb 18 2021 at 20:29):

Okay, so we've got this:

$\mathrm{hom}(FX, Y)$ is the set of functions from the set of objects of the groupoid $X$ to the set $Y$.

The next step is for you to figure out $\mathrm{hom}(X,GY)$, and describe it in just as precise a manner.

Ben Sprott (Feb 18 2021 at 20:30):

So then $hom(X, GY)$ is the set of functors from a groupoid $X$ to a groupoid $GY$. $GY$ is the groupoid found by taking a set and treating each element as an object and adding one isomorphism into the groupoid for each pair of set elements seen as objects of the groupoid.

We can guess at the existence of an isomorphism by starting with the fact that functions map set elements to set elements and functors map objects to objects. In this case, the set elements of $FX$ is the same size as the object set of the groupoid $X$. Likewise, the groupoid $GY$ has an object set which is the same size as the set $Y$. Since the cardinalities are the same on both sides, then the homsets would contain the same number of elements and as such there is an isomorphism between $hom(FX, Y)$ and $hom(X,GY)$.

Something like that?

John Baez (Feb 18 2021 at 20:39):

This sounds great!

One point: I would avoid cardinality arguments. Cardinalities let you prove two sets are isomorphic, but they don't give you an isomorphism. This is why numbers were invented, actually: to prove sets are isomorphic without establishing an isomorphism. They're convenient, but here we're aiming for an actual specific isomorphism between $\mathrm{hom}(FX,Y)$ and $\mathrm{hom}(X,GY)$.

John Baez (Feb 18 2021 at 20:40):

So you gave me a nice description of $\mathrm{hom}(X,GY)$:

So then $hom(X, GY)$ is the set of functors from a groupoid $X$ to a groupoid $GY$. $GY$ is the groupoid found by taking a set and treating each element as an object and adding one isomorphism into the groupoid for each pair of set elements seen as objects of the groupoid.

Now we can and should simplify this description, using both sentences you wrote. Eventually we'll get a much simpler description of $\mathrm{hom}(X,GY)$.

Ben Sprott (Feb 18 2021 at 20:42):

John Baez said:

So you gave me a nice description of $\mathrm{hom}(X,GY)$:

So then $hom(X, GY)$ is the set of functors from a groupoid $X$ to a groupoid $GY$. $GY$ is the groupoid found by taking a set and treating each element as an object and adding one isomorphism into the groupoid for each pair of set elements seen as objects of the groupoid.

Now we can and should simplify this description, using both sentences you wrote. Eventually we'll get a much simpler description of $\mathrm{hom}(X,GY)$.

$hom(X, GY)$ is the set of functors from a groupoid $X$ to a groupoid $GY$, who's objects are the elements of set $Y$ with exactly one isomorphism between any two objects.

John Baez (Feb 18 2021 at 20:43):

$GY$ is not just any old groupoid whose objects are the elements of $Y$.

John Baez (Feb 18 2021 at 20:44):

Okay, I like that better. (I think it's less confusing if you type a new answer instead of going back and changing your old answer.)

John Baez (Feb 18 2021 at 20:46):

Here's how I might say it:

$\mathrm{hom}(X, GY)$ is the set of functors from the groupoid $X$ to the groupoid $GY$ whose objects are the elements of the set $Y$ and having exactly one isomorphism between any two objects.

But you can simplify this a lot more!

John Baez (Feb 18 2021 at 20:47):

To simplify it, you need to think about what these functors are actually like.

Ben Sprott (Feb 18 2021 at 20:49):

Here is a thought about an isomorphism from $hom(X, FY)$ to $hom(GX, Y)$. We take the functor in $hom(X, FY)$ and look only at how it acts on sets, forgetting how it acts on morphisms. This produces a function from from $GX$ to $Y$.

Morgan Rogers (he/him) (Feb 18 2021 at 20:53):

That sounds like the right thing in that direction. What about the other direction?

John Baez (Feb 18 2021 at 20:54):

That's a very good thought, Ben. So then the question is why that business of only remembering what your functor does to objects doesn't lose any information!

John Baez (Feb 18 2021 at 20:55):

If it lost information we'd get a natural transformation but not a natural isomorphism between homsets.

John Baez (Feb 18 2021 at 20:56):

This is why I was trying to get you to ponder what a functor from $X$ to $FY$ is really like.

John Baez (Feb 18 2021 at 20:57):

By the way, when you said "look only at how it acts on sets", you probably meant "look only at how it acts on objects".

Ben Sprott (Feb 18 2021 at 21:04):

John Baez said:

To simplify it, you need to think about what these functors are actually like.

Well, we can look at two objects $x_i, x_j \in X$ and how they map to two objects in $gy_i, gy_j \in GY$ and we can also look at the homset $hom(x_i, x_j)$ and say that this homset is all mapped to a single morphism, the only one we find in $hom(gy_i, gy_j)$. What we can now say is that there is only one way to do that.

John Baez (Feb 18 2021 at 21:06):

Right! Because of how we've defined $GY$, there's no choice about how morphisms in $X$ get mapped to morphisms in $GY$, once you know how the objects of $X$ were mapped to objects in $GY$. More precisely, there's exactly one choice of how to map the morphisms, for any way of mapping the objects.

This is the key to the whole business.

John Baez (Feb 18 2021 at 21:13):

Now the question is whether you can exploit this insight to get a bijection between $\mathrm{hom}(FX, Y)$ and $\mathrm{hom}(X, GY)$, and then to prove this bijection is natural.

Ben Sprott (Feb 18 2021 at 21:18):

Morgan Rogers (he/him) said:

That sounds like the right thing in that direction. What about the other direction?

So, in the other direction we have a function in $hom(FX, Y)$ and we create a functor by again focusing on the objects/set elements. We say that the object part of the functor in $hom(X, GY)$ is just the function from $FX$ to $Y$. How the functor acts on morphisms is totally decided already since there is only one way to chose how a functor acts given that we have already specified how it acts on objects.

We now have to show that the two maps we defined between the homsets forms a bijection, ie that their composite is the identity.

David Michael Roberts (Feb 18 2021 at 21:21):

I want to amplify something said earlier, and it may help: instead of saying "there is a natural isomorphism $hom(FX,Y) \simeq hom(Y,GX)$, it might be better to say "there is an explicitly write-down-able function $hom(FX,Y) \to hom(Y,GX)$ that happens to be onto and one-to-one, and which satisfies a technical condition we can explicitly check after we've written down the funciton". (Or, sometimes, instead of "happens to beonto an one-to-one" we have "and we can explicitly write down its inverse")

And I'd like to strongly, strongly emphasise that arguments about isomorphisms of sets via cardinalities are almost always not what you want in category theory. In particular, looking at my revised definition above, the data is a specified concrete function, not just an anonymous isomorphism. In general, very general and central arguments or constructions like this one tend to work for richer contexts, where cardinality arguments either aren't available or don't work (like, for instance, where $hom(-,-)$ is a vector space, and you want a linear isomorphism)

David Michael Roberts (Feb 18 2021 at 21:23):

(And as I was writing that, Ben's comment landed)

Ben Sprott (Feb 18 2021 at 21:23):

David Michael Roberts said:

And I'd like to strongly, strongly emphasise that arguments about isomorphisms of sets via cardinalities are almost always not what you want in category theory. In particular, looking at my revised definition above, the data is a specified concrete function, not just an anonymous isomorphism. In general, very general and central arguments or constructions like this one tend to work for richer contexts, where cardinality arguments either aren't available or don't work (like, for instance, where $hom(-,-)$ is a vector space, and you want a linear isomorphism)

I keep doing it!!

John Baez (Feb 18 2021 at 21:26):

Ben Sprott said:

So, in the other direction we have a function in $hom(FX, Y)$ and we create a functor by again focusing on the objects/set elements. We say that the object part of the functor in $hom(X, GY)$ is just the function from $FX$ to $Y$. How the functor acts on morphisms is totally decided already since there is only one way to chose how a functor acts given that we have already specified how it acts on objects.

We now have to show that the two maps we defined between the homsets forms a bijection, ie that their composite is the identity.

Yes, this is a good way to show you've found a bijection between $\mathrm{hom}(FX, Y)$ and $\mathrm{hom}(X, GY).$

Another good way is to take one of the two maps you've described, and check that it's one-to-one and onto.

(This is what I was alluding to when I said one of the maps "doesn't lose information": that's an intuitive way of thinking about one-to-oneness.)

Fawzi Hreiki (Feb 18 2021 at 21:27):

Another useful fact is that adjoints compose (paired with the fact that they are essentially unique)

Nick Hu (Feb 18 2021 at 21:27):

John Baez said:

Another good way is to take one of the two maps you've described, and check that it's one-to-one and onto.

(By the way, this is a result of some form of the Axiom of Choice!)

John Baez (Feb 18 2021 at 21:29):

Yes, I'm gonna let myself use the Axiom of Choice and all the usual resources of classical mathematics when I'm talking to Ben Sprott, unless he says he wants to be a constructivist or intuitionist.

Nick Hu (Feb 18 2021 at 21:30):

I just thought it was relevant to our discussion that cardinalities aren't enough, and that you need to give a witness to the isomorphism

Ben Sprott (Feb 18 2021 at 21:30):

John Baez said:

Yes, I'm gonna let myself use the Axiom of Choice and all the usual resources of classical mathematics when I'm talking to Ben Sprott, unless he says he wants to be a constructivist or intuitionist.

lol, I'm just trying to get through this. But I read a lot of John L Bell and Chris Isham and a lot about Heyting algebra and for a long time I was very anti-classical. I had no idea what I was doing.

John Baez (Feb 18 2021 at 21:32):

Nick Hu said:

I just thought it was relevant to our discussion that cardinalities aren't enough, and that you need to give a witness to the isomorphism

Somewhat. In classical math you can define a specific isomorphism of sets by giving a function and proving it's one-to-one and onto. You can't do it by proving the two sets have the same cardinality.

John Baez (Feb 18 2021 at 21:34):

But in our particular example of $\mathrm{hom}(FX, Y) \to \mathrm{hom}(X, GY)$, the easiest way I know to show this function is onto is to show it has a left inverse. And Ben has given a candidate inverse.

John Baez (Feb 18 2021 at 21:35):

So he might as well just prove his candidate inverse is an inverse. Then the haters in the audience, who don't like the axiom of choice, won't start throwing tomatoes at us.

Nick Hu (Feb 18 2021 at 21:36):

I'm under the impression that this definition of isomorphism is more brittle, in the sense that when you categorify or weaken various aspects it might be no longer a good notion of "isomorphism". What you really care about is the isomorphism+inverse pair. It's not that I don't like Choice, but it's good to be aware (pro choice-choice)

John Baez (Feb 18 2021 at 21:39):

Right. I feel like I'm teaching someone to add and I've got experts in the foundations of mathematics listening, making comments about Peano arithmetic. But as long as Ben is happy it's fine.

Nick Hu (Feb 18 2021 at 21:40):

I tend to penalise my students for using proof-by-contradiction when they didn't need to, but perhaps that's me being overly pedantic...

John Baez (Feb 18 2021 at 21:40):

I usually take 'em down to the dungeon and whip 'em.

David Michael Roberts (Feb 18 2021 at 21:42):

To some extent, proofs in this space are like proofs in elementary abstract algebra, where you prove things like 0+0=0. It seems too trivial, but you really have to pay attention to the precise definitions and only work with what you have, importing no prior knowledge.

John Baez (Feb 18 2021 at 21:43):

Regarding contradiction: I get students who say "To prove P implies Q, assume P and not Q. Then from P, we show Q.... But not Q! So, by contradiction, P implies Q." They just love proof by contradiction.

John Baez (Feb 18 2021 at 21:44):

I don't formally penalise them, I just point out how this is sorta silly.

Ben Sprott (Feb 18 2021 at 21:47):

John Baez said:

So he might as well just prove his candidate inverse is an inverse. Then the haters in the audience, who don't like the axiom of choice, won't start throwing tomatoes at us.

I'm pretty tired. Thanks again everyone!

So we have this pair of maps between $hom(X, GY)$ and $hom(FX, Y)$ and here they are:

$f : hom(X, GY) \rightarrow hom(FX, Y)$, which works by taking the functor and only looks at how it maps the objects of $X$ to the objects of $GY$.
$g: hom(FX, Y) \rightarrow hom(X, GY)$, which works by taking the data about how a function maps set elements and producing a functor with that data being used to define how we map objects in the functor. We define no information about how we map morphisms because they are uniquely defined given the first data.

So we have to prove $f \cdot g = Id_{hom(FX, Y)}$ and $g \cdot f = Id_{hom(X, GY)}$.

John Baez (Feb 18 2021 at 21:47):

That's a great resting-place.

Ben Sprott (Feb 18 2021 at 21:49):

Thanks John!

David Michael Roberts (Feb 19 2021 at 02:53):

One suggestion, @Ben Sprott, I would strongly suggest (if you haven't already) getting https://www.maths.ed.ac.uk/~tl/bct/ and work through section 2.1, looking back at the previous chapter if need be. It goes through multiple examples, explains what an adjunction is in clear detail early on without a lot of machinery and so on.

David Michael Roberts (Feb 19 2021 at 02:58):

And, I should add, working through as many of the questions in chapter 1 would be really good exercise. To quote the intro:

As for the exercises, I join every other textbook author in exhorting you to do them; but there is a further important point. In subjects such as number theory and combinatorics, some questions are simple to state but extremely hard to answer. Basic category theory is not like that. To understand the question is very nearly to know the answer. In most of the exercises, there is only one possible way to proceed. So, if you are stuck on an exercise, a likely remedy is to go back through each term in the question and make sure that you understand it in full.

Ben Sprott (Feb 19 2021 at 03:38):

@David Michael Roberts I will look at that!!