Categorical Problems.

[swestrup]

Okay, here's the current thing I'm trying to figure out in the definition of a category. The concept of 'commuting' seems to be undecidable in many cases. For example, lets assume I have a concrete category with three objects, which we'll decide are the integers 1, 2, and 3. Our arrows are functions and the identity function for each object is just f(x)=x. Now, let us assume that we have three particular functions for arrows in mind. f:1->2, g:2->3, and h:1->3.

I am told that the diagram of this category 'commutes' if gf=h. How am I supposed to know that? gf and h are both general functions and the question of whether two general functions are equal is undecidable. Despite this, I find many example given where the arrows are functions and they talk about commuting properties. What gives?

Comments

[sps.livejournal.com]

Sorry, why do you care if it's decidable? This is a mathematical system, not a computational one. If we required it to be computational, it couldn't give us results about computation.

It's just not a question one would normally ask, because we're trying to get a small theory of big objects, not the converse.

But then again, in this case, there's no possible issue. Since f, g and h are uniquely determined—none of those points has any internal structure—the diagram necessarily commutes. 'General function' or not, there is only one function from 1 to 2, and there is only one function from 2 to 3.

[hendrikboom.livejournal.com]

There's a type violation in your question.

If is a function, and f:1->1, what is x in f(x) = x? A member of 1?

For a function f:A->B, A and B are sets, and you can write f(x) when x is an element of A.

[hendrikboom.livejournal.com]

Now if you have some convention in mind in which the integers are encoded as sets in some way, perhaps this might work. But I don't think that's what you have in mind.

[sps.livejournal.com]

I (perhaps carelessly) interpreted him as meaning that the points were structureless, and he was writing -> because +> is ugly and he couldn't find ↦ on his keyboard!

[swestrup]

No, I used -> because that's the notation for a category arrow. When I wrote f: 1->2, I meant that all we know about the function is that it provides an arrow from object '1' to object '2'.

[sps.livejournal.com]

Maybe Hendrik confused me, too ;).