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.

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
@[protected]
@[protected]

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

@[protected]

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

@[protected]

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

@[protected]

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

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

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