Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: cylindric algebras & hyperdoctrines

Naso (Apr 05 2023 at 07:37):

The wikipedia entry on cylindric algebra says : "Hyperdoctrines are a categorical formulation of cylindric algebras". Does anyone know of a reference that explains this?

Reid Barton (Apr 05 2023 at 07:59):

[[hyperdoctrine]] [[Boolean hyperdoctrine]]
Seems like the closest comparison would be between a cylindric algebra and a Boolean hyperdoctrine on the opposite of the category of finite sets. The main difference is that in a cylindric algebra we combine all the formulas into a single Boolean algebra $A$, while in a hyperdoctrine we have a separate Boolean algebra $P(n)$ of formulas in n free variables for each $n$.
Basically, it is similar to the difference between working with or without an explicit context.

Naso (Apr 05 2023 at 08:40):

thank you. I am new to this. When you say a boolean hyperdoctrine on the opposite of the category of sets, do you mean a functor $P : \mathsf{FinSet} \to \mathsf{BoolAlg}$? (since $\mathsf{FinSet} = (\mathsf{FinSet}^{op})^{op}$)

Reid Barton (Apr 05 2023 at 09:08):

Yes but there is a close to 50% chance that I messed up the variance anyways.

Reid Barton (Apr 05 2023 at 09:13):

