Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

November 3, 2007

Concrete Groups and Axiomatic Theories II

Posted by Guest

Guest post by Todd Trimble

While we’re waiting for more videos and notes from the Geometric Representation Theory seminar, now might be a good time to fill in more of the logical background to Jim Dolan’s talks. Last time, we mentioned an amazing Galois correspondence between complete theories of structures on a set XX and concrete groups of transformations on XX. Today I’d like to explain how this correspondence works, with an eye towards discussing Jim’s orbi-simplex idea, and what this has to do with geometry (in particular, the theory of buildings).

The Galois correspondence is in the spirit of Klein’s Erlanger Programm: a structure has a group of transformations, but in a logical sense the group determines the structure. Frankly, I found this sort of surprising at first: theories of structures would seem to be something very general, and groups rather more specific. But I found out recently that the logician Alfred Tarski was also interested in applying Klein’s Erlanger Programm to logic, in his “What are Logical Notions?”

From the Wikipedia article:

Tarski’s proposal was to demarcate the logical notions by considering all possible one-to-one transformations (automorphisms) of a domain onto itself.

Tarski’s “notions”, or types of mathematical structure, are arranged in a hierarchy, where at one end is a completely rigid type of structure (say, the real numbers as ordered field) with only one automorphism, passing through intermediate more relaxed structures (e.g., the reals as topological abelian group, the reals as manifold, the reals as topological space) which admit more automorphisms (diffeomorphisms, homeomorphisms, … what Jim called “something-o-morphisms” in general), winding up with the most relaxed structure of all: the reals as simply a “logical structure”, where every invertible map on the domain of reals is an automorphism. According to Tarski’s thesis, a notion is “logical” if it is preserved by an arbitrary automorphism. This fits in with the ideas we are trying to develop now.

Where we broke off last time, we stated a finitary version of a Galois duality between symmetry and structure:

Theorem. Let X be a finite set. There is a Galois correspondence (a bijective correspondence) between

  • (Complete) theories of structures on XX, i.e., subtheories of P(X *)P(X^{*})
  • Groups of transformations of XX, i.e., subgroups GX!=Aut(X)G \subseteq X! = Aut(X)

Most of my previous post was spent on developing precise categorical meanings for the terms ‘theory’ and ‘complete theory of a structure’, but for now it’s enough to remember just a few things:

  1. For each set XX there is a ‘tautological theory’ P(hom(,X))=P(X *):FinBoolP(hom(-, X)) = P(X^{*}): Fin \to Bool where each pullback operation P(X f):P(X m)P(X n)P(X^f): P(X^m) \to P(X^n) admits a left adjoint X f\exists_{X^f}, which takes the direct image along X f:X nX m.X^f: X^n \to X^m.
  2. A (complete) theory of a structure on XX is by definition a subtheory TT of P(hom(,X))P(hom(-, X)), i.e., a subfunctor i:TP(hom(,X))i: T \subseteq P(hom(-, X)) whose elements {pT(n):n0}\{p \in T(n): n \geq 0\}, the predicates of TT, are closed under application of existential quantifiers X f\exists_{X^f}.

The Galois correspondence works in the way we have come to expect:

  • To each theory TP(X *)T \subseteq P(X^*), we associate the group G=Aut T(X)G = Aut_T(X) of TT-model automorphisms on XX, i.e., bijections ϕ:XX\phi: X \to X such that the following diagram commutes: T(n) i n P(X n) i n P(ϕ n) P(X n) \array{ T(n) & \stackrel{i_n}{\to} & P(X^n) \\ & i_n \; \searrow & \downarrow \; P(\phi^n) \\ & & P(X^n) }
  • Conversely, to each group GX!G \subseteq X!, we associate the theory Th(G,X)Th(G, X) whose predicates are the GG-invariant relations on XX: formally, Th(G,X):nP(X n/G)Th(G, X): n \mapsto P(X^n/G), where X n/GX^n/G is the set of GG-orbits under the action g(x 1,x 2,,x n)=(gx 1,gx 2,,gx n),g \cdot (x_1, x_2, \ldots, x_n) = (g x_1, g x_2, \ldots, g x_n), defines a subfunctor of the tautological theory nP(X n)n \mapsto P(X^n). We let q:X nX n/Gq: X^n \to X^n/G denote the canonical projection.

The analogy to Galois theory is clear. In the first place, we get a Galois connection, i.e., an adjunction of the form

TTh(G,X)GAut T(X)iff\frac{T \subseteq Th(G, X)}{G \subseteq Aut_T(X)} iff

Actually, this fact follows from some very general nonsense: any relation RA×BR \subseteq A \times B whatsoever can be used to set up a Galois connection between subsets AA' of AA and subsets BB' of BB:

A{aA: b:B(a,b)R}B{bB: a:A(a,b)R}iff\frac{A' \subseteq \{a \in A: \forall_{b: B'} (a, b) \in R\} }{B' \subseteq \{b \in B: \forall_{a: A'} (a, b) \in R\} } iff

Indeed, each of the conditions above and below the bar is equivalent to the condition A×BRA' \times B' \subseteq R. In our case, AA is the group of permutations gg on XX, BB is the set of finitary relations pp on XX, and the relation RR is the set of (g,p)(g, p) such that p(x 1,,x n)=p(gx 1,,gx n)p(x_1, \ldots, x_n) = p(g x_1, \ldots, g x_n) [for all nn-tuples (x 1,,x n)(x_1, \ldots, x_n) if pp is nn-ary]. By definition,

Th(G,X)(n)={pP(X n): g:Gp(gx 1,,gx n)=p(x 1,,x n)}Th(G, X)(n) = \{p \in P(X^n): \forall_{g: G} p(g x_1, \ldots, g x_n) = p(x_1, \ldots, x_n)\}


Aut T(X)={gX!: p:Tp(gx 1,,gx n)=p(x 1,,x n)}.Aut_T(X) = \{g \in X!: \forall_{p: T} p(g x_1, \ldots, g x_n) = p(x_1, \ldots, x_n)\}.

To prove the Galois connection is an equivalence (a Galois correspondence) takes a bit more work. First, we prove the easy half of the correspondence: we show G=Aut Th(G,X)(X)G = Aut_{Th(G, X)}(X) for each subgroup GX!G \subseteq X!. (It is easier to believe we can recapture a group from its theory than it is to believe we can recapture a general theory from its group!)

Proof: That GAut Th(G,X)(X)G \subseteq Aut_{Th(G, X)}(X) is clear from the Galois connection. For the other direction, suppose ff is an automorphism of the Th(G,X)Th(G, X)-structure on XX. By definition, this means that for all nn, we have a commutative triangle

P(X n/G) P(q) P(X n) P(q) P(f n) P(X n) \array{ P(X^{n}/G) & \stackrel{P(q)}{\to} & P(X^n) \\ & P(q) \; \searrow & \downarrow \; P(f^n) \\ & & P(X^n) }

Since XX is finite, all the Boolean algebras are finite, and we can invoke the equivalence Fin opBool finFin^{op} \simeq Bool_{fin} (‘baby Stone duality’) to convert this triangle to

X n f n X n q q X n/G \array{ X^n & \stackrel{f^n}{\to} & X^n \\ & q \; \searrow & \downarrow \; q \\ & & X^{n}/G }

Again, since XX is finite, we can let nn be the set XX and argue a la Yoneda: we read off from the triangle that 1 X1_X and f X(1 X)=ff^X(1_X) = f belong to the same GG-orbit. But this means precisely that there exists an element gg of GG such that f(x)=gxf(x) = g x for all xx in XX. We have thus shown that every element ff of Aut Th(G,X)(X)Aut_{Th(G, X)}(X) belongs to the subgroup GG, as desired. QED

We turn now to proving the harder half: that T=Th(Aut T(X),X)T = Th(Aut_T(X), X) for any subtheory TT of P(X *)P(X^*). Again, TTh(Aut T(X),X)T \subseteq Th(Aut_T(X), X) from the Galois connection. So the real work is to prove the opposite inclusion.

We begin by again invoking ‘baby Stone duality’, which asserts that the contravariant Boolean algebra functor P:Fin opBool finP: Fin^{op} \to Bool_{fin} is an equivalence. Thus, any functor T:FinBool finT: Fin \to Bool_{fin} can be written in the form P(A)P(A) for an essentially unique A:Fin opFinA: Fin^{op} \to Fin. This A(n)A(n) is nothing but the set of atomic nn-ary relations in TT. The monic natural transformation

i:TP(hom(,X)),i: T \to P(hom(-, X)),

which is the TT-structure of XX, is thus obtained by applying PP to a uniquely determined quotient map

q:hom(,X)A.q: hom(-, X) \to A.

This morphism in turn is uniquely determined, via Yoneda, by an element α=q X(1 X)A(X)\alpha = q_{X}(1_X) \in A(X), the unique atomic XX-ary relation of TT which contains 1 X1_X. We call α\alpha the universal atomic TT-relation. By the proof of the Yoneda lemma, we have q n(g)=A(g)(α)q_n(g) = A(g)(\alpha) for any g:nXg: n \to X.

We know from the Galois connection that the quotient map q n:X nA(n)q_n: X^n \to A(n) factors uniquely through an epimorphism

X n/Aut T(X)A(n).X^n/Aut_T(X) \to A(n).

We are trying to show that this map is an isomorphism. In other words: if ff and gg are two elements in X nX^n which belong to the same atomic TT-relation in X nX^n, then there exists a TT-structure automorphism ϕ:XX\phi: X \to X which carries gg to ff: f=ϕgf = \phi \circ g.

Lemma: ϕ:XX\phi: X \to X is a TT-structure homomorphism iff q X(ϕ)=q X(1 X)=αq_X(\phi) = q_X(1_X) = \alpha (i.e., if ϕ\phi belongs to the universal atomic TT-relation).

Proof: Using baby Stone duality again, the definition of TT-structure homomorphism translates into commutativity of the triangle

hom(,X) hom(,ϕ) hom(,X) q q A \array{ hom(-, X) & \stackrel{hom(-, \phi)}{\to} & hom(-, X) \\ & q \; \searrow & \downarrow \; q \\ & & A }

By chasing this triangle at the component q Xq_X starting from 1 X1_X, the conclusion easily follows. QED

Now, the TT-structure i:TP(hom(,X))i: T \to P(hom(-, X)) we started with is not just any old monomorphism; crucially, it also preserves existential quantification. I leave it to the reader to show this is equivalent to a rather powerful property of the epimorphism qq: every naturality square

hom(n,X) q n A(n) hom(g,X) A(g) hom(m,X) q m A(m) \array{ hom(n, X) & \stackrel{q_n}{\to} & A(n) \\ hom(g, X) \; \downarrow & & \downarrow \; A(g) \\ hom(m, X) & \stackrel{q_m}{\to} & A(m) }

is weakly cartesian, in the sense that given elements hhom(m,X)h \in hom(m, X), bA(n)b \in A(n) which map to the same element aA(m)a \in A(m), there exists an element fhom(n,X)f \in hom(n, X) which maps to both hh and bb.

Now suppose q n(f)=q n(g)q_n(f) = q_n(g) (=A(g)(α)= A(g)(\alpha)) for two maps f,g:nX.f, g: n \to X. Since the square

hom(X,X) q X A(X) hom(g,X) A(g) hom(n,X) q n A(n) \array{ hom(X, X) & \stackrel{q_X}{\to} & A(X) \\ hom(g, X) \; \downarrow & & \downarrow \; A(g) \\ hom(n, X) & \stackrel{q_n}{\to} & A(n) }

is weakly cartesian, there exists ϕhom(X,X)\phi \in hom(X, X) which maps to both fhom(n,X)f \in hom(n, X) and αA(X)\alpha \in A(X) in the square. Hence hom(g,X)(ϕ)=f\hom(g, X)(\phi) = f, in other words f=ϕgf = \phi \circ g, and also q(X)(ϕ)=αq(X)(\phi) = \alpha, i.e., ϕ\phi is a TT-structure homomorphism (by the lemma above).

All that remains to show is that ϕ\phi is invertible. It suffices to show that every TT-structure homomorphism ϕ\phi has a left inverse which is a TT-structure homomorphism. For this, consider the square

hom(X,X) q X A(X):α hom(X,ϕ) A(ϕ) 1 X:hom(X,X) q X A(X):α \array{ hom(X, X) & \stackrel{q_X}{\to} & A(X): \alpha \\ hom(X, \phi) \; \downarrow & & \downarrow \; A(\phi) \\ 1_X: hom(X, X) & \stackrel{q_X}{\to} & A(X): \alpha }

where we have identified some elements involved in a diagram chase. Since this square is weakly cartesian, there exists ψhom(X,X)\psi \in hom(X, X) such that hom(X,ϕ)(ψ)=1 Xhom(X, \phi)(\psi) = 1_X and q X(ψ)=αq_X(\psi) = \alpha. The first equation says ψ\psi is left inverse to ϕ\phi. The second says ψ\psi is a TT-structure homomorphism. The proof is now complete. QED


  1. As far as I know, the condition that a natural transformation be weakly cartesian was first identified and exploited by André Joyal, to help give a categorical characterization of analytic functors (i.e., sums of functors F n(X)=X n/GF_n(X) = X^n/G, where Gn!G \subseteq n!) in the theory of species. See the appendix of his article Foncteurs analytiques et espèces de structures [in Combinatoire Enumerative (G. Labelle and P. Leroux, eds.), Springer Lecture Notes in Math. 1234 (1986), 126-159].
  2. The Galois theory we have just established is for finite sets XX, but it can be easily adapted so as to apply to infinite sets XX, just by strengthening the logic (i.e., the hyperdoctrine). Thus, instead of taking functors T:FinBoolT: Fin \to Bool into ordinary Boolean algebras, we could instead admit infinite conjunctions and disjunctions by considering functors into completely distributive Boolean algebras (dual to the category of sets). And instead of restricting ourselves to finite-product types X nX^n, we could admit arbitrary products X SX^S. For example, we have a Boolean hyperdoctrine P(hom(,X)):SetCDBoolP(hom(-, X)): Set \to CDBool equipped with quantifiers and a Beck-Chevalley condition, and one can establish a Galois duality between subgroups GX!G \subseteq X! and subtheories TP(hom(,X))T \subseteq P(hom(-, X)) for arbitrary sets XX, by applying the above arguments mutatis mutandis.

Before we end this chapter, I’ll mention a few more things that can be proved using the techniques used above:

  • Up to isomorphism, there is only one model of a complete theory TP(X *)T \subseteq P(X^*), namely the tautological model XX.
  • For this model, every TT-model homomorphism is an automorphism. Hence the category TModT-Mod is equivalent to the group G=Aut T(X)G = Aut_T(X): abstractly, the category of TT-models is equivalent to the category of GG-torsors. The specific action of GG on XX is identified with the underlying-set functor GTModUSet.G \simeq T-Mod \stackrel{U}{\to} Set.
  • For more general (let us say finite) polyadic Boolean algebras TT, the category TModT-Mod is a groupoid. This is in part due to the classical (Boolean) nature of these hyperdoctrines. To be related to the fact that a topos Set CSet^C is a Boolean topos iff CC is a groupoid.
Posted at November 3, 2007 4:50 AM UTC

TrackBack URL for this Entry:

20 Comments & 2 Trackbacks

Re: Concrete Groups and Axiomatic Theories II

Todd, what you say is quite interesting and, IMHO, you and Jim Dolan perhaps might want to consider collaborating on this way of thinking, for example, the two of you might even consider writing a paper on the topic.

For now, I have just one question. Would it at all be possible to obtain an infinite set X from finite sets X? For example, might this be done using the concept from category theory called (co)filtered limit ? (I would especially like to know if an infinite X can be obtained as the limit of increasingly large finite instances of X). Thanks.

Posted by: Charlie Stromeyer Jr on November 3, 2007 1:26 PM | Permalink | Reply to this

Re: Concrete Groups and Axiomatic Theories II

Charlie wrote:

Todd, what you say is very interesting and, IMHO, you and Jim Dolan might want to consider collaborating on this way of thinking […]

They are. They’ve been collaborating for for over a year now, meeting electronically at least once a week, working on this stuff. The Geometric Representation Theory Seminar is presenting the result of that collaboration together with my discussions with Jim.

[…] the two of you might want to consider writing a paper on the topic.

If history is a good guide, Jim will never write a paper on this stuff. Todd just did. (Look up.)

Posted by: John Baez on November 3, 2007 2:06 PM | Permalink | Reply to this

Re: Concrete Groups and Axiomatic Theories II

We are collaborators! Jim and I get together over the internet once or twice a week, using skype and virtual whiteboards and other instruments, and talk about all kinds of things. (Recently it’s been about Verma modules and D-modules and the BGG resolution.) The Galois correspondence I’m writing about now is something we discussed a few years back, although the detailed proofs are more recent.

John and Jim and I are attacking this huge beast called Groupoidification together but from sometimes different directions, trying to bring it under control and tame it. Our assorted talks and writings about it here are precursors to actual papers (I hope!).

I’m not fully awake yet (need that first cup of joe), but I’m not sure I get your mathematical question. It’s true that any set is a filtered colimit (actually, a union as civilians would say :-) ) of its finite subsets…

Posted by: Todd Trimble on November 3, 2007 2:25 PM | Permalink | Reply to this

Re: Concrete Groups and Axiomatic Theories II

Todd, here is what I am thinking of (but please note that even though you are an expert in category theory I am just a beginner in the subject):

