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: Basic question about the category of sets

Sándor Bartha (Jan 16 2025 at 10:32):

Definitions of the category SET usually state that the objects are sets and the morphisms are functions mapping one set to another. However, we cannot consider these functions as sets of pairs (as is customary in set theory) since, from this representation, we cannot recover the codomain. Therefore, would it be more precise, if we understood functions as functions of set theory, to say that the morphisms are function-codomain pairs? Is this question glossed over because it is completely uninteresting pedantry?

fosco (Jan 16 2025 at 11:00):

When one wants to be really pedantic, a morphism in the category of sets is defined as a triple $(A,B,f)$ where $A,B$ are sets, and $f\subseteq A\times B$ is a subset such that [...insert function conditions...]; so, the codomain of a function in this sense is always recoverable: it's the image under the second projection of the triple $(A,B,f)$.

fosco (Jan 16 2025 at 11:02):

Which is essentially to say: the morphism $\mathbb N \to\mathbb R$ sending $0,1,2,\dots$ (as naturals) to $0,1,2,\dots$ (as reals) and the morphism $\mathbb N \to\mathbb Z$ doing the exact same thing are, strictly speaking, different.

A statement that looks completely obvious today, but that took surprisingly long to become obvious.

Sándor Bartha (Jan 16 2025 at 11:28):

Thanks. I only mentioned pairs because the domain is determined by $f$ if it satisfies the function condition, so strictly speaking the domain is not necessary to include in order distinguish morphisms. But I guess triples are more convenient to work with.

Mike Shulman (Jan 16 2025 at 15:12):

This process has even been formalized using the notion of [[protocategory]].