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.
Jean-Baptiste Vienney (Jun 17 2024 at 02:06):The notion of morphism in any category used in practice is usually chosen so that all the properties verified by an object are invariant under isomorphism.
In more details, we consider most of the time only the properties of an object such that if the object verifies this property and if is an object isomorphic to , then the object also verifies this property.
As a practical example, the notions of "being a PID", "being a UFD", "being an euclidean domain", " divides " (where , are elements of a same ring), " is a unit", " is an idempotent", " is a zero divisor" are preserved under ring isomorphism.
As anyone formally explicited, for a categorical doctrine, or for a theory in first-order logic, what are all the properties which are invariant under isomorphisms? or at least formally defined the notion of "property invariant under isomorphism"? In the case of a categorical doctrine, it would require first to define formally what is a categorical doctrine. Maybe we could first be interested in the properties of a category in general such as: "having finite products", "having an initial object". Has anything like this been done?
Eric M Downes (Jun 17 2024 at 02:26):For equivalences, there is this paper by Freyd
Jean-Baptiste Vienney (Jun 17 2024 at 02:49):Thanks, that’s very cool!
Eric M Downes (Jun 17 2024 at 03:23):IIRC it boils down to "equivalences preserve commuting diagrams" which is unshocking, but he has a section on Fregeian logic thats pretty cool.
If I understand your question, it is "(1) what properties of categories are preserved by isomorphism, and (2) how can we encode/prove this in a logical system?". Is that right?
If I got that right I think the answer to part 1 is kind of appropriately trivial: tells us that if we forget the interpretation of "what objects are" and "what morphisms are", the remaining category structure is exactly the same: same arrangement of objects, morphisms, composition data, etc. just with different labels. (The functors cannot be projective must be injective fully faithful, etc.) So the interesting stuff occurs in part 2 or with different models of category. But maybe that's not what you meant.
Jean-Baptiste Vienney (Jun 17 2024 at 15:28):Thank you very much for the reference Eric.
I don’t know precisely what I want to know on the topic « properties invariant by isomorphism/equivalence ». I’m unable to formulate a very clear question. Perhaps, it will get clearer later.
Kevin Carlson (Jun 17 2024 at 17:20):Makkai's FOLDS is a more fleshed out story for a logic allowing one to make only statements invariant under equivalence. https://ncatlab.org/nlab/show/FOLDS
Jean-Baptiste Vienney (Jun 17 2024 at 18:31):Thanks, looks even better!
Jean-Baptiste Vienney (Jun 17 2024 at 18:37):I'm sure there should be difficult questions about properties invariant under isomorphisms in classical mathematics. They should not be easy to classify in general. Because, for instance, having a certain homotopic type or a certain homology, cohomology group of some kind for a topological space is a property invariant under homeomorphism and it is probably not easy to find all these kind of invariants.
Jean-Baptiste Vienney (Jun 17 2024 at 18:38):So, I want to say, this is not a trivial topic. Maybe it depends on what is the exact question you try to answer.
Jean-Baptiste Vienney (Jun 17 2024 at 18:41):These homotopy/homology invariants are trickier to talk about because they involve two different kinds of algebraic structures!
Kevin Carlson (Jun 17 2024 at 20:34):I don't really see your point about homotopy and homology. Describing the entire language of isomorphism invariants in some category could easily be easier than picking out all the specific interesting isomorphism invariants! For homotopy, say, it's pretty clear that you can prove they're homeomorphism invariants by defining them in a language that only uses obviously homeomorphism-invariant pieces like Cartesian products.
Jean-Baptiste Vienney (Jun 17 2024 at 21:18):Ok, I understand. The strategy is not to distinguish among the properties which one are invariant under isomorphisms, but to restrain your language so that you can only talk about such properties.