Tag Archives: cattheory

category theory, math, proof, representations

Proofs using diagrams

Leave a comment

Introduction

This post gives a proof of an easy theorem in category theory using the graph-based logic approach of Graph based logic and sketches, (GBLS) by Atish Bagchi and me.

Formal logic is typically defined in terms of formulas and terms, defined recursively as strings of characters, together with rules of inference. GBLS proposes a new approach to logic where diagrams are used instead of strings of characters. The exposition here spells out the proof in more detail than GBLS does and uses various experimental ways of drawing diagrams using Mathematica.

To follow this proof, you need to be familiar with basic category theory. Most special definitions that are needed are defined in this post where they are first used. Section 1 of GBLS also gives the definitions you need with more context.

The theorem

The Theorem to be proved (it is Theorem 8.3.1 of GBLS) says that, in any category, if the triangles in the diagram below commute, then the outside square commutes. This is easy using the associative law: If $xf=h$ and $kx=g$, then $kh=k(xf)=(kx)f=gf$.

Subject Diagram

So what?

This theorem is not interesting. The point of this post is to present a new approach to proving such theorems, using diagrams instead of strings. The reason that exhibiting the dig
rammatic proof is interesting is that many different kinds of categories have a FL cattheory, including these:

Essentially algebraic string-based logic is described in detail in Partial Horn logic and cartesian categories, by E. Palmgren and Steven Vickers.

Commercial

My concept of form in A generalization of the concept of sketch generalizes sketches to all the categories that can be defined as models of FL cattheories. So the method of proof using diagrams can be applied to theorems about the objects defined by forms.

Concepts needed for the graph-based proof

To prove the theorem, I will make use of $\mathbf{ThCat}$, the FL cattheory for categories.

  • An FL category is a category with all finite limits.
  • GLBS uses the word cattheory for what Category theory for computing science and Toposes, triples and theories call the theory of a sketch.
  • In many books and articles, and in nLab, a “sketch” is what we call the cattheory (or the theory) of a sketch. For us, the sketch is a generating collection of objects, arrows, diagrams, cones and cocones for the cattheory. The category of models of the sketch and the cattheory are equivalent.
  • $\mathbf{ThCat}$ is a category with finite limits freely generated by certain designated objects, arrows, commutative diagrams and limit cones, listed below.
  • A model of $\mathbf{ThCat}$ in $\mathbf{Set}$ (the category of sets, whichever one you like) is an FL functor $\mathfrak{C}:\mathbf{ThCat}\to\mathbf{Set}.$
  • Such a model $\mathfrak{C}$ is a small category, and every small category is such a model. If this statement worries you, read Section 3.4 of GBLS.
  • Natural transformations between models are FL-preserving functors that preserve the structure on the nose.
  • The category of models of $\mathbf{ThCat}$ in $\mathbf{Set}$ is equivalent to the category of small categories and morphisms, which, unlike the category of models, includes functors that don’t preserve things on the nose.
  • $\mathbf{ThCat}$ is an example of the theory of an FL sketch. Chapter 4 of GBLS describes this idea in detail. The theory has the same models as the sketch.
  • The sketch generating $\mathbf{ThCat}$ is defined in detail in section 7.2 of GBLS.

Some objects and arrows of $\mathbf{ThCat}$

I will make use of the following objects and arrows that occur in $\mathbf{ThCat}.$ A formal thing is a construction in $\mathbf{ThCat}$ that becomes an actual thing in a model. So for example a model $\mathfrak{C}$ of $\mathbf{ThCat}$ in $\mathbf{Set}$ is an actual (small) category, and $\mathfrak{C}(\mathsf{ar_2})$ is the set of all composable pairs of arrows in the category $\mathfrak{C}$.

  • $\mathsf{ob}$, the formal set of objects.
  • $\mathsf{ar}$, the formal set of arrows.
  • $\mathsf{ar}_2$, the formal set of composable pairs of arrows.
  • $\mathsf{ar}_3$, the formal set of composable triples of arrows.
  • $\mathsf{unit} : \mathsf{ob}\to \mathsf{ar}$ that formally picks out the identity arrow of an object.
  • $\mathsf{dom},\mathsf{cod} : \mathsf{ar}\to \mathsf{ob}$ that formally pick out the domain and codomain of an arrow.
  • $\mathsf{comp} : \mathsf{ar}_2\to \mathsf{ar}$ that picks out the composite of a composable pair.
  • $\mathsf{lfac}, \mathsf{rfac} :\mathsf{ar}_2\to \mathsf{ar}$ that pick out the left and right factors in a composable pair.
  • $\mathsf{lfac}, \mathsf{mfac},\mathsf{rfac} :\mathsf{ar}_3 \to\mathsf{ar}$ that pick out the left, middle and right factors in a composable triple of arrows.
  • $\mathsf{lass}, \mathsf{rass} : \mathsf{ar}_3 \to \mathsf{ar}_2$: $\mathsf{lass}$ formally takes $\langle{h,g,f}\rangle$ to $\langle{hg,f}\rangle$ and $\mathsf{rass}$ takes it to $\langle{h,gf}\rangle$.

