Cool category construction: Q-trees

[Hurkyl]

Hurray for an alliterative title.

I guess I'll have to apologize in advance if you don't like logic-type stuff, but I thought these were pretty cool! A Q-sequence is basically a formal-logic-like thing you can do in any category.

The basic example is that of a diagrammatic definition. Consider the statement that a given morphism is an isomorphism:

         E
         |
  --->   | --->
.      . |.    .
         | <---

Of course, normally you'd see one of these on a blackboard, and you'd draw the left diagram, say "there exists" and then draw the right diagram on top of the old one... but here we want to consider the "frames" as separate.

One can interpret this diagram in Cat: the two diagrams are presentations of categories, and we have a functor that maps the left diagram into the right diagram.

Of course, that's not enough to do formal logic; let me first introduce the Q-sequence.


A Q-sequence is a finite sequence of objects in a category, morphisms from each object to the next, and a label of "A" or "E" on each of the objects.

The above "definition" of isomorphism is almost a Q-sequence -- the category in the left diagram has the label "E" (which has been drawn above the line separating them). We want to label the other category with an "A".


We can get a Q-sequence to act like a logical predicate. Let's call the above two categories S and T. If we wanted to say that some morphism in a category C was an isomorphism, that is the same as saying:

For the functor S-->C that maps the displayed arrow to the chosen morphism, there exists a functor T-->C such that the following diagram commutes:

S ---> T
 \     |
  \    |
   \   |
    \  V
     > C

Formally, we can define "satisfaction" of a Q-sequence as follows:

Given a Q-sequence of length 1, that is a single object R (for root):

A given morphism R ---> A satisfies the Q-sequence if and only if R has the label "A".

Given a Q-sequence R ---> Q (where Q denotes the rest of the Q-sequence):

A given morphism R ---> A satisfies the Q-sequence if and only if:

If R is labelled "A", and for all morphisms satisfying the Q-sequence Q, we have the commutative diagram

R ---> Q
 \     |
  \    |
   \   |
    \  V
     > A

or if R is labelled "E", and there exists at least one morphism satisfiying Q such that the above diagram commutes.


Here's another Q-sequence in Cat, this one defining that a category has a terminator:

E   A   E   A        E        A
|   | . | . | .      | .      |
|   |   | | | |\     | |\     |
|   |   | | | | \    | | \    |
|   |   | | | |  \   | |  \   |
|   |   | | | |   \  | |   \  |
|   |   | V | V    V | V 1  V |
| T | T | T | T--->T | T--->T |

Note that the first category in this Q-sequence is the empty category, 0. (It's to the left of the first bar)

(Although we usually don't, I've added the right-most quantifier)

(exercise: prove that the functor 0--->A satisfies this Q-sequence if and only if A has a terminator)


Here's another diagrammatic definition, this one stating that for any pair of objects in a category, there is a morphism between them:

A      E
|      |
|      | .--->.
|      |
| .  . +---------
|      |
|      | .<---.
|      |

Notice that this one has a new feature: the diagram splits! This one is saying that given two objects A and B, there exists a morphism A--->B, or there exists a morphism B--->A.


This can't be handled by a Q-sequence, so we need a Q-tree!

A Q-tree is a (rooted) tree whose vertices are objects of the category, whose edges are morphisms leading from the parent to the child, and with each vertex labelled with "A" or "E".

Now, given a Q-tree with root R, a morphism R--->A satisfies the Q-tree iff:

R is labelled "A" and for any of its children S, and any morphism S--->A, we have the commutative diagram

R ---> S
 \     |
  \    |
   \   |
    \  V
     > A

or R is labelled "E", and there exists a child S and a morphism S--->A such that the above diagram commutes.

(Notice that this definition works if we treat a Q-sequence as a Q-tree... it even handles the length-1 Q-sequences correctly)


Cat isn't the only category we can do these things in. For example, I worked out that in Ring, you can write a Q-tree defining the predicate that a ring is a division ring:

       Z
       |(A)
       |
       V
      Z[x]
      /  \(E)
     /    \
    /      \
   /        \
  V          V
Z[x,x^-1]    Z

Where the morphism on the left is the canonical embedding, and the morphism on the right is the one mapping x to zero.

Then, a ring R is a division ring if and only if the map Z--->R satisfies this Q-tree.


Sure, these things resemble logical predicates, but is it fair for me to say that you can do formal-logic like things? Well, with a little bit of thought, you will be able to see how to do any basic logical operation on Q-trees: and, or, negation, and quantification-like things.

For example, negation is simply swapping the "A"s and the "E"s.

In the case of Cat, categories such as:

.--->.  .--->.  .-->.

behave as if they had "free variables". If I call this R, and I let S be the similar category with one less arrow, then I can universally quantify a Q-tree whose root is R as follows:

Let S be the root of the new Q-tree, labelled with "A".
Let R be the only child of S. The functor S--->R maps the arrows of S to the ones that are not being quantifed upon.
Let the old Q-tree "sprout" from R.


The book I've read these from prove an interesting theorem, I don't know how generally useful it is:

Let C and R be two classes of morphisms such that for any x in C, y in R, and diagram

  x
.--->.
|    |
|    |
|    |
V y  V
.--->.

there exists an arrow from the top-right corner to the bottom-left corner.

Then, if your Q-tree uses only morphisms from C, morphisms of R preserve and reflect satisfaction.

That is, if A is the root of the Q-tree...

If A--->B satisfies, and B--->C is in R, then A--->B--->C satisfies.
If A--->C--->B satisfies, and C--->B is in R, then A--->C satisfies.


The book uses this to prove that the properties preserved and reflected by equivalence functors are exactly the properties one can define in the formal language of the diagrams you would draw on the blackboard. (In particular, one cannot identify objects in this language)

I'm sort of curious if this theorem is useful in other contexts.

 

[fresh_42]

This isn't consistent at all. Your Q-sequences are just morphisms which can be concatenated. And given a morphism form A to B, it is not enough to require a morphism from B to A to get an isomorphism. And the S-T-C example is also fulfilled by projections which are far from being bijective.

Functors turning arrows are called contravariant. So they are already part of homological algebra. And although it sometimes looks like homological algebra could be replaced by a logical system, this is not true. The various concepts of homological algebra carry a meaning which you cannot model by logical formalism. If you do it correctly, you will reinvent homological algebra.

I'm afraid there is nothing new under the sun in your post, only quite some gaps.