Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
A more canonical choice of topic for a page in this direction would be something like category with specified type of objects. Then the current entry title could sensibly be relegated to a paragraph on equivalences between such structures.
Notice that for the case of groupoids and sheaves of such – i.e. in the context of stacks – such a notion is standard: one speaks of a stack equipped with an atlas, namely with an effective epimorphism from some 0-truncated object (see also here).
An isomorphism of stacks-equipped-with-atlases is then what you call a functor bijective on objects.
Since stacks are commonly understood in the generality of stacks of categories – 2-sheaves –, it would not be much of a stretch to say that choosing a specified type of objects for a category is to choose an atlas for it, which would serve to make clear that this is a natural structure to consider even outside the topic of foundations. So one might rename this page here to category with an atlas.
In any case, this notion could neatly be defined as choosing an essentially surjective functor from a set to the category. Categories equipped with such structure would form the comma-2-category of Sets eso over categories, and that definition would – it seems to me – at once take care of most of the headache here and in the other entries that you (?) are currently working on.
The actual motivation for creating this particular article is for defining structures like Freyd categories, in a manner which do not violate the principle of equality, where the definitions on the Freyd category article make explicit reference to categories which have the same objects, as well as other structures like Freyd multicategories and dagger categories which use an identity-on-objects functor, which also made explicit reference to categories which have the same objects.
Do the definitions of, i.e. a dagger category, result in a definition which doesn’t violate the principle of equivalence, if we say that i.e. a dagger category is a category with an atlas with an equivalence of atlases between and its opposite category with an atlas , such that etc…?
Given an index set , definition 2.4 indexed by is just a -enriched category, where is interpreted as a discrete category. Definition 2.3 is just a -enriched category, and a -enriched category with an identity-on-objects functor is just a -enriched category, where is the interval category.
I’m not convinced that this article is necessary. Are there any situations in which one cares about “two categories with the same collection of objects” other than where there is an identity on objects functor between them? If not, can’t we just do all the relevant discussion on the latter page?
Do the definitions of, i.e. a dagger category, result in a definition which doesn’t violate the principle of equivalence, if we say that i.e. a dagger category is a category with an atlas with an equivalence of atlases between and its opposite category with an atlas , such that etc…?
I think you’re misunderstanding what Urs is proposing. I think he means defining something like “Given a set/type , a category with atlas consists of a family of sets together with …”. In proof-assistant language, we take the ordinary definition of category and make the set of objects a parameter rather than a field. Once we have this definition, we can define, given two categories with atlas (this is morally analogous to saying “given two morphisms from to ”, hence equivalence-invariant), an “i.o. functor” or “functor with atlas ” between them to consist of functions such that etc.
I think I might like this idea. I think Urs has a good point that this would be a nice way to group all the foundational discussion on this subject, providing a unifying context and preventing it from polluting other pages like dagger-categories and Freyd-categories. But I need to think about it a bit more.
Re #5, there is and . I can think of other examples, but we’re interested in amalgamating two different kinds of arrows in some fashion, and the situation is usually formulated either as a double category, or as the category presented by the two kinds of arrows (and modulo relations between them).
I guess I can also think of Dwyer and Kan’s Simplicial Localizations of Categories which works in “”, the category of categories with a fixed set of objects (and also with simplicial objects in that category). FWIW these are the fibers of the cartesian fibration which might suggest how to organize foundations.
I feel like defining would be the most natural way to formulate the content this page wants to discuss, so I share the sentiment of #2.
Also, for some time, I’ve been rather partial of the description Urs describes in #2 – a category equipped with an essentially surjective functor from a set – for connecting the equivalence-respecting viewpoint on what a category is with the traditional version with a well-defined set of objects.
Also, for some time, I’ve been rather partial of the description Urs describes in #2 – a category equipped with an essentially surjective functor from a set – for connecting the equivalence-respecting viewpoint on what a category is with the traditional version with a well-defined set of objects.
I think whether you describe it that way or in some other way is orthogonal to whether you fix the set/type of objects as a parameter or consider it as a data field.
There is already a page strict category. Isn’t that discussing the same idea we’re talking about here?
No.
Maybe we should just create this page and then hopefully it will be clearer.
Just a propos:
Adrian Clough kindly pointed out to me that the notion of category with atlas in the sense of #2 above (but not under this name) is considered in:
Namely, their Def. 0.12 for says that a “flagged -category” is an -category equipped with a 0-connective -functor
out of an -category .
Here “0-connective” is equivalent to “essentially surjective” (as one would hope, but as also brought out by Def. 0.9 in the article and finding from the top line of p. 3).
I’m afraid now the name reflects the content even less. The page title ’category with an atlas’ refers to a single category. And then the idea launches into the concept of a pair of categories having the same collection of objects.
A 1-categorical analogue of the definition given in #12 is what I would have expected. Is this discussion thread the result of two other threads being merged? Or some discussion happening here in response to an example on the page that then grew out of propotion, but the discussion went elsewhere?
Complaints out the way, is the point of choosing that name is so that one can discuss two different categories with atlas where the domain of the atlas is the same in both cases?
The page will need a serious re-think, in particular the intro section, if the current title is meant to be kept.
I think the page is meant to be redone as indicated by Urs Schreiber’s comment at 2.
OK. But then all the content related to identity-on-objects functor should be removed, and definitely not be the content of the opening section.
Finally had some time to spare.
Have cleared the entry (the previous material, which did not fit with the new title, was all duplicated from identity-on-objects functor, where it may still be found) and then I have written some paragraphs on why to speak of “categories with atlas” and how.
1 to 18 of 18