Speaking in the internal language of a given category , one may try to formulate universal constructions such as of limits/colimits internally.
Given the system of slice categories of (or more generally any indexed category ), then one may regard as the shape of a discrete internal diagram in , and regard the objects in the slice as discrete actual internal diagrams of this shape.
If happens to have a (small) object classifier , then this is particularly evocative, as then (small) such slice objects over equivalent to morphisms , hence are directly analogous to external diagrams in the form of functors .
Now if has good enough properties as a (self-)indexed category in that it is a hyperdoctrine with dependent sum and dependent product operations, then it makes sense to define the internal colimit of a discrete diagram as above as
and the internal limit as
Of course with being, internally, a discrete diagram shape these are, so far, just internal coproducts and internal products, respectively (which is of course the source of the terminology “dependent sum” and “dependent product”).
It is more or less straightforward to extend the above from to , the collection of internal categories in , then consider for a given internal category (hence internal diagram shape) the objects in as not-necessarily discrete diagrams, and proceed as before. For various specific choices of context , this is considered in (Johnstone, below prop. B2.3.20, Pisani 09, p.18, p. 23, HoTTBook, section 6.12).
To see internally the expected universal property of the above definition, consider the internal -diagram constant on any , namely . If there is an object classifier then this corresponds indeed to the constant map . Accordingly an internal cone with tip over the diagram as above is a morphism of -diagrams (hence in ) of the fomr
Now by the defining adjunction of the dependent product, such morphisms are equivalent to morphisms
in , hence by the above definition to morphisms
from into the internal colimit.
This is clearly the internal version of the statement that is extrernally true Set, that the limit of sets over a diagram is the set of all its cones.
Dually, an internal cocone is a morphism
in , and by the defining adjunction of the dependent sum this is equivalently a morphism
exhibiting internally the statement familiar externally from Set that maps out of colimits of a diagram are equivalently cocones under that diagram.
The small object classifier of the (∞,1)-topos ∞Grpd is itself. Hence an -groupoidal-shaped diagram of ∞-groupoids is internally in ∞Grpd a discrete diagram . The slice object classified by this is the pullback of the universal right fibration, which is equivalently its (∞,1)-Grothendieck construction .
Accordingly the above gives the internal limits and colimits
and
There are indeed also the correct external (∞,1)-colimits and (∞,1)-limits, by the discussion here.
For an (∞,1)-topos and an ∞-group object, consider its delooping. Externally this is in general highly non-discrete, but internally this, being -groupoidal, is a disrete diagram shape.
An internal diagram of this shape
is equivalently an ∞-action of on the object named by
Now the internal colimit
is the homotopy quotient of by , equivalently the object of homotopy coinvariants. In ∞Grpd this is given by the Borel construction.
Similarly, the internal limit
is the homotopy invariants of the action.
More generally, the internal left and right Kan extension give the induced representation and coinduced representation constructions. See at ∞-action for more on this.
Francis Borceux, Chapter 8 in Vol 1 Basic Category Theory of: Handbook of Categorical Algebra, Cambridge University Press (1994) (doi:10.1017/CBO9780511525858)
Peter Johnstone, section B2 in Sketches of an Elephant
Claudio Pisani, Balanced Category Theory II (arXiv:0904.1790)
Univalent Foundations Project, section 6.12 of Homotopy Type Theory – Univalent Foundations of Mathematics
Last revised on March 23, 2021 at 05:54:27. See the history of this page for a list of all contributions to it.