[15:00] * b0o-yeah (n=b0o-yeah@unaffiliated/b0o-yeah) has joined #mathematics
[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] * antonfire (n=me@dynamic-oit-vapornet-b-1854.Princeton.EDU) has joined #mathematics
[15:02] <papermachine> First thing, we need a signature, a way of knowing what operations our theory has available.
[15:02] * TRWBW (n=user@201.237.77.138) has joined #mathematics
[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] * ChanServ changes topic to 'Seminar in progress, if you want to ask a question, say ! and wait to be called'
[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] * |fred| (n=fred@e181007253.adsl.alicedsl.de) has joined #mathematics
[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] * sepult (n=buggarag@xdsl-87-78-146-21.netcologne.de) Quit ("Lost terminal")
[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:16] * WeeLubo (n=john@cpc2-ruth6-0-0-cust1011.renf.cable.ntl.com) has left #mathematics
[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] * w3asal (n=jwilcox4@govschool31.nomad.utk.edu) Quit ("Leaving.")
[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:22] * WimC (n=WimC@dhcp-077-249-152-065.chello.nl) has joined #mathematics
[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:23] * justbeingglad (n=justbein@193.19.82.199) Quit ("Leaving.")
[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] * idhtns (n=someguy@140.247.149.186) has joined #mathematics
[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:28] <maxote> !
[15:28] <papermachine> maxote:
[15:28] <maxote> does it require an isomorphism (and non-orthogonal too to accomplish the isomorphism)?
[15:28] <papermachine> does what require an isomorphism?
[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] * Groovy (n=opera@89-212-69-63.dynamic.dsl.t-2.net) has left #mathematics
[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:33] * theoros (n=theoros@unaffiliated/theoros) has joined #mathematics
[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] <maxote>  /non-orthogonal/non-orthogonal projection/  sorry me
[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:38] * dexem (i=exe_@bbservice204.mmpnet213.tnp.pl) has left #mathematics
[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] * burned (n=burned@71-90-228-220.dhcp.gnvl.sc.charter.com) Quit (Remote closed the connection)
[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] * idhtns (n=someguy@140.247.149.186) has left #mathematics
[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 shrugs.
[15:57] <DiffyQ> I dunno, I thought it was neat