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
In algebraic topology and homotopy theory, a cocylinder is a dual construction to a cylinder. In contexts where spatial intuition is involved, it is perhaps more often called a path space $X^I$ or a path space object. In general, however, a cocylinder, $X^I$, may not involve any object $I$ nor use a mapping space in its construction, see cylinder functor for the discussion of the dual point.
These are the duals of cylinders and cylinder functors so can safely be left as an exercise.
Similarly, the mapping cocylinder, which is dual to the mapping cylinder, is equally called the mapping path space or mapping path fibration. It provides a canonical way to factor any map as a homotopy equivalence followed by a fibration.
For a topological space $X$, its cocylinder is simply the path space $X^{[0,1]}$. More generally, in a cartesian closed category with an interval object $I$, the cocylinder of an object $X$ is the exponential object $X^I$. Even more generally, in a model category the cocylinder of any object is the path space object — the factorization of the diagonal morphism $X\to X\times X$ as an acyclic cofibration followed by a fibration.
In any of these cases:
Given a morphism $f\colon X\to Y$, its mapping cocylinder (or mapping path space or mapping path fibration) is the pullback
where $Y^I$ is the cocylinder.
The mapping cocylinder is sometimes denoted $M_f Y$ or $N f$.
If we interchange $ev_0$ and $ev_1$ then we have an upside-down version of a cylinder, sometimes called inverse (or inverted) mapping cocylinder; but usually it is clear just from the context which version is used. They are homotopy equivalent, so usually it does not matter.
In homotopy type theory the mapping cocylinder $Cocyl(f) \to Y$ is expressed as
being the dependent sum over $x$ of the substitution of $f(x)$ for $y_1$ in the dependent identity type $(y_1 = y)$. Equivalently this is the $y$-dependent homotopy fiber of $f$ at $y$
In the case of topological spaces, the mapping cocylinder is the subspace $Cocyl(f)\subset Y^I\times X$ whose elements are pairs $(s,x)$ such that $s(0)=f(x)$.
In homotopy type theory, cocylinders represent identity types, and the mapping cocylinder represents the dependent type $y\colon Y \vdash hfiber(f,y)\colon Type$. This is used crucially in the definition of equivalence in homotopy type theory.
The mapping cocylinder is the central ingredient in the factorization lemma.
One usage is discussed at Hurewicz connection.
The mapping path fibration is used in the construction of the Strøm model structure on topological spaces.
The homotopy fiber can be constructed as the strict fiber of the mapping cocylinder.
examples of universal constructions of topological spaces:
$\phantom{AAAA}$limits | $\phantom{AAAA}$colimits |
---|---|
$\,$ point space$\,$ | $\,$ empty space $\,$ |
$\,$ product topological space $\,$ | $\,$ disjoint union topological space $\,$ |
$\,$ topological subspace $\,$ | $\,$ quotient topological space $\,$ |
$\,$ fiber space $\,$ | $\,$ space attachment $\,$ |
$\,$ mapping cocylinder, mapping cocone $\,$ | $\,$ mapping cylinder, mapping cone, mapping telescope $\,$ |
$\,$ cell complex, CW-complex $\,$ |
(This uses the terminology mapping path space.)