# mathlibdocumentation

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
• = λ (x : B'), _inst_1 (f x)
@[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
• = λ (x : B'), _inst_1 (f x)
@[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), (E' x)] (x : B') :
((f *ᵖ E') x)
Equations
• f = λ (x : B'), _inst_3 (f x)
@[irreducible]
def pullback_topology {B : Type u_3} (E : B → Type u_5) {B' : Type u_7} (f : B' → B)  :

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)  :

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} (f : B' → B) :
theorem pullback.continuous_lift {B : Type u_3} (E : B → Type u_5) {B' : Type u_7} (f : B' → B) :
theorem inducing_pullback_total_space_embedding {B : Type u_3} (E : B → Type u_5) {B' : Type u_7} (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} [ F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), (E x)] [Π (x : B), topological_space (E x)] [ 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} [ F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), (E x)] {K : Type u_8} [ B] (e : 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} [ F] [Π (x : B), add_comm_monoid (E x)] [Π (x : B), (E x)] {K : Type u_8} [ B] [Π (x : B), topological_space (E x)] [ E] (f : K) :
(f *ᵖ E)
Equations