mathlib documentation

topology.vector_bundle.pullback

Pullbacks of topological vector bundles #

We construct the pullback bundle for a map f : B' → B whose fiber map is given simply by f *ᵖ E = E ∘ f (the type synonym is there for typeclass instance problems).

@[protected, instance]
def bundle.pullback.topological_space {B : Type u_3} (E' : B → Type u_6) {B' : Type u_7} (f : B' → B) [Π (x : B), topological_space (E' x)] (x : B') :
Equations
@[protected, instance]
def bundle.pullback.add_comm_monoid {B : Type u_3} (E' : B → Type u_6) {B' : Type u_7} (f : B' → B) [Π (x : B), add_comm_monoid (E' x)] (x : B') :
Equations
@[protected, instance]
def bundle.pullback.module (R : Type u_1) {B : Type u_3} (E' : B → Type u_6) {B' : Type u_7} (f : B' → B) [semiring R] [Π (x : B), add_comm_monoid (E' x)] [Π (x : B), module R (E' x)] (x : B') :
module R ((f *ᵖ E') x)
Equations
@[irreducible]
def pullback_topology {B : Type u_3} (E : B → Type u_5) {B' : Type u_7} (f : B' → B) [topological_space B'] [topological_space (bundle.total_space E)] :

Definition of pullback.total_space.topological_space, which we make irreducible.

Equations
@[protected, instance]
def pullback.total_space.topological_space {B : Type u_3} (E : B → Type u_5) {B' : Type u_7} (f : B' → B) [topological_space B'] [topological_space (bundle.total_space E)] :

The topology on the total space of a pullback bundle is the coarsest topology for which both the projections to the base and the map to the original bundle are continuous.

Equations
theorem pullback.continuous_proj {B : Type u_3} (E : B → Type u_5) {B' : Type u_7} [topological_space B'] [topological_space (bundle.total_space E)] (f : B' → B) :
theorem pullback.continuous_lift {B : Type u_3} (E : B → Type u_5) {B' : Type u_7} [topological_space B'] [topological_space (bundle.total_space E)] (f : B' → B) :
theorem inducing_pullback_total_space_embedding {B : Type u_3} (E : B → Type u_5) {B' : Type u_7} [topological_space B'] [topological_space (bundle.total_space E)] (f : B' → B) :
theorem pullback.continuous_total_space_mk (𝕜 : Type u_2) {B : Type u_3} (F : Type u_4) (E : B → Type u_5) {B' : Type u_7} [topological_space B'] [topological_space (bundle.total_space E)] [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] [topological_space B] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module 𝕜 (E x)] [Π (x : B), topological_space (E x)] [topological_vector_bundle 𝕜 F E] {f : B' → B} {x : B'} :
noncomputable def topological_vector_bundle.trivialization.pullback {𝕜 : Type u_2} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} {B' : Type u_7} [topological_space B'] [topological_space (bundle.total_space E)] [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] [topological_space B] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module 𝕜 (E x)] {K : Type u_8} [continuous_map_class K B' B] (e : topological_vector_bundle.trivialization 𝕜 F E) (f : K) :

A vector bundle trivialization can be pulled back to a trivialization on the pullback bundle.

Equations
@[protected, instance]
noncomputable def topological_vector_bundle.pullback {𝕜 : Type u_2} {B : Type u_3} {F : Type u_4} {E : B → Type u_5} {B' : Type u_7} [topological_space B'] [topological_space (bundle.total_space E)] [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F] [topological_space B] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), module 𝕜 (E x)] {K : Type u_8} [continuous_map_class K B' B] [Π (x : B), topological_space (E x)] [topological_vector_bundle 𝕜 F E] (f : K) :
Equations