Timeline for Missing axiom in the typed definition of a category?
Current License: CC BY-SA 4.0
18 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 18, 2022 at 11:08 | comment | added | David Roberts♦ | 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. | |
| May 8, 2022 at 22:05 | vote | accept | Alec Rhea | ||
| May 8, 2022 at 21:31 | history | became hot network question | |||
| May 8, 2022 at 21:18 | comment | added | Simon Henry | @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 (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) | |
| May 8, 2022 at 19:59 | comment | added | LSpice | 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. | |
| May 8, 2022 at 19:18 | answer | added | Peter LeFanu Lumsdaine | timeline score: 19 | |
| May 8, 2022 at 16:48 | history | edited | LSpice | CC BY-SA 4.0 |
Link to comment; `\bf` -> `\mathbf`
|
| May 8, 2022 at 11:22 | comment | added | Duchamp Gérard H. E. | @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. | |
| May 8, 2022 at 10:40 | history | edited | Alec Rhea | CC BY-SA 4.0 |
added information suggested in comments
|
| May 8, 2022 at 10:36 | comment | added | Alec Rhea | @DavidRoberts I will edit accordingly, thank you for the suggestion. | |
| May 8, 2022 at 10:32 | comment | added | Alec Rhea | @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? | |
| May 8, 2022 at 10:29 | comment | added | Alec Rhea | @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. | |
| May 8, 2022 at 0:34 | answer | added | Duchamp Gérard H. E. | timeline score: 2 | |
| May 7, 2022 at 23:01 | comment | added | David Roberts♦ | 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. | |
| May 7, 2022 at 22:03 | comment | added | Reid Barton | 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. | |
| May 7, 2022 at 21:58 | comment | added | Simon Henry | 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. | |
| May 7, 2022 at 21:45 | history | edited | Alec Rhea | CC BY-SA 4.0 |
edited body
|
| May 7, 2022 at 21:38 | history | asked | Alec Rhea | CC BY-SA 4.0 |