$\mathsf{ob}$, $\mathsf{ar}$, $\mathsf{unit}$, $\mathsf{dom}$, $\mathsf{cod}$ and $\mathsf{comp}$ are given primitives and the others are defined as limits of finite diagrams composed of those objects. This is spelled out in Chapter 7.2 of GBLS. The definition of $\mathbf{ThCat}$ also requires certain diagrams to be commutative. They are all provided in GBLS; the one enforcing associativity is shown later in this post.

Color coding

I will use color coding to separate syntax from semantics.

  • Syntax consists of constructions in $\mathbf{ThCat}.$ The description will always be a commutative diagram in black, with annotations as explained later.
  • The limit of the description will be an object in $\mathbf{ThCat}$ (the form) whose value in a model $\mathfrak{C}$ will be shown in green, because being an element of the value of a model makes it semantics.
  • When a limit cone is defined, the projections (which are arrows in $\mathbf{ThCat}$) will be shown in blue.

Descriptions

In graph-based logic, a type of construction that can be made in a category has a description, which (in the case of our Theorem) is a finite diagram in $\mathbf{ThCat}$. The value of the limit of the description in a model $\mathfrak{C}$ is the set of all instances of that type of construction in $\mathfrak{C}$.

The Subject Diagram

  • This diagram is the subject matter of the Theorem. It is not assumed to be commutative.
  • As in most diagrams in category theory texts, the labels in this diagram are variables, so the diagram is implicitly universally quantified. The Subject Diagram is a generic diagram of its shape.
  • “Any diagram of its shape” includes diagrams in which some of the nodes may represent the same object. An extreme example is the graph in which every node is an object $\mathsf{E}$ and every arrow is its identity arrow. The diagram below is nevertheless an example of the Subject Diagram:

  • Shapes of diagrams are defined properly in Section 2.3 of
    GBLS and in Section 4.1 of Category Theory for Computing Science.

The description of the Subject Diagram

Diagram SDD below shows the Subject Diagram as the limit of its description. The description is the black diagram.


Diagram SDD

Definition of $\mathsf{ar}_2$

The object $\mathsf{ar}_2$ of composable pairs of arrows is defined as a pullback:

In the usual categorical notation this would be shown as

This makes use of the fact that the unnamed blue arrow is induced by the other two projection arrows. In the rest of the post, projection arrows that are induced are normally omitted.

An enrichment of the description

Because $\mathsf{ar}_2$ is defined as a pullback, we can enrich the description of Diagram SDD by adjoining two pullbacks as shown below. This is Diagram 8.10 in GBLS. The enriched diagram has the same limit as the description of Diagram SDD.

Enriched Diagram SDD

Note that the projections from the limit to the two occurrences of $\mathsf{ar}_2$ induce all the other projections. This follows by diagram chasing; remember that the description must be a commutative diagram.

Make the triangles commute

To make the triangles commute, we add two comp arrows to the enriched diagram as shown below. These two arrows are not induced by the description; they are therefore additions to the description — they describe a more restrictive (green) diagram with commutative triangles and so are shown in black.

Diagram TC: The triangles commute

The left comp makes $xf=h$ and the right comp makes $kx=g$.

The outside square commutes

Now we enrich Diagram TC with four objects, <comp,id>, <id,comp> and three comp arrows as shown in bolder black. These objects and arrows already exist in $\mathbf{ThCat}$ and therefore do not change the limit, which must be the same as the limit of Diagram TC.

The outside square commutes

The diagram in bold black is exactly the commutative diagram that requires associativity for these particular objects and arrows, which immediately implies that $gf=kh$, as the Theorem requires.

By the definitions of $\mathsf{ar_2}$ and $\mathsf{ar_3}$, the part of the description in bold black induces the rest of the diagram. Omitting the rest of the diagram would make $\mathsf{ar_2}$ and $\mathsf{ar_3}$ modules in the sense of GBLS, Chapter 7.4. Modules would be vital to deal with proofs more complicated than the one given here.

References

Creative Commons License

This work is licensed under a Creative Commons Attribution-ShareAlike 2.5 License.

Send to Kindle
category theory, math, understanding math

Just-in-time foundations

1 Comment

Introduction

In MathOverflow, statements similar to the following two occurred in comments:

  1. Sets and functions do not form a category
  2. Categories and functors do not form a category.

I cannot find either one of them now, but I want to talk about them anyway.

If you look at the definition of categories in various works (for example references [1] through [3] below) you find that the objects and arrows of a category must each form a “collection” or “class” together with certain operations.   The authors all describe the connection with Grothendieck’s concept of “universe” and define “large categories” and “small categories” in the usual way.  So Statement 1 above is simply wrong.

Statement 2 is more problematic.  The trouble is that if the word “categories” includes large categories then the objects do not form a set even in the second universe.  You have to go to the third universe.

Now there is a way to define categories where this issue does not come up.  It allows us to think about categories without having a particular system such as ZF and universes in mind.

