I am learning category theory and couldn't find a full formal proof of the simplest example I could think of (that $\mathbf{Set}$ is a Category). What's seems the "hello world" of category theory? Anyway, so I am going to write down what I think is the correct proof and hope to discover if I actually understand at least the most basic concept in this subject.

So $\mathbf{Set}$ has the object class $Ob(\mathcal C) = $ "all valid sets by ZFC" and its morphisms/arrows (between any two objects $A,B \in Ob(\mathcal C)$), $C(A,B) = \{ f: A \to B \} $ = "set of all total functions between any two valid sets".

(To my understanding) To show its a Category we need to show:

  1. Morphisms are associative so $h \circ (g \circ f) = ( h \circ g) \circ f$
  2. That every object $A \in Ob(\mathcal C)$ has some identity morphism $\mathbb 1_A: A \to A$ (this is actually the step I am not sure how to show, but I will show my attempt).

I will do 1) first. To show $h \circ (g \circ f) = ( h \circ g) \circ f$ we need to show that for any object $A$ we have $\forall a \in A$:

$$h \circ (g \circ f)(a) = ( h \circ g) \circ f(a)$$

I will use the fact $(g \circ f)(a) = g(f(a))$ (this is one of the problematics steps in my proof because I assume it only works for sets and composition of functions of sets).

LHS: $h \circ (g \circ f)(a) = h ( g \circ f(a) ) = h(g(f(a)))$.

RHS: $( h \circ g) \circ f(a) = ( h \circ g) ( f(a) ) $ but $h \circ g(b) = h(g(b))$ so we have $( h \circ g) ( f(a) ) = h(g(f(a))$.


Before I continue I want to note that this seems where I feel sort of weird about my proof because it seems that the idea of category theory is to reason at the highest level of abstraction and worry not at all about details. Here I introduce two details (that I think are against the spirit of category theory):

  1. I opened the black box of an object $A$ to look at its elements and then use the actual elements of $A$ to proceed with my proof.
  2. I also opened the black box of the morphism $f$ to say exactly what it does in detail what it does to each element of the object $A$ (which in this case is a set).

This just feels wrong against the spirit of what category theory is supposed to be about. Perhaps I am having a hard time abandoning my old ways of thinking about mathematics since I'm so used to set theory. Or perhaps something that doesn't use careful set theory arguments just don't feel convincing. Either way, what would a real category theory proof of this fact look like? How do I know if I am using an argument more typical for category theory and convinced that its correct? Hopefully, a concrete example will help in learning this.

Now I need to show identity. My question is if to do this I need to:

  1. Show $\forall A \in Ob(\mathcal C), \exists \mathbb 1_{A} \in C(A,B)$, $\mathbb 1_A: A \to A$
  2. Show $\forall A,B \in Ob(\mathcal C), f \circ \mathbb 1_{A} = \mathbb 1_B \circ f$

My doubts is that I don't seem to be able to see how to show (1) in general without (2). It's not to hard to show in this specific example using the details of sets that $(1) \iff (2)$ but my suspicion is that (2) is the definition of (1) for general stuff if we are not allow to inspect the details. i.e. to show (1) we need to show that it behaves like the identity, which would to me mean that it doesn't affect other maps if you compose it at the end or before the map $f$ is applied. So basically, my quesiton is, am I trying to show (1) or (2)? Or in general just doing (2) is sufficient since (1) cannot be shown by itself as a stand alone? (note that for this specific example we can show (1) stand alone).

So I will show first how we can show (1) stand alone:

So we want to show some morphism $f \in C(A,A)$ acts as the identity for any $A$. In sets it means $f(a) = a$. Since $C(A,A)$ contains all the functions (and thus mappings) between $A$ and itself $A$, it must contain the map $f(a) = a$. Which completes the proof this $f$ is $\mathbb 1_A$.

Last I will show $(1) \iff (2)$ for this specific case.

Assume $\mathbb 1_A(a) = a$, $\mathbb 1_B(b) = b$. Then we want to show $f( \mathbb 1_A(a)) = \mathbb 1_B( f(a) ) $. Note $f( \mathbb 1_A(a)) = f(a)$. Note $\mathbb 1_B( f(a) ) = f(a)$. Thus, they are the same. So (1) implies (2). Now we want to show (2) implies (1). Asssume $f(\mathbb 1_A(a) ) = \mathbb 1_B ( f(a))$ and we want to show $\forall A \in Ob(\mathcal C)$, $\exists \mathbb 1_A $ s.t. $\mathbb 1_A (a) = a$. Assume by contradiction that (2) holds but (1) does not. So there exists an object $A$ s.t. $\mathbb 1_A (a) = a' \land ( a \not = a )$. So $f( \mathbb 1_A(a) ) = f(a') \not = \mathbb 1_B( f(a) ) = f(a)$, which is a contradiction because (2) holds i.e. $\forall A,B \in Ob(\mathcal C)$ we assumed $f(\mathbb 1_A(a) ) = \mathbb 1_B ( f(a))$. Which is a contradiction because we found some object that violates this. So (1) cannot be false if (2) is false.

