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') :
topological_space ((f *ᵖ E') x)
Equations
- bundle.pullback.topological_space E' f = λ (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') :
add_comm_monoid ((f *ᵖ E') x)
Equations
- bundle.pullback.add_comm_monoid E' f = λ (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), module R (E' x)]
(x : B') :
Equations
- bundle.pullback.module R E' 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)
[topological_space B']
[topological_space (bundle.total_space E)] :
topological_space (bundle.total_space (f *ᵖ E))
Definition of pullback.total_space.topological_space, which we make irreducible.
Equations
- pullback_topology E f = topological_space.induced bundle.total_space.proj _inst_1 ⊓ topological_space.induced (bundle.pullback.lift f) _inst_2
@[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)] :
topological_space (bundle.total_space (f *ᵖ 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) :
topological_vector_bundle.trivialization 𝕜 F (⇑f *ᵖ E)
A vector bundle trivialization can be pulled back to a trivialization on the pullback bundle.
Equations
- e.pullback f = {to_fiber_bundle_trivialization := {to_local_homeomorph := {to_local_equiv := {to_fun := λ (z : bundle.total_space (⇑f *ᵖ E)), (z.proj, (⇑e (bundle.pullback.lift ⇑f z)).snd), inv_fun := λ (y : B' × F), bundle.total_space_mk y.fst (e.symm (⇑f y.fst) y.snd), source := bundle.pullback.lift ⇑f ⁻¹' e.to_fiber_bundle_trivialization.to_local_homeomorph.to_local_equiv.source, target := (⇑f ⁻¹' e.to_fiber_bundle_trivialization.base_set) ×ˢ set.univ, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}, base_set := ⇑f ⁻¹' e.to_fiber_bundle_trivialization.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}, linear' := _}
@[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) :
topological_vector_bundle 𝕜 F (⇑f *ᵖ E)
Equations
- topological_vector_bundle.pullback f = {total_space_mk_inducing := _, trivialization_atlas := (λ (e : topological_vector_bundle.trivialization 𝕜 F E), e.pullback f) '' topological_vector_bundle.trivialization_atlas 𝕜 F E, trivialization_at := λ (x : B'), (topological_vector_bundle.trivialization_at 𝕜 F E (⇑f x)).pullback f, mem_base_set_trivialization_at := _, trivialization_mem_atlas := _, continuous_on_coord_change := _}