Documentation

TauCeti.Topology.Homotopy.HurewiczFibration.Basic

Hurewicz fibrations #

A map p : E → B is a Hurewicz fibration when it is continuous and has the homotopy lifting property (TauCeti.HasHomotopyLiftingProperty) with respect to every space. A proposition cannot quantify over the spaces of all universes, so TauCeti.IsHurewiczFibration.{w} p asks for the homotopy lifting property with respect to every space in the universe w; the property for a universe implies it for every smaller one (TauCeti.IsHurewiczFibration.down), since the homotopy lifting property depends on the space only up to homeomorphism.

Every Hurewicz fibration is a Serre fibration (TauCeti.IsHurewiczFibration.mem_serreFibrations), since the cubes are test spaces. Homeomorphisms, product projections and maps to a subsingleton are Hurewicz fibrations, and Hurewicz fibrations are closed under composition, products and base change.

Main definitions #

Main results #

References #

source
def TauCeti.IsHurewiczFibration {E : Type u₀} {B : Type v₀} [TopologicalSpace E] [TopologicalSpace B] (p : E → B) :
Prop

A map p : E → B is a Hurewicz fibration, for test spaces in the universe w, when it is continuous and has the homotopy lifting property with respect to every space in Type w.

Instances For
    source
    theorem TauCeti.isHurewiczFibration_iff {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} :
    IsHurewiczFibration p ↔ Continuous p ∧ ∀ (A : Type w) [inst : TopologicalSpace A], HasHomotopyLiftingProperty p A

    A map is a Hurewicz fibration, for test spaces in the universe w, if and only if it is continuous and has the homotopy lifting property with respect to every space in Type w.

    source
    theorem Homeomorph.isHurewiczFibration {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (e : E ≃ₜ B) :
    TauCeti.IsHurewiczFibration ⇑e

    A homeomorphism is a Hurewicz fibration.

    source
    theorem TauCeti.IsHurewiczFibration.continuous {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (h : IsHurewiczFibration p) :
    Continuous p

    A Hurewicz fibration is continuous.

    source
    theorem TauCeti.IsHurewiczFibration.hasHomotopyLiftingProperty {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (h : IsHurewiczFibration p) (A : Type w) [TopologicalSpace A] :
    HasHomotopyLiftingProperty p A

    A Hurewicz fibration has the homotopy lifting property with respect to each test space.

    source
    theorem TauCeti.IsHurewiczFibration.down {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (h : IsHurewiczFibration p) :
    IsHurewiczFibration p

    A Hurewicz fibration for test spaces in a universe is one for every smaller universe.

    source
    theorem TauCeti.IsHurewiczFibration.mem_serreFibrations {E B : TopCat} {p : E ⟶ B} (h : IsHurewiczFibration ⇑(CategoryTheory.ConcreteCategory.hom p)) :
    TopCat.serreFibrations p

    A Hurewicz fibration is a Serre fibration: the cubes Iⁿ are among the test spaces.

    source
    theorem TauCeti.IsHurewiczFibration.comp {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {C : Type v'} [TopologicalSpace C] {q : B → C} (hq : IsHurewiczFibration q) (hp : IsHurewiczFibration p) :
    IsHurewiczFibration (q ∘ p)

    Hurewicz fibrations are closed under composition.

    source
    theorem TauCeti.IsHurewiczFibration.prodMap {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {E' : Type u'} {B' : Type v'} [TopologicalSpace E'] [TopologicalSpace B'] {q : E' → B'} (hp : IsHurewiczFibration p) (hq : IsHurewiczFibration q) :
    IsHurewiczFibration (Prod.map p q)

    The product of two Hurewicz fibrations is a Hurewicz fibration.

    source
    theorem TauCeti.IsHurewiczFibration.pullback {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {B' : Type v'} [TopologicalSpace B'] (hp : IsHurewiczFibration p) (g : C(B', B)) :
    IsHurewiczFibration fun (x : { x : B' × E // g x.1 = p x.2 }) => (↑x).1

    The base change of a Hurewicz fibration along any continuous map is a Hurewicz fibration.

    source
    theorem TauCeti.IsHurewiczFibration.comp_homeomorph {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {E' : Type u'} [TopologicalSpace E'] (hp : IsHurewiczFibration p) (e : E' ≃ₜ E) :
    IsHurewiczFibration (p ∘ ⇑e)

    Precomposing a Hurewicz fibration with a homeomorphism gives a Hurewicz fibration.

    source
    theorem TauCeti.IsHurewiczFibration.comp_subtypeVal {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : IsHurewiczFibration p) {S : Set E} (hS : ∀ ⦃e e' : E⦄, e ∈ S → Joined e e' → e' ∈ S) :
    IsHurewiczFibration (p ∘ Subtype.val)

    The restriction of a Hurewicz fibration to a subset of the total space that is closed under joining by paths, for instance a union of path components, is a Hurewicz fibration.

    source
    theorem TauCeti.isHurewiczFibration_of_subsingleton {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} [Subsingleton B] :
    IsHurewiczFibration p

    A map to a subsingleton space is a Hurewicz fibration.

    source
    theorem TauCeti.isHurewiczFibration_fst {B : Type v} [TopologicalSpace B] (F : Type u') [TopologicalSpace F] :
    IsHurewiczFibration Prod.fst

    The projection B × F → B is a Hurewicz fibration.