nLab
homotopy extension property

Contents

Definition

A (continuous) map i:AXi:A\to X of topological spaces is said to satisfy the homotopy extension property (HEP) with respect to a space YY if for any map f˜:XY\tilde{f}:X\to Y and a homotopy F:A×IYF:A\times I\to Y such that F(,0)=f˜iF(-,0)=\tilde{f}\circ i, a homotopy F˜:X×IY\tilde{F}:X\times I\to Y exists such that F˜(i×id I)=F\tilde{F}\circ (i\times id_I)=F.

If we write

f:=f˜i=F(,0); f:=\tilde{f}\circ i=F(-,0) \,;

then this is expressed by means of the commutative diagram

A i X f f˜ σ 0 Y σ 0 F F˜ A×I i×id X×I \array{ A & & \stackrel{i}\to && X \\ &\searrow^f && \swarrow^{\tilde{f}}& \\ {}^{\mathllap{\sigma_0}}\downarrow & &Y && \downarrow^{\mathrlap{\sigma_0}} \\ &\nearrow{F}&&\nwarrow{\exists\tilde{F}}& \\ A\times I &&\stackrel{i\times id}\to&&X\times I }

Here we denote σ 0:x(x,0)\sigma_0:x\mapsto (x,0), so that Fσ 0=F(,0)F\circ\sigma_0=F(-,0). The map f˜\tilde{f} is sometimes said to be the initial condition of a homotopy extension problem. F˜\tilde{F} is the extension of the homotopy FF with given initial condition which itself extends Fσ 0F\circ\sigma_0.

Of course it is superfluous to write the arrow f:AYf:A\to Y: if we erase it, the commutativity of the remaining square just surrounding its position is saying Fσ 0=f˜iF\circ\sigma_0=\tilde{f}\circ i; however it is conceptually nice to think of f˜\tilde{f} as extending some f:=Fσ 0f:=F\circ\sigma_0.

One can instead of the diagram above write a diagram involving adjoint maps. In other words, instead of any homotopy h:A×IYh:A\times I\to Y we use the exponential law to write h:AY Ih':A\to Y^I where the correspondence is given by the formula h(a)(t)=f(a,t)h'(a)(t)=f(a,t). Then the homotopy lifting property is the existence of the diagonal map F˜\tilde{F}' in the diagram:

A F Y I i F˜ ev 0 X f˜ Y. \array{ A &\stackrel{F'}\to& Y^I \\ \downarrow^{i} &{}^{\exists\tilde{F}'}\nearrow& \downarrow^{ev_0} \\ X&\stackrel{\tilde{f}}{\to}& Y } \,.

where ev 0:Y IYev_0:Y^I\to Y is the map of evaluation at zero uu(0)u\mapsto u(0). This is an instance of right lifting property with respect to maps ev 0ev_0.

A map is a Hurewicz cofibration if it satisfies the homotopy extension property with respect to all spaces.

Properties

Proposition

If a map i:AXi:A\to X has the homotopy extension property with respect to a space YY, then for any map g:AZg:A\to Z, the pushout g *(i)=i⨿ AZ:ZX⨿ AZg_*(i)=i\amalg_A Z :Z\to X\amalg_A Z has the homotopy extension property with respect to the space YY.

Proof

We would like to find F˜\tilde{F} to complete the commutative diagram

A g Z f Y I i g *(i) F˜ ev 0 X i *(g) X⨿ AZ F Y. \array{ A &\stackrel{g}\to&Z&\stackrel{f}\to& Y^I \\ \downarrow^{i}&&\downarrow^{g_*(i)} &\nearrow {\tilde{F}}& \downarrow^{ev_0} \\ X&\stackrel{i_*(g)}\to&X\amalg_A Z&\stackrel{F}{\to}& Y } \,.

Consider the external square obtained by composing the horizontal arrows:

A fg Y I i G˜ ev 0 X Fi *(g) Y. \array{ A &\stackrel{f\circ g}\to& Y^I \\ \downarrow^{i} &\nearrow {\exists\tilde{G}}& \downarrow^{ev_0} \\ X&\stackrel{F\circ i_*(g)}{\to}& Y } \,.

By the assumption on ii, there is a G˜\tilde{G} as in the diagram, such that both triangles commute, i.e. ev 0G˜=Fi *(g)ev_0\circ\tilde{G}=F\circ i_*(g) and G˜i=F˜g\tilde{G}\circ i = \tilde{F}\circ g.

If i:AXi:A\to X is satisfying the HEP with respect to YY then there is a diagonal in that external square which is some map G˜:XY I\tilde{G}:X\to Y^I. This map together with f:ZY If:Z\to Y^I, by the universal property of pushout, determines a unique map F˜:X⨿ AZY I\tilde{F}:X\amalg_A Z\to Y^I such that F˜i *(g)=G˜\tilde{F}\circ i_*(g)=\tilde{G} and F˜g *(i)=f\tilde{F}\circ g_*(i)=f. We need to show only that ev 0F˜=Fev_0\circ\tilde{F}=F as F˜g *(i)=f\tilde{F}\circ g_*(i)=f holds by the construction of F˜\tilde{F} as stated.

By the definition of G˜\tilde{G} and the commutativity of the original double square diagram, ev 0F˜i *(g)=ev 0G˜=Fi *(g)ev_0\circ \tilde{F}\circ i_*(g)=ev_0\circ\tilde{G}=F\circ i_*(g) and ev 0F˜g *(i)=ev 0f=Fg *(i)ev_0\circ \tilde{F}\circ g_*(i)=ev_0\circ f=F\circ g_*(i). This is almost what we wanted except that we precompose the wanted identity with both maps into the pushout. Thus by the uniqueness part of the universal property of pushout it follows that ev 0F˜=Fev_0\circ\tilde{F}=F.

Revised on November 9, 2011 13:21:44 by Urs Schreiber (131.174.41.104)