Fibre homotopy equivalences

For maps p : E → B and q : E' → B, a fibre homotopy equivalence from p to q is a pair of maps f : E → E' and g : E' → E over B (q ∘ f = p, p ∘ g = q) whose two composites are homotopic to the identities through maps over B (ContinuousMap.HomotopicWith with the predicate "over B"). Since every stage of such a homotopy maps each fibre into itself, a fibre homotopy equivalence restricts to a homotopy equivalence of the fibres over each point (TauCeti.FiberHomotopyEquiv.fiber).

Main definitions

• TauCeti.FiberHomotopyEquiv p q: fibre homotopy equivalences from p to q.
• TauCeti.fiberMap: the map of fibres induced by a map over B.
• TauCeti.FiberHomotopyEquiv.refl, TauCeti.FiberHomotopyEquiv.symm, TauCeti.FiberHomotopyEquiv.trans: identity, symmetry, and composition of fibre homotopy equivalences.
• TauCeti.FiberHomotopyEquiv.ofHomeomorph: a homeomorphism over B as a fibre homotopy equivalence.
• TauCeti.FiberHomotopyEquiv.compBase: postcomposing the base projections with b : C(B, B').
• TauCeti.FiberHomotopyEquiv.fiber: the homotopy equivalence of the fibres over a point.
• TauCeti.FiberHomotopyEquiv.toHomotopyEquiv: the underlying homotopy equivalence of the total spaces.

Main results

• ContinuousMap.homotopic_of_fiber: a homotopy of maps to the total space staying over one point is a homotopy of maps into the fiber.

structure TauCeti.FiberHomotopyEquiv {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] (p : C(E, B)) (q : C(E', B)) : Type (max u u')

A fibre homotopy equivalence from p : E → B to q : E' → B: maps over B in both directions whose composites are homotopic to the identities through maps over B.

• toFun : C(E, E')

  The forward map, over B.

• invFun : C(E', E)

  The backward map, over B.

• comp_toFun : q.comp self.toFun = p

  The forward map lies over B.

• comp_invFun : p.comp self.invFun = q

  The backward map lies over B.

• left_inv : (self.invFun.comp self.toFun).HomotopicWith (ContinuousMap.id E) fun (f : C(E, E)) => p.comp f = p

  The composite on E is homotopic to the identity through maps over B.

• right_inv : (self.toFun.comp self.invFun).HomotopicWith (ContinuousMap.id E') fun (f : C(E', E')) => q.comp f = q

  The composite on E' is homotopic to the identity through maps over B.

theorem TauCeti.apply_of_comp_eq {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} {f : C(E, E')} (hf : q.comp f = p) {b : B} (e : { e : E // p e = b }) : q (f ↑e) = b

def TauCeti.fiberMap {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} (f : C(E, E')) (hf : q.comp f = p) (b : B) : C({ e : E // p e = b }, { e' : E' // q e' = b })

The map of fibres over b induced by a map f over B.

@[simp]

theorem TauCeti.coe_fiberMap {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} (f : C(E, E')) (hf : q.comp f = p) (b : B) (e : { e : E // p e = b }) : ↑((fiberMap f hf b) e) = f ↑e

theorem TauCeti.fiberMap_comp {E : Type u} {E' : Type u'} {E'' : Type u''} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace E''] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} {r : C(E'', B)} (f : C(E, E')) (g : C(E', E'')) (hf : q.comp f = p) (hg : r.comp g = q) (b : B) : (fiberMap g hg b).comp (fiberMap f hf b) = fiberMap (g.comp f) ⋯ b

theorem TauCeti.fiberMap_id {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (b : B) : fiberMap (ContinuousMap.id E) ⋯ b = ContinuousMap.id { e : E // p e = b }

theorem TauCeti.apply_homotopyWith {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {f₀ f₁ : C(E, E)} (H : f₀.HomotopyWith f₁ fun (f : C(E, E)) => p.comp f = p) (t : ↑unitInterval) (e : E) : p (H (t, e)) = p e

def TauCeti.fiberHomotopy {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {f₀ f₁ : C(E, E)} (H : f₀.HomotopyWith f₁ fun (f : C(E, E)) => p.comp f = p) (h₀ : p.comp f₀ = p) (h₁ : p.comp f₁ = p) (b : B) : (fiberMap f₀ h₀ b).Homotopy (fiberMap f₁ h₁ b)

A homotopy through maps over B restricts to a homotopy of the induced maps of the fibres.

def TauCeti.FiberHomotopyEquiv.fiber {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} (Φ : FiberHomotopyEquiv p q) (b : B) : ContinuousMap.HomotopyEquiv { e : E // p e = b } { e' : E' // q e' = b }

A fibre homotopy equivalence restricts to a homotopy equivalence of the fibres over each point of the base.

@[simp]

theorem TauCeti.FiberHomotopyEquiv.coe_fiber_apply {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} (Φ : FiberHomotopyEquiv p q) (b : B) (e : { e : E // p e = b }) : ↑((Φ.fiber b).toFun e) = Φ.toFun ↑e

@[simp]

theorem TauCeti.FiberHomotopyEquiv.coe_fiber_symm_apply {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} (Φ : FiberHomotopyEquiv p q) (b : B) (e' : { e' : E' // q e' = b }) : ↑((Φ.fiber b).symm.toFun e') = Φ.invFun ↑e'

def TauCeti.FiberHomotopyEquiv.toHomotopyEquiv {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} (Φ : FiberHomotopyEquiv p q) : ContinuousMap.HomotopyEquiv E E'

Forgetting that the maps and homotopies lie over B, a fibre homotopy equivalence is a homotopy equivalence of the total spaces.

@[simp]

theorem TauCeti.FiberHomotopyEquiv.toHomotopyEquiv_apply {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} (Φ : FiberHomotopyEquiv p q) (e : E) : Φ.toHomotopyEquiv.toFun e = Φ.toFun e

@[simp]

theorem TauCeti.FiberHomotopyEquiv.toHomotopyEquiv_symm_apply {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} (Φ : FiberHomotopyEquiv p q) (e' : E') : Φ.toHomotopyEquiv.symm.toFun e' = Φ.invFun e'

def TauCeti.FiberHomotopyEquiv.refl {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : FiberHomotopyEquiv p p

The identity fibre homotopy equivalence of p : C(E, B).

@[simp]

theorem TauCeti.FiberHomotopyEquiv.refl_toFun {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : (refl p).toFun = ContinuousMap.id E

@[simp]

theorem TauCeti.FiberHomotopyEquiv.refl_invFun {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : (refl p).invFun = ContinuousMap.id E

def TauCeti.FiberHomotopyEquiv.symm {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} (Φ : FiberHomotopyEquiv p q) : FiberHomotopyEquiv q p

Symmetry of fibre homotopy equivalences.

@[simp]

theorem TauCeti.FiberHomotopyEquiv.symm_toFun {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} (Φ : FiberHomotopyEquiv p q) : Φ.symm.toFun = Φ.invFun

@[simp]

theorem TauCeti.FiberHomotopyEquiv.symm_invFun {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} (Φ : FiberHomotopyEquiv p q) : Φ.symm.invFun = Φ.toFun

@[simp]

theorem TauCeti.FiberHomotopyEquiv.symm_symm {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} (Φ : FiberHomotopyEquiv p q) : Φ.symm.symm = Φ

def TauCeti.FiberHomotopyEquiv.ofHomeomorph {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} (e : E ≃ₜ E') (he : q.comp ↑e = p) : FiberHomotopyEquiv p q

A homeomorphism e : E ≃ₜ E' commuting with the projections to B is a fibre homotopy equivalence.

@[simp]

theorem TauCeti.FiberHomotopyEquiv.ofHomeomorph_toFun {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} (e : E ≃ₜ E') (he : q.comp ↑e = p) : (ofHomeomorph e he).toFun = ↑e

@[simp]

theorem TauCeti.FiberHomotopyEquiv.ofHomeomorph_invFun {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} (e : E ≃ₜ E') (he : q.comp ↑e = p) : (ofHomeomorph e he).invFun = ↑e.symm

def TauCeti.FiberHomotopyEquiv.trans {E : Type u} {E' : Type u'} {E'' : Type u''} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace E''] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} {r : C(E'', B)} (Φ : FiberHomotopyEquiv p q) (Ψ : FiberHomotopyEquiv q r) : FiberHomotopyEquiv p r

Composition of fibre homotopy equivalences over B.

@[simp]

theorem TauCeti.FiberHomotopyEquiv.trans_toFun {E : Type u} {E' : Type u'} {E'' : Type u''} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace E''] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} {r : C(E'', B)} (Φ : FiberHomotopyEquiv p q) (Ψ : FiberHomotopyEquiv q r) : (Φ.trans Ψ).toFun = Ψ.toFun.comp Φ.toFun

@[simp]

theorem TauCeti.FiberHomotopyEquiv.trans_invFun {E : Type u} {E' : Type u'} {E'' : Type u''} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace E''] [TopologicalSpace B] {p : C(E, B)} {q : C(E', B)} {r : C(E'', B)} (Φ : FiberHomotopyEquiv p q) (Ψ : FiberHomotopyEquiv q r) : (Φ.trans Ψ).invFun = Φ.invFun.comp Ψ.invFun

def TauCeti.FiberHomotopyEquiv.compBase {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {B' : Type u_1} [TopologicalSpace B'] {p : C(E, B)} {q : C(E', B)} (b : C(B, B')) (Φ : FiberHomotopyEquiv p q) : FiberHomotopyEquiv (b.comp p) (b.comp q)

Postcomposing both base projections with b : C(B, B') carries a fibre homotopy equivalence over B to one over B'.

@[simp]

theorem TauCeti.FiberHomotopyEquiv.compBase_toFun {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {B' : Type u_1} [TopologicalSpace B'] {p : C(E, B)} {q : C(E', B)} (b : C(B, B')) (Φ : FiberHomotopyEquiv p q) : (compBase b Φ).toFun = Φ.toFun

@[simp]

theorem TauCeti.FiberHomotopyEquiv.compBase_invFun {E : Type u} {E' : Type u'} {B : Type v} [TopologicalSpace E] [TopologicalSpace E'] [TopologicalSpace B] {B' : Type u_1} [TopologicalSpace B'] {p : C(E, B)} {q : C(E', B)} (b : C(B, B')) (Φ : FiberHomotopyEquiv p q) : (compBase b Φ).invFun = Φ.invFun

theorem ContinuousMap.homotopic_of_fiber {E : Type u_1} {B : Type u_2} {Y : Type u_3} [TopologicalSpace E] [TopologicalSpace Y] {p : E → B} {b : B} (f g : C(Y, ↑(p ⁻¹' {b}))) (K : C(Y × ↑unitInterval, E)) (h₀ : ∀ (y : Y), K (y, 0) = ↑(f y)) (h₁ : ∀ (y : Y), K (y, 1) = ↑(g y)) (hK : ∀ (y : Y) (s : ↑unitInterval), p (K (y, s)) = b) : f.Homotopic g

A homotopy of maps to the total space of a map p, staying over a fixed point b, gives a homotopy of maps into the fiber over b.