[formal-methods] The final element and points.
Jason Dusek
jason.dusek at gmail.com
Mon Jun 15 09:31:41 UTC 2009
Cale on #haskell has taught me everything I know.
--
Jason Dusek
[00:30] solidsnack
So is there a special reason that the points in the category
of sets all originate from the terminal object?
[00:31] Cale
Eh?
[00:31] Cale
solidsnack: You want to know why maps 1 -> A are the same as
elements of A?
[00:31] solidsnack
No.
[00:31] solidsnack
More like, how does this notion apply in other categories?
[00:32] Cale
Well, you can try to transfer it
[00:33] Cale
But the thing which is extra special about the category of
sets (and some other categories)
[00:33] solidsnack
So, one thing we know is that in all categories there is only
one "point" for 1 since we have only on arrow 1 -> 1
[00:33] Cale
is that maps f: A -> B are entirely determined by their
composites with points 1 -> A
[00:33] solidsnack
s/on arrow/one arrow/
[00:33] Cale
Yeah, that is true
[00:33] solidsnack
Interesting.
[00:34] Cale
In, say, the category of groups or vector spaces, the maps
1 -> A are boring
[00:34] Cale
(there's only one)
[00:35] Cale
So, for instance, linear maps A -> B are *not* characterised
by how maps 1 -> A compose with them to give maps 1 -> B
[00:35] Cale
However, it's possible to define the notion of a "generalised element"
[00:35] Cale
A generalised element of A is simply any map whose codomain is A
[00:36] Cale
That is, a map T -> A for some T
[00:36] Cale
This might seem like a silly idea, but it often helps in
trying to decide how ideas from the category of sets should
generalise to other categories
[00:39] Cale
For example, in the category of sets, the Cartesian product of
a pair of sets A and B is a set such that each element of A x
B consists of an element of A and an element of B.
[00:40] Cale
That is, there is a unique element of A x B for each pair of
elements, one from A and one from B
[00:41] Cale
In a general category, we have that for each pair of
generalised elements T -> A and T -> B, there is a unique
generalised element T -> A x B for the categorical product
[00:42] Cale
and the important thing in the category of sets is that we
could recover the components of the pair from the element of
the Cartesian product
[00:43] Cale
So there were projections pi_A: A x B -> A, pi_A (a,b) = a and
pi_B: A x B -> B, pi_B (a,b) = b
[00:44] Cale
and of course, in the categorical case, we keep the idea of
pi_A and pi_B, and function application in those definitions
becomes composition.
[00:45] Cale
Does that make sense?
[00:46] Cale
we have a: T -> A and b: T -> B, giving a unique
(a,b): T -> A x B, such that pi_A . (a,b) = a and
pi_B . (a,b) = b
[00:46] • Cale wonders if solidsnack is still listening :)
[00:47] solidsnack
I am moving back and forth.
[00:47] solidsnack
There is a time for listening, after all :)
More information about the formal-methods
mailing list