# Contents

## Idea

The concept of a homotopy type (homotopy n-type) all of whose homotopy groups are finite groups does not have an established name. Sometimes it is called $\pi$-finiteness. In the context of groupoid cardinality “tameness” is used. In homological algebraof finite type” is used, which in homotopy theory however badly clashes with the concept of finite homotopy type which is crucially different from homotopy type with finite homotopy groups. (Anel 21) uses “truncated coherent spaces”.

## Properties

### (Co-)Limits indexed by homotopy types with finite homotopy groups

see at K(n)-local stable homotopy theory (…)

### Relation to coherent objects

###### Proposition

∞Grpd is a coherent (∞,1)-topos and a locally coherent (∞,1)-topos. An object $X$, hence an ∞-groupoid, is an n-coherent object precisely if all its homotopy groups in degree $k \leq n$ are finite. Hence the fully coherent objects here are the homotopy types with finite homotopy groups.

###### Proposition

The $(\infty, 1)$-category of homotopy types with finite homotopy groups is the initial (∞,1)-pretopos.

### Codensity monad of the inclusion into all homotopy types

The inclusion of homotopy types with finite groups into all homotopy types generates a codensity monad whose algebras lie somewhere between totally disconnected compact Hausdorff condensed $\infty$-groupoids, and all compact Hausdorff condensed $\infty$-groupoids. (See Scholze for more details.)

## References

• G. J. Ellis, Spaces with finitely many non-trivial homotopy groups all of which are finite, Topology, 36, (1997), 501–504, ISSN 0040-9383.

• Jean-Louis Loday, Spaces with finitely many non-trivial homotopy groups (pdf)

• Peter Scholze, Infinity-categorical analogue of compact Hausdorff, MO answer

Discussion as an elementary (∞,1)-topos: