mathlib3 documentation

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:

Tags #

fiber bundle, fibre bundle, fiberwise product, pullback

The trivial bundle #

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} (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
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₂)] :
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} [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) :
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
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₂.

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

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} [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)] :
(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 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₂) :
((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} [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
@[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₂] :

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
@[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)] :

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

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
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 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
Instances for trivialization.pullback