homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
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 algebra “of 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”.
see at K(n)-local stable homotopy theory (…)
∞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.
(Lurie SpecSchm, example 3.13)
The $(\infty, 1)$-category of homotopy types with finite homotopy groups is the initial (∞,1)-pretopos.
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.)
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:
Formalization in homotopy type theory (via Agda):
Last revised on August 12, 2023 at 14:08:02. See the history of this page for a list of all contributions to it.