Over ten years ago in the journal Science [1], the Fields medalist and topologist Michael Freedman made this suggestion for solving the famous P/NP problem for which there is now a $1 million dollar prize from Claymath:

First, think roughly of the concept of ‘limit’ as the residue of an infinite process. Freedman then wanted to construct increasingly large finite instances X of polynomial time solvable problems such that the infinite version X is solvable. The hope is then that for NP-complete problems such as the traveling salesman problem the infinite version of such a problem would not be solvable. Freedman was not sure how to construct such ‘limits’.

Although Freedman’s suggestion sounds simple enough it is actually very difficult to realize concretely. I know this the hard way because both Freedman and I have separately and only very occasionally tried to do this. Nevertheless, I have recently taken these two steps in an effort to make some progress:

1) I have tried to think about such computational limits via ideas from both Jens Blanck’s approach to topology from domain theory and also from profinite topology. Actually, if I am correct these two approaches are related in some ways, as one example, the Baire category theorem holds for a profinite group.

Also, various types of domains can be described as various types of categories. I have not yet learned how this works but it is explained, for example, in the book “Continuous Lattices and Domains” by G. Gierz et al.

2) I have read almost every paper on both finite and infinite instances of constraint satisfaction problems (CSPs). Below, are the four very best papers about infinite CSPs and you might like the paper [2] because it is algebraic and categorical. Also, paper [3] contains a reference to Freedman’s own interesting paper on an infinite version of the Boolean satisfiability problem (i.e., infinite SAT).

Todd, the question I have for you or any other category theory expert is this:

Can category theory shed any light upon the possible role of limits for problems in computational complexity, recursion theory or logic? For example, might category theory enable one to construct an infinite CSP out of increasingly large finite versions of the same CSP? Thanks.

I have more ideas about this but I don’t want to overload you with too much info at once. If one of you category theorists can figure out an answer to my question then I might be able to figure out some of the relevant computer science because my job requires me to do some (proprietary) research in computer science and because I have access to both the Harvard and MIT libraries.

1] Science, vol 275 (March 14, 1997), page 1570.

2] Constraint satisfaction problems with infinite templates

[3] On the computational limits of infinite satisfaction

[4] The last paper in the book Computational complexity and statistical physics

[5] Periodic constraint satisfaction problems: Polynomial-time algorithms

Posted by: Charlie Stromeyer Jr on November 3, 2007 6:44 PM | Permalink | Reply to this

P vs. NP; nomenclature

Sorry, I don’t have much of a response to this at the moment. The P vs. NP problem is reputed to be one of these very fundamental and apparently almost intractably difficult problems, but I have no personal experience with it. (My usual reaction to any of these Clay problems is: this has gotta be one of the hardest ways to earn a million bucks!)

The paper (2) you mentioned did look sort of interesting; I’m sure I’d like it even more if I knew more model theory and universal algebra. (I tend to learn mathematics on a need-to-know basis, and on this basis I’ve picked up some model theory here and there, but not a great deal.) But there are these funny little nomenclatural clashes that crop up. For example, the term “ω\omega-categorical template” in the abstract immediately caught my eye; I thought, “wow, ω\omega-categories!” until I found out the author was referring to ω\omega-categoricity (only one countable model up to isomorphism), something totally different. The word “limit” is another which may give rise to misunderstanding unless the context is carefully spelled out.

Some years ago, Jim Stasheff invited me to attend a mini-conference on algebraic topology at UW-Madison, and was introducing me to various people like Sufian Husseini as someone interested in weak nn-categories. Husseini seemed to light up a little bit and immediately wanted me to meet one of his students who was also working in this area. So I began talking with his student, but it took an uncomfortably long while to discover (when he didn’t know what a bicategory was) that what he was talking about was Lusternik-Schnirelmann category. Oh.

Jim seemed to think it hilarious when I told him that story, and said something like, “See, I’ve been warning these guys about using the word ‘category’…”

Posted by: Todd Trimble on November 4, 2007 2:38 PM | Permalink | Reply to this

Re: P vs. NP; nomenclature

Todd, thank you for your reply and you are correct about the difficulty of the P/NP problem. The reason why both Freedman and I have only very rarely (and separately) thought about this problem is because it is beastly (almost insanely) difficult. On the other hand, if no one thinks about this problem then no progress will be made.

However, I am not right now interested in trying to solve the P/NP problem per se, but interested rather in the question of whether the concept of ‘limit’ has any potential role for questions in computability, recursion theory , logic or even geometry (with the exception of von Neumann’s continuous geometry which I already know can be obtained as the profinite limit of increasingly large finite instances of projective geometry).

Also, I did not at all mean for you to be mislead by the term “w-categorical”. Rather, this paper is categorical in the sense described by some of its references such as reference 7, and in the sense that universal algebra and model theory are categorical.

Please read my three very brief and speculative comments here. Please tell me what is the name within category theory for the concept I describe in point 1 of comment 1, i.e., what is the name for the concept of uniqueness of limits within category theory? Thanks.

Also, please note that I read from the book “Fuzzy Topology” which gives a rigorous example of convergence to an infinte set at the MIT Science Library. This approach to point-free topology is based upon the concept of fuzzy sets.

I can’t explain to you how convergence to an infinite set works because doing so would take about 40-60 pages of typing! However, if this book might interest any experts in category theory then I might be willing to buy you a copy of the book if it is not available via inter-library loan.

(By the way, if anyone does read about domain theory and profinite math then you might be interested in the work of Professor Abbas Edalat because it contains a variety of profinite math derived within the context of domain theory.)

Finally, Todd, if you and Jim Dolan are discussing at all the generalized BGG resolutions then you might want to look at this paper which I referred Jim to because it uses a category theory approach to the subject which is cool (at least it is cool for just a few of us nerds :-). If you do look at this paper then it might be fun to discuss this paper here in the cafe, however, I would not want to intrude upon any work you might be doing with Jim (especially since I already have more than enough of my own work to do).

