The homotopy fibre of the fibre inclusion of a Hurewicz fibration

Let p : E → B be a continuous map, e₀ : E a point and F = p⁻¹(p e₀) the fibre through it. The mapping-path fibre over e₀ of the inclusion F → E is the space TauCeti.FiberInclusionPathFiber p e₀ of paths in E that start in F and end at e₀. Each such path lies over a loop at p e₀, which gives the continuous map TauCeti.FiberInclusionPathFiber.loop p e₀ to the loop space Ω B (p e₀).

When p is a Hurewicz fibration this map is again a Hurewicz fibration, and it is a fibre homotopy equivalence over Ω B (p e₀), so the homotopy fibre of F → E is homotopy equivalent to Ω B (p e₀). This identifies Ω B as the homotopy fibre of F → E, the step extending the fibre sequence F → E → B of p to the left.

• The section TauCeti.FiberInclusionPathFiber.loopSection sends a loop β to the reverse of the lift of the reversed loop starting at e₀; it is a section on every loop component.
• The homotopy from the section after loop to the identity lifts, over the constant square (s, t) ↦ β t, the given path on one side, the section on the other and e₀ on the end (TauCeti.IsHurewiczFibration.exists_homotopy_lifts).

No connectedness or other hypothesis is put on E or B, and the equivalence is unbased: the lifts need not fix the constant path at e₀.

Main definitions

• TauCeti.FiberInclusionPathFiber p e₀: the homotopy fibre over e₀ of the inclusion of the fibre of p through e₀.
• TauCeti.FiberInclusionPathFiber.loop: the projection to the loop space Ω B (p e₀).
• TauCeti.FiberInclusionPathFiber.loopSection: a section of loop.
• TauCeti.FiberInclusionPathFiber.loopFiberHomotopyEquiv: loop as a fibre homotopy equivalence over Ω B (p e₀).
• TauCeti.FiberInclusionPathFiber.loopHomotopyEquiv: the homotopy equivalence with the loop space.

Main results

• TauCeti.FiberInclusionPathFiber.isHurewiczFibration_loop: loop is a Hurewicz fibration.
• TauCeti.FiberInclusionPathFiber.loopSection_comp_loop_homotopicWith: the section after loop is homotopic to the identity through maps over Ω B (p e₀).

References

• G. W. Whitehead, Elements of Homotopy Theory, GTM 61, Springer, 1978, Chapter I.7.
• A. Hatcher, Algebraic Topology, Section 4.3.
• J. P. May, A Concise Course in Algebraic Topology, Chapter 8.

@[reducible, inline]

abbrev TauCeti.FiberInclusionPathFiber {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) (e₀ : E) : Type u

The homotopy fibre over e₀ of the inclusion of the fibre p⁻¹(p e₀) into E: a point x of the fibre together with a path in E from x to e₀.

