Serre fibrations

A map p : E → B has the homotopy lifting property with respect to a space A when every homotopy H : I × A → B whose initial map lifts along p to f : A → E lifts along p to a homotopy G : I × A → E starting at f. A Serre fibration is a map with the homotopy lifting property with respect to every disk Dⁿ. Equivalently, it has the right lifting property with respect to the inclusions ι₀ : Dⁿ ⟶ Dⁿ ⊗ I of the disks as the bottoms of their cylinders, and this is how TauCeti.TopCat.serreFibrations is defined, as a MorphismProperty of TopCat. Defining it as a right lifting property makes Mathlib's general theory of lifting properties apply: Serre fibrations contain the isomorphisms, are closed under composition, retracts and products, and are stable under base change.

The homotopy lifting property itself, TauCeti.HasHomotopyLiftingProperty, is in TauCeti.Topology.Homotopy.Lifting.Basic. Since the closed unit ball of ℝⁿ is homeomorphic to the cube Iⁿ, a Serre fibration is equivalently a map with the homotopy lifting property with respect to every cube (TauCeti.TopCat.mem_serreFibrations_iff_cube); cubes are the convenient test spaces for subdivision arguments.

A map of fibrations is a commutative square, and it induces maps between the fibres (CategoryTheory.CommSq.fiberMap, in TauCeti.Topology.Category.TopCat.Fiber). The base change of a fibration along a map g : B' ⟶ B is again a fibration (TauCeti.TopCat.mem_serreFibrations_pullbackFst), with the same fibres (TopCat.Hom.fiberPullbackFstIso, in TauCeti.Topology.Category.TopCat.Pullback).

Main declarations

• TauCeti.TopCat.serreFibrations: Serre fibrations, the right lifting property with respect to the inclusions ι₀ : Dⁿ ⟶ Dⁿ ⊗ I.
• TauCeti.TopCat.exists_path_lift_of_mem_serreFibrations: a Serre fibration lifts paths. In particular a point joined in the base to a point with path-connected fibre is joined to it in the total space (TauCeti.TopCat.joined_of_mem_serreFibrations), and a point of the base joined to the image has a nonempty fibre (TauCeti.TopCat.nonempty_fiber_of_mem_serreFibrations).
• TauCeti.TopCat.mem_serreFibrations_iff and TauCeti.TopCat.mem_serreFibrations_iff_cube: Serre fibrations are the maps with the homotopy lifting property for every disk, equivalently for every cube.
• IsCoveringMap.mem_serreFibrations and TauCeti.TopCat.mem_serreFibrations_fst: covering maps and product projections are Serre fibrations.
• TauCeti.TopCat.mem_serreFibrations_pullbackFst: the base change of a Serre fibration is a Serre fibration.
• TauCeti.TopCat.mem_serreFibrations_restrictPreimage: the restriction of a Serre fibration over a subset of the base is a Serre fibration.

References

• A. Hatcher, Algebraic Topology, Section 4.2, the homotopy lifting property and the definition of a fibration.
• J.-P. Serre, Homologie singulière des espaces fibrés. Applications, Ann. of Math. 54 (1951).
• The definition of TauCeti.TopCat.serreFibrations as the right lifting property with respect to a family of morphisms follows Mathlib's SSet.innerFibrations.

theorem TauCeti.TopCat.hasLiftingProperty_ι₀_iff {A E B : TopCat} {p : E ⟶ B} : CategoryTheory.HasLiftingProperty TopCat.ι₀ p ↔ HasHomotopyLiftingProperty ⇑(CategoryTheory.ConcreteCategory.hom p) ↑A

A morphism p of TopCat has the right lifting property with respect to the inclusion ι₀ : A ⟶ A ⊗ I of A as the bottom of its cylinder exactly when it has the homotopy lifting property with respect to A.

def TauCeti.TopCat.serreFibrations : CategoryTheory.MorphismProperty TopCat

Serre fibrations: the morphisms of TopCat with the right lifting property with respect to the inclusions ι₀ : Dⁿ ⟶ Dⁿ ⊗ I of the disks as the bottoms of their cylinders, that is, with the homotopy lifting property with respect to every disk.

instance TauCeti.TopCat.instIsMultiplicativeTopCatSerreFibrations : serreFibrations.IsMultiplicative

instance TauCeti.TopCat.instRespectsIsoTopCatSerreFibrations : serreFibrations.RespectsIso

instance TauCeti.TopCat.instIsStableUnderBaseChangeTopCatSerreFibrations : serreFibrations.IsStableUnderBaseChange

instance TauCeti.TopCat.instIsStableUnderRetractsTopCatSerreFibrations : serreFibrations.IsStableUnderRetracts

instance TauCeti.TopCat.instIsStableUnderProductsOfShapeTopCatSerreFibrations (J : Type u_1) : serreFibrations.IsStableUnderProductsOfShape J

