nLab homotopy n-type

Redirected from "truncated types".
Contents

Context

Homotopy theory

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

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Idea

The notion of homotopy nn-type is a coarsened variant of the notion of homotopy type, that latter notion being recovered for n=n = \infty.

For instance a homotopy 1-type has trivial homotopy groups above degree 2, and a homotopy 2-type has trivial homotopy groups above degree 3.

Among the most important invariants of a topological space XX or, more generally, of an object XX in an ∞-stack (∞,1)-topos are its homotopy groups π k(X)\pi_k(X). We say that an object XX for which all π k(X)\pi_k(X) with k>nk \gt n are trivial is a homotopy nn-type. More precisely, these are the n-truncated objects and one says that two object XX, YY are of the same homotopy nn-type if there is a zig-zag of morphisms connecting them that induces isomorphisms on homotopy groups π k(X)π k(Y)\pi_k(X) \stackrel{\simeq}{\to} \pi_k(Y) for 0kn0 \leq k \leq n.

Homotopy nn-types are, thus, the equivalence classes of an equivalence relation imposed on objects in Top (or objects in another (∞,1)-topos). Thus, we often say, roughly, that two spaces ‘have the same homotopy nn-type’ if their homotopy groups agree up to π n\pi_n, and ‘a homotopy nn-type’ can equally well be represented by any space having that nn-type. This is analogous to the definition of ‘a real number’ as an equivalence class of Cauchy sequences. However, as usual in homotopy theory, merely having isomorphic homotopy groups is not enough; rather there needs to be a map inducing such an isomorphism. Thus, the relevant equivalence relation relates two spaces when there is a zigzag of maps between them, all inducing isomorphisms on homotopy groups π k\pi_k for knk\le n. One can then show that any space is equivalent, in this sense, to one having trivial homotopy groups above level nn, so that the other definition is also correct.

The use of topological spaces is not, of course, essential; we could just as well use any other structure that models the same homotopy theory, such as simplicial sets, simplicial groupoids, or (for connected spaces) simplicial groups. Moreover, the fact that homotopy nn-types can be modeled by spaces that are ‘homotopically trivial’ above level nn raises the possibility of finding reasonably complete algebraic models for such nn-types.

Definition

A continuous map XYX \to Y is a homotopy nn-equivalence if it induces isomorphisms on π i\pi_i for 0in0 \leq i \leq n at each basepoint. Two spaces share the same homotopy nn-type if they are linked by a zig-zag chain of homotopy nn-equivalences.

More formally, inverting the nn-equivalences in Top gives a homotopy category Ho n(Top)\Ho_n(\Top), and two spaces have the same homotopy nn-type if they become isomorphic in Ho n(Top)\Ho_n(\Top).

For any space XX, you can kill its homotopy groups in higher dimensions by attaching cells, thus constructing a new space YY so that the inclusion of XX into YY is a homotopy nn-equivalence; up to (weak) homotopy equivalence, the result is the same for any space with the same homotopy nn-type as XX. Accordingly, a homotopy nn-type may alternatively be defined as a space with trivial π i\pi_i for i>ni \gt n, or as the unique (weak) homotopy type of such a space, or as its fundamental \infty-groupoid (which should be an nn-groupoid, by one direction of the homotopy hypothesis).

One can also construct model structures on Top\Top whose homotopy categories are the categories Ho n(Top)\Ho_n(\Top). This is one of the original examples of Bousfield localization. From this perspective, the above replacement of a space by one having trivial π k\pi_k for k>nk\gt n is an example of fibrant replacement.

Algebraic models

We will use simplicial groups and simplicial groupoids rather than spaces below as they are already partially algebraicised. So in the definition above, ‘space’ means a simplicial group(oid) and ‘continuous map’ means a homomorphism of simplicial group(oid)s.

Considerable effort has gone into finding ‘good’ algebraic models for (connected) homotopy nn-types. In low dimensions the results are ‘old’ or ‘classical’. We will consider connected cases (simplicial groups) only. The extension to the non-connected case (simplicial groupoids) is ‘routine’.

  • The 1-type of a connected space is completely determined by its fundamental group, so groups form an algebraic model for homotopy 1-types. For the non pointed case, we can say groupoids form an algebraic model.

  • Crossed modules form an algebraic model for (connected) homotopy 2-types by a result of Mac Lane and Whitehead,

  • S. Mac Lane and J. H. C. Whitehead, On the 3-type of a complex, Proc. Nat. Acad. Sci. U.S.A., 36, (1950), 41 – 48.

The use of crossed modules of groupoids and their classifying space for the non pointed case is explained under homotopy 2-type.

  • Finding the algebraic model for the nn-types is just a start. Ideally one searches for algebraic models of all the higher homotopy structure as well. This was done by Jean-Louis Loday using the notion of a cat-n-group.

  • The method initiated by J.H.C. Whitehead was to approximate homotopy theory by models which analysed particular types of behaviour. One of his most widely followed models is that of stable homotopy theory. The opposite method was to find algebraic models of restricted classes of spaces, such as 2-types, or with cells in a small range of dimensions. H.-J. Baues has followed up many of the latter ideas.

It is sensible to regard crossed complexes as giving a linear model of homotopy types. These crossed complexes are equivalent to strict globular \infty-groupoids. Although these are restricted model of homotopy types, they are convenient in many aspects, because of the many analogies with the familiar chain complexes.

Crossed complexes capture operations of the fundamental groupoid, but not quadratic information such as Whitehead products (for dimensions >1\gt 1). However one can define nn-fold crossed complexes inductively as crossed complexes internal to (n1)(n-1)-fold crossed complexes. So one can give the

(Conjecture) double crossed complexes capture the quadratic information on homotopy types, triple crossed complexes capture the cubic information, etc., etc.

This has the possibility of leading to computations, by applying van Kampen theorems to specific levels.

Examples and special cases

homotopy leveln-truncationhomotopy theoryhigher category theoryhigher topos theoryhomotopy type theory
h-level 0(-2)-truncatedcontractible space(-2)-groupoidtrue/​unit type/​contractible type
h-level 1(-1)-truncatedcontractible-if-inhabited(-1)-groupoid/​truth value(0,1)-sheaf/​idealmere proposition/​h-proposition
h-level 20-truncatedhomotopy 0-type0-groupoid/​setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/​groupoid(2,1)-sheaf/​stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoid(3,1)-sheaf/​2-stackh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoid(4,1)-sheaf/​3-stackh-3-groupoid
h-level n+2n+2nn-truncatedhomotopy n-typen-groupoid(n+1,1)-sheaf/​n-stackh-nn-groupoid
h-level \inftyuntruncatedhomotopy type∞-groupoid(∞,1)-sheaf/​∞-stackh-\infty-groupoid

References

In homotopy theory

Discussion in traditional homotopy theory:

In homotopy type theory

Discussion of homotopy n n -types/ n n -truncated objects in homotopy type theory:

Last revised on November 16, 2023 at 21:37:45. See the history of this page for a list of all contributions to it.