Mapping-path replacements

The mapping-path space of f : C(B, K) consists of a point of B and a path starting at its image. It has the subspace topology from B × C(I, K), with the compact-open topology on paths. Constant paths include B into this replacement; shrinking the path by γ(t) ↦ γ(s * t) gives a strong deformation back to that inclusion.

Commutative squares act on replacements, compatibly with the source projection, endpoint and shrinking homotopy. These constructions require no separation or local compactness assumptions on B or K: only the interval is used as an exponentiable domain. The endpoint-fibre comparisons are developed separately.

References

• G. W. Whitehead, Elements of Homotopy Theory, Chapter I.7.

@[reducible, inline]

abbrev TauCeti.MappingPathSpace {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) : Type (max 0 u v)

The mapping-path replacement, with its product/subspace compact-open topology.

def TauCeti.MappingPathSpace.proj {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) : C(MappingPathSpace f, B)

Forget the path in a mapping-path replacement.

@[simp]

theorem TauCeti.MappingPathSpace.proj_apply {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (p : MappingPathSpace f) : (proj f) p = (↑p).1

def TauCeti.MappingPathSpace.endpoint {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) : C(MappingPathSpace f, K)

Evaluate a replacement path at its final endpoint.

@[simp]

theorem TauCeti.MappingPathSpace.endpoint_apply {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (p : MappingPathSpace f) : (endpoint f) p = (↑p).2 1

def TauCeti.MappingPathSpace.incl {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) : C(B, MappingPathSpace f)

Include the source using constant paths.

@[simp]

theorem TauCeti.MappingPathSpace.incl_val {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (b : B) : ↑((incl f) b) = (b, ContinuousMap.const (↑unitInterval) (f b))

@[simp]

theorem TauCeti.MappingPathSpace.proj_comp_incl {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) : (proj f).comp (incl f) = ContinuousMap.id B

@[simp]

theorem TauCeti.MappingPathSpace.endpoint_comp_incl {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) : (endpoint f).comp (incl f) = f

def TauCeti.MappingPathSpace.shrinkHomotopy {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) : ((incl f).comp (proj f)).Homotopy (ContinuousMap.id (MappingPathSpace f))

Shrink a path toward its starting point, keeping the source coordinate fixed.

@[simp]

theorem TauCeti.MappingPathSpace.shrinkHomotopy_point {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (s : ↑unitInterval) (p : MappingPathSpace f) : (↑((shrinkHomotopy f) (s, p))).1 = (↑p).1

@[simp]

theorem TauCeti.MappingPathSpace.shrinkHomotopy_path {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (s t : ↑unitInterval) (p : MappingPathSpace f) : (↑((shrinkHomotopy f) (s, p))).2 t = (↑p).2 (s * t)

@[simp]

theorem TauCeti.MappingPathSpace.shrinkHomotopy_incl {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (s : ↑unitInterval) (b : B) : (shrinkHomotopy f) (s, (incl f) b) = (incl f) b

The shrinking homotopy fixes every constant-path inclusion throughout.

def TauCeti.MappingPathSpace.homotopyEquiv {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) : ContinuousMap.HomotopyEquiv B (MappingPathSpace f)

The constant-path inclusion is a homotopy equivalence, inverse to projection.

@[simp]

theorem TauCeti.MappingPathSpace.homotopyEquiv_apply {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (b : B) : (homotopyEquiv f).toFun b = (incl f) b

@[simp]

theorem TauCeti.MappingPathSpace.homotopyEquiv_symm_apply {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (p : MappingPathSpace f) : (homotopyEquiv f).symm.toFun p = (proj f) p

def TauCeti.MappingPathSpace.map {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] {f : C(B, K)} {B' : Type u'} {K' : Type v'} [TopologicalSpace B'] [TopologicalSpace K'] {f' : C(B', K')} (a : C(B, B')) (b : C(K, K')) (h : b.comp f = f'.comp a) : C(MappingPathSpace f, MappingPathSpace f')

A commutative square sends a replacement point to its image and postcomposes its path.

@[simp]

theorem TauCeti.MappingPathSpace.map_val {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] {f : C(B, K)} {B' : Type u'} {K' : Type v'} [TopologicalSpace B'] [TopologicalSpace K'] {f' : C(B', K')} (a : C(B, B')) (b : C(K, K')) (h : b.comp f = f'.comp a) (p : MappingPathSpace f) : ↑((map a b h) p) = (a (↑p).1, b.comp (↑p).2)

@[simp]

theorem TauCeti.MappingPathSpace.proj_comp_map {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] {f : C(B, K)} {B' : Type u'} {K' : Type v'} [TopologicalSpace B'] [TopologicalSpace K'] {f' : C(B', K')} (a : C(B, B')) (b : C(K, K')) (h : b.comp f = f'.comp a) : (proj f').comp (map a b h) = a.comp (proj f)

Projection is natural in a commutative square.

@[simp]

theorem TauCeti.MappingPathSpace.endpoint_comp_map {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] {f : C(B, K)} {B' : Type u'} {K' : Type v'} [TopologicalSpace B'] [TopologicalSpace K'] {f' : C(B', K')} (a : C(B, B')) (b : C(K, K')) (h : b.comp f = f'.comp a) : (endpoint f').comp (map a b h) = b.comp (endpoint f)

Endpoint evaluation is natural in a commutative square.

@[simp]

theorem TauCeti.MappingPathSpace.map_comp_incl {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] {f : C(B, K)} {B' : Type u'} {K' : Type v'} [TopologicalSpace B'] [TopologicalSpace K'] {f' : C(B', K')} (a : C(B, B')) (b : C(K, K')) (h : b.comp f = f'.comp a) : (map a b h).comp (incl f) = (incl f').comp a

The constant-path inclusion is natural in a commutative square.

@[simp]

theorem TauCeti.MappingPathSpace.map_id {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] {f : C(B, K)} : map (ContinuousMap.id B) (ContinuousMap.id K) ⋯ = ContinuousMap.id (MappingPathSpace f)

theorem TauCeti.MappingPathSpace.map_comp {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] {f : C(B, K)} {B' : Type u'} {K' : Type v'} [TopologicalSpace B'] [TopologicalSpace K'] {f' : C(B', K')} {B'' : Type u''} {K'' : Type v''} [TopologicalSpace B''] [TopologicalSpace K''] {f'' : C(B'', K'')} (a : C(B, B')) (b : C(K, K')) (h : b.comp f = f'.comp a) (a' : C(B', B'')) (b' : C(K', K'')) (h' : b'.comp f' = f''.comp a') : (map a' b' h').comp (map a b h) = map (a'.comp a) (b'.comp b) ⋯

Mapping-path replacements preserve composition of commutative squares.

@[simp]

theorem TauCeti.MappingPathSpace.map_shrinkHomotopy {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] {f : C(B, K)} {B' : Type u'} {K' : Type v'} [TopologicalSpace B'] [TopologicalSpace K'] {f' : C(B', K')} (a : C(B, B')) (b : C(K, K')) (h : b.comp f = f'.comp a) (s : ↑unitInterval) (p : MappingPathSpace f) : (map a b h) ((shrinkHomotopy f) (s, p)) = (shrinkHomotopy f') (s, (map a b h) p)

Shrinking commutes with the map induced by a commutative square.