## 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 community | 6 Servers |

Timestamp | Message | |
---|---|---|

3 Feb 2020 | ||

20:56:30 | Joel Sjögren | You proved it by choosing x := id_A. |

20:57:39 | chexxor | Id_A is x where X is A, but what if X is a non-A? |

20:57:50 | Christian Bertram | Yes, 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 | Oh wait, nvm. I'm thinking from a programming language interpretation of that. |

20:58:57 | chexxor | Ugh, I am so bad at math. Never sure if I'm doing it right. I need my computer-checker, lol. |

21:00:25 | Christian Bertram | Okay :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 | That's why I thought it was intuitive too, but I can't prove it. |

21:08:40 | Joel 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 | Joel 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 | Christian Bertram | I 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 | Joel Sjögren | Np good question :) |

21:16:53 | Joel Sjögren | There is a ladder of concepts: equality, isomorphism, equivalence, biequivalence, ... |

21:17:15 | Joel Sjögren | I haven't learned what precisely biequivalence means yet. |

21:19:42 | Christian Bertram | Okay, 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 | Joel Sjögren | * There is a ladder of concepts: equality, isomorphism, equivalence, biequivalence, ... |

21:20:04 | Joel Sjögren | Yes exactly. |

21:24:34 | Joel 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 | Christian Bertram | Okay, so an equivalence is more than just an isomophism in the category of small categories? |

21:30:12 | Joel Sjögren | Yes, isomorphism of categories is as bad a concept as equality between objects of a category. |

21:32:29 | Joel 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 | Joel Sjögren | As you see then, equivalence is defined in terms of isomorphism, like isomorphism is defined in terms of equality. |

21:33:47 | Christian Bertram | Ah okay, interesting! It's nice to hear about what I am reading now is building up to, from someone further ahead :) |

21:35:34 | Joel 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 | Christian Bertram | No, I have not gotten around to learning type theory yet (I hope to!) |

21:41:46 | Joel Sjögren | You can try Agda. |

21:45:53 | Christian Bertram | I 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 | Christian Bertram | In reply to @joel135:matrix.orgOkay, thank you for the suggestion. I've been meaning to check it out for some time. |

21:52:05 | Joel Sjögren | * Yes, isomorphism of categories is as bad a concept as equality between objects of a category. |

22:08:01 | Søren Skeie joined the room. | |

4 Feb 2020 | ||

12:45:32 | Joel 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". |

Back to Room List