Fibres of mapping-path replacements

The mapping-path fibre over k retains the source point and a path ending at k. Flattening the two endpoint constraints identifies it homeomorphically with the literal fibre of the replacement's endpoint map. For a constant map from a point, this is exactly the native compact-open path space, and hence at equal endpoints the native loop space. In particular, this identification does not presume that an endpoint fibre is nonempty.

The fibre of the source projection over b is the space of paths from f b to k. It is empty exactly when f b and k lie in different path components (MappingPathFiber.isEmpty_projFiber_iff). A chosen reference path α from f b to k makes it homotopy equivalent to the loop space Ω K k (MappingPathFiber.projFiberHomotopyEquivLoopSpace): a path γ is sent to the loop α.symm.trans γ, and a loop ℓ back to the path α.trans ℓ. This equivalence depends on α; no identification independent of a reference path is asserted.

The full based path space is contractible by the shrinking homotopy, whereas its endpoint fibres generally are not. No fibration or homotopy exact-sequence theorem is asserted here.

References

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

@[reducible, inline]

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

The mapping-path fibre, with the subspace topology from B × C(I, K).

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

The source projection of the mapping-path fibre.

@[simp]

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

def TauCeti.MappingPathFiber.endpointHomeomorph {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) : MappingPathFiber f k ≃ₜ { p : MappingPathSpace f // (MappingPathSpace.endpoint f) p = k }

Flattening identifies the two-constraint path fibre with the literal endpoint fibre.

@[simp]

theorem TauCeti.MappingPathFiber.endpointHomeomorph_val {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) (p : MappingPathFiber f k) : ↑↑((endpointHomeomorph f k) p) = ↑p

@[simp]

theorem TauCeti.MappingPathFiber.endpointHomeomorph_symm_val {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) (p : { p : MappingPathSpace f // (MappingPathSpace.endpoint f) p = k }) : ↑((endpointHomeomorph f k).symm p) = ↑↑p

def TauCeti.MappingPathFiber.pullbackHomeomorph {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) : MappingPathFiber f k ≃ₜ { x : B × MappingPathFiber (ContinuousMap.id K) k // f x.1 = (proj (ContinuousMap.id K) k) x.2 }

MappingPathFiber f k is the base change along f of the fixed-end path fibration proj (ContinuousMap.id K) k.

@[simp]

theorem TauCeti.MappingPathFiber.pullbackHomeomorph_val_fst {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) (p : MappingPathFiber f k) : (↑((pullbackHomeomorph f k) p)).1 = (↑p).1

@[simp]

theorem TauCeti.MappingPathFiber.pullbackHomeomorph_val_snd_val {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) (p : MappingPathFiber f k) : ↑(↑((pullbackHomeomorph f k) p)).2 = (f (↑p).1, (↑p).2)

@[simp]

theorem TauCeti.MappingPathFiber.pullbackHomeomorph_symm_val {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) (x : { x : B × MappingPathFiber (ContinuousMap.id K) k // f x.1 = (proj (ContinuousMap.id K) k) x.2 }) : ↑((pullbackHomeomorph f k).symm x) = ((↑x).1, (↑(↑x).2).2)

theorem TauCeti.MappingPathFiber.proj_eq_comp_pullbackHomeomorph {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) : ⇑(proj f k) = (fun (x : { x : B × MappingPathFiber (ContinuousMap.id K) k // f x.1 = (proj (ContinuousMap.id K) k) x.2 }) => (↑x).1) ∘ ⇑(pullbackHomeomorph f k)

The base-change identification lies over B.

def TauCeti.MappingPathFiber.projFiberHomeomorphPath {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) (b : B) : { p : MappingPathFiber f k // (proj f k) p = b } ≃ₜ Path (f b) k

The fibre of the source projection over b is the native space of paths from f b to k.

@[simp]

theorem TauCeti.MappingPathFiber.projFiberHomeomorphPath_apply {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) (b : B) (p : { p : MappingPathFiber f k // (proj f k) p = b }) (t : ↑unitInterval) : ((projFiberHomeomorphPath f k b) p) t = (↑↑p).2 t

@[simp]

theorem TauCeti.MappingPathFiber.projFiberHomeomorphPath_symm_val_val {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) (b : B) (γ : Path (f b) k) : ↑↑((projFiberHomeomorphPath f k b).symm γ) = (b, γ.toContinuousMap)

theorem TauCeti.MappingPathFiber.nonempty_projFiber_iff {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) (b : B) : Nonempty { p : MappingPathFiber f k // (proj f k) p = b } ↔ Joined (f b) k

The fibre of the source projection over b is nonempty exactly when f b is joined to k by a path.

theorem TauCeti.MappingPathFiber.isEmpty_projFiber_iff {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) (b : B) : IsEmpty { p : MappingPathFiber f k // (proj f k) p = b } ↔ ¬Joined (f b) k

The fibre of the source projection over b is empty exactly when f b and k lie in different path components.

noncomputable def TauCeti.MappingPathFiber.projFiberHomotopyEquivLoopSpace {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) (b : B) (α : Path (f b) k) : ContinuousMap.HomotopyEquiv { p : MappingPathFiber f k // (proj f k) p = b } (LoopSpace K k)

A reference path α from f b to k makes the fibre of the source projection over b homotopy equivalent to the loop space Ω K k. A path γ from f b to k is sent to the loop α.symm.trans γ, and the homotopy inverse sends a loop ℓ to the path α.trans ℓ.

@[simp]

theorem TauCeti.MappingPathFiber.projFiberHomotopyEquivLoopSpace_apply {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) (b : B) (α : Path (f b) k) (p : { p : MappingPathFiber f k // (proj f k) p = b }) : (projFiberHomotopyEquivLoopSpace f k b α).toFun p = α.symm.trans ((projFiberHomeomorphPath f k b) p)

@[simp]

theorem TauCeti.MappingPathFiber.projFiberHomotopyEquivLoopSpace_symm_apply {B : Type u} {K : Type v} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (k : K) (b : B) (α : Path (f b) k) (ℓ : LoopSpace K k) : (projFiberHomotopyEquivLoopSpace f k b α).symm.toFun ℓ = (projFiberHomeomorphPath f k b).symm (α.trans ℓ)

def TauCeti.mappingPathFiberConstHomeomorphPath {K : Type v} [TopologicalSpace K] (b k : K) : MappingPathFiber (ContinuousMap.const Unit b) k ≃ₜ Path b k

Forget the redundant source point to identify a constant-map fibre with native paths.

@[simp]

theorem TauCeti.mappingPathFiberConstHomeomorphPath_apply {K : Type v} [TopologicalSpace K] (b k : K) (p : MappingPathFiber (ContinuousMap.const Unit b) k) (t : ↑unitInterval) : ((mappingPathFiberConstHomeomorphPath b k) p) t = (↑p).2 t

@[simp]

theorem TauCeti.mappingPathFiberConstHomeomorphPath_symm_val {K : Type v} [TopologicalSpace K] (b k : K) (γ : Path b k) : ↑((mappingPathFiberConstHomeomorphPath b k).symm γ) = ((), γ.toContinuousMap)

@[reducible, inline]

abbrev TauCeti.mappingPathFiberConstHomeomorphLoopSpace {K : Type v} [TopologicalSpace K] (k : K) : MappingPathFiber (ContinuousMap.const Unit k) k ≃ₜ LoopSpace K k

At equal endpoints the constant-map fibre is the native compact-open loop space.

@[simp]

theorem TauCeti.mappingPathFiberConstHomeomorphLoopSpace_refl {K : Type v} [TopologicalSpace K] (k : K) : (mappingPathFiberConstHomeomorphLoopSpace k) ⟨((), ContinuousMap.const (↑unitInterval) k), ⋯⟩ = Path.refl k

The constant path in the fibre corresponds to the constant native loop.

instance TauCeti.instContractibleSpaceMappingPathSpaceUnitConst {K : Type v} [TopologicalSpace K] (k : K) : ContractibleSpace (MappingPathSpace (ContinuousMap.const Unit k))

The based path space (without a fixed final endpoint) is contractible.