This seminar by papermachine took place on 8th February 2009 20:00 UTC, in #mathematics channel of irc.freenode.net.

The timestamps displayed in the IRC text are UTC-5.

Any explanation or errors regarding this seminar should be recorded in the discussion page.

[15:01] <papermachine> Alright, everyone who's here might as well be here [15:01] <papermachine> So let's begin. [15:01] <papermachine> This seminar doesn't really overlap very much with the last one on model theory. [15:02] <papermachine> But we'll be doing things analogous to what we did before, so let's recap for like ten seconds. [15:02] <papermachine> First thing, we need a signature, a way of knowing what operations our theory has available. [15:02] <papermachine> It has constant symbols, function symbols, and relation symbols [15:03] <papermachine> So the theory of groups will have a signature of (1, *, ^-1) [15:03] <papermachine> or maybe (0, +, -) [15:03] <papermachine> the symbols themselves don't matter [15:03] <papermachine> all that matters is whether they're functions or relations [15:03] <papermachine> and how many arguments they take. [15:04] <papermachine> So fixing a signature, we can write down first-order sentences, defining them inductively [15:04] <papermachine> first terms as strings of symbols from the signature, with variables [15:04] <papermachine> then relations of terms, and the special relationship of model-equality a = b [15:05] <papermachine> and then quantified sentences, using Ax[ ... ] and Ex [ ... ] (which are my symbols today) [15:05] <papermachine> We select some of these sentences to be axioms; their deductive closure constitutes a 'theory' [15:06] <papermachine> The theory of groups is the set of all sentences that can be deduced from the group axioms. [15:06] <papermachine> A model of that theory is a set that interprets the signature of the theory, providing functions to function symbols and relations to relation symbols [15:07] <papermachine> Z_2 is a model of the theory of groups because it has 0 for 0, + mod 2 for +, and x + 1 mod 2 for -x. [15:07] <papermachine> Further, we say it's a model of the theory of groups because we we interpret those axioms within the model, they hold true. [15:08] <papermachine> Now, classical group theory (meaning pre-70's) took as its external theory normal set theory [15:08] <papermachine> That means when we're talking about models, we use the language of set theory [15:09] <papermachine> I don't want to talk about foundations very much, but I saw an estimate once that to do real model theory, you probably need about three uncountable ordinals, or something like that [15:09] <papermachine> ... that sounds like a lot. [15:10] <papermachine> So with the invention of category theory, there should be a way to shift paradigms, to be all witty and postmodern-sounding, and rewrite this stuff using CT-concepts [15:10] <papermachine> Now, my CT isn't so sharp, so you may have to warn me if I say something obviously not true. [15:10] <papermachine> in the late 60's, a guy named Ehresmann came up with a way of doing this using what he called (in French) sketches. [15:11] <papermachine> You can find a few of his papers on Numdam, but they're in french and difficult to understand. [15:11] <papermachine> Luckily, Wells and Barr took pity on us monolingual Americans and wrote a couple papers on the subject [15:11] <papermachine> Along with a few other people, like Makkai and some other guy I can't remember. [15:12] <papermachine> That's basically how I learned about sketches, and all that I know about them. My CT isn't strong enough to understand the big theorems, so today I want to sketch (har har) some examples of sketches [15:12] <papermachine> and show how you get the same expressiveness that you do with the set-theoretical language [15:13] <papermachine> so any questions about that before we start up? [15:13] <papermachine> Alright. [15:13] <papermachine> So first we need a category-analog of a signature. [15:14] <papermachine> Lawvere had a good idea, called the full clone. [15:14] <papermachine> This only works for signatures that only have functions; but that's not a big deal. [15:14] <papermachine> You start with the category whose objects are the natural numbers [15:15] <papermachine> Then you add an arrow from n to 1 if there's a function with arity n in the signature. [15:15] <DiffyQ> ! [15:15] <papermachine> Yo [15:15] <papermachine> DiffyQ: [15:15] <DiffyQ> One arrow per function or just one if there are any functions at all? [15:15] <papermachine> One arrow per function. [15:15] <DiffyQ> Cool. Carry on. [15:15] <papermachine> So in the group example you have an arrow 2 -> 1, an arrow 1 -> 1, and an arrow 0 -> 1 (for the identity) [15:16] <papermachine> Then, you add arrows for projections and injections, as if all the numbers were secretly powers of some object X [15:16] <papermachine> \(a, b) -> a, stuff like that [15:17] <papermachine> Finally, you add identity arrows, and closure under composition, and you've got yourself a category [15:17] <papermachine> You can take functors from this category to special categories whose objects are all products of some object X, and even get a sort of model theory out of it [15:17] <papermachine> but it's kind of unwieldy. [15:18] <papermachine> So the idea is to get rid of all the junk that had to get added on to make the full clone into a category. [15:18] <papermachine> What happens to a category when you take away composite arrows and identity arrows? [15:18] <papermachine> anyone [15:18] <_llll_> directed graph [15:19] <papermachine> right [15:19] <papermachine> So what Barr calls a trivial sketch is just going to be a directed graph [15:19] <papermachine> The objects of this directed graph are going to represent, in a way, the sorts of the theory [15:19] <papermachine> I don't know if sorts are really the same thing as types, but I think the word type is better known [15:20] <papermachine> Most familiar theories only have one basic type, but to get functions of higher arity you need products of that type [15:20] <papermachine> But perhaps I'm getting ahead of myself. Let's go back to that directed graph. [15:20] <koeien> ! [15:20] <papermachine> The simplest directed graph has one node and no edges. [15:21] <papermachine> koeien: [15:21] <koeien> so the directed graph we are talking about contains the arrows of the functions + the projections/injections, or were the last also thrown away? [15:21] <papermachine> Yeah, we threw everything away. [15:21] <koeien> so only the functions (3 in the case of group theory) [15:21] <papermachine> Right now let's just talk about what the nodes are. [15:21] <koeien> ok [15:21] <koeien> thanks [15:22] <papermachine> To get to group theory, we'll need something more sophisticated than a directed graph. [15:22] <papermachine> Okay, so we have a single type, X. It's the only node, and there aren't any edges. [15:22] <papermachine> We want a functor-like thing from this graph to the category of sets to be a model for this sketch [15:23] <papermachine> The same way we had a function-like thing called interpretation from symbols to sets [15:23] <papermachine> We can't use functors, because a sketch isn't a category, and if we make it a category we'll be toting around N and a bunch of useless projections [15:24] <papermachine> So instead we make Set forget that it's a category, and call a 'sketch morphism' a graph homomorphism from a sketch to the underlying graph of the category of sets. [15:24] <papermachine> So nodes go to sets, and edges go to arrows pointing the same way. [15:25] <papermachine> For the sketch with one node and no edges, a model, i.e., a sketch morphism into Set, just picks out a special set from Set. [15:25] <papermachine> sets are surely models for the theory of sets. [15:25] <papermachine> Which is what the one-node sketch sketches. [15:25] <papermachine> A better sketch has two nodes, NODE and EDGE, and two arrows, EDGE --source--> NODE and EDGE --target--> NODE [15:26] <papermachine> If you follow a sketch morphism of this graph into Set, you find two sets with two parallel functions, i.e., a model of graphs [15:26] <papermachine> *directed graphs [15:26] <papermachine> This is great, but we don't have a way to make axioms hold true. [15:27] <papermachine> In CT, equations tend to be replaced with commutative diagrams [15:27] <papermachine> So lets enlarge our notion of a sketch to include some other diagrams [15:27] <papermachine> And enlarge our notion of sketch morphism to force these diagrams to map to commutative diagrams in the graph of the category. [15:29] <papermachine> We only require sketch morphisms to be one way, from the sketch to the underlying graph of the category. [15:30] <papermachine> And the image of a diagram in a sketch under this sketch morphism has to map to a commutative diagram in the category. [15:30] <papermachine> For example, we can add to the sketch of graphs an extra arrow EDGE --flip--> EDGE [15:31] <papermachine> together with a diagrams saying source . flip = target, target . flip = source, and flip . flip = id [15:32] <papermachine> This gives us the sketch of directed graphs where every edge has another edge that reverses it [15:32] <papermachine> I guess you'd call them self-dual directed graphs, or something. [15:32] <papermachine> It's kind of an artificial example. [15:32] <_llll_> i think you'd just call that "a graph" [15:32] <papermachine> Eh, there are more edges than there should be [15:33] <papermachine> I feel like you'd have to have some sort of equivalence relation ... I dunno. [15:33] <papermachine> Anyway. [15:34] <papermachine> What we have so far gives us the model theory of multi-sorted, linear, equational theories [15:34] <papermachine> multi-sorted because we can have more than one type, like we did with nodes and edges [15:34] <papermachine> linear because all the functions are 1-arity, and there aren't any relations. [15:34] <papermachine> We want n-arity functions, and to get that we need products of types. [15:35] <papermachine> From what little CT I know, a product is just a cone over a diagram that doesn't have any edges. [15:35] <papermachine> So that's exactly the data that we'll add to our notion of a sketch, and we'll force sketch morphisms to take those discrete cones to limit cones in the category. [15:35] <papermachine> Now my examples get even worse :) [15:35] <DiffyQ> ! [15:36] <papermachine> DiffyQ: [15:36] <DiffyQ> So do we require the categories we map into to have limits? [15:36] <DiffyQ> Or are we just doing Set? [15:36] <papermachine> All I really know is Set [15:36] <DiffyQ> Well that certainly has limits. [15:36] <papermachine> I know they do it to other categories, like Top [15:36] <papermachine> does that have the right limits? [15:37] <papermachine> It has products, modulo choice [15:37] <DiffyQ> It always has products. They might just be empty without choice. [15:37] <_llll_> yes, and pretty much every "big" category you'd want will have all limits [15:37] <DiffyQ> So, yeah, it's fine, go on. [15:37] <papermachine> Okay. [15:38] <papermachine> If these cones are also finite, you get what are called finite-product sketches [15:38] <papermachine> My horrible example of these are magmas, with signature (*) and no salient properties :) [15:39] <papermachine> You have a diagram with one node, X; together with a product cone X <- X2 -> X, and an arrow X2 -> X for the multiplication. [15:39] <papermachine> models of this have to map X2 to the X x X, so all is right with the world. [15:40] <papermachine> You can add on to this, X3 for an associativity square [15:40] <papermachine> X0 = 1 for constants [15:40] <papermachine> and even more diagrams, and eventually get a diagram for the theory of groups [15:40] <DiffyQ> ! [15:40] <papermachine> DiffyQ: [15:40] <DiffyQ> How does X0 work? [15:40] <papermachine> empty cone [15:40] <DiffyQ> Oh, durr. Okay. [15:41] <papermachine> Confused me too :) [15:41] <papermachine> I won't walk through that because it's a bit of effort to get all the right projections [15:41] <DiffyQ> So it just goes to the terminal object? [15:41] <papermachine> Yeah, like the definition of a group object (I think) [15:42] <DiffyQ> I.e., under no conditions, there's a unique map from anything to X0, which is what the empty cone would say. [15:42] <papermachine> Right [15:42] <DiffyQ> Err, the image of X0. [15:42] <papermachine> I understood what you meant. [15:42] <papermachine> In Set, that'll map to the singleton, which in turn will pick out whatever element of X is the identity [15:43] <antonfire> ! [15:43] <papermachine> antonfire: [15:43] <antonfire> So if you use Top instead of Set with the same sketch, do you get topological groups right away? [15:43] <papermachine> That's what I've been told. [15:43] <DiffyQ> That's neat. [15:43] <_llll_> yes, you're just doing group objects at this poitn [15:44] <papermachine> right. [15:44] <papermachine> FP-sketches will get you the multi-sorted equational theories, but that leaves out a lot of things [15:44] <papermachine> notably, fields [15:45] <papermachine> Right? multiplicative inverse over a field is a partial function, so it can't be done equationally. [15:45] <_llll_> 1!=0 in a field too [15:45] <papermachine> Good point. [15:46] <papermachine> So the way I tend to believe this is like this [15:46] <papermachine> If we restrict ourselves to the non-zero parts of a field, everything is well defined [15:46] <papermachine> so what we need to do is paste that zero on there [15:47] <papermachine> And the way they seem to do this is by writing the type of the field as the sum F = I + Z [15:47] <papermachine> F is the type of the field, I is the invertible elements, and Z is zero [15:47] <papermachine> Now to get that sum, you need discrete cocones, and doing a similar thing to the definition of a sketch and sketch morphism, you make the cocone diagrams go to limit cocones [15:48] <papermachine> A sketch with discrete, finite cocones is called a finite limit sketch, and it will get you the whole shebang of typical algebra. [15:49] <papermachine> Now you'll notice we actually have four definitions of a sketch, and there's a bunch of others [15:49] <papermachine> To make sure the definitions are right, they tend to call them doctrines. [15:49] <papermachine> So people talk about the finite product doctrine, or the finite limit doctrine, and so on. [15:50] <papermachine> And that's the limit of my knowledge of sketches at the moment. I'm still working on catching my CT up to snuff. [15:50] <papermachine> So feel free to ask embarassing questions that I can't answer :) [15:50] <papermachine> If you're interested, I can tar up the papers I have, though they're all available on various people's websites. [15:51] <_llll_> it would be nice to see how the field thing works, handling fields is iirc something you just Don't Do in universal algbera type formulations [15:51] <papermachine> I could draw it out if given enough time. [15:52] <papermachine> I'll see if I can get a scan of it with the seminar notes [15:52] <papermachine> There's also several different field sketches, and only one of them is good for topological fields, or so Barr says in I think Toposes, Triples, and Theories. [15:53] <_llll_> also, presumably there s a category of sketches (or doctrinres), so you could do sketches into the underlying set of Sketch (or Doctrince) [15:53] <papermachine> I'm pretty sure that's how they recover a definition for model equivalence [15:54] <_llll_> err, underlying catgeory, not underlying set [15:54] <papermachine> Natural transformations between such and such functors [15:54] <papermachine> I really need to learn more CT :( [15:55] <_llll_> i guess another question is why we should bother with all this, ok so a model for set theory is a sketch into Set, but you already had to have a "Set" there [15:55] <_llll_> but then i guess being able to fit fields into the same formualtion is worth soething [15:56] <papermachine> The equational way of doing things is really annoying sometimes. [15:56] <DiffyQ> The point, I think, is to be able to do model theory in a categorical framework. [15:56] <_llll_> but why is doing something in a categorical framework a sensible goal? [15:57] <papermachine> My motivation is the syntactic sugar [15:57] <DiffyQ> I dunno, I thought it was neat