homotopy hypothesis-theorem
delooping hypothesis-theorem
stabilization hypothesis-theorem
n-category = (n,n)-category
n-groupoid = (n,0)-category
A subcategory of a category is called replete if it respects isomorphism of morphisms in the arrow category of . It is a subcategory for which the property of (strictly) belonging to it is not evil.
A subcategory of is replete if for any in and any isomorphism in , both and are also in . Equivalent ways to state this include:
Since repleteness is a “closure condition,” the intersection of any collection of replete subcategories is again replete. Therefore, any subcategory is contained in a smallest replete subcategory, called its repletion. We can construct the repletion of explicitly as follows:
Repleteness and repletions are most often applied to full subcategories, in which case the repletion is simply the full subcategory of determined by those objects which are isomorphic to some object of . In particular, in this case, the repletion is equivalent to . More generally, we can say:
The inclusion is an equivalence if and only if the inclusion is pseudomonic.
The inclusion of a replete subcategory is always pseudomonic, so if is an equivalence, and in particular full and faithful, then must also be pseudomonic.
Conversely, if is pseudomonic, then every morphism of can be written as for some morphism in and isomorphisms and in . If the domain and codomain are in , then since is pseudomonic, both and must also be in , hence such a morphism is itself necessarily in . Thus the inclusion is full. It is clearly faithful and essentially surjective, so it is an equivalence.
The replete image of a functor is the repletion of its image. The replete full image of a functor is the repletion of its full image, i.e. the full subcategory of its target determined by those objects isomorphic to some object in its image. See also essential image.
More generally, for , a subcategory of an -category is replete if all equivalences in whose either source or target is in are themselves in . In particular, all -cells equivalent in to some -cell in are themselves in (because they are sources of some equivalence in ). Then replete subcategories of -categories are those which are replete in this sense.
Here we are using the weakest notion of equivalence; one could also talk about -replete -subcategories if every -equivalences in belongs to if either its source or target does. Then using the usual definition of ‘category’ as a model for -categories, replete subcategories are already those which are -replete (indeed, -equivalence is isomorphism in this model); but using a model of -categories in which hom-sets are setoids (as is common, for example, in type-theoretic foundations), we must insist on -repleteness.
Note that a subcategory of an -category is -replete if and only if:
Do we want this parametrised equivalence? I see that isomorphism is -equivalence and equality is -equivalence, which is ugly enough but the sort of thing that does happen. But I've never actually heard anybody say that, for example, some objects of a -category are -equivalent. Why not just say that they're equivalent? (If anything, I'd rather say that they're -isomorphic and let ‘equivalent’ mean -isomorphic always.) —Toby
Mike: Definitely, unqualified “equivalent” in an -category should mean -equivalent, or equivalently (if you like your -categories to be secretly -categories) it should mean -equivalent. I think that is by far the most common usage, so it won’t have to change. However, there are occasionally reasons to speak about stronger sorts of equivalence; for instance in a strict 2-category it is occasionally important to distinguish between isomorphism and equivalence. People do also talk about “biequivalence” for bicategories and “2-equivalence” for 2-categories. I would venture that -equivalence in an -category for is not likely to be useful unless your -category is some sort of semistrict, but in that case it might occasionally turn out to be helpful.
Zoran Škoda: The -cells in -category are by default -equivalent (what is of course maximal weakness and equals infty-equivalent), while it is possible that they are equivalent in more strict sense, for example isomorphic (there is a strictly invertible 1-arrow in between); for higher cells equivalence is the same as equivalence in lower dimension category which is its hom, thuis the number is not by default for k cells k bigger than 0; of course you are right that all these maximal equivalences are in the same time equivalences in higher sense because there is no difference since higher dimensional cells do not exist different than identities. But regarding that sometimes stricter versions are needed, not only maximal the terminology can be kept precise. For example in Cat one can consider both isomorphic and equivalent categories and these are two different notions; and of course equal categories as the strictest possible notion of (-1)-equivalence. I do not recall if I first read this in print from Leinster’s book, but before that Igor explained me those after his readings of Australian school works.
Toby: Not every concept of -category even has a concept of equivalence of objects other than -equivalence (or more generally a concept of equivalence for -morphisms other than -equivalence). I find it confusing to put in all of these prefixes to describe what even you, Zoran, agree is the default notion. So I have given this default first, and then added a note about using stricter levels of equivalence when available.
Zoran, you might also want to address these issues at equivalence.