The idea would be: We could define one Boolean hyperdoctrine by picking our favorite language of first-order logic and then letting $P(I)$ be the set of formulas in this language with free variables from $I$, say denoted by $x_i$, $i \in I$. (Then, we should quotient these formulas by bi-implication but I'll ignore this.) For fixed $I$, $P(I)$ is a Boolean algebra because we can form conjunctions, disjunctions, negations of formulas.
Now if we have a map $f : I \to J$ of sets, then we get a homomorphism $P(I) \to P(J)$ of Boolean algebras that takes every occurrence of $x_i$, and replaces it with $x_{f(i)}$. In other words, it carries out a substitution where we are only allowed to substitute variables by other variables.

Reid Barton (Apr 05 2023 at 09:18):

The map $P(f) : P(I) \to P(J)$ is supposed to have a left adjoint, which turns out to encode the existential quantifier $\exists x_{\alpha}$ if $f$ is an inclusion $I \to I \cup \{\alpha\}$, and to encode imposing an equality $x_\beta = x_\gamma$, if $f$ is the function that identifies two elements $\beta$, $\gamma$ of $I$. So, that corresponds somehow to the $c$'s and $d$'s of the cylindric algebra.

Reid Barton (Apr 05 2023 at 09:27):

I'm using "formulas" because this is somehow the original motivating example, but it's also important to note that the elements of the Boolean algebras $P(I)$ (or of a cylindric algebra) can be anything, like subsets of $2^I$; then we're working with the semantics of the formulas, and not the syntax itself.

Reid Barton (Apr 05 2023 at 09:29):

It seems that maybe "cylindric algebras" and "hyperdoctrines" are notions used by mostly disjoint sets of people, so probably your best bet is to look for introductory material about each separately.

John Baez (Apr 05 2023 at 15:53):

Reid Barton said:

Yes but there is a close to 50% chance that I messed up the variance anyways.

But in the end you checked that you got the variance right.

John Baez (Apr 05 2023 at 15:55):

I wrote an introduction to hyperdoctrines, meaning functors $F: \mathsf{FinSet} \to \mathsf{BoolAlg}$ with a couple of properties, here:

• First-order categorical logic: the series.

John Baez (Apr 05 2023 at 15:56):

It's actually a dialog between Michael Weiss (an expert on some more traditional topics in logic) and me.

John Baez (Apr 05 2023 at 15:57):

These hyperdoctrines are indeed related to Tarski’s cylindric algebras - and also Halmos’ polyadic boolean algebras.

Evan Washington (Apr 06 2023 at 04:47):

I believe the variance is meant to go the other way. I think the argument given by Michael Weiss is basically 'right' but it actually shows that the functor is meant to be contravariant. Suppose we think of an $n$-tuple of variables (let's stay single-sorted for a moment) as a map $x: n \to V$. If you have a function $f: m \to n$, then we naturally get an $m$-tuple given by the composite $f \circ x$. So given a formula $\phi(x)$ on an $n$-tuple, we'll get a formula $\phi(x_f)$ on an $m$-tuple $x_f$. And to be extra explicit, $x_f$ is the $m$-tuple $x_{f(1)}, ..., x_{f(m)}$. One way, I think, to keep these straight is to think about the contravariant and covariant powerset functors. The contravariant one takes functions to boolean algebra homomorphisms (and in fact gives the equivalence $\mathsf{FinSet}^\mathrm{op} \simeq \mathsf{FinBool}$), but the covariant one does not (to convince yourself of this, think about the image under $f$ of the top element of the algebra).

Evan Washington (Apr 06 2023 at 05:03):

As to the original question, the only source I could find explicitly showing a correspondence between polyadic algebras and hyperdoctrines was this from Daigenault. He doesn't quite show this, but I think roughly the way things go is: polyadic algebras of dimension $\kappa$ are 'equivalent' to hyperdoctrines on $\mathsf{Set}_{\kappa}$. Cylindric algebras of dimension $\kappa$ should correspond to hyperdoctrines with equality on $\mathsf{Set}_\kappa$. The key idea in all this is that the operators $\exists(I)$ on the boolean algebra of formulas in variables from $V$, say $H(V)$ corresponds to the composite of $H(\iota) \circ \exists_\iota$ where $\iota : (V - I) \to V$. So the trick is picking out the adjoint functors corresponding to the monads $\exists(I)$.

Reid Barton (Apr 06 2023 at 05:31):

This is confusing because there are several hyperdoctrines around that look quite similar.
Here is another way to describe the one I was talking about:
Boolean algebras are the algebras for some algebraic theory Bool, so there's definitely a free functor F : FinSet -> BoolAlg, which is covariant and sends maps of finite sets to boolean algebra homomorphisms; that's my hyperdoctrine. (I don't have to restrict F to finite sets, and maybe to compare to cylindric algebras I don't want to, but let me stick to finite sets for now.)

Reid Barton (Apr 06 2023 at 05:33):

If $I$ is a finite set and we agree to denote the generator of $F(I)$ corresponding to $i \in I$ by $x_i$, then we see that the elements of $F(I)$ are terms generated by the variables $x_i$ and the operations of the theory of Boolean algebras, so things like $x_1 \vee x_2 \wedge \neg x_3$, quotiented by the relations of the theory (= up to logical equivalence).

Reid Barton (Apr 06 2023 at 05:36):

Ah wait this doesn't quite work yet because I still have to put in the quantifiers. But it does have the correct substitution structure.
You could say this is a "hyperdoctrine without quantifiers".

Reid Barton (Apr 06 2023 at 05:37):

i.e. I still have a functor F : FinSet -> BoolAlg (whose variance is what was concerned about), I just don't assume that the maps F(f) have adjoints on either side.

Reid Barton (Apr 06 2023 at 05:39):

There's a different hyperdoctrine $P : \mathrm{FinSet}^\mathrm{op} \to \mathrm{BoolAlg}$ that sends a set $S$ to its power set; I think you were describing that one.

John Baez (Apr 06 2023 at 05:39):

In my conversation with Michael Weiss we fixed a set $V$, the universe of discourse. Then an $S$-ary predicate $P$ picks out a subset of $V^S$, which we think of as a map $P : V^S \to 2$, or an element $P \in 2^{V^S}$.

So we're getting a Boolean algebra $B(S) = 2^{V^S}$ for each finite set $S$, and we're claiming this gives a covariant functor

$B: \mathsf{Finset} \to \mathsf{BoolAlg}$

John Baez (Apr 06 2023 at 05:40):

It's easy to get confused here for several reasons, and since it's late in the evening and I've had some wine I wouldn't believe I'm right if I hadn't convinced Michael against his opposition in our conversation, and then proceeded to write many articles on this topic without an "oops".

John Baez (Apr 06 2023 at 05:44):

In particular it's confusing because there's both a covariant and a contravariant power set functor. But here we are using the contravariant power set functor

$2^- \colon \mathsf{Set} \to \mathsf{BoolAlg}$

assigning to each set its boolean algebra of subsets, and each map between sets the corresponding "inverse image" or "preimage" operation, which is a Boolean algebra homomorphism.

(Sorry for using a "contravariant functor" instead of a covariant functor between categories, one with an op on top - I know it's a bit old-fashioned but I think it'll serve my purpose better here.)

John Baez (Apr 06 2023 at 05:46):

So the hyperdoctrine Michael Weiss and I were discussing is the covariant functor

$B: \mathsf{Finset} \to \mathsf{BoolAlg}$

sending $S$ to $B(S) = 2^{V^S}$, given by the composite of contravariant functors

$V^-: \mathsf{FinSet} \to \mathsf{Set}$

and

$2^-: \mathsf{Set} \to \mathsf{BoolAlg}$

John Baez (Apr 06 2023 at 05:51):

I think there's a 51% chance I got the variances right.