Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: equality of morphisms

David Egolf (Dec 11 2021 at 00:23):

Assume we are working in a category with morphisms $a$ and $b$ with domain $X$ and codomain $Y$. Assume we also have a morphism $c$ with domain $Y$ and codomain $Z$.

Let us assume that $a=b$. I want to show that we must have $ca = cb$. I think this is related to showing that $=$ is a "congruence relationship" with respect to composition.

I don't immediately see how to prove this from the definition of a category I see in "Category Theory in Context" by Riehl. That definition mentions equality between morphisms, telling us that:

• $1_Y f = f$ and $f 1_X = f$ for any $f: X \to Y$
• For any composable triple of morphisms $f$, $g$ $h$, we have $(fg)h = f(gh)$

It feels like we need to say a little bit more about $=$ to prove the statement I want.
Maybe it is standard to require "$=$ is an equivalence relationship". So, $=$ is reflexive, symmetric and transitive.

However, $a=b$ doesn't always imply $c * a=c * b$ for some notion of composition $*$ even if $=$ is an equivalence relationship.
For example, say we are working in the integers, and we say $a=b$ exactly when the ratio $a/b$ is of the form $2^k$ for some integer $k$. Then, we generally don't have $a+1 = b+1$ even though $a=b$ and $1=1$ under this equivalence relationship.

