# mathlib3documentation

topology.fiber_bundle.constructions

# 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 fiber F over the base B

• fiber_bundle.prod: for fiber bundles E₁ and E₂ over a common base, a fiber bundle structure on their fiberwise product E₁ ×ᵇ E₂ (the notation stands for λ x, E₁ x × E₂ x).

• fiber_bundle.pullback: for a fiber bundle E over B, a fiber bundle structure on its pullback f *ᵖ E by a map f : B' → B (the notation is a type synonym for E ∘ f).

## Tags #

fiber bundle, fibre bundle, fiberwise product, pullback

### The trivial bundle #

@[protected, instance]
Equations
def bundle.trivial.trivialization (B : Type u_1) (F : Type u_2)  :

Local trivialization for trivial bundle.

Equations
Instances for bundle.trivial.trivialization
@[simp]
theorem bundle.trivial.trivialization_source (B : Type u_1) (F : Type u_2)  :
@[simp]
theorem bundle.trivial.trivialization_target (B : Type u_1) (F : Type u_2)  :
@[protected, instance]
def bundle.trivial.fiber_bundle (B : Type u_1) (F : Type u_2)  :
F)

Fiber bundle instance on the trivial bundle.

Equations

### 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 E₁)] [topological_space 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
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 E₁)] [topological_space E₂)] :
inducing (λ (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}))

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

Equations
theorem trivialization.prod.continuous_to_fun {B : Type u_1} {F₁ : Type u_2} {E₁ : B Type u_3} [topological_space E₁)] {F₂ : Type u_4} {E₂ : B Type u_5} [topological_space E₂)]  :
noncomputable def trivialization.prod.inv_fun' {B : Type u_1} {F₁ : Type u_2} {E₁ : B Type u_3} [topological_space E₁)] {F₂ : Type u_4} {E₂ : B Type u_5} [topological_space E₂)] [Π (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₂.

Equations
theorem trivialization.prod.left_inv {B : Type u_1} {F₁ : Type u_2} {E₁ : B Type u_3} [topological_space E₁)] {F₂ : Type u_4} {E₂ : B Type u_5} [topological_space E₂)] [Π (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 ) :
x) = x
theorem trivialization.prod.right_inv {B : Type u_1} {F₁ : Type u_2} {E₁ : B Type u_3} [topological_space E₁)] {F₂ : Type u_4} {E₂ : B Type u_5} [topological_space E₂)] [Π (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) :
x) = x
theorem trivialization.prod.continuous_inv_fun {B : Type u_1} {F₁ : Type u_2} {E₁ : B Type u_3} [topological_space E₁)] {F₂ : Type u_4} {E₂ : B Type u_5} [topological_space E₂)] [Π (x : B), has_zero (E₁ x)] [Π (x : B), has_zero (E₂ x)] :
noncomputable def trivialization.prod {B : Type u_1} {F₁ : Type u_2} {E₁ : B Type u_3} [topological_space E₁)] {F₂ : Type u_4} {E₂ : B Type u_5} [topological_space E₂)] [Π (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 fiberwise 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} {F₁ : Type u_2} {E₁ : B Type u_3} [topological_space E₁)] {F₂ : Type u_4} {E₂ : B Type u_5} [topological_space E₂)] [Π (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} {F₁ : Type u_2} {E₁ : B Type u_3} [topological_space E₁)] {F₂ : Type u_4} {E₂ : B Type u_5} [topological_space E₂)] [Π (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₂) = {proj := x, snd := (e₁.symm x w₁, e₂.symm x w₂)}
@[protected, instance]
noncomputable def fiber_bundle.prod {B : Type u_1} (F₁ : Type u_2) (E₁ : B Type u_3) [topological_space E₁)] (F₂ : Type u_4) (E₂ : B Type u_5) [topological_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)] [ E₁] [ 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} (F₁ : Type u_2) (E₁ : B Type u_3) [topological_space E₁)] (F₂ : Type u_4) (E₂ : B Type u_5) [topological_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)] [ E₁] [ 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') :
Equations
• = λ (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)  :

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

Equations
• f =
@[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)  :

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_1} (F : Type u_2) (E : B Type u_3) {B' : Type u_4} (f : B' B) :
theorem pullback.continuous_lift {B : Type u_1} (F : Type u_2) (E : B Type u_3) {B' : Type u_4} (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} (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} [Π (x : B), topological_space (E x)] [ 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} [Π (b : B), has_zero (E b)] {K : Type u_5} [ B] (f : K) :

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

Equations
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} [Π (b : B), has_zero (E b)] {K : Type u_5} [ B] [Π (x : B), topological_space (E x)] [ E] (f : K) :
f *ᵖ E
Equations