theorem TauCeti.FiberInclusionPathFiber.ext {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {e₀ : E} {x y : FiberInclusionPathFiber p e₀} (h : ∀ (t : ↑unitInterval), (↑x).2 t = (↑y).2 t) : x = y

A point of the homotopy fibre of a fibre inclusion is determined by its path.

theorem TauCeti.FiberInclusionPathFiber.ext_iff {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {e₀ : E} {x y : FiberInclusionPathFiber p e₀} : x = y ↔ ∀ (t : ↑unitInterval), (↑x).2 t = (↑y).2 t

theorem TauCeti.FiberInclusionPathFiber.apply_path_zero {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {e₀ : E} (x : FiberInclusionPathFiber p e₀) : p ((↑x).2 0) = p e₀

The path of a point of the homotopy fibre of the fibre inclusion starts in the fibre.

def TauCeti.FiberInclusionPathFiber.loop {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) (e₀ : E) : C(FiberInclusionPathFiber p e₀, LoopSpace B (p e₀))

The path of a point of the homotopy fibre of the fibre inclusion lies over a loop at p e₀: the projection from the homotopy fibre of the fibre inclusion to the loop space.

@[simp]

theorem TauCeti.FiberInclusionPathFiber.loop_apply {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) (e₀ : E) (x : FiberInclusionPathFiber p e₀) (t : ↑unitInterval) : ((loop p e₀) x) t = p ((↑x).2 t)

theorem TauCeti.FiberInclusionPathFiber.isHurewiczFibration_loop {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e₀ : E) (hp : IsHurewiczFibration ⇑p) : IsHurewiczFibration ⇑(loop p e₀)

The loop projection is a Hurewicz fibration. For a Hurewicz fibration p, the projection from the homotopy fibre of the inclusion of the fibre through e₀ to the loop space Ω B (p e₀) is a Hurewicz fibration.

noncomputable def TauCeti.FiberInclusionPathFiber.loopSection {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e₀ : E) (hp : IsHurewiczFibration ⇑p) : C(LoopSpace B (p e₀), FiberInclusionPathFiber p e₀)

A section of the loop projection: a loop β at p e₀ is sent to the reverse of the lift of the reversed loop t ↦ β (1 - t) from e₀, a path from the fibre to e₀ over β. The section is defined on every loop component.

@[simp]

theorem TauCeti.FiberInclusionPathFiber.loop_loopSection {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e₀ : E) (hp : IsHurewiczFibration ⇑p) (β : LoopSpace B (p e₀)) : (loop p e₀) ((loopSection e₀ hp) β) = β

The section of the loop projection lies over the given loop.

@[simp]

theorem TauCeti.FiberInclusionPathFiber.loop_comp_loopSection {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e₀ : E) (hp : IsHurewiczFibration ⇑p) : (loop p e₀).comp (loopSection e₀ hp) = ContinuousMap.id (LoopSpace B (p e₀))

The section of the loop projection is a right inverse of the loop projection.

theorem TauCeti.FiberInclusionPathFiber.loopSection_comp_loop_homotopicWith {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e₀ : E) (hp : IsHurewiczFibration ⇑p) (hp' : IsHurewiczFibration ⇑p) : ((loopSection e₀ hp).comp (loop p e₀)).HomotopicWith (ContinuousMap.id (FiberInclusionPathFiber p e₀)) fun (f : C(FiberInclusionPathFiber p e₀, FiberInclusionPathFiber p e₀)) => (loop p e₀).comp f = loop p e₀

The section of the loop projection is a fibrewise homotopy inverse. The composite of the loop projection and its section is homotopic to the identity through maps over Ω B (p e₀).

noncomputable def TauCeti.FiberInclusionPathFiber.loopFiberHomotopyEquiv {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e₀ : E) (hp : IsHurewiczFibration ⇑p) : FiberHomotopyEquiv (loop p e₀) (ContinuousMap.id (LoopSpace B (p e₀)))

The loop projection is a fibre homotopy equivalence. For a Hurewicz fibration p, the projection from the homotopy fibre of the inclusion of the fibre through e₀ to the loop space Ω B (p e₀) is a fibre homotopy equivalence over Ω B (p e₀) with its identity map.

@[simp]

theorem TauCeti.FiberInclusionPathFiber.loopFiberHomotopyEquiv_toFun {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e₀ : E) (hp : IsHurewiczFibration ⇑p) : (loopFiberHomotopyEquiv e₀ hp).toFun = loop p e₀

@[simp]

theorem TauCeti.FiberInclusionPathFiber.loopFiberHomotopyEquiv_invFun {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e₀ : E) (hp : IsHurewiczFibration ⇑p) : (loopFiberHomotopyEquiv e₀ hp).invFun = loopSection e₀ ⋯

noncomputable def TauCeti.FiberInclusionPathFiber.loopHomotopyEquiv {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e₀ : E) (hp : IsHurewiczFibration ⇑p) : ContinuousMap.HomotopyEquiv (FiberInclusionPathFiber p e₀) (LoopSpace B (p e₀))

The homotopy fibre of the fibre inclusion is the loop space of the base. For a Hurewicz fibration p, the space of paths in E from the fibre through e₀ to e₀ is homotopy equivalent to the loop space Ω B (p e₀), by composing the paths with p.

@[simp]

theorem TauCeti.FiberInclusionPathFiber.loopHomotopyEquiv_apply {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e₀ : E) (hp : IsHurewiczFibration ⇑p) (x : FiberInclusionPathFiber p e₀) : (loopHomotopyEquiv e₀ hp).toFun x = (loop p e₀) x

@[simp]

theorem TauCeti.FiberInclusionPathFiber.loopHomotopyEquiv_symm_apply {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e₀ : E) (hp : IsHurewiczFibration ⇑p) (β : LoopSpace B (p e₀)) : (loopHomotopyEquiv e₀ hp).symm.toFun β = (loopSection e₀ ⋯) β