nLab semi-simplicial object

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

Contents

Idea

A semi-simplicial object is like a simplicial object, but without degeneracy maps. In Set it is a semi-simplicial set.

Definition

In terms of functors

For 𝒞\mathcal{C} a category or (∞,1)-category, a semi-simplicial object XX in 𝒞\mathcal{C} is a functor or (∞,1)-functor

X:Δ + op𝒞 X \colon \Delta_+^{op} \to \mathcal{C}

from Δ +\Delta_+, the wide subcategory of the simplex category on the injective functions (the co-face maps).

In homotopy type theory

One may try to formulate semi-simplicial types in homotopy type theory. See semi-simplicial types in homotopy type theory and see the discussion at (IAS).

Properties

Directedness

As opposed to the simplex category Δ\Delta, the subcategory Δ +\Delta_+ is a direct category.

Examples

References

For more references see also at semi-simplicial set and semi-Segal space.

Semi-simplicial bundles

Discussion of semi-simplicial fiber bundles is in

  • M. Barratt, V. Gugenheim and J. C. Moore, On semisimplicial fibre bundles, Amer. J. Math. 81 (1959), 639-657.

  • S. Weingram, The realization of a semisimplicial bundle map is a kk-bundle map (pdf)

In homotopy type theory

Discussion of formulation of semsiplicial types in the context of homotopy type theory (for use as discussed at category object in an (infinity,1)-category) is in

Coq-code for semi-simplicial types in homotopy type theory had been proposed in

but its execution requires augmenting homotopy type theory with an auxilirary extensional identity type, discussed in

See at Homotopy Type System (“HTS”) for more on this.

More along these lines is in

Last revised on July 13, 2023 at 14:38:09. See the history of this page for a list of all contributions to it.