IsHomeomorphicTrivialFiberBundle.isOpenMap_proj
theorem IsHomeomorphicTrivialFiberBundle.isOpenMap_proj :
∀ {B : Type u_1} {F : Type u_2} {Z : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
[inst_2 : TopologicalSpace Z] {proj : Z → B}, IsHomeomorphicTrivialFiberBundle F proj → IsOpenMap proj
The theorem `IsHomeomorphicTrivialFiberBundle.isOpenMap_proj` states that for all types `B`, `F`, and `Z` with topological spaces, given a projection function from `Z` to `B`, if `Z` is a trivial fiber bundle with fiber `F` over `B`, then the projection function is an open map. In other words, the image of an open set in `Z` under the projection function is an open set in `B`. A trivial fiber bundle in this context is a topological space that is homeomorphic to the product of its base with a discrete space.
More concisely: Given a projection function from a trivial fiber bundle over a topological space to its base space, the projection function is an open map.
|
IsHomeomorphicTrivialFiberBundle.surjective_proj
theorem IsHomeomorphicTrivialFiberBundle.surjective_proj :
∀ {B : Type u_1} {F : Type u_2} {Z : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
[inst_2 : TopologicalSpace Z] {proj : Z → B} [inst_3 : Nonempty F],
IsHomeomorphicTrivialFiberBundle F proj → Function.Surjective proj
This theorem states that for any types `B`, `F`, and `Z` that are equipped with topological structures, given a projection function `proj : Z → B` and assuming that there exists at least one element in `F`, if the space `Z` is a trivial fiber bundle over the base `B` with fiber `F` (meaning there exists a homeomorphism to `B × F` that sends `proj` to the first element of the pair), then the projection function `proj` is surjective. In other words, for every element `b` in `B`, there exists an element `z` in `Z` such that `proj(z) = b`.
More concisely: If `Z` is a trivial fiber bundle over `B` with fiber `F` and `proj : Z → B` is its projection function, then `proj` is surjective.
|
IsHomeomorphicTrivialFiberBundle.continuous_proj
theorem IsHomeomorphicTrivialFiberBundle.continuous_proj :
∀ {B : Type u_1} {F : Type u_2} {Z : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
[inst_2 : TopologicalSpace Z] {proj : Z → B}, IsHomeomorphicTrivialFiberBundle F proj → Continuous proj
This theorem states that the projection from a trivial fiber bundle to its base is continuous. In other words, for any types `B`, `F`, and `Z` with associated topological spaces, if `Z` is a trivial fiber bundle over `B` with fiber `F` (meaning there exists a homeomorphism from `Z` to `B × F` such that the projection function `proj` maps to the first component of the product), then the projection function `proj` from `Z` to `B` is continuous.
More concisely: If `Z` is a trivial fiber bundle over `B` with fiber `F`, then the projection function `proj` from `Z` to `B` is continuous.
|
IsHomeomorphicTrivialFiberBundle.quotientMap_proj
theorem IsHomeomorphicTrivialFiberBundle.quotientMap_proj :
∀ {B : Type u_1} {F : Type u_2} {Z : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
[inst_2 : TopologicalSpace Z] {proj : Z → B} [inst_3 : Nonempty F],
IsHomeomorphicTrivialFiberBundle F proj → QuotientMap proj
The theorem `IsHomeomorphicTrivialFiberBundle.quotientMap_proj` states that for any types `B`, `F`, and `Z` with corresponding topological spaces, and any function `proj` from `Z` to `B`, if `Z` can be viewed as a trivial fiber bundle with fiber `F` over `B` (in the sense that there is a homeomorphism between `Z` and the product space `B × F` that sends `proj` to the projection onto the first factor), then `proj` is a quotient map. A function is a quotient map if it is surjective (every element in the target space is an image of some element in the domain) and for any subset of the target space, it is open if and only if its preimage under the function is open in the domain space. This theorem also assumes that `F` is nonempty.
More concisely: If a function from a space to its base space makes a trivial fiber bundle over the base space homeomorphic to the product space, then the function is a quotient map. (Assuming the fiber is nonempty.)
|
isHomeomorphicTrivialFiberBundle_snd
theorem isHomeomorphicTrivialFiberBundle_snd :
∀ {B : Type u_1} (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F],
IsHomeomorphicTrivialFiberBundle F Prod.snd
The theorem `isHomeomorphicTrivialFiberBundle_snd` states that for any types `B` and `F` with defined topological spaces, the second projection function `Prod.snd` is a trivial fiber bundle with fiber `F`. In other words, there exists a homeomorphism (a function that is both continuous and bijective, with a continuous inverse) from the product `B × F` to another space, such that the projection onto `B` from this other space is equivalent to the second projection function `Prod.snd`. This is a key property of product spaces in topology.
More concisely: The second projection function of a product space is a trivial fiber bundle homeomorphism with fiber `F`.
|
IsHomeomorphicTrivialFiberBundle.proj_eq
theorem IsHomeomorphicTrivialFiberBundle.proj_eq :
∀ {B : Type u_1} {F : Type u_2} {Z : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
[inst_2 : TopologicalSpace Z] {proj : Z → B},
IsHomeomorphicTrivialFiberBundle F proj → ∃ e, proj = Prod.fst ∘ ⇑e
This theorem states that for any types `B`, `F`, and `Z`, where `B`, `F`, and `Z` are topological spaces, and given a projection `proj` from `Z` to `B`, if `Z` is a trivial fiber bundle with fiber `F` over base `B` that is homeomorphic to the product space `B × F`, then there exists a function `e` such that the projection function `proj` is equal to the composition of the first projection function `Prod.fst` and the application of `e`. In other words, every point in `Z` projected onto `B` via `proj` can be obtained by first applying the mapping `e` and then taking the first component of the resulting pair in `B × F`.
More concisely: Given a trivial fiber bundle with projection `proj` from a topological space `Z` to `B` with fiber `F`, if `Z` is homeomorphic to `B × F`, then there exists a function `e` such that `proj = Prod.fst ∘ e`.
|
isHomeomorphicTrivialFiberBundle_fst
theorem isHomeomorphicTrivialFiberBundle_fst :
∀ {B : Type u_1} (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F],
IsHomeomorphicTrivialFiberBundle F Prod.fst
This theorem states that the first projection in a product, denoted as `Prod.fst`, is a trivial fiber bundle. Here, the term "trivial fiber bundle" refers to a space that has a projection onto a base 'B' and is homeomorphic to the product of the base and a fiber 'F'. In simpler terms, it means that you can smoothly transform the space into the product of the base and the fiber such that the projection onto the base stays the same. In this case, the theorem is stating that the first projection in a product, which takes a pair and returns its first element, has this property for any given topological space 'B' and fiber 'F'.
More concisely: The first projection of a product is a trivial fiber bundle. Equivalently, the first projection of a product space is a homeomorphism onto its base space times the fiber.
|