Downcasing Categories

• 1. DNC for Categories
• 2. Downcasing categorical diagrams (in general)
• 3. Why we want to allow pseudopoints
• 4. Quantifiers, categorically

1. DNC for Categories
=====================

2. Downcasing categorical diagrams (in general)
===============================================
One day I realized that the same notation that I was using for sets
did also work - with no changes in the syntax, only in the semantics -
for categories.

Here's a comparison; in the second situation, at the right, \catC is
an arbitrary category.

A is a set     	       	  |  A is an object of \catC, A∈|\catC|
B is a set		  |  B is an object of \catC, B∈|\catC|
			  |
A ---> B   (a function)	  |  A ---> B (a morphism)
a |--> b   (a function)	  |  a |--> b (a morphism)
			  |
A is the space of `a's	  |  Now:
B is the space of `b's	  |  ``an `a''' is an abuse of language
A = E[a]		  |  ``a  `b''' is an abuse of language
B = E[b]		  |  `a|->b' has semantics - it's a morphism -
			  |  but `a' and `b' have no semantics
An `a' is a point of A,	  |
a `b' is a point of B,	  |  `a's and `b's are not points in this case,
a∈A, b∈B.		  |  just ``pseudopoints'', and pseudopoints
			  |  don't need to exist - they may be just
			  |  syntactical devices
			  |
			  |  To enforce the distinction we say
			  |  ``object of'' instead of ``space of''
			  |  and we write O[·] instead of E[·]
			  |
			  |  A is the objects of `a's
			  |  B is the objects of `b's
			  |  A = O[a]
			  |  B = O[b]

Note: it's almost impossible to understand this is the general case
without examples...

L

3. Why we want to allow pseudopoints
====================================
For example, for subobjects.
Implications can be seen as inclusions.

  ∀a∈A.P(a)⊃Q(a)
  {a∈A|P(a)} \subset {a∈A|Q(a)}

Categorically,

  {a|P(a)} ------> {a|Q(a)}     /{a|P(a)}\      /{a|Q(a)}\
     v                v         |   v    |      |   v    |
     |                |         |   |    | ---> |   |    |
     v                v         |   v    |      |   v    |
     A -------------> A         \   A    /      \   A    /

This is a morphism between two objects of Set^>->, where
Set^>-> is the category of monic arrows between objects of Set.
Set^>-> is also called Sub(Set) - the category of subojects of Set.

Notational trick:

                                 /{a|P(a)}\      /{a|Q(a)}\
				 |   v    |      |   v    |
  {a||P(a)} ---> {a||Q(a)}  :=	 |   |    | ---> |   |    |
				 |   v    |      |   v    |
				 \   A    /      \   A    /

The `|' in {a|P(a)} is called the ``such that'' bar;
we're doubling it to represent subobjects.
We downcase that into:

  a||P(a) |-> a||Q(a)

this morphism - in Set^>-> is not just a mapping of points...
in fact, it's two morphisms in Set - a|P(a) |-> a|Q(a) and a|->a -
plus the information that the square below commutes:

  a|P(a) |---> a|Q(a)
    /            /
    |            |
    v            v
    a |--------> a

More generally:

          b:=b(a)
  a|P(a) |-------> b|Q(b)
    /                /
    |                |
    v     b:=b(a)    v
    a |------------> b

a||P(a) |-> b||Q(b) means ∀a.P(a)⊃Q(b(a)).
Note the use of a bit of ``physicist's notation'' here -
in the presence of a function f = a|->b the value of b can
be seen as a function of a, and a physicist would write
b=f(a) or b=b(a)... we will prefer b=b(a) to avoid using
new letters, and the dictionary will translate such
expressions (atrocities!) into something mathematically
sound.

4. Quantifiers, categorically
=============================
In Set^>-> the functors that quantify over a variable
are adjoints to ``weakening functors'' that add a dummy
variable to the domain:

  {a,b||P(a,b)} |---> {a||∃b.P(a,b)}      P(a,b) ===> ∃b.P(a,b)
       |                    |                - 	         -
       |         <->        |		     |	  <->	 |
       v                    v		     v	      	 v
   {a,b||Q(a)} <------| {a||Q(a)}          Q(a) <====== Q(a)
       |                    |		     -	      	 -
       |         <->        |		     |	  <->	 |
       v                    v		     v	         v
  {a,b||R(a,b)} |---> {a||∀b.R(a,b)}      R(a,b) ===> ∀b.R(a,b)

      A×B ----------------> A  	       	    a,b	|------> a

These functors do not operate on the whole of Set^>-> -
they go from one ``fiber'' of Set^>-> to another.

The best way to formalize this is via /fibrations/;
Set^>-> is a fibration over Set.

A fibration is composed of:
an ``entire category''               Set^>->
a ``base category''                  Set
a ``projection functor''             Cod: Set^>-> -> Set
and enough ``cartesian liftings''.   (?!?!?! - next slide)

In our diagrams we will not usually draw the projection functors.
Instead we will just draw the objects of the entire category
over their projections - and we will often omit the part
of their names that can be recovered from the projections.
In the diagram above we wrote just `Q(a)', not `a||Q(a)'.