[INCLUDE TH/speedbar.blogme]
[SETFAVICON dednat4/dednat4-icon.png]
[lua: LR = R ]
[# 
(defun c () (interactive) (find-blogme3-sh0-if "2007dnc-cats"))
;;    http://angg.twu.net/2007dnc-cats.html
;; file:///home/edrx/TH/L/2007dnc-cats.html
#]
[lua:
  -- (eev-math-glyphs-edrx)
  eev_math_glyphs_edrx()
]

[htmlize [J Downcasing Categories]

[WITHINDEX
[#
 # «.dnc-for-cats»		(to "dnc-for-cats")
 # «.downcasing-cat-diagrams»	(to "downcasing-cat-diagrams")
 # «.why-pseudopoints»		(to "why-pseudopoints")
 # «.quantifiers-categorically»	(to "quantifiers-categorically")
 #]

[RULE ----------------------------------------]

[tsec «dnc-for-cats»  (to ".dnc-for-cats")
[++N]. DNC for Categories
=========================
]

[tsec «downcasing-cat-diagrams»  (to ".downcasing-cat-diagrams")
[++N]. 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...


]
[tsec «why-pseudopoints»  (to ".why-pseudopoints")
[++N]. 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.

]

[#  TODO: 
   add ( P ) as a notation for pseudopoints (like a,b||P)
       (a,b)
#]

[tsec «quantifiers-categorically»  (to ".quantifiers-categorically")
[++N]. 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)'.

]

[#  TODO: 
   add equality.
#]



]

]
[#
 # Local Variables:
 # coding: raw-text-unix
 # modes: (fundamental-mode blogme-mode)
 # End:
#]