Understanding Arrows and Sets in Category Theory | Exploring Foundations of Math

[phoenixthoth]

I was wondering how set theory could be categorized. I've heard that category theory can serve as an alternate foundation for math. But a fundamental symbol in the language is ∈. How is this done with arrows?

I was trying to figure out how arrows might be elements of a set (that isn't not a set of arrows), trying to develop an intuition on this. Here's what I came up with. A sequence is kinda two things (it's really only the second, technically):
1. a list of ELEMENTS
2. an ARROW from N to a set

Hmm...

 

[matt grime]

Not sure whaty you're doing, but it's quite easy to have a category whose arrows are not a set. For instance if we take CAT the category of all categoreis whose morphisms are (EDIT) functors (EDIT), then it isn't s proper category.

There are othe examples, though I can think of no natural ones.

 

[Hurkyl]

A thing of type X is denoted by a morphism with codomain X.

Now, suppose x is of type X and f is of type Ω^X.

The intuition about Ω^X is that it is the power object of X... or better yet, it "contains" the characteristic functions of the subobjects of X.

So, "x in f" is simply evaluating f at x.

x in f := W --> X x Ω^X --> Ω

The latter arrow is the evaluation morphism. W is the "appropriate" thing -- it is the product of the domains of x and f... or sometimes a subobject of that.


So, the statement "π in R⁺" can be encoded as:

R is a categorical real number object (As opposed to being the constant symbol of the language)

π = 1 --> R
R⁺ = 1 --> Ω^R
π in R⁺ = 1 --> R x Ω^R --> Ω (= true)

Since π is a constant symbol of type R, and R⁺ is a constant term of type Ω^R.

(Incidentally, R is also a constant symbol of type Ω^R)

 

[Hurkyl]

Incidentally, this is the basic idea:

From any well-pointed topos with a natural numbers object, we can construct a model of RZC.

RZC is restricted Zermelo set theory + axiom of choice, or "bounded Zermelo". The restricted part means that all quantifiers are restricted. I.E. we can make statements like [itex]\forall x \in b: P(x)[/itex], but not [itex]\exists x: P(x)[/itex].


A topos is well-pointed if, given f, g: A --> B, we have:
(f = g) if and only if xf = xg for any global element x = 1 --> A.

A natural numbers object is an N with arrows:

1 --> N --> N
(first arrow is 0, second arrow is s)

such that for any 1 --> X --> X, there is a unique h:N-->X such that:

1 --> N --> N
|     |     |
V     V     V
1 --> X --> X

Where the vertical arrows are identity, h, and h.

The natural numbers object is necessary to satisfy the axiom of infinity -- I believe that you simply need a well-pointed topos to get RZC - infinity.


Anyways, the basic idea of the model is that sets are trees -- given a set S, S is the node, and all the elements of S are its children, and so on.

A tree is specified by an object T and a binary relation on T that satisfies some axioms. (i.e. a subobject of TxT) The binary relation is read <=, and x <= y is supposed to mean "y descends from x". (i.e. there is some chain y in s1 in s2 in ... in x... the chain can be length 1, so x <= x)

The tree must satisfy some axioms to be considered a "set".


For example, what is the null set?

With the tree model, the null set is a tree consisting of a single node with no children. Categorically, we take 1 to be the object, and the identity on 1x1 to be the binary relation. (Every node descends from every node!)

So, I guess the right way to handle this is to take a given (T, R --> TxT) pair that denotes a tree, and model it as the global element:

1 --> Ω^T x (TxT)^R

Recall that the fact T is a subobject of T corresponds to a morphism 1 --> Ω^T, and R --> TxT corresponds to a morphism 1 --> (TxT)^R.


So, the null set would be given by a morphism:

1 --> Ω¹ x (1x1)^1x1

which (I believe) is isomorphic to the true (: 1 --> Ω).

Something about this is irritating me. (for example, I would really like the empty set to be the morphism 1 --> 1, but I think that's just a minor symptom) I'll get back to you when I figure out what it is.


PS: any idea how to write something like [itex]1 \rightarrow \Omega[/itex], but put some text over the &rarr;?

 

[mathwonk]

as a young student i enjoyed the book:
Abelian Categories - An Introduction to the Theory of Functors (Harper's Series in Moden Mathematics) by
Freyd, Peter

 

[matt grime]

There is a command in latex \stackrel{ X }{ Y } where X and Y are any two latex symbols. IT puts X over Y.

 

[Hurkyl]

[tex]1 \stackrel{true}{\rightarrow} \Omega[/tex]

Ok next question -- how do I get an arrow that will stretch as necessary?

 

[matt grime]

aah, that will depend on how good tha latex module is.

the short answer is use \longrightarrow, and hope it works

there is a stretch command though I can't remember it. Most typesetting of diagrams uses an external package such as xypic.

 

[Hurkyl]

[tex]1 \stackrel{true}{\longrightarrow} \Omega[/tex]

Bleh, looks like that's as long as it gets. Still, it's better than putting captions on my ASCII art!

 

[matt grime]

Here's a hack I thought of: make an arrow. Or, make a dash, with some command, and then insert negative spaces and then put an arrow.

[tex]--- \longrightarrow[/tex]


by inserting negative spaces becomes

[tex]-\!\!\!-\!\!\!-\!\!\! \longrightarrow[/tex]

 

[Hurkyl]

Ah, that's nifty!

 

[matt grime]

And useful. Once I needed the negation of the symbol for "is isomorphic to" so i had to make one by over writing two symbols cos I couldn't find it in any latex manual.

 

[robphy]

X \longrightarrow Y
[tex]X \longrightarrow Y[/tex]

X \overrightarrow{\qquad} Y:
[tex]X \overrightarrow{\qquad} Y [/tex]

X \overrightarrow{\qquad\qquad} Y:
[tex]X \overrightarrow{\qquad\qquad} Y [/tex]

X \overrightarrow{\qquad\qquad\qquad\qquad} Y
[tex]X \overrightarrow{\qquad\qquad\qquad\qquad} Y [/tex]

[tex]X \stackrel{f}{\overrightarrow{\qquad\qquad\qquad\qquad}} Y [/tex]

 

[matt grime]

That's a much better solution than my hack. But is there anyway to get xypic or even paul taylor's diagrams package included? these typeset commuting square objects, and allow for arbitrary starting and ending points, different kinds of arrows, bending arrows, and arrows going over and under.

 

[Hurkyl]

Well, I opened a thread in the feedback forum requesting it. Could you suggest which package would be best, and where chroot could get it?

 

[Hurkyl]

Anyways, an answer I probably should have given to phoenixthoth's original post is this:


The goal of using category theory as a foundation for mathematics is, as I understand it, not by using category theory to model set theory -- it's by using category theory as a substitute for set theory.

In most foundational things, sets are a convenience -- one doesn't need to talk about sets to define, say, a ring. Nor does one need sets to talk about ring homomorphisms, or even modules!

Sets are just conveniences; set theory provides a unified language for discussing mathematics, and a lot of routine things one might like to do, like develop a basic theory of functions, has already been done in set theory.

Well, the same is true of category theory. It also provides a language and basic constructions one would like to do stuff.