Do we need to additionally require the property that if $a,b,c,d$ are morphisms with $a = b$ and $c = d$, and we can compose $a$ after $c$, then we have $ac = bd$? (At least, it seems to me that we would want this to be true, but I don't see how it follows from the definition of a category given in "Category Theory in Context").

Reid Barton (Dec 11 2021 at 00:33):

$=$ is the ordinary equality of elements of a set, which everything respects. You don't get to "say" what $=$ is.

Reid Barton (Dec 11 2021 at 00:38):

So
David Egolf said:

Let us assume that $a=b$. I want to show that we must have $ca = cb$.

is just the ordinary fact that you can substitute equals for equals.

Reid Barton (Dec 11 2021 at 00:40):

But it's true that if you want to define a category by constructing its hom-sets as quotients by equivalence relations, then you had better check that the composition operation respects those equivalence relations.

David Egolf (Dec 11 2021 at 00:42):

Reid Barton said:

$=$ is the ordinary equality of elements of a set, which everything respects. You don't get to "say" what $=$ is.

That makes sense. Maybe the right way to think about this is that there are restrictions placed on the composition operator, so that certain statements hold. In particular, I am then wondering if it is an additional constraint we are placing on the composition operator to make it so $a=b \implies ca=cb$.

David Egolf (Dec 11 2021 at 00:49):

After some more thought, I think I get it.
If $a=b$ as sets (and not in some fancier equivalence relationship) then $ca$ is the same thing as a set as $cb$.

David Egolf (Dec 11 2021 at 00:49):

This is just because if you put the same things into the composition operator, you must get the same things out.

David Egolf (Dec 11 2021 at 00:51):

(Thanks, Reid Barton!)

Mike Shulman (Dec 11 2021 at 01:01):

I don't know if this is helpful or more confusing, but in constructive mathematics and type theory there is also a thing called an "E-category", where the homs are not sets but [[setoids]]. In that case you do need to assume explicitly that the specified "equality" relation is reflexive, symmetric, and transitive, and that it is respected by composition.

Mike Shulman (Dec 11 2021 at 01:02):

But as Reid says, in the ordinary definition of category, the homs are just sets, and $=$ is just equality, which is respected by everything automatically. Just like for elements $g,h,k\in G$ of a group, if $g=h$ then automatically $gk=hk$.

David Egolf (Dec 11 2021 at 01:12):

That is helpful, @Mike Shulman . Super cool!

John Baez (Dec 11 2021 at 17:37):

David Egolf said:

Let us assume that $a=b$. I want to show that we must have $ca = cb$. I think this is related to showing that $=$ is a "congruence relationship" with respect to composition.

People have already answer this perfectly well, but I will too:

In a sense you're right - but in the ordinary rules of logic, called "first-order logic with equality", equality is a congruence relation with respect to everything, so there's no work to be done here! Check out this:

• Wikipedia, First-order logic: equality and its axioms.

When most mathematicians talk about stuff, they implicitly use these rules, which they typically absorb unconsciously as an undergrads. So when you question these rules as you've just done, they will typically either say "come on, that's obvious", or refer you to material on logic like I just did, or start talking about rarely-used alternative approaches where one might take a new look at these rules.

David Egolf (Dec 11 2021 at 17:50):

Thanks! It's great to see those axioms listed explicitly at the link you provided.
If we define the function $\mu$ ("left composition by $c$") by $\mu(x) = cx$, then I think the "substitution for functions" axiom tells us that:
$a=b \implies \mu(a) = \mu(b)$
And so indeed $ca=cb$.

John Baez (Dec 11 2021 at 17:56):

Right! For most purposes, the rules in that Wikipedia article on first-order logic are among the basic "rules of the road" in math. That is, you're supposed to use them almost unconsciously - or in the case of mathematicians who have never formally studied logic, actually unconsciously.

John Baez (Dec 11 2021 at 17:58):

We tell students stuff like "4+1 = 5 so (4+1)/2 = 5/2", and we usually don't say why; we expect them to just pick it up.

John Baez (Dec 11 2021 at 18:00):

But it's good to know what's really going on here.

David Egolf (Dec 11 2021 at 18:20):

John Baez said:

We tell students stuff like "4+1 = 5 so (4+1)/2 = 5/2", and we usually don't say why; we expect them to just pick it up.

Yes, I've used statements like that so much so that I unconsciously "know" that I can do this in a number of specific settings.
I think what got me to sit up and pay to attention was the idea that this works in any category, including those I've never worked with.

Mike Shulman (Dec 11 2021 at 18:47):

Perhaps also interesting is that in other foundations for mathematics, like type theory, all those axioms of equality can be proven from a more basic "induction principle".

Guillaume Boisseau (Dec 12 2021 at 08:14):

Yet another way to answer your question is to say that the axioms of a category include that composition is a function. That means that it takes equal things to equal things

Guillaume Boisseau (Dec 12 2021 at 08:15):

I remember being annoyed at the lack of precision surrounding equality too. If that also bothers you, you might find HoTT delightful

John Baez (Dec 12 2021 at 15:14):

Anyone annoyed about lack of precision concerning equality in traditional mathematics (e.g. category theory) should study first-order logic with equality, since this is the theory that underlies all traditional mathematics - and it's completely taken for granted in most math courses.

It's also great to study newer approaches like HoTT, but I don't think you can fully appreciate these if you don't know the nitty-gritty details of the traditional approach.

Mike Shulman (Dec 12 2021 at 15:30):

I'm not going to disagree that people should study first-order logic with equality, but I think the claim that it "is" what underlies traditional mathematics, given that most mathemaicians haven't studied it, is a bit tendentious. It's certainly true that traditional mathematics can be formalized into FOLwE, and that this formalization has been the one traditionally advocated by logicians; but traditional mathematics can also be formalized into other foundational systems, without making much difference at the informal level where most mathematicians work.

John Baez (Dec 12 2021 at 17:16):

I claim it's not tendentious in the following sense: if you take an ordinary graduate math course, you're expected to assent automatically to manipulations of equality permitted by first-order logic with equality, and not to those that don't follow from this and the various theories stacked on top of this. For example a good traditional math grad student should raise their hand if the teacher says the fundamental group of the circle "equals" $\mathbb{Z}$, at least until this has been discussed. Then the teacher will traditionally say they're really just isomorphic, with a specific isomorphism given when you pick a generator for the fundamental group, but that we "use this isomorphism to identify them", and hereby just say they're equal.

John Baez (Dec 12 2021 at 17:19):

Of course traditional mathematics can be formalized in a host of other systems, some of which are better at dealing with some issues. But that's not what I was talking about.

David Egolf (Dec 12 2021 at 17:41):

I've been learning about opposite categories, and ran into a related question on the equality of morphisms - in the context of the source and target functions:

Say we are working in the category of sets and functions between them.
Let $f:\{1\} \to \{2,3\}$ and $g:\{1\} \to \{2\}$ be functions.
Set $f(1) = 2$ and $g(1) = 2$.
Viewing each function as a collection of ordered pairs, we have: $f = \{(1,2)\}$ and $g = \{(1,2)\}$.
So, $f$ and $g$ are equal (as sets), as they have the same elements.

Now, we want to consider the target of $f$ and $g$.
The target of a morphism $f$ is given by evaluating the target function $t$ on $f$, and is given by $t(f)$.
Based on the discussion above, if $f = g$, we must have $t(f) = t(g)$.
However, I intended $t(f) = \{2,3\}$ and $t(f) = \{2\}$, and these are not equal.
Something appears to have gone wrong!

To fix this, I think can one require a "function" to actually be a triple, with the first element being the usual ordered-pair information, the second element being its source, and the last element being its target.
However, it seems like this makes working with opposite categories a bit more annoying. For example, in this case I believe we no longer have this equality of hom-sets: $C(a,b) = C^{op}(b,a)$ for a category $C$ and objects $a$ and $b$. That is because each function now carries information about its source and target, and so the opposite of a morphism is not equal to itself anymore.
I notice that "Category Theory in Context" and the "opposite category" page on nLab don't seem to do this, so I suspect I am missing a better way to resolve this.

Nathanael Arkor (Dec 12 2021 at 17:47):

The usual solution, as you suggest, is for the data of a function to include its codomain. This doesn't cause any problems with the opposite category: the function is not encoding its codomain in the category, but rather its codomain as a function. So we really have two codomains: the function codomain and the morphism codomain. These match in Set, but are flipped in Set° (because a morphism from A to B in Set° will be a function with codomain A).

David Egolf (Dec 12 2021 at 17:50):

Oh, I see! That is a bit confusing to think about, but it does appear to solve all these problems!

Jean-Baptiste Vienney (Dec 12 2021 at 17:57):

To my knowledge, in category theory, when you consider a category where the morphisms are functions, the target of a morphism is always the codomain of the function. Here, you are confusing the target of your function with the image of the function. Your $t(f)$ is the image of $f$ and so it is $\{2\}$, but previously you have written that the codomain of $f$ is $\{2,3\}$ which is perfectly fine because the target of a function is always included in the codomain but they are not necessarily equal. If you want these to be equal, you can take the category of sets and functions where the codomain of a function is defined as its image. Or you can take the category of sets and surjective functions. I hope I don't say foolery, I haven't read all the discussion.

Patrick Nicodemus (Dec 12 2021 at 18:05):

I agree with Nathanael's answer. In set theory a function isn't often taken to include its codomain as part of the data, but category theory draws heavily from topology and in topology it's common to talk about maps from one space into another. For example, a closed loop in a space $X$ can be identified with a continuous map from the circle $S^1$ to $X$.

Jules Hedges (Dec 12 2021 at 18:07):

There are 2 different equivalent definitions of a category: (1) a class of objects, and for every pair of objects a hom-set between them; and (2) a class of objects, a class of morphism, and a pair of functions mapping every morphism to its source and target object (plus stuff for identities that isn't important here). Both these definitions are important because (1) generalises to enriched categories and (2) generalises to internal categories

Translating from (1) to (2) involves taking a big disjoint union: the class of all morphisms in a category is $\sum_{x, y \in \mathbf{Ob}} \hom (x, y) = \{ (x, y, f) \mid x, y \in \mathbf{Ob}, f \in \hom (x, y) \}$

So for definition (1) a morphism in $\mathbf{Set}$ is a function, and for definition (2) a morphism in $\mathbf{Set}$ is a triple consisting of a pair of sets and a function between them

David Egolf (Dec 12 2021 at 18:07):

Hi @Jean-Baptiste Vienney !
I am not worried about differences between the codomain (the set of possible outputs of a function) and the image (the actual outputs of a function) here. Instead, I was noticing that there can be two functions with different codomains that have the same input-output ordered pairs, and was wondering how to handle this in the context of assigning the categorical source and target of functions.
I hope I understood your comment properly!

David Egolf (Dec 12 2021 at 18:11):

Jules Hedges said:

So for definition (1) a morphism in $\mathbf{Set}$ is a function, and for definition (2) a morphism in $\mathbf{Set}$ is a triple consisting of a pair of sets and a function between them

Interesting! Would my $f$ and $g$ described above be equal, then, under definition (1)? If they would be, then I would be concerned that they would be required to have the same target, too.

Jean-Baptiste Vienney (Dec 12 2021 at 18:12):

Ok, sorry, I didn't understood well what you want to do :grinning_face_with_smiling_eyes: . Well, ok I don't see any other solution that putting the codomain in a triple.

Jules Hedges (Dec 12 2021 at 18:16):

David Egolf said:

Jules Hedges said:

So for definition (1) a morphism in $\mathbf{Set}$ is a function, and for definition (2) a morphism in $\mathbf{Set}$ is a triple consisting of a pair of sets and a function between them

Interesting! Would my $f$ and $g$ described above be equal, then, under definition (1)? If they would be, then I would be concerned that they would be required to have the same target, too.

This is where things get a bit tricky. Under the One True Official Standard definitions of set theory, $f = g$ as functions, as you say. But in category theory we would consider it meaningless to even ask whether elements of 2 different homsets are equal or not. You can formalise that with a type theoretic foundation, but most people don't bother with foundations and just do this with common sense

Nathanael Arkor (Dec 12 2021 at 18:17):

There aren't any set-theoretic issues even with this approach. But you no longer associate the codomain to each individual function: the codomain is given by the hom-set you are considering. So $f$ may be elements of multiple hom-sets, but it's never ambiguous as to what the target is.

Nathanael Arkor (Dec 12 2021 at 18:18):

But as Jules says, it's simpler to pretend the hom-sets are all distinct, because it doesn't make a difference in practice, and there is less chance for confusion.

David Egolf (Dec 12 2021 at 18:26):

Nathanael Arkor said:

There aren't any set-theoretic issues even with this approach. But you no longer associate the codomain to each individual function: the codomain is given by the hom-set you are considering. So $f$ may be elements of multiple hom-sets, but it's never ambiguous as to what the target is.

I see. If I understand, in this approach, if I want to know if I can compose $m$ after $n$, then I would need to consider if there exists any hom-sets $H_m$ and $H_n$ so that $H_m$ contains $m$, $H_n$ contains $n$ and the target of $H_n$ is the source of $H_m$.
I would also be curious how this works with functors, which are required to respect sources and targets.

Nathanael Arkor (Dec 12 2021 at 18:29):

Rather, you have hom-sets $C(x, y)$ and $C(y, z)$, and you have a composition operator $C(x, y) \times C(y, z) \to C(x, z)$. So in your example, $f$ would be an element of $\mathbf{Set}(\{ 1 \}, \{ 2 \})$ and $\mathbf{Set}(\{ 1 \}, \{ 2, 3 \})$ (and others besides), but this doesn't actually cause any problems, because you never consider $f$ in isolation: only as an element of a specific hom-set, where the target is known.

David Egolf (Dec 12 2021 at 18:34):

Thanks, that clears things up!
Then there is no problem with functors either, because each "version" of $f$ has a clearly-defined unique source and target, based on which hom-set it is in.

Guillaume Boisseau (Dec 12 2021 at 20:05):

Which amounts to dealing with types instead of sets. Which is the cleaner way most of the time imo

Patrick Nicodemus (Dec 12 2021 at 20:28):

Great thread to make that point in, as equality in type theory is so clean and simple.

Jules Hedges (Dec 12 2021 at 20:31):

In a sense, the "meaningful" sentences of (1-)category theory are no more or less than "these 2 elements of the same hom-set are equal", which is exactly what we say when we say that a diagram commutes

Mike Shulman (Dec 12 2021 at 23:16):

John Baez said:

I claim it's not tendentious in the following sense: if you take an ordinary graduate math course, you're expected to assent automatically to manipulations of equality permitted by first-order logic with equality, and not to those that don't follow from this and the various theories stacked on top of this.

That's more or less true. But:

1. As the rest of this thread indicates, there are true statements about equality in (the representation of ZFC-style set theory in) first-order logic with equality that mathematicians are also expected to learn not to assent to, and
2. Your statement would be equally true with various other foundations replacing "first-order logic with equality". Not HoTT, of course, as you point out, but other kinds of type theory would certainly suffice.