A syntactic definition of category

A category consists of objects and arrows, together with four methods of construction M1 – M4 satisfying laws L1 -L7.  I treat “object” and “arrow” as predicates:  object[f] means f is an object and arrow[a] means a is an arrow.  “=” means equals in the mathematical sense.

M1 Source If arrow[f], object[f.source].
M2 Target If arrow [f], object[f.target].
M3 Identity If object[a],  arrow[a.identity].
M4 Comp If arrow[g] and arrow[f] and  f.target = g.source, then arrow[(g,f).comp].
L1. If object[a],  a.identity.source = a.
L2. If object[a], a.identity.target = a.
L3. If arrow[g] and arrow[f] and  f.target = g.source, then (g,f).comp.source = f.source.
L4. If arrow[g] and arrow[f] and  f.target = g.source, then (g,f).comp.target = g.target.
L5. If object[a] and arrow[f] and f.source = a, then (f, a.identity) = f.
L6.  If object[a] and arrow[g] and g.target = a, then (a.identity, g) = g.
L7.  If arrow[h] and arrow[g] and arrow[f] and h.source= g.target and g.source = f.target, then (h,(g,f).comp = ((h,g).comp, f.comp).
Remarks on this definition
1. I have deliberately made this definition look like a specification in an object oriented program (see [6]), although the syntax is not the same as any particular oo language.  It is as rigorous a mathematical definition as you could want, and it could presumably be compiled in some oo language, except that I don’t know if oo languages allow the conditional definition of a method as given in M4.
2.  I could have given the definition in mathematical English, for example “If f is an arrow then the source of f is an object”.  My point in providing the impenetrable definition above is to make a connection (admittedly incompletely established) with a part of math (the theory of oo languages) that is definitely rigorous but is not logic.  An informal definition in math English of course could also be transformed rigorously into first order logic.
3.  This definition is exactly equivalent to the FL sketch for categories given in my post [5].  That sketch has models in many categories, not just Set, as well as its generic model living in the corresponding FL-cattheory (or in the classifying topos it generates).
4.  Saunders Mac Lane defined metacategory in precisely this way in [1].  That was of course before anyone every heard of oo languages.  I think he should have made that the definition of category.

Just-in-time foundations

Mathematicians work inside the categories Set (sets and functions) and Cat (categories and functors) all the time, including functors to or from Cat or Set. When they consider a category, the use theorems that follow from the definition above.  They do not have to have foundations in mind.

Once in awhile, they are frustrated because they cannot talk about the set of objects of some category.  For example, Freyd’s solution set condition is required to prove the existence of a left adjoint because of that problem.  The ss condition is a work-around for a familiar obstruction to an easy way to prove something.  I can imagine coming up with such a work-around without ever giving a passing thought to foundations, in particular without thinking of universes.

When you work with a mathematical object, the syntax of the definitions and theorems give you all you need to justify the claim that something is a theorem.  You absolutely need models of the theory to think up and understand proofs, but the models could be sets or classes with structure, or functors (as in sketch theory), or you may work with generic models which may require you to use intuitionistic reasoning.  You don’t have to have any particular kind of model in mind when you work in Set or Cat.

When you do run into something like the impossibility of forming the set of objects of some category (which happens in any model theory environment that uses classical rather than intuitionistic reasonins) then you may want to consider an approach through some theory of foundations.  That is what most mathematicians do: they use just-in-time foundations. For example, in a particular application you may be happy to work in a topos with a set-of-all-objects, particularly if you are a certain type of computer scientists who lives in Pittsburgh.  You may be happy to explicitly consider universes, although I am not aware of any category-theoretical results that do explicitly mention universes.

But my point is that most mathematicians think about foundations only when they need to, and most mathematicians never need to think about foundations in their work. Moral: Don’t think in terms of foundations unless you have to.

This point of view is related to the recent discussions of pragmatic foundations [7] [8].

Side remark

The situation that you can’t always construct a set of somethings is analogous to the problem that you have in working with real numbers:  You can’t name most real numbers. This may get in the way of some analyst wanting to do something, I don’t know.  But in any branch of math, there are obstructions to things you want to do that really do get in your way.  For example, in beginning linear algebra, it may have occurred to you, to your annoyance, that if you have the basis of a subspace you can extend it to the basis for the whole space, but if you have a basis of the whole space, and a subspace, the basis may not contain a basis of the subspace.

References and links

  1. Saunders Mac Lane, Categories for the working mathematician. Springer-Verlag, 1971.
  2. Wikipedia article on category theory
  3. Michael Barr and Charles Wells, Category Theory for Computing Science, Third Edition (1999). Les Publications CRM, Montreal (publication PM023).
  4. Discussion of functions in abstractmath.org.
  5. Definitions into Mathematical Objects 7.
  6. Object oriented programming in Wikipedia.
  7. M. Gelfand, We Do Not Choose Mathematics as Our Profession, It Chooses Us: Interview with Yuri Manin.
  8. Discussion in n-category cafe.
Send to Kindle