Standard constructions on fiber bundles #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains several standard constructions on fiber bundles:
-
bundle.trivial.fiber_bundle 𝕜 B F: the trivial fiber bundle with model fiberFover the baseB -
fiber_bundle.prod: for fiber bundlesE₁andE₂over a common base, a fiber bundle structure on their fiberwise productE₁ ×ᵇ E₂(the notation stands forλ x, E₁ x × E₂ x). -
fiber_bundle.pullback: for a fiber bundleEoverB, a fiber bundle structure on its pullbackf *ᵖ Eby a mapf : B' → B(the notation is a type synonym forE ∘ f).
Tags #
fiber bundle, fibre bundle, fiberwise product, pullback
The trivial bundle #
@[protected, instance]
def
bundle.trivial.bundle.total_space.topological_space
(B : Type u_1)
(F : Type u_2)
[t₁ : topological_space B]
[t₂ : topological_space F] :
def
bundle.trivial.trivialization
(B : Type u_1)
(F : Type u_2)
[topological_space B]
[topological_space F] :
Local trivialization for trivial bundle.
Equations
- bundle.trivial.trivialization B F = {to_local_homeomorph := {to_local_equiv := {to_fun := λ (x : bundle.total_space F (λ (_x : B), F)), (x.proj, x.snd), inv_fun := λ (y : B × F), {proj := y.fst, snd := y.snd}, source := set.univ (bundle.total_space F (λ (_x : B), F)), target := set.univ (B × F), map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}, base_set := set.univ B, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
Instances for bundle.trivial.trivialization
@[simp]
theorem
bundle.trivial.trivialization_source
(B : Type u_1)
(F : Type u_2)
[topological_space B]
[topological_space F] :
@[simp]
theorem
bundle.trivial.trivialization_target
(B : Type u_1)
(F : Type u_2)
[topological_space B]
[topological_space F] :
@[protected, instance]
def
bundle.trivial.fiber_bundle
(B : Type u_1)
(F : Type u_2)
[topological_space B]
[topological_space F] :
fiber_bundle F (bundle.trivial B F)
Fiber bundle instance on the trivial bundle.
Equations
- bundle.trivial.fiber_bundle B F = {total_space_mk_inducing := _, trivialization_atlas := {bundle.trivial.trivialization B F}, trivialization_at := λ (x : B), bundle.trivial.trivialization B F, mem_base_set_trivialization_at := _, trivialization_mem_atlas := _}
theorem
bundle.trivial.eq_trivialization
(B : Type u_1)
(F : Type u_2)
[topological_space B]
[topological_space F]
(e : trivialization F bundle.total_space.proj)
[i : mem_trivialization_atlas e] :
Fibrewise product of two bundles #
@[protected, instance]
def
fiber_bundle.prod.topological_space
{B : Type u_1}
(F₁ : Type u_2)
(E₁ : B → Type u_3)
(F₂ : Type u_4)
(E₂ : B → Type u_5)
[topological_space (bundle.total_space F₁ E₁)]
[topological_space (bundle.total_space F₂ E₂)] :
topological_space (bundle.total_space (F₁ × F₂) (λ (x : B), E₁ x × E₂ x))
Equip the total space of the fiberwise product of two fiber bundles E₁, E₂ with
the induced topology from the diagonal embedding into total_space E₁ × total_space E₂.
Equations
- fiber_bundle.prod.topological_space F₁ E₁ F₂ E₂ = topological_space.induced (λ (p : bundle.total_space (F₁ × F₂) (λ (x : B), E₁ x × E₂ x)), ({proj := p.proj, snd := p.snd.fst}, {proj := p.proj, snd := p.snd.snd})) prod.topological_space
theorem
fiber_bundle.prod.inducing_diag
{B : Type u_1}
(F₁ : Type u_2)
(E₁ : B → Type u_3)
(F₂ : Type u_4)
(E₂ : B → Type u_5)
[topological_space (bundle.total_space F₁ E₁)]
[topological_space (bundle.total_space F₂ E₂)] :
The diagonal map from the total space of the fiberwise product of two fiber bundles
E₁, E₂ into total_space E₁ × total_space E₂ is inducing.
def
trivialization.prod.to_fun'
{B : Type u_1}
[topological_space B]
{F₁ : Type u_2}
[topological_space F₁]
{E₁ : B → Type u_3}
[topological_space (bundle.total_space F₁ E₁)]
{F₂ : Type u_4}
[topological_space F₂]
{E₂ : B → Type u_5}
[topological_space (bundle.total_space F₂ E₂)]
(e₁ : trivialization F₁ bundle.total_space.proj)
(e₂ : trivialization F₂ bundle.total_space.proj) :
Given trivializations e₁, e₂ for fiber bundles E₁, E₂ over a base B, the forward
function for the construction trivialization.prod, the induced
trivialization for the fiberwise product of E₁ and E₂.
theorem
trivialization.prod.continuous_to_fun
{B : Type u_1}
[topological_space B]
{F₁ : Type u_2}
[topological_space F₁]
{E₁ : B → Type u_3}
[topological_space (bundle.total_space F₁ E₁)]
{F₂ : Type u_4}
[topological_space F₂]
{E₂ : B → Type u_5}
[topological_space (bundle.total_space F₂ E₂)]
{e₁ : trivialization F₁ bundle.total_space.proj}
{e₂ : trivialization F₂ bundle.total_space.proj} :
continuous_on (trivialization.prod.to_fun' e₁ e₂) (bundle.total_space.proj ⁻¹' (e₁.base_set ∩ e₂.base_set))
noncomputable
def
trivialization.prod.inv_fun'
{B : Type u_1}
[topological_space B]
{F₁ : Type u_2}
[topological_space F₁]
{E₁ : B → Type u_3}
[topological_space (bundle.total_space F₁ E₁)]
{F₂ : Type u_4}
[topological_space F₂]
{E₂ : B → Type u_5}
[topological_space (bundle.total_space F₂ E₂)]
(e₁ : trivialization F₁ bundle.total_space.proj)
(e₂ : trivialization F₂ bundle.total_space.proj)
[Π (x : B), has_zero (E₁ x)]
[Π (x : B), has_zero (E₂ x)]
(p : B × F₁ × F₂) :
bundle.total_space (F₁ × F₂) (λ (x : B), E₁ x × E₂ x)
Given trivializations e₁, e₂ for fiber bundles E₁, E₂ over a base B, the inverse
function for the construction trivialization.prod, the induced
trivialization for the fiberwise product of E₁ and E₂.
theorem
trivialization.prod.left_inv
{B : Type u_1}
[topological_space B]
{F₁ : Type u_2}
[topological_space F₁]
{E₁ : B → Type u_3}
[topological_space (bundle.total_space F₁ E₁)]
{F₂ : Type u_4}
[topological_space F₂]
{E₂ : B → Type u_5}
[topological_space (bundle.total_space F₂ E₂)]
{e₁ : trivialization F₁ bundle.total_space.proj}
{e₂ : trivialization F₂ bundle.total_space.proj}
[Π (x : B), has_zero (E₁ x)]
[Π (x : B), has_zero (E₂ x)]
{x : bundle.total_space (F₁ × F₂) (λ (x : B), E₁ x × E₂ x)}
(h : x ∈ bundle.total_space.proj ⁻¹' (e₁.base_set ∩ e₂.base_set)) :
trivialization.prod.inv_fun' e₁ e₂ (trivialization.prod.to_fun' e₁ e₂ x) = x
theorem
trivialization.prod.right_inv
{B : Type u_1}
[topological_space B]
{F₁ : Type u_2}
[topological_space F₁]
{E₁ : B → Type u_3}
[topological_space (bundle.total_space F₁ E₁)]
{F₂ : Type u_4}
[topological_space F₂]
{E₂ : B → Type u_5}
[topological_space (bundle.total_space F₂ E₂)]
{e₁ : trivialization F₁ bundle.total_space.proj}
{e₂ : trivialization F₂ bundle.total_space.proj}
[Π (x : B), has_zero (E₁ x)]
[Π (x : B), has_zero (E₂ x)]
{x : B × F₁ × F₂}
(h : x ∈ (e₁.base_set ∩ e₂.base_set) ×ˢ set.univ) :
trivialization.prod.to_fun' e₁ e₂ (trivialization.prod.inv_fun' e₁ e₂ x) = x
theorem
trivialization.prod.continuous_inv_fun
{B : Type u_1}
[topological_space B]
{F₁ : Type u_2}
[topological_space F₁]
{E₁ : B → Type u_3}
[topological_space (bundle.total_space F₁ E₁)]
{F₂ : Type u_4}
[topological_space F₂]
{E₂ : B → Type u_5}
[topological_space (bundle.total_space F₂ E₂)]
{e₁ : trivialization F₁ bundle.total_space.proj}
{e₂ : trivialization F₂ bundle.total_space.proj}
[Π (x : B), has_zero (E₁ x)]
[Π (x : B), has_zero (E₂ x)] :
continuous_on (trivialization.prod.inv_fun' e₁ e₂) ((e₁.base_set ∩ e₂.base_set) ×ˢ set.univ)
noncomputable
def
trivialization.prod
{B : Type u_1}
[topological_space B]
{F₁ : Type u_2}
[topological_space F₁]
{E₁ : B → Type u_3}
[topological_space (bundle.total_space F₁ E₁)]
{F₂ : Type u_4}
[topological_space F₂]
{E₂ : B → Type u_5}
[topological_space (bundle.total_space F₂ E₂)]
(e₁ : trivialization F₁ bundle.total_space.proj)
(e₂ : trivialization F₂ bundle.total_space.proj)
[Π (x : B), has_zero (E₁ x)]
[Π (x : B), has_zero (E₂ x)] :
trivialization (F₁ × F₂) bundle.total_space.proj
Given trivializations e₁, e₂ for bundle types E₁, E₂ over a base B, the induced
trivialization for the fiberwise product of E₁ and E₂, whose base set is
e₁.base_set ∩ e₂.base_set.
Equations
- e₁.prod e₂ = {to_local_homeomorph := {to_local_equiv := {to_fun := trivialization.prod.to_fun' e₁ e₂, inv_fun := trivialization.prod.inv_fun' e₁ e₂ (λ (x : B), _inst_7 x), source := bundle.total_space.proj ⁻¹' (e₁.base_set ∩ e₂.base_set), target := (e₁.base_set ∩ e₂.base_set) ×ˢ set.univ, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}, base_set := e₁.base_set ∩ e₂.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
Instances for trivialization.prod
@[simp]
theorem
trivialization.base_set_prod
{B : Type u_1}
[topological_space B]
{F₁ : Type u_2}
[topological_space F₁]
{E₁ : B → Type u_3}
[topological_space (bundle.total_space F₁ E₁)]
{F₂ : Type u_4}
[topological_space F₂]
{E₂ : B → Type u_5}
[topological_space (bundle.total_space F₂ E₂)]
(e₁ : trivialization F₁ bundle.total_space.proj)
(e₂ : trivialization F₂ bundle.total_space.proj)
[Π (x : B), has_zero (E₁ x)]
[Π (x : B), has_zero (E₂ x)] :
theorem
trivialization.prod_symm_apply
{B : Type u_1}
[topological_space B]
{F₁ : Type u_2}
[topological_space F₁]
{E₁ : B → Type u_3}
[topological_space (bundle.total_space F₁ E₁)]
{F₂ : Type u_4}
[topological_space F₂]
{E₂ : B → Type u_5}
[topological_space (bundle.total_space F₂ E₂)]
(e₁ : trivialization F₁ bundle.total_space.proj)
(e₂ : trivialization F₂ bundle.total_space.proj)
[Π (x : B), has_zero (E₁ x)]
[Π (x : B), has_zero (E₂ x)]
(x : B)
(w₁ : F₁)
(w₂ : F₂) :
@[protected, instance]
noncomputable
def
fiber_bundle.prod
{B : Type u_1}
[topological_space B]
(F₁ : Type u_2)
[topological_space F₁]
(E₁ : B → Type u_3)
[topological_space (bundle.total_space F₁ E₁)]
(F₂ : Type u_4)
[topological_space F₂]
(E₂ : B → Type u_5)
[topological_space (bundle.total_space F₂ E₂)]
[Π (x : B), has_zero (E₁ x)]
[Π (x : B), has_zero (E₂ x)]
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₁ E₁]
[fiber_bundle F₂ E₂] :
fiber_bundle (F₁ × F₂) (λ (x : B), E₁ x × E₂ x)
The product of two fiber bundles is a fiber bundle.
Equations
- fiber_bundle.prod F₁ E₁ F₂ E₂ = {total_space_mk_inducing := _, trivialization_atlas := {e : trivialization (F₁ × F₂) bundle.total_space.proj | ∃ (e₁ : trivialization F₁ bundle.total_space.proj) (e₂ : trivialization F₂ bundle.total_space.proj) [_inst_12 : mem_trivialization_atlas e₁] [_inst_13 : mem_trivialization_atlas e₂], e = e₁.prod e₂}, trivialization_at := λ (b : B), (fiber_bundle.trivialization_at F₁ E₁ b).prod (fiber_bundle.trivialization_at F₂ E₂ b), mem_base_set_trivialization_at := _, trivialization_mem_atlas := _}
@[protected, instance]
def
trivialization.prod.mem_trivialization_atlas
{B : Type u_1}
[topological_space B]
(F₁ : Type u_2)
[topological_space F₁]
(E₁ : B → Type u_3)
[topological_space (bundle.total_space F₁ E₁)]
(F₂ : Type u_4)
[topological_space F₂]
(E₂ : B → Type u_5)
[topological_space (bundle.total_space F₂ E₂)]
[Π (x : B), has_zero (E₁ x)]
[Π (x : B), has_zero (E₂ x)]
[Π (x : B), topological_space (E₁ x)]
[Π (x : B), topological_space (E₂ x)]
[fiber_bundle F₁ E₁]
[fiber_bundle F₂ E₂]
{e₁ : trivialization F₁ bundle.total_space.proj}
{e₂ : trivialization F₂ bundle.total_space.proj}
[mem_trivialization_atlas e₁]
[mem_trivialization_atlas e₂] :
mem_trivialization_atlas (e₁.prod e₂)
Pullbacks of fiber bundles #
@[protected, instance]
def
bundle.pullback.topological_space
{B : Type u_1}
(E : B → Type u_3)
{B' : Type u_4}
(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)
@[irreducible]
def
pullback_topology
{B : Type u_1}
(F : Type u_2)
(E : B → Type u_3)
{B' : Type u_4}
(f : B' → B)
[topological_space B']
[topological_space (bundle.total_space F E)] :
topological_space (bundle.total_space F f *ᵖ E)
Definition of pullback.total_space.topological_space, which we make irreducible.
Equations
- pullback_topology F 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_1}
(F : Type u_2)
(E : B → Type u_3)
{B' : Type u_4}
(f : B' → B)
[topological_space B']
[topological_space (bundle.total_space F E)] :
topological_space (bundle.total_space F 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
- pullback.total_space.topological_space F E f = pullback_topology F E f
theorem
pullback.continuous_proj
{B : Type u_1}
(F : Type u_2)
(E : B → Type u_3)
{B' : Type u_4}
[topological_space B']
[topological_space (bundle.total_space F E)]
(f : B' → B) :
theorem
pullback.continuous_lift
{B : Type u_1}
(F : Type u_2)
(E : B → Type u_3)
{B' : Type u_4}
[topological_space B']
[topological_space (bundle.total_space F E)]
(f : B' → B) :
theorem
inducing_pullback_total_space_embedding
{B : Type u_1}
(F : Type u_2)
(E : B → Type u_3)
{B' : Type u_4}
[topological_space B']
[topological_space (bundle.total_space F E)]
(f : B' → B) :
theorem
pullback.continuous_total_space_mk
{B : Type u_1}
(F : Type u_2)
(E : B → Type u_3)
{B' : Type u_4}
[topological_space B']
[topological_space (bundle.total_space F E)]
[topological_space F]
[topological_space B]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
{f : B' → B}
{x : B'} :
noncomputable
def
trivialization.pullback
{B : Type u_1}
{F : Type u_2}
{E : B → Type u_3}
{B' : Type u_4}
[topological_space B']
[topological_space (bundle.total_space F E)]
[topological_space F]
[topological_space B]
[Π (b : B), has_zero (E b)]
{K : Type u_5}
[continuous_map_class K B' B]
(e : trivialization F bundle.total_space.proj)
(f : K) :
A fiber bundle trivialization can be pulled back to a trivialization on the pullback bundle.
Equations
- e.pullback f = {to_local_homeomorph := {to_local_equiv := {to_fun := λ (z : bundle.total_space F ⇑f *ᵖ E), (z.proj, (⇑e (bundle.pullback.lift ⇑f z)).snd), inv_fun := λ (y : B' × F), {proj := y.fst, snd := e.symm (⇑f y.fst) y.snd}, source := bundle.pullback.lift ⇑f ⁻¹' e.to_local_homeomorph.to_local_equiv.source, target := (⇑f ⁻¹' e.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.base_set, open_base_set := _, source_eq := _, target_eq := _, proj_to_fun := _}
Instances for trivialization.pullback
@[protected, instance]
noncomputable
def
fiber_bundle.pullback
{B : Type u_1}
{F : Type u_2}
{E : B → Type u_3}
{B' : Type u_4}
[topological_space B']
[topological_space (bundle.total_space F E)]
[topological_space F]
[topological_space B]
[Π (b : B), has_zero (E b)]
{K : Type u_5}
[continuous_map_class K B' B]
[Π (x : B), topological_space (E x)]
[fiber_bundle F E]
(f : K) :
fiber_bundle F ⇑f *ᵖ E
Equations
- fiber_bundle.pullback f = {total_space_mk_inducing := _, trivialization_atlas := {ef : trivialization F bundle.total_space.proj | ∃ (e : trivialization F bundle.total_space.proj) [_inst_9 : mem_trivialization_atlas e], ef = e.pullback f}, trivialization_at := λ (x : B'), (fiber_bundle.trivialization_at F E (⇑f x)).pullback f, mem_base_set_trivialization_at := _, trivialization_mem_atlas := _}