!juhLavcoMtmOVJnyJr:matrix.org

Category Theory

48 Members
a place to discuss category theory, both applied and theoretical, and any other related things | part of the +mathematics:matrix.org community6 Servers

Load older messages


Timestamp Message
3 Feb 2020
20:56:30@joel135:matrix.orgJoel Sjögren You proved it by choosing x := id_A.
20:57:39@chexxor:matrix.orgchexxorId_A is x where X is A, but what if X is a non-A?
20:57:50@cbertram:matrix.orgChristian BertramYes, but I am not sure that if the statement is still true, if fx=gx for all x not equal to id_A, and we don't know if it is true for x=id_A?
20:58:10@chexxor:matrix.orgchexxor Oh wait, nvm. I'm thinking from a programming language interpretation of that.
20:58:57@chexxor:matrix.orgchexxor Ugh, I am so bad at math. Never sure if I'm doing it right. I need my computer-checker, lol.
21:00:25@cbertram:matrix.orgChristian BertramOkay :P I also initially thought it was intuitive though. Because generalized elements, if I understand correctly, are supposed to be a counterpart to the statement in Sets, that f=g if fx=gx for all elements x in the domain of f and g? But I am guessing
21:01:26@chexxor:matrix.orgchexxor That's why I thought it was intuitive too, but I can't prove it.
21:08:40@joel135:matrix.orgJoel Sjögren It is not a very natural situation, when we exclude id_A. For instance if there is any "other" object A' which is isomorphic to A then we can recover the case x := id_A. (Do you see how?) But there should be a counterexample. Consider a category with objects {0 1 2 3} and arrows {u : 1 -> 2, v : 1 -> 2}. We intend u and v to be unequal by definition, yet ux = vx for all X and x : X -> 1 except id_1 : 1 -> 1 -- vacuously!
21:12:58@joel135:matrix.orgJoel Sjögren (The reason I put "other" in quotes is that one usually does not talk about equality between objects in a general category. It is not a thing which is invariant under equivalence of categories. But in specific cases like the finite one above it can still be ok to talk about it.)
21:13:28@cbertram:matrix.orgChristian BertramI also thought about a counterexample with such very small categories, but thought that it maybe applied to only slightly larger categories, where X is not the same object as the domain of the arrows we are checking equality on. But good point about it not being very natural to exclude an object like that. Thank you :)
21:14:03@joel135:matrix.orgJoel Sjögren Np good question :)
21:16:53@joel135:matrix.orgJoel SjögrenThere is a ladder of concepts: equality, isomorphism, equivalence, biequivalence, ...
21:17:15@joel135:matrix.orgJoel Sjögren I haven't learned what precisely biequivalence means yet.
21:19:42@cbertram:matrix.orgChristian BertramOkay, so the more abstract the structures you look at become, the higher (in the ladder) the type of "equivalence/equality" you care about becomes? Or what do you mean?
21:19:46@joel135:matrix.orgJoel Sjögren * There is a ladder of concepts: equality, isomorphism, equivalence, biequivalence, ...
21:20:04@joel135:matrix.orgJoel Sjögren Yes exactly.
21:24:34@joel135:matrix.orgJoel Sjögren In general when you look inside things or you look at at arrows between things, you climb down this ladder and things become simpler. So while equivalence is the correct notion between two categories A and B, isomorphism is the correct notion between objects x and y of the same category A, and equality is the correct notion between morphisms f and g in the common set Hom_A(x, y).
21:29:03@cbertram:matrix.orgChristian BertramOkay, so an equivalence is more than just an isomophism in the category of small categories?
21:30:12@joel135:matrix.orgJoel SjögrenYes, isomorphism of categories is as bad a concept as equality between objects of a category.
21:32:29@joel135:matrix.orgJoel Sjögren An equivalence of categories is a pair of functors f : X <->Y : g together with a pair of isomorphisms between fg (resp gf) and id.
21:33:23@joel135:matrix.orgJoel Sjögren As you see then, equivalence is defined in terms of isomorphism, like isomorphism is defined in terms of equality.
21:33:47@cbertram:matrix.orgChristian BertramAh okay, interesting! It's nice to hear about what I am reading now is building up to, from someone further ahead :)
21:35:34@joel135:matrix.orgJoel Sjögren In this way the notions are nicely ordered, but there are some subtleties. When I said "the same category" or "the common set" above I didn't intend to use either of those three notions, but something like intensional/definitional equality as used in type theory. Do you know intensional equality?
21:37:40@cbertram:matrix.orgChristian BertramNo, I have not gotten around to learning type theory yet (I hope to!)
21:41:46@joel135:matrix.orgJoel Sjögren You can try Agda.
21:45:53@cbertram:matrix.orgChristian BertramI think I have a idea of what definitional equality from reading ncatlab.org. I think I see why that distinction is important here
21:47:08@cbertram:matrix.orgChristian Bertram
In reply to @joel135:matrix.org
You can try Agda.
Okay, thank you for the suggestion. I've been meaning to check it out for some time.
21:52:05@joel135:matrix.orgJoel Sjögren * Yes, isomorphism of categories is as bad a concept as equality between objects of a category.
22:08:01@skeie:matrix.orgSøren Skeie joined the room.
4 Feb 2020
12:45:32@joel135:matrix.orgJoel Sjögren I think I was wrong when I said "isomorphism of categories is as bad a concept as equality between objects of a category". It is more true that "isomorphism of objects in a general 2-category is as bad a concept as equality between objects of a category" while "isomorphism of categories is as good a concept as equality between sets".

Show newer messages


Back to Room List