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.
John Onstead (Sep 19 2024 at 02:40):Category theory is an amazingly expressive theory that allows one to describe a vast array of mathematical objects in relation to one another. However, for all its wonders, there's one key flaw: in a category where the objects are sets with extra structure, there is only one canonical and appropriate notion of morphism, which is the one that precisely preserves that extra structure. This can cause typing issues if one wants to define morphisms between objects of different categories, leading to a loss of expressiveness and limitations on the maps one can define in CT relative to the kinds of maps you can define in traditional material set-based math. One key place this crops up is in vector spaces and topological vector spaces. The appropriate notion of map for these structures are linear maps, and this is unfortunate because this is an extremely limiting restriction and we often want to define nonlinear maps between these spaces. We can try to solve the problem with representability, where an appropriate map in one setting is in correspondence with a "not allowed" map in another, and by extension adjunctions and monads (such as what can be done with (co)differential categories). However these are not general solutions.
So here I want to stop complaining about this problem and finally come up with a general solution to it. It comes in the form of double categories, specifically a type of double category known as a double category with companions AKA an F-category. An F-category is defined to be a category with two different types of morphism: loose and tight, where the tight morphisms are meant to be generalized by the loose morphisms. Examples of this in effect include the category of categories with strict functors as tight morphisms and pseudo/lax/oplax functors as loose morphisms, or the category of categories with normal functors as tight morphisms and profunctors as loose morphisms (the latter of which is the proarrow equipment of Cat).
John Onstead (Sep 19 2024 at 02:40):Here's how I want to apply F-categories to the problem. Let's say you have a category C and forgetful functor U: C -> D, and want to define a D-morphism between the underlying objects of C while still keeping track of the extra structure the objects in C have over those in D. For instance, defining a continuous function between topological vector spaces based on the forgetful functor U: TopVect -> Top. In normal category theory, you can either work in C where you are limited to the morphisms found there, or you can work in D where you have more morphisms at your disposal, but you've lost the structure on the objects you wanted to maintain by "forgetting" it. But using F-categories, we can define an F-category where the objects and tight morphisms are just exactly those of C, and the loose morphisms are the morphisms between the underlying objects of C in D. Symbolically, HomTight(A, B) ~ HomC(A, B) and HomLoose(A, B) ~ HomD(U(A), U(B)). The good news is you can do this for any forgetful functor U. An F-category corresponds to a bijective on objects, faithful functor between a category of tight and loose morphisms. Given any faithful ("forgetful") functor U: C -> D, you can use bo/ff factorization via the full image to get a bijective on objects and faithful functor C -> Im(U), thus automatically defining the F-category we desire.
With this F-category we can define for any faithful functor, we have the best of both worlds. We can define a non-structure preserving map between two objects without having to forget about the structure we've specified on them! It even works for non-structure preserving maps not generated by a forgetful functor, such as defining the F-category of sets, functions, and binary relations or partial functions. The latter, for instance, can allow us to define a partial map of sets A x A -> A without having to use the coproduct, which is important since it allows for a much easier definition of partial monoids or partial groups that would not have worked otherwise (since the single category of partial maps between sets does not define products the correct way, at least not as far as I know). I see a lot of potential in this idea, and I'm surprised this isn't more widely discussed since it solves such a big problem with category theory. Anyways, this is the idea. Let me know what you think of it and if you have any comments!
Kevin Carlson (Sep 19 2024 at 04:56):This is nice, nothing wrong with it; for myself, I see it as mostly a straightforward rephrasing of the notion of two categories with a forgetful functor between them. In fact is the category of b.o. full embeddings and you’re seemingly describing an object of here, rather than -enriched categories, which is what -category usually means. To make an enriched category out of the situation , it would probably be more natural to consider a category enriched over the category whose objects are monomorphisms in Set (rather than Cat, as with .) That is, you could give an -category such that the hom-object is the monomorphism
Kevin Carlson (Sep 19 2024 at 04:57):With that said, you’re presuming a lot when you say this “solves such a big problem in category theory.” Specifically, you’re assuming this typing issue is a big problem, and that this solves it, and that there’s not already another solution.
Kevin Carlson (Sep 19 2024 at 04:58):I don’t think either of the first two claims is true, and I can prove that the third one isn’t. For instance, the boff factorization you mention precisely allows you to construct a category whose objects are topological vector spaces and whose morphisms are continuous maps.
Kevin Carlson (Sep 19 2024 at 04:59):But talking about the boff factorization is already a bit overly fancy here; the reason why I don’t agree that this is a big problem in category theory is that nobody’s ever been sitting around going “oh geez, I really wanted a continuous map between these topological vector spaces but I just can’t figure out how to put them in the right category!” On paper, this is easy to do, so it doesn’t worry people. It’s true that on the computer people have to make these things more explicit. But I don’t think there’s been any fundamental mystery about how to do so when you need to. Hope this doesn’t come across as coming down hard on your thoughts; it’s a cool idea, just explaining why it might not make anybody jump up and down.
John Onstead (Sep 19 2024 at 05:19):Kevin Carlson said:
it would probably be more natural to consider a category enriched over the category M whose objects are monomorphisms in Set (rather than Cat, as with F.) That is, you could give an M-category
Ah thanks for the suggestion! I looked up M-category and it appeared to be exactly what I was talking about, they even mention on the nlab that you can get an M-category from any faithful functor just as I described! The M-category seems more natural to the 1-categorical setting, although an M-category does appear to be the same as an F-category when you view a 1-category as a 2-category where the 2-morphisms are all trivial (a locally discrete 2-category)!
Kevin Carlson said:
But I don’t think there’s been any fundamental mystery about how to do so when you need to. Hope this doesn’t come across as coming down hard on your thoughts; it’s a cool idea, just explaining why it might not make anybody jump up and down.
Thanks for the explanation! It makes sense; what might seem like a problem for someone might not be so much of a problem for someone else, depending on their philosophy. To illustrate, my philosophy of category theory fixates heavily on the structure preserving nature of morphisms, so while it is possible to define a category with a bijective correspondence of objects with C and with morphisms of D, those morphisms in D don't preserve the structure of objects of C. As such I find it difficult to accept an interpretation of the objects of the full image as being objects of C; rather, I see them as objects of D with the extra property that they can have the structure of objects in C equipped onto them. Another way to look at it is through the Yoneda perspective, which identifies an object with the surrounding environment of its category via all the morphisms into and out of it. If you change the morphisms in the category, then you are essentially also changing the nature of the objects described by that category under this kind of reasoning. Again this is just my personal philosophy but hopefully it gives insight into why I fixate so much on these typing issues!
Alex Kreitzberg (Sep 19 2024 at 05:51):I've been confused with and trying to understand something similar.
I have an image of a sphere in my mind, and I could imagine messing with it with Euclidean transforms, or projective transforms, or continuous transforms, and what becomes isomorphic changes as we consider what the ambient setting of maps are.
If I want to conclude something about a sphere in the category of topological spaces, and translate that to the category of Euclidean spaces, how to I keep my head on straight?
I think there's a chain of faithful forgetful Functors between the categories
And the idea is if a relationship is true in a category to the right, then we know it's true in a category to the left. Relationships are reflected.
It's just weird to think of one conceptual object as existing in multiple categories.
John Onstead (Sep 19 2024 at 05:58):You've stumbled upon something very interesting about category theory, which is that categories are very contextual. You can think of a category as being a certain context in which we study an object, determined by which structure we are highlighting. Structure is basically some kind of information we can put on a set, and in many cases complex mathematical objects have a whole bunch of "extra structure" all defined on some underlying set. If we want to examine the object under the lens of one of its structures, and ignore the rest, we can switch to a context where that structure takes center stage, which is precisely the category where the morphisms are those that preserve that particular structure. The actual switching is aided by the forgetful functor, which forgets all the irrelevant structure so that the only structure left on our sets is the one we are interested in studying at that moment. Highly encourage you to visit the nlab page on stuff, structure, property since seeing math in this philosophy is very mind opening!
Kevin Carlson (Sep 19 2024 at 06:43):John Onstead said:
As such I find it difficult to accept an interpretation of the objects of the full image as being objects of C; rather, I see them as objects of D with the extra property that they can have the structure of objects in C equipped onto them.
Most of what you say makes good sense to me, but one technical point: the middle guy in the boff factorization of a functor is not the full image, since of course the functor onto the full image is usually not bijective on objects. Instead its objects are really exactly the same as the original objects of the domain. (If you’re really “”evil””, you can define an identity on objects/identity on morphisms factorization!) (The full image comes from the essentially surjective/fully faithful factorization system, which is a 2-categorical thing in that these classes are only pseudo-orthogonal, or from the surjective on objects/injective on objects+fully faithful factorization system, which is a proper 1-categorical one.)
Kevin Carlson (Sep 19 2024 at 06:47):It is true that the boff factorization produces categories whose morphisms are not nicely given as the structure-preserving morphisms of their objects, and that might be the glint of a where this thinking starts to bear clearer fruit. But that gets back to my second complaint, that I don’t see that your -categories actually solve the problem in this sense. They might be a start at a solution, though; I think you’d want to explain what it means to have a “natural -category” in the sense that its homs are somehow the “automatic” structure-preserving -object of morphisms between its objects. Something like a tower of nested algebraic theories might be relevant here, or I suppose higher order theories to handle spaces.
Kevin Carlson (Sep 19 2024 at 06:53):Alex Kreitzberg said:
It's just weird to think of one conceptual object as existing in multiple categories.
One response to this is to say that when you have a picture of the sphere in your mind, it’s probably round, i.e. your picture includes the quantitative arrangement of its points relative to each other. It’s also smooth, eg you have no trouble identifying when a curve drawn on its surface is differentiable. So you’re picturing the sphere as an object of a category where there is shape and smoothness. The sphere is likely not a specific size, in which case you may be in, say, the category of Riemannian manifolds and conformal maps—your picture of the sphere is then essentially assembled from your idea of angles between curves drawn on its surface, such as latitude and longitude lines.
Kevin Carlson (Sep 19 2024 at 06:55):It’s still quite interesting to observe that when you visualize a topological map of the sphere, you’re likely to visualize the round sphere deforming, say, getting a weird asymmetrical protuberance on one side. This is actually visualizing a homotopy between two continuous maps into , so something in quite a different category, but if you just look at the endpoints of the deformation then it can be viewed as visualizing a continuous map between the image of two Riemannian manifolds under the forgetful functor to topological spaces. This psychology is quite intriguing to think through and I think not many people do so very explicitly, although there are some famous examples of Bill Thurston that kind of ring a bell.
Alex Kreitzberg (Sep 19 2024 at 07:17):Right, I suppose I thought to mention it here because it seems like my intuition travels between these different categories effortlessly.
And I can't tell whether it's just applying functors automatically, or if it's picking the right category for the problem (like in your first example) or if key structures are getting thrased.
This is interesting, but my intuition is running ahead of my understanding!
I asked a non math friend what an interval mapped into a sphere looks like - and they immediately suggested a path on a sphere! They're clearly not thinking in Set and they don't know topology!
If they have to parallel park, I'm sure they'll think in a Euclidean way.
What does it look like when you think in both styles at the same time? What does this look like when you write stuff down?
That's how I'm interpreting the difficult in the original post (but maybe they disagree with this interpretation)
John Onstead (Sep 19 2024 at 09:14):Kevin Carlson said:
the middle guy in the boff factorization of a functor is not the full image, since of course the functor onto the full image is usually not bijective on objects
Hmm, the nlab page says of full image that "it is the object through which the (bo,ff) factorization of a functor factors". Maybe there's different notions of "full image"?
Kevin Carlson said:
that I don’t see that your M-categories actually solve the problem in this sense. They might be a start at a solution, though; I think you’d want to explain what it means to have a “natural M-category” in the sense that its homs are somehow the “automatic” structure-preserving M-object of morphisms between its objects.
In an M-category defined via the factorization of a faithful/forgetful functor U: C -> D, the hom HomTight(-, -) is automatically defined to be the structure preserving morphisms of the objects of C simply because HomTight(-, -) ~ HomC(-, -). If you are wondering how we know the morphisms of C are the correct notion of structure preserving morphism for the objects of C in the first place, you can use something like model theory. In this case, find the theory that describes your mathematical object, find the functor category of model functors into Set, and see if there's an equivalence between that and C. If so, then indeed you have the "correct" notion of structure preserving map in C, and so by default the M-category will also have this.
The goal of using the M-category is to have a concept of non structure preserving map between objects while still keeping track of the structure on those objects. In this way, the loose morphisms act as the non structure preserving map (like the morphisms in a "full image") while the tight morphisms are the structure preserving maps that are there to help us keep track of what the structure is. They kind of act like labels, constantly reminding us what the structure on our objects are, even as we zoom around along the non structure preserving maps.
Mike Shulman (Sep 19 2024 at 14:59):Yes, the nLab's definition of "full image" is actually the category in the bo-ff factorization. But there's another definition, which Kevin presumably has in mind, where the objects are a subset of the objects in the codomain. However, the two definitions are equivalent categories (assuming the axiom of choice).
Mike Shulman (Sep 19 2024 at 15:37):I agree with Kevin that there is no technical problem here, and that you'll rub people the wrong way by claiming to be solving a "key flaw" in category theory. But it's true that we do often change the names of categories and their objects whenever we change the morphisms even if at a technical level the set of objects didn't change.
For instance, the opposite of the category of frames is called the category of locales, and the opposite of the category of commutative rings is called the category of affine schemes. And more closely related to your examples, the category whose objects are metric spaces and whose morphisms are continuous maps is arguably better known as the category of metrizable spaces: since the morphisms are only continuous, they only preserve topology and not metric nature, so we should really think of the objects as only "having" topological structure with the property that it could have come from a metric. Similarly, the category of topological vector spaces and continuous maps could be called the category of "vectorizable topological spaces".
Kevin Carlson (Sep 19 2024 at 15:43):John Onstead said:
Hmm, the nlab page says of full image that "it is the object through which the (bo,ff) factorization of a functor factors". Maybe there's different notions of "full image"?
Ah, annoying; the nLab has a strong preference to work up to equivalence but I would prefer to have the full image be an actual subcategory, which the boff factorization is not. But whatever you call it, the point holds that its objects are by definition literally objects of the domain.
Kevin Carlson (Sep 19 2024 at 15:43):Oh yeah, Mike has already said pretty much that.
Kevin Carlson (Sep 19 2024 at 15:45):But it does seem to me like the difference between the category of metric spaces and continuous maps and the category of metrizable spaces, which is nothing more than making a bunch of isomorphic copies of each object for every choice of specific metric (and similarly for “vectorizable” spaces), while usually insignificant, is relevant to the kind of concerns you’re having here.
Mike Shulman (Sep 19 2024 at 16:04):One way to make that distinction more real is to work in homotopy type theory. A category in HoTT has a type of objects plus sets (0-types) of morphisms. The type of objects can rarely be supposed to also be a set, so its identity types are a priori additional data vis-a-vis categories defined in set theory.
We get a theory that's closest to traditional category theory by requiring categories to be "univalent", meaning that for objects and , the identity type is equivalent to the type of isomorphisms from to (defined using the hom-sets) -- these are so important I usually prefer to call them simply "categories", and use "precategory" for the version without a condition on the identity type of the type of objects.
(Univalent) categories are closed under most category-theoretic constructions, and in particular most "naturally defined" categories of structured objects are univalent. But they're not closed under the obvious analogue of the bo-ff factorization. So if you start from the univalent category of metric spaces with its forgetful functor to the univalent category of topological spaces and perform the bo-ff factorization, you'll get a (pre)category whose type of objects is the type of metric spaces, and hence whose identity types consist (up to equivalence) of isometries, but whose hom-sets consist of continuous maps. This is not equivalent to the full subcategory of metrizable topological spaces.
Mike Shulman (Sep 19 2024 at 16:05):This is, of course, very similar to the M-category or double-category approach: a precategory whose types of objects are 1-types (which is always what you get from the bo-ff factorization applied to univalent categories) is, from a classical point of view, basically an M-category whose tight morphisms are all isomorphisms.
Alex Kreitzberg (Sep 19 2024 at 16:24):Wait, to see if I understand, there's a sense where you can track that objects are the same shape under isometries - while emphasizing you care about continuous transformations between them? And that's different than a metrizable subcategory of Top?
Kevin Carlson (Sep 19 2024 at 16:33):Mike's precategory of metric spaces and continuous maps has the property that an equality between two metric spaces is exactly an isometry between them, while an isomorphism is a homeomorphism. Homotopy type theory frees up equality from the usually-irrelevant set-theoretic equality, so here (if you're OK with precategories) you can use equality for your stricter notion of isomorphism. It's worth noting that this precategory doesn't remember the non-invertible metric space maps; that would need directed type theory, which is an ongoing project but more bleeding edge.
John Baez (Sep 19 2024 at 17:17):Alex Kreitzberg said:
It's just weird to think of one conceptual object as existing in multiple categories.
No, it's not weird. This is how math works. First, "the sphere" is NOT one conceptual object in any sort of precise sense. There are many spheres:
There's the 'metric space sphere' where we can measure distances between points. In fact there are at least 2 really important metric space spheres: one where we measure distances along the surface of there sphere, and one where we measure distances in the ambient . This sphere has a 3-dimensional Lie group of symmetries.
There's the 'topological space sphere' where we only equip the sphere with a topology, not a metric. This sphere has a huge infinite-dimensional topological group of symmetries.
There's the 'smooth manifold sphere' where we make the sphere into a manifold. This sphere has a infinite-dimensional Frechet Lie group of symmetries, which is huge - but tiny compared to the symmetry group of the topological space sphere.
There's the 'set sphere' where we treat the sphere as a set. This has an even larger symmetry group, of cardinality greater than the continuum, consisting of all permutation of points on the sphere.
There's the 'complex analytic sphere' where we treat the sphere as a complex analytic manifold of complex dimension 1. This has a 6-dimensional real Lie group of symmetries (which is a 3-dimensional complex Lie group).
And so on: you need to separately learn theorems about each of these objects.
John Baez (Sep 19 2024 at 17:19):As you guessed, all these different objects in different categories are related by functors between those different categories.
John Baez (Sep 19 2024 at 17:22):Math does not operate solely within one category at a time! Except for very limited tasks, we need to be working with a bunch of categories , and functors between them, and natural transformations between those. When we study 'the sphere' or 'the integers' or 'the real numbers', we are looking at not a single object, but multiple objects, in different categories, that are mapped to each other by functors.
Most mathematicians do this naturally and almost unconsciously, saying things like "the sphere has a 3d real Lie group of symmetries that preserve its metric, but a 3d complex Lie group of symmetries that preserve its complex structure".
One of the jobs of the category theorist is to formalize what's going on here - but not scold the mathematicians who do all this naturally. That would be like scolding a dolphin for not having taken swimming lessons.
Mike Shulman (Sep 19 2024 at 17:24):And there's also a 'homotopy sphere' which we treat as an -groupoid, which has an -group of symmetries.
John Baez (Sep 19 2024 at 17:38):Yes, that's a wonderful sphere. We don't even know all the homotopy groups of this homotopy 2-sphere. But here's a cool way to describe them.
Let's say a braid is "Brunnian" if when you remove any one strand, the remaining braid becomes the identity: you can straighten out all the remaining strands to make them vertical. It's a fun little exercise to check that Brunnian braids form a subgroup of all braids. So, we have an n-strand Brunnian braid group .
A braid is a bunch of points moving around on a plane as time goes by. We can also define 'spherical braids' where they move around on a sphere. And we can define spherical Brunnian braids. Let's call the group of n-strand spherical Brunnian braids .
There's an obvious map
coming from the inclusion of the plane in (the sphere is the plane plus a point at infinity).
And then we have
Theorem. The nth homotopy group of the sphere, , is isomorphic to .
John Baez (Sep 19 2024 at 17:39):This was proved here:
John Baez (Sep 19 2024 at 17:41):This is one of the most shocking facts I know.
John Onstead (Sep 19 2024 at 19:07):Mike Shulman said:
One way to make that distinction more real is to work in homotopy type theory. A category in HoTT has a type of objects plus sets (0-types) of morphisms. The type of objects can rarely be supposed to also be a set, so its identity types are a priori additional data vis-a-vis categories defined in set theory.
So if you start from the univalent category of metric spaces with its forgetful functor to the univalent category of topological spaces and perform the bo-ff factorization, you'll get a (pre)category whose type of objects is the type of metric spaces, and hence whose identity types consist (up to equivalence) of isometries, but whose hom-sets consist of continuous maps. This is not equivalent to the full subcategory of metrizable topological spaces.
This is a very interesting construction and I think it's also a really good way to do what I wanted. I'm a little surprised that, when trying to think about ways of keeping track of types in category theory, I didn't use, well, types and type theory! But this approach makes sense to me- the typing on the objects of a category tell you how to interpret those objects in a purely mathematical way, no external interpretation needed. So even when you do switch up the morphisms (like moving to the full image under a faithful functor), the "tag" is still there to tell you what the objects of your category are supposed to be! It also seems to be more efficient than using all the structure preserving maps as the "tag" instead, although as pointed out later, it might be a challenge to "mix" structure preserving and non structure preserving maps in a type theory category like you can do in an M-category.
Though I do have some lingering questions about this. I don't know much about type theory, so I'm not sure if the "tag" a type gives to a collection of objects is just a purely declarative syntactic statement or if it can encode deeper meaning. That is, if it's either just a way to say "Hey! These objects have a vector space structure", but then leave exactly what a "vector space structure" is to the imaginations of the mathematicians, or if it's possible to associate the actual construction or axioms of a vector space structure with that particular type. My second question would be: what is the difference between a precategory or univalent category, and a category internal to a category of types?
Mike Shulman (Sep 19 2024 at 19:24):Well, each type in type theory has a definition. So "the type of vector spaces" is a type whose elements are sets along with addition, scalar multiplication, etc. In that sense the type is associated to the definition of a vector space.
However, if I work with an arbitrary (pre)category, then its type of objects is just a type. It just has elements and equalities between them (and equalities between those, etc.), it doesn't have any other general notion of "structure" on its elements that would specialize in particular cases to, say "the structure of a vector space".
This is the same as set theory, by the way: any particular set has particular elements that may be structured, but an abstract set just has elements without knowing anything about them.
Mike Shulman (Sep 19 2024 at 19:27):As for your second question, a precategory is very much like a category internal to the category of types. In HoTT there isn't a 1-category of all types, but there is at least morally an -category of them, and a precategory is basically the same as an internal category in that -category whose hom-types are sets. (And under that restriction, you can define it without needing to refer to the entire -category, which is a good thing since we don't know how to do that in vanilla HoTT.) The definition of precategory is formulated with hom-types dependent on the object type rather than in the usual internal-category style, but they're equivalent.
John Onstead (Sep 19 2024 at 23:52):I now want to expand on this subject a bit. With either the M-category or type theory idea, for forgetful functor U: C -> D you can define a D-map between two C-objects, but what if you want to define a D-map from a D object into a C object, or from a C object into a D object? It seems you need to do this a lot as well sometimes (such as if, for instance, you wanted to define a continuous map from a topological space into a topological vector space to see whether or not it is differentiable or smooth). The M-category approach I gave above will not suffice, and neither will the type theory approach (since all objects in such a category will of course need to be of the same type). I've come up with the following idea but I don't know exactly what it is or if it has been discovered before.
First, we need to define a category with both the objects of D and the full image of U, and I'll call it UD. We could do a disjoint union, but I want it so that HomUD(a, b) ~ HomD(F(a), b) for a in Im(U), b in D, and F: Im(U) -> D the fully faithful functor part of the bo/ff factorization. I guess it's like a disjoint union, but you are then freely adding isomorphisms between a and F(a) for all a in Im(U). I'm going to just assume there's a canonical projection (perhaps associated to the universal property defining UD if it exists) C -> UD which sends C into the Im(U) part of UD in exactly the same way as the bijective on objects functor from the bo/ff factorization. But this time the functor is no longer bijective on objects, so we have to fix that to get this into being an M category again.
John Onstead (Sep 19 2024 at 23:54):We can do this by freely adding the rest of the objects of D to C, which takes the form of a disjoint union C u Disc(D), where Disc(D) is the category D when we remove all non-identity morphisms. We get the canonical projection C -> C u Disc(D). We can then define a bijective on objects and faithful functor C u Disc(D) -> UD that maps C into the Im(U) part of UD (just as the original bijective on objects functor C -> Im(U) ) when composed with the projection C -> C u Disc(D), and that maps all the other objects floating around in C u Disc(D) to some object of D in a one to one way. The end result is an M-category where the objects are both the objects of C and D, the tight morphisms are all the ones in C, and the loose morphisms are all the ones in D. You can now define a D-morphism between a D-object d and a C-object c, and even D-morphisms between the underlying object U(c) of c in C and c itself (of which will include a D-isomorphism).
Have you ever encountered such a construction as UD and the functor C u Disc(D) -> UD before? Let me know!
Mike Shulman (Sep 20 2024 at 00:53):I didn't follow your definition entirely, but it looks a lot like the [[cograph of a functor]].
John Onstead (Sep 20 2024 at 01:26):Mike Shulman said:
I didn't follow your definition entirely, but it looks a lot like the [[cograph of a functor]].
The cograph looks almost like what I'm trying, it's just missing morphisms going the other way. Hom(x, y) in the cograph of a functor F, for x in the domain and y in the codomain category of F, is bijective with Hom(F(x), y) in the codomain of F, which indeed is what I'm looking for. However, there is an empty hom set going the opposite way, whereas in my construction Hom(y, x) in the construction would also be bijective with Hom(y, F(x)) in the codomain. This would allow D-morphisms both into and out of objects of C. So it seems related, it could be some sort of a localization of the cograph.
Mike Shulman (Sep 20 2024 at 01:36):And the morphisms in your category between two objects in the domain of are the morphisms between their images in ?
Mike Shulman (Sep 20 2024 at 01:38):If so, then what you have is the "categorical mapping cylinder". I don't think it has an nLab page, but it is a (cofibration, trivial fibration) factorization in the [[canonical model structure on Cat]]. Classically, it's equivalent to , but I guess its precategory version in HoTT isn't.
John Onstead (Sep 20 2024 at 03:53):This seems right, but I really do wish that a full definition was written down so I could confirm! I couldn't find any resources on it though, only resources talking about the topological or homotopical mapping cylinder.
The construct would be equivalent to D since while we are adding in extra objects to D (all the objects of C), we are setting an isomorphism from each of them into an object in D. Though this really does bring up a whole other side to this discussion of typing in category theory when it comes to how to interpret equivalence of categories. Essentially, if two categories are equivalent, does that mean the objects of those categories are the same as well? I've seen cases where the objects are treated as "the same", for instance if you have multiple ways of defining the same mathematical object, you can check they do define the same object if the category of models of the theories for each way of defining it are equivalent. This might be called a "Morita equivalence" or something like that but I may be misremembering. Of course, we are meant to interpret the objects as "the same" via the principle of equivalence.
However, sometimes we are asked to treat two sides of an equivalence as a duality rather then direct equality. So the objects are meant to be interpreted as being different, just that there's some operation we can do to switch back and forth between them. In fact, many interesting connections between branches of math (such as what was recently proven with the geometric Langlands conjecture) involve proving an equivalence of categories, but obviously the objects in both categories are meant to be different or else the equivalence would be so obvious it wouldn't need to be proven in the first place! Since M-categories might not help here, I'm guessing distinguishing between equivalences for same and not same objects would require the type theory interpretation, where the type categories can be non-equivalent even when their "underlying" normal categories are.
Mike Shulman (Sep 20 2024 at 04:07):There's an explicit definition on p4 of Rezk's note A model category for categories.
Mike Shulman (Sep 20 2024 at 04:11):if two categories are equivalent, does that mean the objects of those categories are the same as well?
They're not identical: if I have an object of one category, it isn't itself an object of the other category, although it corresponds to one under the equivalence. When treating equivalent categories as "the same", we likewise treat each object as "the same" as its correspondent(s) on the other side, but formally speaking there is a "transport" involved replacing one by the other.
Mike Shulman (Sep 20 2024 at 04:12):In classical set-theoretic foundations, there's no sense in which the sets of objects of two equivalent categories are "the same" other than the sense expressed by the equivalence of categories itself. In particular, the two sets of objects could even have different cardinalities.
Mike Shulman (Sep 20 2024 at 04:15):But in HoTT, when two univalent categories are equivalent, then their types of objects are equivalent as types.
Mike Shulman (Sep 20 2024 at 04:15):However, they're not definitionally equal: you still have to apply the equivalence to get from an object of one category to an object of the other one.
John Onstead (Sep 20 2024 at 14:29):Mike Shulman said:
There's an explicit definition on p4 of Rezk's note A model category for categories.
Thanks, this turned out to be exactly what I was looking for. It seems from that article that this is constructed by a pushout in Cat that "looks like" the pushout in Top that generates the mapping cylinder there, which gives me the universal property I wanted as well!