theorem TauCeti.TopCat.mem_serreFibrations_iff_hasLiftingProperty {E B : TopCat} {p : E ⟶ B} : serreFibrations p ↔ ∀ (n : ℕ), CategoryTheory.HasLiftingProperty TopCat.ι₀ p

A morphism is a Serre fibration exactly when it has the right lifting property with respect to every inclusion ι₀ : Dⁿ ⟶ Dⁿ ⊗ I.

theorem TauCeti.TopCat.mem_serreFibrations_iff {E B : TopCat} {p : E ⟶ B} : serreFibrations p ↔ ∀ (n : ℕ), HasHomotopyLiftingProperty ⇑(CategoryTheory.ConcreteCategory.hom p) ↑(Metric.closedBall 0 1)

A morphism is a Serre fibration exactly when it has the homotopy lifting property with respect to the closed unit ball of ℝⁿ for every n.

theorem TauCeti.TopCat.mem_serreFibrations_iff_cube {E B : TopCat} {p : E ⟶ B} : serreFibrations p ↔ ∀ (n : ℕ), HasHomotopyLiftingProperty (⇑(CategoryTheory.ConcreteCategory.hom p)) (Fin n → ↑unitInterval)

A morphism is a Serre fibration exactly when it has the homotopy lifting property with respect to the cube Iⁿ for every n.

theorem TauCeti.TopCat.mem_serreFibrations_of_hasHomotopyLiftingProperty {E B : TopCat} {p : E ⟶ B} (h : ∀ (A : Type u) [inst : TopologicalSpace A], HasHomotopyLiftingProperty (⇑(CategoryTheory.ConcreteCategory.hom p)) A) : serreFibrations p

A morphism with the homotopy lifting property with respect to every space in its universe is a Serre fibration.

theorem TauCeti.TopCat.exists_path_lift_of_mem_serreFibrations {E B : TopCat} {p : E ⟶ B} (hp : serreFibrations p) {e : ↑E} {b : ↑B} (γ : Path ((CategoryTheory.ConcreteCategory.hom p) e) b) : ∃ (Γ : C(↑unitInterval, ↑E)), Γ 0 = e ∧ ⇑(CategoryTheory.ConcreteCategory.hom p) ∘ ⇑Γ = ⇑γ

A Serre fibration lifts paths: a path in B starting at p e lifts to a path in E starting at e.

theorem TauCeti.TopCat.joined_of_mem_serreFibrations {E B : TopCat} {p : E ⟶ B} (hp : serreFibrations p) {x y : ↑E} [PathConnectedSpace ↑(TopCat.Hom.fiber p ((CategoryTheory.ConcreteCategory.hom p) y))] (h : Joined ((CategoryTheory.ConcreteCategory.hom p) x) ((CategoryTheory.ConcreteCategory.hom p) y)) : Joined x y

Path lifting into a path-connected fibre. If the fibre of a Serre fibration p over p y is path-connected, then a point x whose projection is joined to p y is joined to y.

theorem TauCeti.TopCat.nonempty_fiber_of_mem_serreFibrations {E B : TopCat} {p : E ⟶ B} (hp : serreFibrations p) {x : ↑E} {b : ↑B} (h : Joined ((CategoryTheory.ConcreteCategory.hom p) x) b) : Nonempty ↑(TopCat.Hom.fiber p b)

Lifting the end point of a path. If a point b of the base of a Serre fibration p is joined to a point of the image of p, then the fibre of p over b is nonempty.

theorem TauCeti.TopCat.mem_serreFibrations_restrictPreimage {E B : TopCat} {p : E ⟶ B} (hp : serreFibrations p) (t : Set ↑B) : serreFibrations (TopCat.ofHom ((TopCat.Hom.hom p).restrictPreimage t))

The restriction p⁻¹(t) → t of a Serre fibration p over any subset t of the base is a Serre fibration.

theorem TauCeti.TopCat.mem_serreFibrations_fst {B F : TopCat} : serreFibrations (CategoryTheory.SemiCartesianMonoidalCategory.fst B F)

The projection B ⊗ F ⟶ B is a Serre fibration.

theorem TauCeti.TopCat.mem_serreFibrations_pullbackFst {E B B' : TopCat} {p : E ⟶ B} (hp : serreFibrations p) (g : B' ⟶ B) : serreFibrations (TopCat.pullbackFst g p)

The base change {(b', e) | g b' = p e} ⟶ B' of a Serre fibration p along any map g : B' ⟶ B is a Serre fibration.

theorem IsCoveringMap.mem_serreFibrations {E B : TopCat} {p : E ⟶ B} (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) : TauCeti.TopCat.serreFibrations p

A covering map is a Serre fibration.