4

$\newcommand\bHom{\mathbf{Hom}}\newcommand\bOb{\mathbf{Ob}}\newcommand\bRel{\mathbf{Rel}}$This question is probably stupid and definitely bureaucratic, but

Is writing $f\circ g$ for the composition of morphisms in the ‘many hom-classes’ definition of a category unambiguous?

The ‘many hom-classes’ definition of a category (as given e.g. on the nlab) says that for each pair of arrows $(f,g)\in\bHom_\mathcal{C}(Y,Z)\times\bHom_\mathcal{C}(X,Y)$ we ‘have an arrow’ $f\circ g\in\bHom_\mathcal{C}(X,Z)$, but if the hom-classes may not be disjoint how do we know that the arrows we ‘have’ from identical composable arrow pairings in differing hom-class pairs match up?

Rephrased using the language of composition functions, the above definition is the same as a collection of functions $$\{\circ_{XYZ}:\bHom_\mathcal{C}(Y,Z)\times\bHom_\mathcal{C}(X,Y)\to\bHom_\mathcal{C}(X,Z)\}_{X,Y,Z\in\bOb_\mathcal{C}}.$$ The axioms then specify associativity and unitarity, but how do we know that we don't have objects $X,Y,Z,X',Y',Z'\in\bOb_\mathcal{C}$ and arrows $$f\in\bHom_\mathcal{C}(Y,Z)\cap\bHom_\mathcal{C}(Y',Z'), \\ g\in\bHom_\mathcal{C}(X,Y)\cap\bHom_\mathcal{C}(X',Y'),$$ so $$(f,g)\in\bigl(\bHom_\mathcal{C}(Y,Z)\times\bHom_\mathcal{C}(X,Y)\bigr)\cap\bigl(\bHom_\mathcal{C}(Y',Z')\times\bHom_\mathcal{C}(X',Y')\bigr),$$ such that $$\circ_{XYZ}(f,g)\neq\circ_{X'Y'Z'}(f,g)?$$ Note that these composites live in $\bHom_\mathcal{C}(X,Z)$ and $\bHom_\mathcal{C}(X',Z')$, respectively, and as David Roberts points out in the comments these classes can be disjoint even if the original hom-classes aren't.

If it is possible to have objects and arrows as above the notation $f\circ g$ is obviously ambiguous — also obvious is that we could fix this with an additional axiom (scheme?) if it were a problem.

Is this situation already precluded by the other axioms/data present in the many hom-classes definition of a category?

For an example where we have identical arrow pairings in differing hom-classes but composition still matches up, consider any two composable relations $R,S\in\bOb_{\bRel}$. By definition $R$ and $S$ are subsets of some Cartesian squares $Y\times Z$ and $X\times Y$ (respectively), but we can take $X'$, $Y'$, $Z'$ to be any strict superclasses of $X$, $Y$, $Z$ (respectively) and observe that $R$ and $S$ are also subsets of $Y'\times Z'$ and $X'\times Y'$ (respectively), so $$R\in\bHom_{\bRel}(Y,Z)\cap\bHom_{\bRel}(Y',Z'), \\ S\in\bHom_{\bRel}(X,Y)\cap\bHom_{\bRel}(X',Y').$$ Here we obviously still have that the composition functions coincide, but this is arguably due to the fact that $\bRel$ is most naturally presented as a one hom-class category. Again, I understand that this question is very pedantic at best — the patience involved in any clarification is greatly appreciated.

LSpice
  • 11,423
Alec Rhea
  • 9,009
  • 6
    I'm not sure this constitute an answer but the general practice is that composition is implicitely considered as a functions of f,g,X,Y and Z (or as a collections of function as you said). But people often considered that the Hom set are disjoints - so that X,Y,Z can be parsed from f and g and so don't need to be explicitly written out. The definition as written on the nLab is indeed technically incorrect, but it is a very common abuse of notations, which is almost mandatory to keep the notation readable. – Simon Henry May 07 '22 at 21:58
  • 4
    Suppose $K$ is a field and $V$ a vector space over $K$. I can add elements of a field and I can add elements of a vector space. Now if $a$ and $b$ happen to belong to $K \cap V$ then I can form the sum in $K$ or the sum in $V$. Is there an axiom saying they have to agree? I think most would agree the question is meaningless or unimportant. It is the same with the composition operations for different $X$, $Y$, $Z$ in a category. – Reid Barton May 07 '22 at 22:03
  • 1
    The two annotated composition operations have different codomains, which can be disjoint, even if the original hom-sets were not. In your inequality you should also include the information of where these composites are, like in the three previous displayed pieces of maths, and then it should help disentangle what is and isn't possible. – David Roberts May 07 '22 at 23:01
  • 1
    @SimonHenry If I understand your comment correctly, composition is generally viewed as a function of five variables equivalent to the family of functions I mentioned; in the one function definition, do we always have that $\circ(X,Y,Z,f,g)=\circ(X',Y',Z',f,g)$? If so, is this an axiom or a consequence of the other axioms already present? If not, how is this equivalent to the one hom-class definition that comes equipped with a composition function? Note that by 'one hom-class definition' I mean we take $dom$ and $cod$ to be entire relations, so we can still have overlapping hom-classes. – Alec Rhea May 08 '22 at 10:29
  • @ReidBarton I ran into this issue when trying to prove that the $2$-category of 'typed definition categories' is isomorphic to the $2$-category of 'one hom-class with domain and codomain entire relations' categories. Without this additional axiom, how do we even get an equivalence between the typed definition and the 'one hom-class with domain/codomain functions' definition of a category, where composition is a single function and thusly agrees on all hom-classes? In particular, how do we even construct the composition function for the one hom-class category corresponding to a typed category? – Alec Rhea May 08 '22 at 10:32
  • @DavidRoberts I will edit accordingly, thank you for the suggestion. – Alec Rhea May 08 '22 at 10:36
  • @SimonHenry (+1) Your description is all right, The definition as written on the nLab is "literally" incorrect, but everybody has in mind that the Hom-sets are disjoint. This is sometimes explicit as in ref [3] of my answer, sometimes mentioned in the remarks [2,4] and Serre's graphic metaphor [1] is perfect IMHO. – Duchamp Gérard H. E. May 08 '22 at 11:22
  • 2
    For what it's worth, I have had two long, long research projects (the most recent one took 5 years from conception to completion) that sprang from my naturally encountering—in the course of "real" questions—questions that, like the one you're asking, at first sight seem somewhere between meaningless and unnecessary. So just consider this a word of support for the often thankless task of trying to pursue these seeming "trivialities" to their conclusion. – LSpice May 08 '22 at 19:59
  • 3
    @AlecRhea : No there is no reason to expect thist to be true (and it is easy to make it false on purpose), and I've never seen anyone add this as an axiom explicitely. It's just that composition depends on X,Y,Z implicitely and we don't bother writing out explicitely. Also most category theorist tends to prefer "structural" set theoretic foundation (https://ncatlab.org/nlab/show/structural+set+theory), in which the question you are asking doesn't even make sense (in a structural set theory it doesn't make sense to ask whether two abstract sets intersect or not) – Simon Henry May 08 '22 at 21:18
  • 1
    May I say I appreciate you asking this question here. Concrete implementation issues like these can be no joke in practice on a computer, even if mathematically they are invisible and seem frivolous or pointless to some. – David Roberts May 18 '22 at 11:08

2 Answers2

19

There is no missing axiom. The notation is potentially ambiguous, but rarely (if ever) so in practice.

The situation is just the same as writing addition in arbitrary abelian groups as $x + y$. Formally, the operation “$+$” depends not just on $x,y$ but (before them) on a choice of group $G$ — explicitly, we could write it as $x +_G y$. And so the notation $x+y$ can potentially be ambiguous — $x$ and $y$ could belong to two different Abelian groups, whose addition operations disagree on $x+y$. But it would be nonsense to suggest that algebraists need to assume different groups considered must always be disjoint, or that their addition must always agree on intersections. We simply agree that the notation $x + y$ implicitly depends on the intended group, and make sure that this is always clear from context. And in the very rare situations where ambiguity would arise, we distinguish it explicitly by writing $+_G$ or some similar annotation. Similarly, composition $f \circ g$ is formally also dependent on the category and objects involved, $\mathrm{comp}(\mathcal{C},X,Y,Z,f,g)$ (so for a fixed category, it is a function of the objects and arrows) — but in the notation, we usually write just $f \circ g$, with the rest inferred from context.

This notational point is formally addressed in computer proof assistants, where functions have implicit arguments. This is essential for formalising many notations used in mathematical practice. In particular, the many-hom-sets definition of categories has been formalised by multiple authors many times (including myself), and shown equivalent to the class-of-arrows definition for instance here, in the TypeTheory Coq library over UniMath. So we can be very confident that there is no missing axiom.

(Counter to Duchamp Gérard’s answer, I do not think all (or even most) category theorists assume hom-sets are always disjoint. What I think all agree is that if we start from the many-hom-sets definition, then “the class of all arrows of $C$” must mean the disjoint union of the hom-sets, not the pure set-theoretic union. But when working with the many-hom-sets definition, the “class of all arrows” is not taken as primary — it is fairly rarely used, and when it’s used, there’s no problem with the original hom-sets being sub-objects of it rather than literal set-theoretic subsets.)

(Also, as Andreas Blass and Simon Henry note in comments, if we’re working in a type-theoretic or structural set-theoretic foundation, then asking if abstract sets are disjoint is not even well-defined. Intersection is defined between subsets of any given set/type; but in structural foundations, abstract sets not automatically subsets of an ambient universal class.)

Peter LeFanu Lumsdaine
  • 18,946
  • 1
    This is interesting to think about, thank you — if you could find one of those links/references it would be greatly appreciated. – Alec Rhea May 08 '22 at 19:47
  • 5
    In view of the word "typed" in the title, I'm inclined to say that, from a sufficiently type-theoretic point of view, it doesn't make sense to ask whether two different hom-sets (or hom-types) are disjoint, because it doesn't make sense to ask whether an element of one and an element of the other are equal. – Andreas Blass May 08 '22 at 20:03
  • 2
    @AndreasBlass: Absolutely — I’ve now added a remark mentioning that point. I originally omitted it as I try not to proselytise type theory uninvitedly — but as you point out, OP mentions “typed” already in the question, so… – Peter LeFanu Lumsdaine May 08 '22 at 21:13
  • 4
    The same remark can be made about any kind of structural set theory (not just type theory) - and I belive it is a relatively uncontroversial fact that a majority of category theorist prefer structural set theories over materials ones as foundation – Simon Henry May 08 '22 at 21:23
  • I think I might have just had a ‘click’ — are you basically saying that composition is an entire relation instead of a function (similar to dom and cod), but that we can use the trick that for any entire relation $R:X\to Y$ there is canonically a function $f_R:\coprod_{y\in Y} R^{-1}(y)\to Y$ (projection onto the index set) with $f_R\cong R$ in ${\bf Rel}/Y$ iff $R$ is functional, and this construction (or something equivalent) allows us to ‘parse up’ all the potentially multivalued data in the many hom-classes definition of a category into nice functions for the one hom-class definition? – Alec Rhea May 09 '22 at 01:57
  • 2
    @DuchampGérardH.E. It wasn’t me, and I appreciate the effort you’ve put in even if we ultimately disagree. +1 – Alec Rhea May 09 '22 at 07:34
  • 2
    @AlecRhea (+1) This is the true game. You're welcome. – Duchamp Gérard H. E. May 09 '22 at 08:11
  • 1
    @AlecRhea: That view may work, but I don’t think it’s what I had in mind — since you say “potentially multivalued”, you’re presumably considering the set-theoretic union $\bigcup_{X,Y} C(X,Y)$. I’m saying you should never take that union — and in a structural foundation, you can’t! To build a class-of-arrows category from a hom-sets category, take $C_1 := \coprod_{X,Y} C(X,Y) = {(X,Y,f)\ |\ X,Y \in C_0,\ f \in C(X,Y)}$. Then composition is defined on $C_1 \times_{C_0} C_1$ by $(X,Y,f) \circ (Y,Z,g) := f \circ_{X,Y,Z} g$. Everything is functional the whole way — nothing is ever multi-valued. – Peter LeFanu Lumsdaine May 09 '22 at 13:37
  • 1
    @PeterLeFanuLumsdaine This is, up to a permutation, exactly the repair proposed by Adámek, Herrlich, and Strecker (reference [4] made precise in the two last lines of my answer) and the spirit of David Roberts's subsequent comment. I am glad to see that, even if it was said that we disagreed philosophically, it seems that we eventually agree technically. – Duchamp Gérard H. E. May 09 '22 at 14:25
  • 2
    @DuchampGérardH.E.: Yes, and I appreciate your well-referenced answer! But I still don’t understand why you view it as a “repair” — to me it seems simply a comparison between two equivalent definitions, both perfectly adequate. I think what our answers really together show is that category theory is a big enough community to include sub-communities with very different outlooks. Just as you say that category theorists of your acquaintance assume disjoint hom-sets, I think that most I’ve heard discuss these issues prefer structural foundations, and consider the disjointness unnecessary. – Peter LeFanu Lumsdaine May 09 '22 at 16:09
  • 1
    @PeterLeFanuLumsdaine OK, I understand. The word "repair" was used a bit lightheartedly. To be faithful with what I have in mind I would have chosen "resolution". I like the idea of category theory as hosting a big multifaceted community. – Duchamp Gérard H. E. May 09 '22 at 17:59
  • @PeterLeFanuLumsdaine For your information, yesterday I returned to Mac Lane where the functions $dom,cod$ are explicitly built-in the axioms (see my late edit). – Duchamp Gérard H. E. May 18 '22 at 07:29
  • @DuchampGérardH.E.: Oh yes — I agree, most textbook definitions (certainly most older ones) use the dom/cod definition — and it has several advantages, especially in an introduction, e.g. more clearly exhibiting categories as a kind of algebraic structure on sets. On the other hand, definitions of enriched categories always use the many-hom-sets definition, with no disjointness condition — since it can’t be stated in that generality! — and authors have no qualms about saying that “categories enriched in sets” = “locally small categories”. – Peter LeFanu Lumsdaine May 18 '22 at 08:31
  • @PeterLeFanuLumsdaine Thank you for your comment. I had the enrichment processes on my route (later) so, I will observe this precise point better than I would have done otherwise. – Duchamp Gérard H. E. May 18 '22 at 11:20
1

$\newcommand\dom{\mathit{dom}}\newcommand\codom{\mathit{codom}}\newcommand\Ar{\mathit{Ar}}\newcommand\Ob{\mathit{Ob}}\newcommand\Hom{\mathit{Hom}}\newcommand\bHom{\mathbf{Hom}}\newcommand\vertex{\mathit{vert}}\newcommand\edge{\mathit{edge}}$As far as I know, it is clear in the mind of every category theorists (at least, the ones of my acquaintance and in founding texts as [5]) that, a category $\mathcal{C}$ comes with the usual axioms and two (mono-valued) maps $\dom$, $\codom$ from the class $\Ar(\mathcal{C})$ to the class $\Ob(\mathcal{C})$ so that if $f\in \Hom_{\mathcal C}(X,Y)$ is given we have $\dom(f)=X$, $\codom(f)=Y$. Now, if $$f\in\bHom_\mathcal{C}(Y,Z)\cap\bHom_\mathcal{C}(Y',Z')$$ and $$g\in\bHom_\mathcal{C}(X,Y)\cap\bHom_\mathcal{C}(X',Y')$$ we must have $X=X'$, $Y=Y'$, $Z=Z'$. The situation is very much like in graph theory, for the definition of a Directed Multigraph, a Quiver or an Automaton. I pick the definition in [1].

A Graph (understand Directed Multigraph) $\Gamma$ consists of a set $X=\vertex\Gamma$ and a set $Y=\edge\Gamma$ and two maps $o:\ Y\to X$ (origin) and $t:\ Y\to X$ (target).

This issue is explicitly unearthed and treated in [2] page 11 Remark 1.1.2 (e)

“If $f ∈ \mathcal{A}(A, B)$, we call $A$ the domain and $B$ the codomain of $f$. Every map in every category has a definite domain and a definite codomain. (If you believe it makes sense to form the intersection of an arbitrary pair of abstract sets, you should add to the definition of category the condition that $\mathcal{A}(A, B) \cap \mathcal{A}(A', B') = \emptyset$ unless $A = A'$ and $B = B'$.)”

The (mono-valued) functions are sometimes explicitly set up in the building axioms, see [3] page 11 definition 1.1.1 and, starting from axioms from which the MO could legitimately interpret these “functions” as “constructed” whereas they are “thought” as univalued (it is explicit in Serre) in the mind of many category theorists, one can repair this deficiency with triplets as in [4], page 22 Remark 3.2 point (3). I think this last construction can overcome the last construction you mention.

Late edit .- I had, this morning, the curiosity to come back to Mac Lane [5]. You can find there in chapter 1 section 2 the definition of a category through a graph with two functions $dom,cod$, very much in the spirit of Serre [1].

[1] Jean-Pierre Serre (1977), Trees, Springer.

[2] Tom Leinster, Basic Category Theory, Cambridge University Press (2014).

[3] Emily Riehl, Category theory in context, Cambridge University Press (2014).

[4] Jiřı́ Adámek, Horst Herrlich, and George E. Strecker, Abstract and Concrete Categories, The Joy of Cats.

[5] Mac Lane, Saunders, Categories for the Working Mathematician. Graduate Texts in Mathematics. Vol. 5 (Second ed.). Springer. ISBN 0-387-98403-8. Zbl 0906.18001.

Duchamp Gérard H. E.
  • 3,686
  • 2
    Hi Gérard — the issue is that this definition of a category begins with the data of the ${\bf Hom}\mathcal{C}(X,Y)$’s, and we may have that $X\neq X’$, $Y\neq Y’$, but $f\in{\bf Hom}\mathcal{C}(X,Y)\cap{\bf Hom}\mathcal{C}(X’,Y’)$ — in this case the constructed ‘functions’ dom, cod both send $f$ to more than one object and thusly fail to actually be functions (they are entire surjective relations, though). The ‘fix’ to this is to consider the coproduct $\coprod{X,Y\in{\bf Ob}\mathcal{C}}{\bf Hom}\mathcal{C}(X,Y)$ and use the projections down into the index set for dom and cod. – Alec Rhea May 08 '22 at 02:02
  • (that being said, all of this is ultimately tangential to the question I have) – Alec Rhea May 08 '22 at 02:04
  • I understand your concern and added an edit. Let me think of it. – Duchamp Gérard H. E. May 08 '22 at 05:35
  • 1
    Your edit does address one way to rectify the issue and I appreciate the thought you’re putting into this, but requiring the hom-classes to be disjoint runs into (fixable) issues as well. For instance, if you begin with a category having disjoint hom-classes together with an arbitrary monad, the EM category will not in general have disjoint hom-classes and so fails to be a category (!) by this definition. This can be fixed by passing to the disjoint union discussed above, but it feels ‘wrong’ to me for the definition of a category to fail to capture such ‘natural’ constructions. – Alec Rhea May 08 '22 at 06:57
  • 1
    Yes, we can take arrows to be triplets to overcome this issue and again arrive at disjoint hom-classes, but I was curious if the axioms given for the many hom-class definition of a category in the standard references yielded agreement for composition functions or if additional axioms are required. Using ‘artificial constructions’ to get around the issue and make the hom-classes disjoint is kind of talking around the question at hand. – Alec Rhea May 08 '22 at 09:16
  • 1
    Your domain and codomain functions can be annotated too... namely $dom_{X,Y},cod_{X,Y}\colon Hom_C(X,Y) \to Obj$, both constant at the respective values, where $Obj$ is the collection of objects, however these should be collected. – David Roberts May 08 '22 at 10:00
  • @DavidRoberts (+1) OK, this is also correct. – Duchamp Gérard H. E. May 08 '22 at 14:47
  • 1
    @DuchampGérardH.E.: I didn’t downvote it myself, but I disagree strongly with its central claims, as explained in my answer; I guess those who downvoted it disagreed on similar grounds. – Peter LeFanu Lumsdaine May 09 '22 at 07:04
  • 2
    @PeterLeFanuLumsdaine Thank you for the info ! I, myself, upvoted immediately (and before seeing any -1) your answer because I appreciated your metaphor with addition and abelian groups as well as the connection with Coq and UniMath (for which I am not competent). My answer was an attempt to give classical references within (standard) category texts. I maintain however that all category theorists of my acquaintance surmise in their mind that the Hom-sets are pairwise disjoint. Finally, no problem for me to recognize that you answer is richer. – Duchamp Gérard H. E. May 09 '22 at 08:09