[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