mathlib3 documentation

topology.fiber_bundle.is_homeomorphic_trivial_bundle

Maps equivariantly-homeomorphic to projection in a product #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains the definition is_homeomorphic_trivial_fiber_bundle 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 is_homeomorphic_trivial_fiber_bundle {B : Type u_1} (F : Type u_2) {Z : Type u_3} [topological_space B] [topological_space F] [topological_space 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
source
@[protected]
theorem is_homeomorphic_trivial_fiber_bundle.proj_eq {B : Type u_1} {F : Type u_2} {Z : Type u_3} [topological_space B] [topological_space F] [topological_space Z] {proj : Z → B} (h : is_homeomorphic_trivial_fiber_bundle F proj) :
∃ (e : Z ≃ₜ B × F), proj = prod.fst ∘ ⇑e
source
@[protected]
theorem is_homeomorphic_trivial_fiber_bundle.surjective_proj {B : Type u_1} {F : Type u_2} {Z : Type u_3} [topological_space B] [topological_space F] [topological_space Z] {proj : Z → B} [nonempty F] (h : is_homeomorphic_trivial_fiber_bundle F proj) :
function.surjective proj

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

source
@[protected]
theorem is_homeomorphic_trivial_fiber_bundle.continuous_proj {B : Type u_1} {F : Type u_2} {Z : Type u_3} [topological_space B] [topological_space F] [topological_space Z] {proj : Z → B} (h : is_homeomorphic_trivial_fiber_bundle F proj) :
continuous proj

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

source
@[protected]
theorem is_homeomorphic_trivial_fiber_bundle.is_open_map_proj {B : Type u_1} {F : Type u_2} {Z : Type u_3} [topological_space B] [topological_space F] [topological_space Z] {proj : Z → B} (h : is_homeomorphic_trivial_fiber_bundle F proj) :
is_open_map proj

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

source
@[protected]
theorem is_homeomorphic_trivial_fiber_bundle.quotient_map_proj {B : Type u_1} {F : Type u_2} {Z : Type u_3} [topological_space B] [topological_space F] [topological_space Z] {proj : Z → B} [nonempty F] (h : is_homeomorphic_trivial_fiber_bundle F proj) :
quotient_map proj

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

source
theorem is_homeomorphic_trivial_fiber_bundle_fst {B : Type u_1} (F : Type u_2) [topological_space B] [topological_space F] :
is_homeomorphic_trivial_fiber_bundle F prod.fst

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

source
theorem is_homeomorphic_trivial_fiber_bundle_snd {B : Type u_1} (F : Type u_2) [topological_space B] [topological_space F] :
is_homeomorphic_trivial_fiber_bundle F prod.snd

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