Posted by: Charlie Stromeyer Jr on November 4, 2007 5:52 PM | Permalink | Reply to this

Re: categories, limits and logics

Here are four comments on the above in terms of category theory:

1) Universal algebra is a special branch of model theory, and this wikipedia entry on universal algebra briefly mentions its relationship to category theory. For example, the great F.W. Lawvere showed in his PhD thesis that every algebraic theory corresponds to a cartesian category and vice versa. This wikipedia entry provides a free link to Lawvere’s thesis.

2) Aha, I just found one answer to my question! This paper uses category theory to argue that limits ARE important for logics (however, I won’t be able to see this paper until I go back to the library).

3) The forthcoming “Rosetta stone” paper by Mike Stay and John Baez might give us some clues about the role of limit(s) for logics. This is because the paper applies the framework of symmetric monoidal closed categories to both topology and logic, and because the concept of convergence is a basic and defining notion of topology.

I look forward to reading this paper. In preparation for this paper, what is a good intro to the concept of SMCCs? Preferably, I would like to read an intro written by John Baez such as one of his TWFs. Thanks.

4) There are various papers which show how fuzzy sets (which generalize classical sets) can be described via categories such as this paper and this paper. This means that the concept of convergence to an infinite set can be understood via the language of category theory.

(However, likewise, I will have to wait until I go to the library to see these papers. Also, even though I think I understand the concept of convergence to an infinite set I am just a beginner in category theory - with the sole exception of one type of higher commutative n-gerbes).

Posted by: Charlie Stromeyer Jr on November 5, 2007 2:30 PM | Permalink | Reply to this

Re: categories, limits and logics

Charlie asks:

what is a good intro to the concept of SMCCs? Preferably, I would like to read an intro written by John Baez such as one of his TWFs. Thanks.

I didn’t find an intro on John’s website, but there are other fine options. Saunders Mac Lane treats smc cats in his classic Categories for the Working Mathematician. I’d recommend that book generally to anyone starting out in category theory who wants to learn more.

If you’re looking for something online, you might look around in John Armstrong’s blog (or ‘blath’ as he prefers to call it), where he treats smc cats and many other categorical topics ab initio. (You’ll land right in the thick of symmetric monoidal closed categories if you click here.) If you get really serious about the theory of closed categories and enriched categories, you’d probably want to delve into Max Kelly’s masterful treatise, although I wouldn’t recommend that to beginners.

I’d also recommend this inspiring paper by Lawvere on closed category theory.

Posted by: Todd Trimble on November 5, 2007 9:23 PM | Permalink | Reply to this

Re: Concrete Groups and Axiomatic Theories II

Interesting about Tarski. I know he worked with Jonsson, using what they called ‘generalized Brandt groupoids’ (equivalent to what we call ‘groupoids’) to model relation algebras.

Jonsson, B. and A. Tarski, “Boolean algebras with operators, Part I,” American Journal of Mathematics, vol. 73 (1951), pp. 891-939; “Part II,” vol. 74 (1952), pp. 127-162.

This paper by Stephen Comer seeks to generalise their work.

Posted by: David Corfield on November 4, 2007 1:22 PM | Permalink | Reply to this

a more natural proof of the “harder half”

I find your proof of the “harder half” a bit difficult to follow.

Well, so I did not follow it (as I’m not familiar with all the concepts around category theory) but I’ll write a proof in simpler terms.

So let’s take a theory T. An element of Th(Aut T(X),X) is a subset of some X^n that is a union of obits of the action of Aut T(X) on X^n. What is to prove is that it is definable in the logic of the theory T.

Since X^n is finite, this union of orbits is definable by simple logical connectors out of a list of predicates that separate the orbits.
Thus we are reduced to proving that any two orbits of Aut T(X) in X^n can be separated by some formula in the theory T.

In other words, if we take any two n-tuples (x_1,…,x_n) and (y_1,…,y_n) in X^n, then, we have to prove that
- Either there is an automorphism that maps (x_1,…,x_n) to (y_1,…,y_n)
- Or there is a formula R where R(x_1,…,x_n) is true and R(y_1,…,y_n) is false.

Logically we can reduce the problem to the case when all x_1,…,x_n are different, by quotienting {1,…n} by the equivalence relation (x_i=x_j) and directly getting a formula we need ifever (y_i=y_j) is not the same equivalence relation.

Finally, we just have to extend the injective map (x_i -> y_i) into a permutation of X, so that it will be an automorphism. Indeed, letting m=(Card X -n), if we could find more x’_1…x’_m and y’_1…y’_m so that x’_j -> y’_j extends x_i -> y_i into a permutation of X, such that there is still no formula R’ where R’(x_1,…,x_n,x’_1,…x’_m) is true and R’(y_1,…,y_n,y’_1,…y’_m) is false, then this is an automorphism of X (if it was not, there would be some logical relation between some p variables that would differ in the bijection, and a point of X^p that makes the difference provides a definition of R’).

Let us process this extension by induction on the remaing elements of X, which is supposed to be finite. To simplify the conventions, let us write it only for the first step, while the next steps are formally identical with larger values of n.
Starting with x_1,…,x_n that can be mapped to y_1,…y_n, take an arbitrary x’ outside {x_1,…,x_n} and look for candidates y’ that x’ could be mapped to. The case of impossibility is described in the following way:
For every z outside {y_1,…,y_n}, there is a formula R_z such that R_z (x_1,…,x_n,x’) is true and R_z (y_1,…,y_n,z) is false.
But then, the formula “there exists x’ such that the conjunction of the formulas R_z(x_1,…,x_n,x’) over all z, is true” is a formula that is true for (x_1,…,x_n )but false when substituted by (y_1,…,y_n), contradicting the assumption of non-existence of such a formula.

