Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
A finite -limit is an (∞,1)-limit over a finitely presented (∞,1)-category – a finite (∞,1)-category.
If we model our (∞,1)-categories by quasicategories, then this can be made precise by saying it is a limit over some simplicial set with finitely many nondegenerate simplices. Note that such a simplicial set is rarely itself a quasicategory; we regard it instead as a finite presentation of a quasicategory.
An (∞,1)-functor out of an (∞,1)-category that has all finite -limits preserves these finite -limits as soon as it preserves (∞,1)-pullbacks and the terminal object.
This appears as (Lurie, cor. 4.4.2.5).
Let be a small (∞,1)-category with finite -limits, and an (∞,1)-topos. Write for the (∞,1)-category of (∞,1)-presheaves on .
If a functor preserves (∞,1)-colimits and finite -limits of representables, then it preserves all finite -limits.
This appears as (Lurie, prop. 6.1.5.2).
Binary products, pullbacks, and terminal objects are all finite -limits.
Unlike the case in 1-category theory, the splitting of idempotents is not a finite -limit.
Relation to homotopy type theory:
Last revised on July 6, 2023 at 23:16:19. See the history of this page for a list of all contributions to it.