Though, obviously, this last specific proof is only true for $\mathbf{Set}$. Which is not what I expect to happen in general because I obviously applead to the properties of sets and functions (and even went to what I think is the wrong way to think about this and reason over the details of how the mappings work exactly and what the elements of the object are in detail, which I assume is wrong, but I don't know any better or how a real category theory proof of this that is 100% formal would look like).

Does someone know how to transform my detailed proof to a true category theory proof which at the same time is 100% formal? (which 100% formal I am hoping means it would be easy to translate to a theorem prover like Coq, or I guess I am unsure how to define formal in this case of category theory, but I am 100% sure what it means in "traditional mathematics", which is why my proof looks the way it does). I guess I am asking, what is a "proof" in category theory (as opposed to standard set theory mathematics).

  • $\begingroup$ not sure why someone thinks its unclear what I'm asking. What is an example of a correct proof in Category Theory and what is the proof template for showing something is a Category. $\endgroup$ – Charlie Parker Nov 11 '18 at 19:27
  • $\begingroup$ My proof is just to show an example of what I personally consider a correct proof. Though, it might be wrong and if it can be pointed out why and how is the correct template to follow in category theory, that would be great. $\endgroup$ – Charlie Parker Nov 11 '18 at 19:28
  • $\begingroup$ useful: quora.com/… $\endgroup$ – Charlie Parker Nov 13 '18 at 1:52
  • $\begingroup$ Why do you think that a proof means something different in category theory? It is just mathematics! $\endgroup$ – TheGeekGreek Nov 13 '18 at 19:50
  • $\begingroup$ @TheGeekGreek its totally reasonable to assume this unless you don't think deeply about mathematics. Category theory doesn't have the standard foundations of set theory ZFC axioms that avoid Paradoxes. Things are abstract objects with arrows and usually doesn't inspect what the objects are so not even standard reasoning about sets seems common. Since classical FOL is developed assuming ZFC and meta-logic essentially mimic FOL as we prove FOL is "correct", then what logic do we even use to define category theory? $\endgroup$ – Charlie Parker Nov 15 '18 at 5:34

This just feels wrong against the spirit of what category theory is supposed to be about. Perhaps I am having a hard time abandoning my old ways of thinking about mathematics since I'm so used to set theory. Or perhaps something that doesn't use careful set theory arguments just don't feel convincing.

This is totally wrong. The proof you wrote is exactly the way the proof should be written. You are proving a statement about one particular category (namely, $\mathbf{Set}$), and so you will need to get your hands dirty and actually work with the objects and morphisms of that category concretely. Category theory doesn't make it so that you magically don't have to do any set theory/algebra/geometry or whatever. It's just a language for stating the results you find.

The only circumstance in which it would be reasonable to expect an argument that "stays within category theory" is if you are proving a statement that is true about all categories (or all categories satisfying certain special properties). In that case obviously you would work with an abstract category where you know nothing except the category axioms.

The moral here is that category theory isn't special, and neither are proofs in category theory. There is no difference between a "true category theory proof" and any other mathematical proof. Categories are just a type of abstract algebraic structure like any other, and you reason about them the same way you would any algebraic structure. If you had to prove that some structure was a group, what would you do? You would actually look at the elements and operation of the structure and check that they satisfy the group axioms.

Now I need to show identity. My question is if to do this I need to:

  1. Show $\forall A \in Ob(\mathcal C), \exists \mathbb 1_{A} \in C(A,B)$, $\mathbb 1_A: A \to A$
  2. Show $\forall A,B \in Ob(\mathcal C), f \circ \mathbb 1_{A} = \mathbb 1_B \circ f$

Here you are just getting totally confused. These aren't two separate statements. Indeed, as you've written it, the $\mathbb{1}_A$ in statement (1) and the $\mathbb{1}_A$ in statement (2) don't even have the same meaning, since in (1) it is bound by a quantifier while in (2) it is free (and so (2) is not even a statement that can be true or false).

Instead, they are two parts of a single statement, which would be correctly stated as:

For each $A\in Ob(\mathcal C)$ there exists $1_A\in C(A,A)$ such that:

  • for all $B\in Ob(\mathcal C)$ and $f\in C(B,A)$, $1_A\circ f=f$, and

  • for all $C\in Ob(\mathcal C)$ and $g\in C(A,C)$, $g\circ 1_A=g$.

Notice here that the verification of these properties of $1_A$ happens inside the existential quantifier binding $1_A$. So, to prove this statement for $\mathbf{Set}$, what do you do? You consider an arbitrary set $A$, define some particular function $1_A:A\to A$, and then verify that the function you defined satisfies the two bullet points above. This is very simple: just define $1_A:A\to A$ to be the function such that $1_A(a)=a$ for all $a\in A$. Then you can verify $1_A\circ f=f$ for any $f:B\to A$ and $g\circ 1_A=g$ for any $g:C\to A$ by evaluating each side an an arbitrary element of the domain and proving they are the same, just like you did to verify associativity.

(As an aside, all of this is assuming that your definition of a category is stated in a certain way, such that the identity maps are not part of the structure of a category but are instead just a property of that structure. It is actually probably better to define the identity maps to be part of the structure itself (though it doesn't really make a difference because the identity maps turn out to be uniquely determined, if they exist). In other words, to even say what your putative category is, you have to specify the morphism $1_A$ for each object $A$, just like you have to specify the collections of objects and morphisms and the composition operation. Then, you have to verify that this specified morphism satisfies the two bullet points above.)

| cite | improve this answer | |
  • $\begingroup$ Ok, good to know I still need to do the normal maths and I'm not crazy. My question I think is, I am not sure what exact template I need to follow to show something is a category. I think what confuses me is disentangling the definition of identity and composition. I assume we need to show composition respects the identity ($f \circ 1_A = 1_B \circ f $) and it's also associative. But that's not enough to show an identity exists for all objects $A \in Ob(C)$. Right? $\endgroup$ – Charlie Parker Nov 11 '18 at 19:20
  • $\begingroup$ So what I am trying to understand is how do I know when I've proved an identity exists, what property do I need to check? Is the property you boxed the property I need to check in the context of any arbitrary category? $\endgroup$ – Charlie Parker Nov 11 '18 at 19:20
  • $\begingroup$ Yes, the statement I boxed is the entirety of what you need to prove to verify the identity axiom for an arbitrary putative category $\mathcal{C}$. $\endgroup$ – Eric Wofsey Nov 11 '18 at 19:21
  • $\begingroup$ So just to be 100% sure and explicit. I need to show 3 things. The 1) identity property exists, 2) Composition respects identity and 3) Composition is associative and then I'm done (and in showing those things I might need to use any of the standard mathematics I am used to and love, of course, depending on what mathematical structures I claim are categories I might need one type of set theory or another or something else etc, right?). $\endgroup$ – Charlie Parker Nov 11 '18 at 19:23
  • $\begingroup$ Er, what do you mean by "composition respects identity"? There are only two things you need to check: (A) the identities axiom I boxed in the answer, and (B) composition is associative. $\endgroup$ – Eric Wofsey Nov 11 '18 at 19:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.