I’m interested in these subjects because I started writing an exposition of mathematics that aims to explain all basic concepts from their beginnings in all the most elegant and rigourous ways possible. (I’m sorry, it’s only in French for now there, and still unfinished).
To sum up briefly some special features of my approach:
I introduce by general ideas of metamathematics. Then I explain what is a set (it is the domain of a variable), then what is the difference between a set and a class, explained in about 3 pages with help of the flow of time (“contrary to a set, a class remains able to contain elements that do not yet exist”) after a discussion of a harder variant of the liar paradox (“this sentence is well-defined and false”).
I accept 3 types of objects in my set theory: pure (or any) elements, sets and maps. A couple (x,y) is defined to be a map from a fixed pair (left->x, right->y), in order for the cartesian product to be a particular case of product of families of sets.
I explain that what is doubtful in set theory is the axiom of power set, that rigourously should be presented not as a pure axiom but as also an extension of the language of set theory that names these power sets.
After some relatively more usual presentation of basic concepts of set theory, I enter a detailed study of Galois connections, complete lattices and the fixed point theorem.
Only then, based on it, I define finiteness of sets (with no use of natural numbers, and independently of the axiom of choice), and finally introduce the axiom of infinity in the form “there exists an infinite set”.

I also wrote an explanation of the replacement axioms, that is much deeper than what is usually told about it. That is, the naive interpretation of these axioms that is found in all courses violates the distinction between sets and classes, and this would a priori open the risk to lead to contradiction. Fortunately, a careful reinterpretation of the replacement axioms shows a good reason to trust their consistency (while only the consistency of the power set axiom remains doubtful), but also shows how tremendously strong they are (this is no secret for those who know the proof of the equivalence between replacement and the Reflection principle, but this understanding should be more widespread).

After a simple (but “dynamical”) presentation of model theory (that is still a draft), I plan to go on with universal algebra and category theory up to tensor calculus, for use to students in physics. But I do not work very fast and it may take a few more years to reach there.

Posted by: Sylvain Poirier on November 6, 2007 3:07 AM | Permalink | Reply to this

Re: a more natural proof of the “harder half”

Sylvain, you might be interested in the book “Accessible Categories: The Foundations of Categorical Model Theory” by M. Makkai and R. Pare, Conemporary Mathematics volume 104 (1989), American Mathematical Society.

You can read a free and brief review of the book by John Gray right here. This book considers infinitary logic that allows quantifiers over infinite sets of variables, and this book interests me because it provides a second answer to my earlier question by describing how limits (and colimits) within category theory are relavant for logic (but I won’t be able to see this book until I return to the library).

Posted by: Charlie Stromeyer Jr on November 6, 2007 1:01 PM | Permalink | Reply to this

Re: a more natural proof of the “harder half”


First of all, I’m glad you were stimulated to construct a proof that you find easier to follow. And you may be right, that the majority of mathematicians, presented with your proof and mine, would find yours easier to follow; perhaps it takes a certain type of experience of categorical thinking to appreciate what I’m doing. (Then again, this is the nn-Category Café! So I don’t feel too guilty for inflicting this on the readership. :-))

I do suspect that my proof, so different in character, suggests (for those who follow it!) generalizations or connections to other branches of mathematics which would not at all be apparent in a more traditional presentation, and that’s really what this is about. More about this may come out in comments.

Since you say you are writing about logic and foundations, I would warmly encourage you to examine the categorical point of view. One terrific insight, due to Lawvere, is the analogy which in one form reads (roughly)

restriction:induction::substitution:quantificationrestriction: induction :: substitution: quantification

which suggests interactions between representation theory and logic which I don’t think are obvious from traditional presentations of logic. As we get deeper into the themes of the Geometric Representation Theory seminar, these connections will become more and more useful to us (and so my post was really written for those who are seriously trying to absorb some of the deeper undercurrents of things being said there).

Posted by: Todd Trimble on November 6, 2007 3:27 PM | Permalink | Reply to this

Re: a more natural proof of the “harder half”

Thinking about the predicate logic/representation theory analogy of Lawvere, what would be the analogue of your post for representations?

Let’s stick with single-typed theories. Then given a group GG, for any object nn in FinSet there is the group G nG^n, and the category of representations Vect G nVect^{G^n}. So there’s a functor Rep(G *):FinsetCatRep(G^*): Finset \to Cat. I guess the codomain should be better specified. Some kind of rig category?

Then we might look for a Galois correspondence between sub-‘theories’ of Rep(G *)Rep(G^*) and sub-thingies of Aut(G)Aut(G). Would we be looking at Aut(G)Aut(G) as a 2-group?

And would we have been better off allowing GG to be a groupoid?

Posted by: David Corfield on November 7, 2007 8:56 AM | Permalink | Reply to this

Re: a more natural proof of the “harder half”

Some kind of rig category?

I meant of course, the category of some kind of rig categories?

I suppose if we opted for groupoids instead of groups, we might even have a 2-functor Rep(G *):GrpoidCatRep(G^*): Grpoid \to Cat, where Rep(G *)(H)=Vect G HRep(G^*)(H) = Vect^{G^H}.

Posted by: David Corfield on November 7, 2007 2:14 PM | Permalink | Reply to this

Re: a more natural proof of the “harder half”

David, you’re asking a lot of great questions; I’m deriving a lot of encouragement and stimulation from them. Thanks very much!

Now that you ask me directly: I’m not quite sure how (or if) my post generalizes to representations of groupoids, but let me sketch a few things I’m vaguely thinking about, and how they relate to the Tale of Groupoidification.

I’d like to be a little bit flexible in the framework I adopt: hyperdoctrines are great and all, but a more explicitly 2-categorical framework seems to be called for right about now. For example, instead of dealing with functors T:FinBoolT: Fin \to Bool, it’s in some ways nicer to deal directly with a bicategory of relations Rel(T)Rel(T), whose objects are the types mm (finite product types), where a 1-cell mnm \to n is a TT-relation (an element of T(m+n)T(m + n)), and where a 2-cell is an inclusion (or entailment) between TT-relations. In fact, in my private calculations, this is the framework I normally work with.

