MW: We’re reviewing hyperdoctrines, which are specially nice functors B: FinSet → BoolAlg. When we have such a functor, any map f of finite sets gives a homomorphism of boolean algebras, B(f). But we’ve seen this is a morphism and a functor. (“It’s a floor wax and a dessert topping!”) What do you think about the term “adjoint morphism”? It might help keep the two levels straight.
JB: I think any attempt to keep levels straight in category theory by making up new terminology is doomed to fail. It’s better to learn to live in a world where everything operates on multiple levels. For example: every functor is a morphism, namely a morphism in the category Cat. Every category is an object in Cat. And so on. It’s dizzying at first, but once you can keep your balance you begin to gain super-powers.
While I’m at it, I’d like remind our massive audience that B(f) is more than a mere functor in two ways. First, obviously, it’s not going between arbitrary categories: it’s going between boolean algebras. Second, it’s not just an arbitrary functor between categories that happen to be boolean algebras: it’s a homomorphism of boolean algebras. An arbitrary functor between boolean algebras must preserve the ordering that says which propositions imply which, but B(f) is better: it must preserve all the boolean algebra operations, including negation and the nullary operations T and F (aka ⊤and ⊥, aka verum and falsum, or true and false if you speak English).
On the other hand, we shouldn’t jump to the conclusion that the left or right adjoint of B(f) will be a boolean algebra homomorphism. If we get into those adjoints we’ll see.
MW: As a lover of ZF set theory, I have no standing to complain about multiple levels! All right, full speed ahead.
When we regard a boolean algebra B as a category, that means we treat B is a poset, under the relation of implication: p≤q when p→q=⊤. We looked at the injection f:{x}→{x,y}, where B(f) sends P(x) to (P(x)∧y=y). (That “y=y” is just to make the pseudo-dependence on y explicit. Short-hand for “P(x) regarded as a predicate on the two variables x and y”. I’ll leave it out when things are clear enough without it.)
So the right adjoint condition reads
P(x) ≤ Q(x,y) iff P(x) ≤ ∀yQ(x,y)
since when P(x) implies Q(x,y) regardless of the value of y, P(x) implies ∀yQ(x,y). And conversely. So universal quantification is right adjoint to injection. Likewise,
Q(x,y) ≤ P(x) iff ∃yQ(x,y) ≤ P(x)
So existential quantification is the left adjoint. This may look a little stranger. The way to think about it: P(x)∧y=y has the same truth-value regardless of the value of y. If we can find even one y for which Q(x,y) implies P(x)∧y=y, that’s enough to insure that P(x) holds if Q(x,y) does (for that y).
Or just use the fact that p ⇔ q is equivalent to ¬p ⇔ ¬q, and p≤q iff ¬q≤¬p. So negating both sides of the “∀ equation” gives us
¬Q(x,y) ≤ ¬P(x) iff ¬∀yQ(x,y) ≤ ¬P(x)
and of course ¬∀yQ(x,y) is equivalent to ∃y¬Q(x,y). Since P and Q represent arbitrary predicates, it’s okay to knock out all the negation signs.
The surjection g:{x,y}→{x} gave us equality, after a fashion. B(g) sends Q(x,y) to Q(x,x). Right adjoint:
Q(x,x) ≤ P(x) iff Q(x,y) ≤ (x=y→P(x))
using the propositional fact that p→(q→r) means the same as (p∧q)→r. The right adjoint sends P(x) to x=y→P(x).
Left adjoint:
P(x) ≤ Q(x,x) iff (P(x)∧x=y) ≤ Q(x,y)
The left adjoint sends P(x) to P(x)∧x=y.
I suppose we should next look a completely general map in FinSet. Perhaps all the interesting phenomena come from compositions of our two special cases? Maybe the Beck-Chevalley and Frobenius conditions play their parts here?
JB: In FinSet (and many other categories, but far from all) every morphism is an epimorphism followed by a monomorphism. That’s a fancy way to say that every map between finite sets is a surjection followed by an injection.
Just now you looked at the surjection g:{x,y}→{x}, and this illustrates what a general surjection does for us when we have a hyperdoctrine B: FinSet → BoolAlg. It gives a map of boolean algebras that takes any formula with some set of free variables and identifies variables, getting a formula with a smaller set of free variables. As you just illustrated, the right and left adjoints of this take any formula X with the smaller set of free variables and make it into a formula with the larger set of free variables—but in two different ways. The left adjoint takes the conjunction of X with a bunch of equations saying which variables got identified. The right adjoint forms an implication that says “if the variables that got identified are equal, then X”.
Before that you looked at the injection f:{x}→{x,y}, and this illustrates what a general injection does for us. It gives a map of boolean algebras that takes any formula with some set of free variables and throws in extra variables, getting a formula that formally involves a larger set of free variables, but where the new extra variables are actually unused. We saw the left and right adjoints of this map both take any formula with the larger set of free variables and make it into a formula with the smaller set of free variables—but again, in two different ways. The left adjoint existentially quantifies over all the extra variables. The right adjoint universally quantifies over them.
So now we can understand what our hyperdoctrine does to an arbitary map. Any map between finite sets is of the form fg where first we do a surjection g and then an injection f. So we know what B(fg) = B(f )B(g) does. First we identify some variables, then we throw in new extra variables that are actually unused!
Next, a nice lemma in category theory: the left adjoint of a composite is the composite of the left adjoints! But things get turned around, so the left adjoint of B(fg) is the left adjoint of B(f) followed by the left adjoint of B(g). So, first we take the conjunction of our formula with a bunch of equations, and then we stick a bunch of existential quantifiers in front of it.
Similarly, the right adjoint of a composite is the composite of the right adjoints, again turned around. So now we first say our formula is implied by a bunch of equations, and then we stick a bunch of universal quantifiers in front of that.
Does this make sense? Did I get it right? I find it easy to slip up with all these lefts and rights and ∃s and ∀s and ⋀s and →s. However, I have managed to beat into my brain that ∃ is a left adjoint and ∀ is a right adjoint. I think this is essential knowledge for any would-be categorical logician.
I also know this: none of what I just said uses the Beck-Chevalley and Frobenius conditions! What those conditions do is impose some laws of logic relating the various logical operations we’ve just gotten. Remember, the adjoints to our B(f)s and B(g)s aren’t boolean algebra homomorphisms, so there are a bunch of rules that they may not obey. There are some rules they do obey just by virtue of being adjoints. But alas, these aren’t enough to satisfy a logician. So we need Beck-Chevalley and Frobenius to come rescue us!
MW: Okay! I’ll need to do a bigger example to perfuse these ideas into my head. (I prefer prefusion to beating, at least when it comes to my head.) Also I should check whether those adjoints are algebraic homomorphism, and not just order-preserving maps. I’m sure some aren’t, or you wouldn’t keep bringing it up!
But I think this post is a good length right now, so that’s on the agenda for the next one.
Diagonal Argument 
There’s a uniform formula for the adjoints of B(f) for f: X={x1,…,xn} → Y={y1,…,ym}: the right adjoint takes P(y1,…,ym) to ∀y1…∀ym(f(x1)=x1 ∧ … ∧ f(xn)=xn → P(y1,…,ym)), and the left adjoint takes P(y1,…,ym) to ∃y1…∃ym(f(x1)=x1 ∧ … ∧ f(xn)=xn ∧ P(y1,…,ym)).
In principle, X and Y should be disjoint for this to work correctly; alternatively, you can rename all of the elements of Y in the final results, since they’re dummy variables there. But as long as f acts as the identity on an element of X∩Y, then it’s equivalent (and gives a simpler result) to instead remove the spurious quantifier arising from its membership in Y and remove the redundant equality statement arising from its membership in X.
In particular, for the inclusion {x} → {x,y}, the proper thing to do is to rename x in {x,y} to z, so that the adjoints take P(x,y) to ∀z∀y((z=x) → P(z,y)) and ∃z∃y((z=x)∧P(z,y)); but these simplify to ∀yP(x,y) and ∃yP(x,y). (Note that you wrote Q for my P when doing this example.) And for the projection {x,y} → {x}, the proper thing to do is to rename x in {x} to z, so that the adjoints take P(x) to ∀z((z=x ∧ z=y) → P(z)) and ∃z((z=x ∧ z=y) ∧ P(z)); but these simplify to (y=x) → P(x) and (y=x) ∧ P(x). (Here you wrote P for my P.)
Nice!
There’s a subtety to your first two equations; I missed it the first time I read it. You have for the right adjoint
∀y1…∀ym(f(x1)=x1 ∧ … ∧ f(xn)=xn → P(y1,…,ym))
and similarly for the left adjoint. I wondered at “f(x1)=x1”—how did fixed points get into the picture?
But the “f(x1)” is a meta-term; that is, it stands whichever yi is the target of x1 under f. This becomes clear with your examples.
Yes, the whole thing ended up being more confusing than I anticipated because of things like this, but I persevered!