HepLean Documentation

Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle

Maps equivariantly-homeomorphic to projection in a product #

This file contains the definition IsHomeomorphicTrivialFiberBundle F p, a Prop saying that a map p : Z → B between topological spaces is a "trivial fiber bundle" in the sense that there exists a homeomorphism h : Z ≃ₜ B × F such that proj x = (h x).1. This is an abstraction which is occasionally convenient in showing that a map is open, a quotient map, etc.

This material was formerly linked to the main definition of fiber bundles, but after a series of refactors, there is no longer a direct connection.

source
def IsHomeomorphicTrivialFiberBundle {B : Type u_1} (F : Type u_2) {Z : Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] (proj : Z → B) :
Prop

A trivial fiber bundle with fiber F over a base B is a space Z projecting on B for which there exists a homeomorphism to B × F that sends proj to Prod.fst.

Equations
Instances For
    source
    theorem IsHomeomorphicTrivialFiberBundle.proj_eq {B : Type u_1} {F : Type u_2} {Z : Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {proj : Z → B} (h : IsHomeomorphicTrivialFiberBundle F proj) :
    ∃ (e : Z ≃ₜ B × F), proj = Prod.fst ∘ ⇑e
    source
    theorem IsHomeomorphicTrivialFiberBundle.surjective_proj {B : Type u_1} {F : Type u_2} {Z : Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {proj : Z → B} [Nonempty F] (h : IsHomeomorphicTrivialFiberBundle F proj) :
    Function.Surjective proj

    The projection from a trivial fiber bundle to its base is surjective.

    source
    theorem IsHomeomorphicTrivialFiberBundle.continuous_proj {B : Type u_1} {F : Type u_2} {Z : Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {proj : Z → B} (h : IsHomeomorphicTrivialFiberBundle F proj) :
    Continuous proj

    The projection from a trivial fiber bundle to its base is continuous.

    source
    theorem IsHomeomorphicTrivialFiberBundle.isOpenMap_proj {B : Type u_1} {F : Type u_2} {Z : Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {proj : Z → B} (h : IsHomeomorphicTrivialFiberBundle F proj) :
    IsOpenMap proj

    The projection from a trivial fiber bundle to its base is open.

    source
    theorem IsHomeomorphicTrivialFiberBundle.isQuotientMap_proj {B : Type u_1} {F : Type u_2} {Z : Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {proj : Z → B} [Nonempty F] (h : IsHomeomorphicTrivialFiberBundle F proj) :
    IsQuotientMap proj

    The projection from a trivial fiber bundle to its base is open.

    source
    @[deprecated IsHomeomorphicTrivialFiberBundle.isQuotientMap_proj]
    theorem IsHomeomorphicTrivialFiberBundle.quotientMap_proj {B : Type u_1} {F : Type u_2} {Z : Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {proj : Z → B} [Nonempty F] (h : IsHomeomorphicTrivialFiberBundle F proj) :
    IsQuotientMap proj

    Alias of IsHomeomorphicTrivialFiberBundle.isQuotientMap_proj.

    The projection from a trivial fiber bundle to its base is open.

    source
    theorem isHomeomorphicTrivialFiberBundle_fst {B : Type u_1} (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] :
    IsHomeomorphicTrivialFiberBundle F Prod.fst

    The first projection in a product is a trivial fiber bundle.

    source
    theorem isHomeomorphicTrivialFiberBundle_snd {B : Type u_1} (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] :
    IsHomeomorphicTrivialFiberBundle F Prod.snd

    The second projection in a product is a trivial fiber bundle.