Rel(T)Rel(T) is an example of what is called a cartesian bicategory, a notion introduced by Carboni and Walters. This notion was intended to cover the very examples Lawvere has in mind when he speaks of a “generalized calculus of relations”, which covers not only the bicategory of relations in a suitably nice category CC (technically, a regular category, like for example the category of TT-algebras for an equational theory TT), but also bicategories of spans (in a finitely complete category) or of internal profunctors. Probably now is not the time to embark on a technical discussion of these things; I can give references later (while researching these references, I found a fragment from a draft paper of a paper on relational calculus and C.S. Peirce’s system Beta by Gerry Brady and me, which gives a terse definition in full 2-categorical generality). But the idea is that such a bicategory of generalized relations is a monoidal bicategory whose tensor product is “cartesian product” – not a categorical (2-)product with the usual universal property, but which is determined up to equivalence by the property that it becomes a categorical product upon restriction to those 1-cells which behave in a ‘functional’ manner, which Carboni and Walters call maps (‘functionality’ is neatly expressed as the condition that the 1-cell is a left adjoint in the bicategory, e.g., in the bicategory of sets and relations, left adjoints are precisely the functions). In the case of Rel(T)Rel(T), there is an injection FinMap(Rel(T))Fin \to Map(Rel(T)) of the base category.

On the groupoid side, there are a number of interesting options. The one I’m most familiar with is the cartesian bicategory whose 0-cells are small groupoids GG, whose 1-cells are profunctors GHG -\mapsto H, and whose 2-cells are transformations. (The ‘functional relations’ are just functors between groupoids.) As I commented over here, this cartesian bicategory satisfies a Beck-Chevalley condition, which brings it even closer to the usual calculus of relations [in the literature, such cartesian bicategories are called discrete].

But much more intriguing at the moment is where the 0-cells are groupoids, whose 1-cells are spans of groupoids (composed by weak pullbacks), and whose 2-cells are transformations. It’s clear a lot of people (e.g., Jeff Morton) have contemplated this example; I’m embarrassed to admit that I haven’t checked whether this is a cartesian bicategory, but maybe this confession will goad me into checking that out. Variations on that theme would include groupoids over some given groupoid, such as the groupoid implicit in most of John’s talks, namely the groupoid of finite-dimensional vector spaces over F qF_q. Jim and John and I have looked at a lot of examples of qq-deformation in that setting (what sort of kick-started the Tale in the first place), and this is a kind of ‘covariant picture’ whose contravariant counterpart is the theory of linear species (due to Joyal and Street). Linear species are functors

GL(F q)Vect ;GL(F_q) \to Vect_{\mathbb{C}};

these form a monoidal category under a certain tensor product which decategorifies to the multiplication on J.A. Green’s modular representation ring over F qF_q. (I’m sorry; I don’t have time to explain all this now, and I’m anyway hoping John or Jim might jump in at some point.)

I honestly don’t know what form ‘Galois theory’ would take for any of these options; perhaps the ‘Galois group’, whatever it is, is better conceived as a 2-group of some sort, as you suggest. I’d have to think hard about that. But in my first post, I sort of threw out

is related … also perhaps to the theory of classifying toposes and their “Galois theory”.

and half-wondered whether anyone would bite. What I was vaguely thinking there was connecting up the baby theory in these posts with the results of a very interesting monograph by Joyal and Tierney, on how to capture the classifying topos of some theory as a topos of localic representations of a localic groupoid of model isomorphisms (to put it very roughly), extending Grothendieck’s Galois-theoretic description of the etale topos as continuous discrete representations of a profinite fundamental group.

Generalized Galois Theory has also been pursued by Janelidze, Borceux, and Dubuc; should follow up on that at some point.

(This comment feels like a bit of a brain dump; my apologies.)


  • A. Carboni and R.F.C. Walters, Cartesian Bicategories I, JPAA 49 (1987), 11-32.
  • A. Carboni, G.M. Kelly, R.F.C. Walters, R.J. Wood, Cartesian Bicategories II, submitted Aug. 2007. (This is what Kelly was working on when he died.)
  • A. Joyal and R.H. Street, The category of representations of the general linear groups over a finite field, J. Alg. 176 (3) (1995), 908-946.
  • A. Joyal and M. Tierney, An Extension of the Galois Theory of Grothendieck, Memoirs of the AMS 309 (1984).
Posted by: Todd Trimble on November 7, 2007 7:22 PM | Permalink | Reply to this

Re: a more natural proof of the “harder half”

In fact, in my private calculations, this is the framework I normally work with.

Rather aptly, where your name appears on page 260 of my book, Penrose’s appears opposite, saying, along with Rindler, about the abstract tensor notation:

Unfortunately the notation seems to be of value mainly for private calculations because it cannot be printed in the normal way.

There I mention the paper you wrote with Geraldine Brady on String diagrams and Peirce’s Beta graphs.

I’d love to know whether Jim’s sense that after propositional and predicate logic comes modal logic, is independent of Peirce’s ideas about Alpha, Beta, Gamma systems. As you know, the Gamma system aims to capture modality, and has the sheets on which the diagrams appear coloured in heraldic tinctures (azure, gules, argent, sable, etc.)

This comment feels like a bit of a brain dump

If you can’t dump your brain here, where else?

For the record, I should note that where above I’m wondering about Vect G HVect^{G^H} for GG and HH groupoids, Jeff Morton is already doing that kind of thing. For example on page 62 of his paper, he’s talking about [[Π 1(B),G],Vect][[\Pi_1(B), G], Vect], so looking at the groupoid of maps from the fundamental groupoid of a space into a group, and then mapping that groupoid into Vect.

Posted by: David Corfield on November 8, 2007 11:31 AM | Permalink | Reply to this

Re: Concrete Groups and Axiomatic Theories II

So, Todd, what happens when we move away from single type theories? If we want to consider theories with two types, XX and YY, can we phrase a similar Galois duality?

We might consider subtheories of P(X *)×P(Y *)P(X^*) \times P(Y^*) and groups of transformations which are subgroups of X!×Y!X ! \times Y !.

