Quick
index
main
eev
eepitch
maths
angg
blogme
dednat6
littlelangs
PURO
(C2,C3,C4,
 λ,ES,
 GA,MD,
 Caepro,
 textos,
 Chapa 1)

emacs
lua
(la)tex
maxima
git
lean4
agda
forth
squeak
icon
tcl
tikz
fvwm
debian
irc
contact

Downcasing Categories

Quick index:
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)'.