mathlib documentation

topology.fiber_bundle.constructions

Standard constructions on fiber bundles #

This file contains several standard constructions on fiber bundles:

Tags #

fiber bundle, fibre bundle, fiberwise product, pullback

The trivial bundle #

@[protected, instance]
Equations

Local trivialization for trivial bundle.

Equations
Instances for bundle.trivial.trivialization

Fibrewise product of two bundles #

@[protected, instance]
def fiber_bundle.prod.topological_space {B : Type u_1} (E₁ : B Type u_2) (E₂ : B Type u_3) [topological_space (bundle.total_space E₁)] [topological_space (bundle.total_space E₂)] :
topological_space (bundle.total_space (λ (x : B), E₁ x × E₂ x))

Equip the total space of the fibrewise product of two fiber bundles E₁, E₂ with the induced topology from the diagonal embedding into total_space E₁ × total_space E₂.

Equations
theorem fiber_bundle.prod.inducing_diag {B : Type u_1} (E₁ : B Type u_2) (E₂ : B Type u_3) [topological_space (bundle.total_space E₁)] [topological_space (bundle.total_space E₂)] :
inducing (λ (p : bundle.total_space (λ (x : B), E₁ x × E₂ x)), (p.fst, p.snd.fst, p.fst, p.snd.snd⟩))

The diagonal map from the total space of the fibrewise 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 E₁)] {F₂ : Type u_4} [topological_space F₂] {E₂ : B Type u_5} [topological_space (bundle.total_space E₂)] (e₁ : trivialization F₁ bundle.total_space.proj) (e₂ : trivialization F₂ bundle.total_space.proj) :
bundle.total_space (λ (x : B), E₁ x × E₂ x) B × F₁ × F₂

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 fibrewise product of E₁ and E₂.

Equations
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 E₁)] {F₂ : Type u_4} [topological_space F₂] {E₂ : B Type u_5} [topological_space (bundle.total_space 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 (λ (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 fibrewise product of E₁ and E₂.

Equations
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 E₁)] {F₂ : Type u_4} [topological_space F₂] {E₂ : B Type u_5} [topological_space (bundle.total_space 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 (λ (x : B), E₁ x × E₂ x)} (h : x bundle.total_space.proj ⁻¹' (e₁.base_set e₂.base_set)) :
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 E₁)] {F₂ : Type u_4} [topological_space F₂] {E₂ : B Type u_5} [topological_space (bundle.total_space 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) :
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 E₁)] {F₂ : Type u_4} [topological_space F₂] {E₂ : B Type u_5} [topological_space (bundle.total_space 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)] :
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 E₁)] {F₂ : Type u_4} [topological_space F₂] {E₂ : B Type u_5} [topological_space (bundle.total_space 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)] :

Given trivializations e₁, e₂ for bundle types E₁, E₂ over a base B, the induced trivialization for the fibrewise product of E₁ and E₂, whose base set is e₁.base_set ∩ e₂.base_set.

Equations
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 E₁)] {F₂ : Type u_4} [topological_space F₂] {E₂ : B Type u_5} [topological_space (bundle.total_space 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)] :
(e₁.prod e₂).base_set = e₁.base_set e₂.base_set
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 E₁)] {F₂ : Type u_4} [topological_space F₂] {E₂ : B Type u_5} [topological_space (bundle.total_space 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₂) :
((e₁.prod e₂).to_local_homeomorph.to_local_equiv.symm) (x, w₁, w₂) = x, (e₁.symm x w₁, e₂.symm x w₂)
@[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 E₁)] (F₂ : Type u_4) [topological_space F₂] (E₂ : B Type u_5) [topological_space (bundle.total_space 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
@[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 E₁)] (F₂ : Type u_4) [topological_space F₂] (E₂ : B Type u_5) [topological_space (bundle.total_space 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₂] :

Pullbacks of fibre 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') :
Equations
@[protected, instance]

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

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

Equations
Instances for trivialization.pullback