But we might want to restrict to situations where we have the same subgroup of X!X ! and Y!Y !.

Posted by: David Corfield on November 6, 2007 9:10 AM | Permalink | Reply to this

Re: Concrete Groups and Axiomatic Theories II

Okay, good question! Let me see.

In the case of just one basic type XX, the general types for our relational theory are nn-fold products X nX^n. And the morphisms of the base category between such types are just those which are definable from finite product structure (diagonal maps, projections); these are precisely the pullback operations X f:X nX mX^f: X^n \to X^m, where f:mnf: m \to n is a function in FinFin. In other words, the category of types and pullback operations in this case is equivalent to Fin opFin^{op}: this is the free category with finite products generated from a single type XX.

In the multi-typed case, the base category of types ought to be the free category with finite products generated by the set of basic types SS. One can construct this by a variety of means, for example by string diagrams. Alternatively, one can describe the free category with finite coproducts Coprod(S)Coprod(S) generated from SS as a “wreath product” FinSFin \int S, and then take the opposite category. The objects of FinSFin \int S are tuples (m;s 1,,s m)(m; s_1, \ldots, s_m) where mm is an object of FinFin and the s is_i are elements (types) of SS. Morphisms

(m;s 1,,s m)(n;t 1,...,t n)(m; s_1, \ldots, s_m) \to (n; t_1, ..., t_n)

are functions f:mnf: m \to n such that s i=t f(i)s_i = t_{f(i)}. (Remark: FinSFin \int S has pushouts because both FinFin and the discrete category SS have pushouts.)

In this language, an SS-typed theory would be a functor (and let’s stick with the finitary case for now):

T:FinSBool finT: Fin \int S \to Bool_{fin}

where each T(f)T(f) has a left adjoint (quantification), subject to Beck-Chevalley, and so on. Actually, in the finitary case a Boolean algebra map T(f)T(f) automatically has a left and right adjoint, so the only condition one needs to keep track of is Beck-Chevalley. By baby Stone duality, the functor TT is tantamount to an atomic relations functor

A:(FinS) opFinA: (Fin \int S)^{op} \to Fin

and the Beck-Chevalley condition translates into saying that AA takes pullbacks in (FinS) op(Fin \int S)^{op} to weak pullbacks (weakly cartesian squares) in FinFin.

If we interpret each type sSs \in S as a finite set X sX_s, then there is an induced product-preserving functor

τ:(FinS) opFin\tau: (Fin \int S)^{op} \to Fin

which extends sX ss \mapsto X_s, unique up to isomorphism. The corresponding tautological theory is

FinSτ opFin opPBool finFin \int S \stackrel{\tau^{op}}{\to} Fin^{op} \stackrel{P}{\to} Bool_{fin}

and τ\tau itself is therefore the atomic relations functor for this theory.

A key fact is that τ\tau is representable: a representing object in FinSFin \int S is

X:=( sSX s;X ss sS)X := (\sum_{s \in S} X_s; \langle X_{s} \cdot s \rangle_{s \in S})

as we can verify from the calculation hom(s,X)X shom(s, X) \cong X_s [here X ssX_{s} \cdot s denotes a string of X sX_s copies of ss].

A subtheory of the tautological theory now translates to a quotient map of τhom(,X)\tau \cong hom(-, X):

q:hom(,X)Aq: hom(-, X) \to A

which is weakly cartesian in the sense of my post. From here on out it’s smooth sailing; everything in my post translates smoothly into this more general setting. Here

Aut(X)= sS(X s)!Aut(X) = \prod_{s \in S} (X_s)!

and we get a Galois correspondence between subgroups GAut(X)G \subseteq Aut(X) and subtheories of TP(τ)P(hom(,X))T \subseteq P(\tau) \cong P(hom(-, X)). Also, τ op\tau^{op} preserves coproducts (by definition), and PP takes coproducts to products, so

P(τ)(m;s 1,,s m)= i=1 mP(X s i).P(\tau)(m; s_1, \ldots, s_m) = \prod_{i = 1}^m P(X_{s_i}).

All of which is saying that basically, you were right on the money.

Posted by: Todd Trimble on November 7, 2007 2:15 PM | Permalink | Reply to this

Re: Concrete Groups and Axiomatic Theories II

Does Chu help us think about the Galois connection?

Posted by: David Corfield on November 6, 2007 9:50 AM | Permalink | Reply to this

Re: Concrete Groups and Axiomatic Theories II

Todd, you might be interested to know that Rogers also applies ideas from Klein’s Erlanger Programm to logic. From the wikipedia entry on recursion theory (which is a branch of mathematical logic):

Rogers (1967) has suggested that a key property of recursion theory is that its results and structures should be invariant under computable bijections [isomrphisms in the category Set] on the natural numbers (this suggestion draws on the ideas of the Erlangen program in geometry). The idea is that a computable bijection merely renames numbers in a set, rather than indicating any structure in the set, much as a rotation of the Euclidean plane does not change any geometric aspect of lines drawn on it. Since any two infinite computable sets are linked by a computable bijection, this proposal identifies all the infinite computable sets (the finite computable sets are viewed as trivial). According to Rogers, the sets of interest in recursion theory are the noncomputable sets, partitioned into equivalence classes by computable bijections of the natural numbers.

By the way, I should pay more attention to what David Corfield says for this reason:

“The philosopher’s role is to tell the AI specialist that he doesn’t know what he’s talking about, to put it bluntly.” - Gian-Carlo Rota

Posted by: Charlie Stromeyer Jr on November 7, 2007 11:18 PM | Permalink | Reply to this
Read the post Albert Lautman
Weblog: The n-Category Café
Excerpt: The philosophy of Albert Lautman
Tracked: February 4, 2008 2:41 PM
Read the post A Strange Link
Weblog: The n-Category Café
Excerpt: Tim Porter on global actions
Tracked: April 1, 2008 7:55 AM

Post a New Comment