[formal-methods] Elements -- internal and external.

[Jason Dusek]

  The discussion we had on the channel was naturally more
  relevant the problem than is the paper :) Too bad it's
  unlogged.

--
Jason Dusek




[19:34] solidsnack
  Are the objects of a category in a set? If not, what are they in?
[19:35] solidsnack
  In other words, can we say "the set of objects in a category..." for all
  categories?
[19:37] solidsnack
  Hence we could also have the set of arrows from one category to another, &c.
[19:41] solidsnack
  Hmm, it seems that objects and morphisms are in classes in general.
[19:47] Cale
  solidsnack: There are too many in general.
[19:47] Cale
  For example, there is a category of all sets, but no set of all sets.
[19:49] FunctorSalad_
  it depends on your foundations
[19:51] solidsnack
  Heh.
[19:51] solidsnack
  I am trying to work the latter half of this problem from "Conceptual
  Mathematics": http://hpaste.org/fastcgi/hpaste.fcgi/view?id=6531#a6531
[19:52] solidsnack
  It is relatively straightforward to argue in terms of "internal diagrams"
  for sets; but I think this result should apply to all categories.
[19:52] solidsnack
  So I wonder if that is right and how I make that argument.
[19:54] Cale
  You can often generalise arguments about elements of sets by generalising
  elements of A to arbitrary maps T -> A
[19:55] Cale
  (where T is just some other object)
[19:56] Cale
  and then applying a function f: A -> B to an element x: T -> A is just
  composition.
[19:56] FunctorSalad_
  the converse isn't true for arbitrary cats
[19:56] Cale
  Well, s/function/arrow/ :)
[19:56] FunctorSalad_
  e.g. cat of groups has only trivial global elements
[19:56] FunctorSalad_
  (global elements of A = hom(1,A))
[19:57] Cale
  But try it with proper generalised elements :)
[19:57] Cale
  hmm :)
[19:58] solidsnack
  From where I am sitting, it seems like Cale is saying the generalization is
  viable and FunctorSalad_ is saying it's not.
[19:58] FunctorSalad_
  Cale: h = id, f mono?
[19:58] FunctorSalad_
  then it'd say any mono splits, which is false too
[19:59] solidsnack
  Cale: You are saying, I should start with sets and then argue about maps
  from `T -> A`? (They seem to be hinting at that by introducing maps
  `1 -> A`)
[20:00] FunctorSalad_
  ok, back with hands free ;) (no, not that)
[20:00] Cale
  solidsnack: Well, maps 1 -> A are directly in correspondence with elements
  of A in the category of sets, but in many categories, the maps 1 -> A are
  boring and don't tell you much
[20:02] Cale
  But yeah, in this case, there's not really any way to argue that such a g
  exists based on that, even with generalised elements.
[20:08] solidsnack
  Oh?
[20:09] FunctorSalad_
  btw I need a good intuition for monos that don't split too :(
[20:09] FunctorSalad_
  I know examples, but I can't put my finger on the general idea
[20:09] solidsnack
  So I should argue in the category set and just stick with that?
[20:09] Cale
  yeah, but have a look at http://www.maths.gla.ac.uk/~tl/elements.pdf
[20:09] FunctorSalad_
  solidsnack: the proposition is false in general cats, yes
[20:11] FunctorSalad_
  in groups the split monos are semidirect products, but these are weird too ;)
[20:11] FunctorSalad_
  in TOP they are inclusion of subspaces that have a retract
[20:14] FunctorSalad_
  solidsnack: as an example where it fails even for general elements, take the
  category of groups, f :: (Z,+) -> (Z,+); f = (*2), h = identity on (Z,+)
[20:14] FunctorSalad_
  there's no group homomorphism g with f.g = id
[20:16] FunctorSalad_
  correction: g.f = id
[20:16] FunctorSalad_
  (the other neither, but that wasn't the issue :))
[20:18] Cale
  and since f has no kernel, if f . a1 = f . a2 for some morphisms
  a1,a2: G -> Z, then indeed, a1 = a2
[20:46] solidsnack
  Yeah, I see how that works for the example you give.