Category Theory Informal Seminars, Bristol — Proving Yoneda Lemma
Recorded at Category Theory informal seminars, Bristol (2007), featuring John Mayberry, Richard Pettigrew. From the Michael Wright Collection, held by the Archive Trust for Research in Mathematical Sciences & Philosophy.
- Identifier
mw0000242-cc-b- Format
- Audio recording
- Collection
- Michael Wright Collection
- Repository
- Archive Trust for Research in Mathematical Sciences & Philosophy
- Rights
- Made available for personal scholarly use. Rights in recordings are generally held by the speakers or their estates. If you believe this recording infringes your rights, please contact [email protected].
Read the automatically generated transcript
This transcript was generated by speech-recognition software from an archival recording and has not been hand-corrected. It will contain recognition errors — particularly for proper names and technical terminology — so please verify against the audio before quoting. Timestamps play the recording from that moment.
0:00 Okay, well let's see if sometime between now and next Friday we can actually formulate that exactly. You can sort of see what Bobaki was trying to do. He was thinking, I mean, if you look at concrete categories, there are all kinds of weird things, anomalies that happen. I mean, what does this mean in more primitive terms? If you take the idea of a structure, a mathematical structure... Hello? How are you? We are, we just proved your neighbor's lemma so you can come and be wired by our sort of smoke nut. it's not very difficult actually it is it's exactly the problem he was talking about yeah we came up against the problem you were talking about evaluating functions rather than composing them so you're right you'll be coming back up love it, ok, see you in a second ok, bye I'm absolutely impressed So it's already impressive. Okay, let's go back to square one. Now, Pockty, all these idiot philosophers talking about structuralism. Let's talk about... Yeah, there's something really telling me that no philosopher at maths, barring Colin McClarty and maybe one or two others have ever mentioned Junaid Islam in the whole literature on structuralism I don't know that Collins mentioned it it does sound like it's pretty important
2:30 okay so what's going on here I think that the idea is that the most general sort of bone-headed definition of a mathematical structure is that it's a set or sets equipped with a morphology. The simplest cases are the algebraic and ordered ones where the morphology is just an operation on the underlying set. Or sets, for example, when you're doing vector spaces. And I suppose from that point of view that you'd want to think of the morphology. Say you're talking about vector spaces as structures. you'd want to think it's a structure with two underlying sets the scalars and the vectors and then on the scalars the scalars have a structure namely the field structure and the vectors have the group structure and you've got the axioms connecting them so you would want to include in your morphology enough to describe everything So I guess when you're talking about a real manifold, that you've got to include the, you've got to include, you've got to include the, the reason I'm asking I was saying I've got to conclude the reals as a structure so you have one underlying set as a set of reals but you've also got to do you've got to do and I don't think there's a kind of natural way of talking about indimensional things except just saying that I don't think there's a sort of internal definition of n-dimensional. Anyway, let's leave that aside. The point is, the Bobaki program was to sort of generalize that by, as I remember it,
5:00 I mean, basically, what you want to do is to, you want to talk about the elements. If these are the elements of the, in the case of the one underlying set, then you take a set theoretical fragment of a universe over it, and then the things have got to be everything that's part of the morphology has got to be an object somewhere in this structure. And it's a bit of a, I mean, it's more than a bit of a mess. It's a god-awful mess, because it's trying to do it in complete generality. Yeah. Okay, but so what's the vision that is popping up here is somehow that these these masses here will correspond to functors into the category of sets to produce the functors into the category of sets are going to, as it were, reconstruct the morphology. Because The idea is that you want, that you want, somehow what you want is that the objects of the category of whatever these general, this sort of arbitrary structure, you want the objects of this category to be a structure of this kind, and you want the amorphisms to be ordinary maps defined on the underlying set or sets of the structure into the underlying set of the other structure, right? So that's got to be the constant thing. So maybe you want there to be a single underlying set in every I mean, presumably, you could have weird morphisms of vector spaces, a weird kind of very sort of new-form version of a morphism of a vector space, which would have combined a linear
7:30 transition. Say you've got vector spaces over some field, and now you've got a morphism from that field into a smaller field, onto a smaller field, and now you combine a linear transformation on that field with one of these things. And so that would be amorphism in this more generous this sort of set up. I mean, does anybody really want to look at Bobocky's appendix? I wonder... No, I mean, I think the thing is, what is a concrete category? it's a it's a collection of objects and a constraint upon what counts as a morphism from one of these collections to another and the constraints are what we call a morphology but they could be I mean that's what's strange about the whole business because you know I mean, a concrete category has to be specified and set theoretically. You know, if you want to specify and set the category of groups, you've got to say what the group is, and then it's got to be set with a minor operation. You want to specify that you're always going to be grouped from the morphisms, you've got to say it for every two elements of the group. Yes, the ugly face of set theory keeps leering at you no matter how you try to escape it. That's why I think this business of thinking that it's a whole business as an attempt to get rid of set theory as a foundation is just a screwy way of looking at it. I mean, I actually think maybe the best way to say it would be that it's trying to, it's moving the whole picture of mathematical arguments and the vision of abstraction you have up one extra level, but it's still anchored in the old, in the same way of doing it. Well, I guess you do get these comical categories given by categorical axioms, don't you? So maybe you've not done that for data consistent and things.
10:00 You know, where you don't specify it as... I don't know. You don't specify, you don't say, it's objects are some sets, and the arrows are some functions between sets. You just give the axioms that specify what category is, and then append to those certain constraints on when you have morphisms of this sort than you have. I thought it's to some extent a kind of Well, I'll have to send you this piece by this Canadian guy because apparently the big change that took place in the 60s was La Vieira's thesis and one of the things two of the things that were supposed to come out of that thesis of adjoinness. And the second, and also, he invented something called algebraic categories, which are a sort of sort of categorical, category theoretical way of looking at algebra. Maybe that's what you're, maybe that's what you were sort of describing. Because there's not one of percent theory as well, Sorry, I don't know how to make it happen. I don't know. Yeah. Yeah, I mean... You can't do nothing. ...the category of sets. Well, yeah, I mean, it's just business of taking membership to be arrows from terminal objects. Right, okay. Because in the category of sets, singletons are terminal objects because given any set, there's only one a singleton okay so then so any singleton so so any terminal object in this category a map from that terminal object to another object is an element of that other object so the elements become maps from a and then you know these representations are unique up to isoborphism because, of course, there's only one map connecting two singletons. So, you know, so all that stuff.
12:30 And the third thing that this guy refers to is the attempt to axiomatize the category of categories and the category of sets. Now, that's where the thing impends on my consciousness. because both McLean and Laubierre in the 60s had a grotesquely inadequate view of what set theoretical foundations consisted in. That is to say, and both, I mean, well, there's sort of more up front about stuff. Well, no, McLean does it too, I mean, in this book. the problem then having gotten as far as they had the problem as they saw it was to produce a theory a first order theory of the category of categories which was like the first order theory of sats first order theory of the category of categories which was analogous to the first order theory of the category of sats I guess that's it Well, I mean, that's just completely inadequate. LaVere has abandoned all such ambitions. I think, I'm pretty sure. McLean kept on withering on about this stuff as up until the 80s, and he was still going on about how the axioms for a well-pointed Talpos would serve just as well as the axioms for Zermelo-Francol. Right. And, of course, it's perfectly true. They will. I mean, neither will serve at all, as I said, as a foundation for mathematics, except if it's true by default. but that's not what yeah that's not what he meant so I'm curious whether Wallbeer just abandoned all this is about categorical foundations
15:00 without explicitly saying so. And maybe just as it were restricted himself to constructions and arguments and so on that could be just explained in category-theoretic terms. without giving some kind of story about why all these assumptions that you make are true and so on. Right, yeah. So he sort of says, well, you go about it like this, and he seems to feel free to give examples. But when you're expounding this stuff, you're tempted to want to say, well, what does this mean in terms of I'm already familiar with? Yes, yes. This is an exciting new question. Actually, what it demonstrated was how little it has to do with understanding what the need of them is. Let's go any closer to understanding. But we've done the calculations. Richard has. uh... but the confusions arise because of this business you were talking about the difference between composing and evaluating yeah actually it wouldn't be a bad idea because then no but i mean can you raise the whole business without getting completely lost let's live dangers well it's all of course there's also less than a month we should read the book then. We'll figure it out. Maybe we'll figure it out for ourselves. The more virtuous... Well, have you... Did you get it from the book, or... and then... Well, the book... Well, no. He got it from the book by the following thing. He just noticed that what... But what Boissot does is to... Boissot does is to... Can you describe... He just describes. He shows that this function... calculates the inverse function to this thing he claims is an isomorphism. Okay. So, so that's the way to do it. Okay, so. Okay, so what are we trying to prove? So,
17:30 given categories, are we working with A or something, given A, and, and functor from A into set, and I'm also trying to prove that, um, and A, there, and, and, and, and, yeah, but he always thinks you can get, since we're working locally, small things, he always thinks you can get, well, no, no, no, no, don't put any restrictions, Oh, sorry, and, yeah, that's right. Yes, we've got and... And and. Yeah. Yeah. We can define. Define. Which takes... That's a natural transformation. Between that and that. Oh, yes, that's an isomorphic to that. OK, so we've got to prove it. So, firstly, is it obvious that the collection of these micro-transformations will be a set? Or is that just the consequence of this theorem that it turns out to be a set? That's a set. Now, it doesn't look like it should always be a set, actually. I don't think it is even, I don't think it even is a set. It's usually a class. Yeah, it's only once when you get... If A is large, it can't be a set. these damn things for every a. Right? Yeah. So that's already large, huh? Okay, so, but it's restrictive if f is a function such that it takes category into sat. But why is that restrictive? Well, because then you've got fewer natural transformations. I guess. I don't see why. I mean, this is not a set. I think we forget about all that crap. You know, each element of this is going to be a set. Yeah, but then, granted, yeah, every time.
20:00 I guess. Is that a match or something? Maybe not. Anyway, let's figure it out. No, I mean, I mean, the question is, is the left-hand side of this thing on the equivalence, is that part is that isn't even part of the that it's not bad happily here's a little bit we don't want to say it's not phi that maps this this is it's phi of this is that phi of this is that the function theta of f and a so a is fixed off, but it's theta sub f. No. Okay, so we fix A with any natural transformation into that. The point is that the set of natural transformations and the image of A under F are the same thing, the same size, that sort? Up to isomorphism. But the same size, yeah. The same size is just that size, isn't it? No, no, there might be a proper class of these things, but they would all, but, but, they would all... No, but remember, this is in set. So these have to, this is Stuart's question. This guarantees that this is set size, because this is in set, and it's isomorphic to this, byjective with this. Ah, because nat of that is just, let's see, nat... wasn't it fryer can you be surefire tablet I'll find it, sorry, B. Oh, yeah, a horn, a horn, a horn, a horn, a horn, sorry, and. Yeah, so given, given a category A in an object, A in it, and some puncture from A to somewhere else. To some puncture A in it particularly.
22:30 To some, well, no, to some, to some arbitrary category, to some arbitrary category B, um, what does Nat, what does this thing on the left-hand side look like? Yeah. particular is it a set? So if this wasn't a set, if this was some other category, B, then would you be guaranteed that this thing here even meant anything? Was a set. Or could it be a class? Is it this thing, this assumption that there is a function It's our friend. The cat's agreeing to sat, that's, um... It's hard to believe that it is, because you should even... you should just bring him to a plane. It's the last part to say, I don't know why we can just take... Well, it turns out we can prove this thing, but we don't even understand what it says. not on the philosophical sense of understanding what it says but just understand what it says on the absolute surface of it okay well let's try and yeah okay so the idea we can define this thing as a function of a and f but that goes without saying right I mean that yeah well Well, let's see what it is. Well, maybe we should say the weight bar soon, what? Phi should be phi sub a, a, a and f. Yeah, well, let's take that as red so as not to have experience. There are so many subscripts by the end of this time. That's a good one. The point is that the way we were trying to do it was use metal-ane's definition of this direction and should it's injecting a surjective. which is both what will work eventually, or so does it by defining this direction and then another function, the other direction, showing that one's the inverse of the other, and so that shows there's a bi-jection. So, um, so, define phi as follows. Right, so, phi of some natural transformation, alpha,
25:00 from this and to this. It's going to be alpha A, evaluated at 1A. OK, so let's draw up the thing first. So you don't need those down dots. OK, so A goes across to B. So this is, be at the moment this is for later okay so that's you up in your first category and then in B you have so this is not on set? Yes I'm on set Alpha by alpha into F of A, cross by F of A. Again, don't worry about this, but I'll come back to that. So that's a bit fine with that. And that's alpha B. So this is all set. OK, so the moment what you take some natural transformation alpha, then it's the value that this takes. You want to take this natural transformation alpha and take it something here. What you take is you take the identity element of A, so 1A up here, and then you take the value of alpha at that identity element. So the identity element is a member of this category, of omega. the function yes i did as a member of all right we can have a crack that down by the natural transformation because they are not transformation alpha and we give them as our first five yes we drag that down and we have now finally so it's a little bit of a what we want Yeah, because 1a is an element in the, this thing, is in the definition of 1a, this one has definitely got to be an f-a, okay, so that's your first function, and then your
27:30 second function, is going to take members of this, sorry, members of this, to match all transformations. Okay, so to specify a natural transformation, you have to specify its value at some element B, so B is going to be a member of a category, as a category, okay? Some member of a category. Hold on just a minute, so the little A there is something here, okay, so A in here. Okay, okay. And you're going to take it back to a natural transformation. So to specify the natural transformation, so this thing here is a natural transformation. So that's a natural transformation like alpha. Yeah. And then at the element B. Yeah. At the elementary element. And then what does it do at an element of B? Well, it takes an element of this into this. So you've got to know, so an element of this will look like this, F from A to B again. and so if you have F from A to B then you want to know a typical element of Oh, sorry, yes, yes, yes So it's a natural transformation so it's going to take an element of this and to this so take an element of this, which is F A comes to B So to specify what this is you've got to specify its value of B for every B and every F Yeah, so every b and a, every a from a to b. Yeah, exactly. Good? Good. So the value of that is the functor function from here to here of this a. Okay? Okay. Evaluated at this a. Okay. So it takes an element of this. I want to know what the natural transformation is that it takes, you know, takes this functor up here down into this one, or if they give it a B, then it's going to be the result of, it's going to be the natural transformation. So if it takes, yeah, that's an element B, it's going to take an F, an element F of this,
30:00 I guess an element B, and that's an element F here. So this thing is going to be the result of taking this down by the functor and then applying it to A. So that's going to be an F of B, which is what we want. Yeah. So again, it's just sort of making something that's of the right type, with the right dimensionality, and then, by theory or magic, it's the right thing to entertain. That's why I say, all this book about saying there exists a unique and all this kind of stuff should be replaced by, we can define. Yeah. In fact, what we should say is, we can define maps phi and psi such as this, and then comment that this, in effect, is a... Yeah, because the crucial point is what makes this natural, if I can use an inappropriate term here. What makes it natural is everything is done constructively and... Well, in terms of calculations... ...smugly say something like, well, we don't do anything that's non-constructive. you know, we didn't have to say that we've done a construct of it because it's true about well, that's how I know about it that everything is construed but the interesting consequence of that may be that when you talk about when you get to talking about these really large things, then you've got to have a constructive notion of identity and that's going to complicate the mathematics on these large categories possibly, I guess Well, anyway, let's go on and see how this works. So this, yeah, so then the only thing we have to show are two things. So F is in this, alpha is a member of this thing. From here to here. Then, psi of phi of alpha equals alpha. And we've got to show that if A is a member of F A, then phi of psi of R A equals A. Okay, so 1 of the 2. So if R is a natural transformation in there... From this to this. Now, you've got to show that taking it this way first and then going back the way is the same. and if this is a number of this, then do it this way first. Good. So, the reason I...
32:30 Okay, so here's one and two, then, I guess. Here's one. Oh, here it is. For... I'll do two for assumptions, it seems like that. Yeah, but, I mean, basically, what you need is two equations, and then you've got it. Yeah, exactly. So, two, we have to show that... equals that. So, take some element A. Oh, actually, is this the way it's typical? No, it's the typical way. It's going from two to, it's going from there to there. But psi on the outside is the hard way. Psi on X is the hard way. Okay. So, let's, okay, trying to get this. It requires a proof of this. So, why is this the case? Well, what is phi? No, what's basically it's just all the way through steps, so it's I of F of A of A to some number. F of B. Hang on, what's going on here? I don't know what the hell you're talking about. Oh, yeah, yeah, of course. This is a... Yeah, sorry, sorry. So you want to know, this is exactly the problem you were saying, Stuart. So what is this? The phi of A is a natural transformation. So, sorry, psi of A is a natural transformation. So phi of that natural transformation is that natural transformation evaluated at a, and then evaluated at phi, and then that equals, by this equation, big F of, well, what's left in this case is 1a. That, well, we're into the A. Now, F of one A is just the identity on F A. So, it's one F A of A, which equals A.
35:00 See, my feeling is that really, instead of 1 sub A, we should be talking about 5B sub A, because we're in set, right? Yeah. But 1 with the subscript is the standard. Just for agri-fing that. Yeah, but I know, but the problem here is that that's not functioning as the identity map. 1A is not functioning as the identity morphism. functioning as an identity element there. Hmm? How do you mean? No, this is still the identity morphism. It just happens. The one morphism in sets is ID. Yeah. But... No one's not so sure about this. Yeah, you know that in set, you have A into A by 1A, then 1A or something, and A is in A, then 1A if it's that. Yeah. That's all you need for that bit. So, okay, so as we've got this, that's the first, well, second, not number two, then number one, let's suppose you have this, phi of, okay, so this is some natural transformation, alpha. So phi of alpha is just this So it's psi of alpha A And you have to show You're trying to show that this thing equals this thing So to show that two natural transformations are the same You have to show that evaluated any B and X So really what we want to know is what that evaluator would be. And then f is, so the better way of seeing it is to do it. It is, so what is this? It's f of f.
37:30 This is where we're getting stuck with the composition and evaluation thing. We've got this as a function in itself. So, you've got f of f of, um, alpha, I think that in the bracket a, so it is of phi of alpha. Okay? Now, phi of alpha equals alpha a, 1a. Okay. Now, then you use the commutativity thing, okay? So, well, first of all, you've got to see what this takes, what alpha, what a, sorry, a of f takes 1a to. Okay, so, this A to B. So, A of F is a morphism from this to this. And like we saw before, all you do is you just compose maps. Okay? So it takes I, it takes the identity over here to the identity composed with F. But that's just F. Which is what? Which way high is it? But it's still just F, right? Yeah, yeah, yeah. That's right, it's a problem. I think it's allowed to push it back. So the important point is that this... Okay, so, now, so from the commutativity of this diagram, you know that starting here with 1A, going across there takes you to f and then down there so the result of starting here, so I guess this half of the thing takes 1a alpha b of f yeah, alpha b Yeah, that's right. Oh dear. All that. Yeah. Okay? Yeah. And then this one goes, takes 1A, sort of here, by, first of all, alpha A1A, by this, and then to F, F A, of that thing.
40:00 yeah i'm not used to do this and it's the same this is the same so it's a useful thing right it's just that we don't learning but at least although the whole of the world on the other uh... really needed those two questions because what you've got was the way that you just every remembering that five years for the goals the uh... s these are and then you're done yet they see that there's the one because then you know what you have i mean everything else is was coming up with the natural transformations and knowing that the natural transformation is defined at every bay for every end because there's another case where I find this application and function first of all takes a of a member of a category to a function from... that's why natural transformations are weird they take their functions from this two functions from this to this. They're very weird. It might be easier to think of the natural transformation not as being indexed in that way, but as just having another argument. You can hardly do that, but you can't always evaluate it at all arguments, because it takes a member B of this to a function from the functor, first functor, evaluated at B, to the second functor evaluated at B. See, so if you didn't, if you have your second, if you did your natural transformations as alpha of B, F, that wouldn't have a value unless F was a number of, yeah.
42:30 Sorry, in fact, you may not have to even be an F, it's just because we've got this function thing here. So A, unless B was a number of your first thing evaluated at, A is a number of the first thing evaluated at B. So it's got to, the thing that your natural transformation evaluated first in B takes things from, is the first function applied to B. It's an arrow, basically. Yeah, I see, yeah. So, you know, it's a bit of a problem, but I don't know what to do. Because they do this in the, I think it talks about a family of maps or something. Well, that's a spider cancer. An indexed family of maps, that's that easy. I don't see any problem. No, no, no. An indexed family of maps isn't always a map defined on a union cross index set. No, no, no. Yeah. Okay. Look, I haven't gotten the diagram down. But now, I'm a laborious task of saying what it means. Interpretation. So maybe we should look at this Maclean stuff. Maybe we should look at this Maclean stuff for next week. This stuff about universal elements. Yeah, because that's how he introduces it. You see how much easier it is to start with some question, however naive and stupid, because it motivates you to get into the stuff. I mean, we're ending up reading Maclean's book in an unorthodox order. We've done... I guess we're all categories. He's got front categories, products, covariance, and opposites. So we've done homicides, so we've done large categories. We've done quite a lot of the stuff, actually, that just get tired. We've done it just by going through Gorsair. So... He actually talks about covariance and opposites. So go in the same section, so I can eliminate it.
45:00 Now, these are to try to trace the history back as far as possible. Kurevich seems to be the first person who did anything. Who did what? The fundamental idea of representing a function by an arrow. First appeared in Topology by 1940, probably a paper of lectures by W. Kurevich, in relative homotopy groups. You mean where you had the arrow from A to B, the function from A to B? Is that what you mean? I don't know. I don't know. I don't know. Let me see if I can find out. Yes, the major advance was in discovering that you always had to specify both the domain and the co-domain when you were doing these things. And of course that's true, because otherwise you can't make these basic distinctions of ethics and mollies and so on. uh... a little bit uh... wiggins with a thought police coming in to throw us out is that was included and it would be because well and it's like we have uh-huh uh-huh uh-huh uh-huh fucking andronis yes and a big and a big a big t-shirt saying maths department yeah with a pitbull yeah i don't know that that initial was actually physically thrown did he tell you that last week oh yeah he was physically thrown out of dresswell's office no i was wearing glasses I don't think you have to apologize for not having fought back. I mean, it would be stupid. I mean, even if you didn't have your glasses on and were equipped with body armor and everything else, I wouldn't want to tangle with Gerswell.
47:30 No, but the problem is that, I mean, that's the... I mean, as the head of group, he's absolutely... He's absolutely a mess fit. He's absolutely incapable of doing anything as the head of group. He's not doing anything as the head of group. so all you can do is if you just tell him that you don't like something it turns out that he just throws you out of his office he says well given that the atmosphere in the department is as bad as it is we should still run it why the atmosphere is as bad as it is then he threw him out then he throws you out said I'm not going to talk about it don't talk about it, it'll go away Oh well. Well, we figured out, we actually got a proof of Yelena's lemon. But we still don't know what it said. See, you're doing something. John, I'm going to run out because I've got a bunch of things to do. Yeah. But, I've cleaned the kitchen and I've put another ball of laundry into the machine. find this well it includes my my my my sheets of yours so yeah and and and but shows so or and she has been a very very something was like a laundry basket in my bathroom which is in fact repository for for underpants multi-sweighers et cetera now as it goes into a bag and out into the trash But, I mean, I... Well, my problem is this Nirani thing, I think, here's this torn pair of underpants, I might be able to put this to some use, like for a rag or something. Yeah, yeah, yeah. The best thing is just throw all this shit away. I wanted to ask you, would you move that stuff from the washer into the dryer? Yeah, yeah, yeah, I'll do that, yeah. Okay, and have you got a plan for the meal tonight? Oh, but she won't be too hungry, so we'll just have something. Well, she's not going to have anything to eat before she comes. Yeah, that's true. Well, I'll think about something. I'm going to sit down and write a series of notes for my students because they're suffering. All right. Okay. Well, fair enough. I don't need to know about that.
50:00 I'm worried about that. No, no, no. I mean, well, so I think I'll be home by around, say, 6 or something in the last three hours. But if I extrapolate from yesterday's experience, you said you'd be home at 4. Okay, you've got to be back home in time to go down to the train to get Maria. Oh, dear. Well, you know what this panic's all about? Maria's coming up to stay free now. Yes. And, you know, these two guys that just allow things to deteriorate into this, you know, I mean, the house is more or less like the lion house at the zoo, and we've got to do a major cleanup movement. I mean, she'll come and think, oh, God, these guys are messy, but I guess it's not too bad. What is that? We're busting our ass to get it clean, as clean as it is. I don't envy him doing the kitchen. It wasn't too out of shape. Because I've been keeping it. I've been keeping it. I've been pretty good about that. As the rest of the house, it's a massive. Thank you.
Transcript not yet available for this recording.