# mathlibdocumentation

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.

def is_homeomorphic_trivial_fiber_bundle {B : Type u_1} (F : Type u_2) {Z : Type u_3} (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
@[protected]
theorem is_homeomorphic_trivial_fiber_bundle.proj_eq {B : Type u_1} {F : Type u_2} {Z : Type u_3} {proj : Z B} (h : proj) :
(e : Z ≃ₜ B × F), proj =
@[protected]
theorem is_homeomorphic_trivial_fiber_bundle.surjective_proj {B : Type u_1} {F : Type u_2} {Z : Type u_3} {proj : Z B} [nonempty F] (h : proj) :

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

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

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

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

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

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

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

theorem is_homeomorphic_trivial_fiber_bundle_fst {B : Type u_1} (F : Type u_2)  :

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

theorem is_homeomorphic_trivial_fiber_bundle_snd {B : Type u_1} (F : Type u_2)  :

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