# Documentation

Mathlib.Topology.FiberBundle.Constructions

# Standard constructions on fiber bundles #

This file contains several standard constructions on fiber bundles:

• Bundle.Trivial.fiberBundle 𝕜 B F: the trivial fiber bundle with model fiber F over the base B

• FiberBundle.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 fun x ↦ E₁ x × E₂ x).

• FiberBundle.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 #

instance Bundle.Trivial.topologicalSpace (B : Type u_1) (F : Type u_2) [t₁ : ] [t₂ : ] :
theorem Bundle.Trivial.inducing_toProd (B : Type u_1) (F : Type u_2) [] [] :
def Bundle.Trivial.homeomorphProd (B : Type u_1) (F : Type u_2) [] [] :
≃ₜ B × F

Homeomorphism between the total space of the trivial bundle and the Cartesian product.

Instances For
def Bundle.Trivial.trivialization (B : Type u_1) (F : Type u_2) [] [] :
Trivialization F Bundle.TotalSpace.proj

Local trivialization for trivial bundle.

Instances For
@[simp]
theorem Bundle.Trivial.trivialization_source (B : Type u_1) (F : Type u_2) [] [] :
().toLocalHomeomorph.toLocalEquiv.source = Set.univ
@[simp]
theorem Bundle.Trivial.trivialization_target (B : Type u_1) (F : Type u_2) [] [] :
().toLocalHomeomorph.toLocalEquiv.target = Set.univ
instance Bundle.Trivial.fiberBundle (B : Type u_1) (F : Type u_2) [] [] :

Fiber bundle instance on the trivial bundle.

theorem Bundle.Trivial.eq_trivialization (B : Type u_1) (F : Type u_2) [] [] (e : Trivialization F Bundle.TotalSpace.proj) [i : ] :

### Fibrewise product of two bundles #

instance FiberBundle.Prod.topologicalSpace {B : Type u_1} (F₁ : Type u_2) (E₁ : BType u_3) (F₂ : Type u_4) (E₂ : BType u_5) [] [] :
TopologicalSpace (Bundle.TotalSpace (F₁ × F₂) fun x => 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 TotalSpace F₁ E₁ × TotalSpace F₂ E₂.

theorem FiberBundle.Prod.inducing_diag {B : Type u_1} (F₁ : Type u_2) (E₁ : BType u_3) (F₂ : Type u_4) (E₂ : BType u_5) [] [] :
Inducing fun p => ({ 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 TotalSpace F₁ E₁ × TotalSpace F₂ E₂ is Inducing.

def Trivialization.Prod.toFun' {B : Type u_1} [] {F₁ : Type u_2} [] {E₁ : BType u_3} [] {F₂ : Type u_4} [] {E₂ : BType u_5} [] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) :
(Bundle.TotalSpace (F₁ × F₂) fun x => 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₂.

Instances For
theorem Trivialization.Prod.continuous_to_fun {B : Type u_1} [] {F₁ : Type u_2} [] {E₁ : BType u_3} [] {F₂ : Type u_4} [] {E₂ : BType u_5} [] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Trivialization F₂ Bundle.TotalSpace.proj} :
ContinuousOn () (Bundle.TotalSpace.proj ⁻¹' (e₁.baseSet e₂.baseSet))
noncomputable def Trivialization.Prod.invFun' {B : Type u_1} [] {F₁ : Type u_2} [] {E₁ : BType u_3} [] {F₂ : Type u_4} [] {E₂ : BType u_5} [] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) [(x : B) → Zero (E₁ x)] [(x : B) → Zero (E₂ x)] (p : B × F₁ × F₂) :
Bundle.TotalSpace (F₁ × F₂) fun x => 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₂.

Instances For
theorem Trivialization.Prod.left_inv {B : Type u_1} [] {F₁ : Type u_2} [] {E₁ : BType u_3} [] {F₂ : Type u_4} [] {E₂ : BType u_5} [] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Trivialization F₂ Bundle.TotalSpace.proj} [(x : B) → Zero (E₁ x)] [(x : B) → Zero (E₂ x)] {x : Bundle.TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x} (h : x Bundle.TotalSpace.proj ⁻¹' (e₁.baseSet e₂.baseSet)) :
theorem Trivialization.Prod.right_inv {B : Type u_1} [] {F₁ : Type u_2} [] {E₁ : BType u_3} [] {F₂ : Type u_4} [] {E₂ : BType u_5} [] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Trivialization F₂ Bundle.TotalSpace.proj} [(x : B) → Zero (E₁ x)] [(x : B) → Zero (E₂ x)] {x : B × F₁ × F₂} (h : x (e₁.baseSet e₂.baseSet) ×ˢ Set.univ) :
theorem Trivialization.Prod.continuous_inv_fun {B : Type u_1} [] {F₁ : Type u_2} [] {E₁ : BType u_3} [] {F₂ : Type u_4} [] {E₂ : BType u_5} [] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Trivialization F₂ Bundle.TotalSpace.proj} [(x : B) → Zero (E₁ x)] [(x : B) → Zero (E₂ x)] :
ContinuousOn () ((e₁.baseSet e₂.baseSet) ×ˢ Set.univ)
noncomputable def Trivialization.prod {B : Type u_1} [] {F₁ : Type u_2} [] {E₁ : BType u_3} [] {F₂ : Type u_4} [] {E₂ : BType u_5} [] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) [(x : B) → Zero (E₁ x)] [(x : B) → Zero (E₂ x)] :
Trivialization (F₁ × F₂) Bundle.TotalSpace.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₁.baseSet ∩ e₂.baseSet.

Instances For
@[simp]
theorem Trivialization.baseSet_prod {B : Type u_1} [] {F₁ : Type u_2} [] {E₁ : BType u_3} [] {F₂ : Type u_4} [] {E₂ : BType u_5} [] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) [(x : B) → Zero (E₁ x)] [(x : B) → Zero (E₂ x)] :
().baseSet = e₁.baseSet e₂.baseSet
theorem Trivialization.prod_symm_apply {B : Type u_1} [] {F₁ : Type u_2} [] {E₁ : BType u_3} [] {F₂ : Type u_4} [] {E₂ : BType u_5} [] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) [(x : B) → Zero (E₁ x)] [(x : B) → Zero (E₂ x)] (x : B) (w₁ : F₁) (w₂ : F₂) :
↑(LocalEquiv.symm ().toLocalHomeomorph.toLocalEquiv) (x, w₁, w₂) = { proj := x, snd := (Trivialization.symm e₁ x w₁, Trivialization.symm e₂ x w₂) }
noncomputable instance FiberBundle.prod {B : Type u_1} [] (F₁ : Type u_2) [] (E₁ : BType u_3) [] (F₂ : Type u_4) [] (E₂ : BType u_5) [] [(x : B) → Zero (E₁ x)] [(x : B) → Zero (E₂ x)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₁ E₁] [FiberBundle F₂ E₂] :
FiberBundle (F₁ × F₂) fun x => E₁ x × E₂ x

The product of two fiber bundles is a fiber bundle.

instance instMemTrivializationAtlasProdInstTopologicalSpaceProdProdTopologicalSpaceInstTopologicalSpaceProdProdProd {B : Type u_1} [] (F₁ : Type u_2) [] (E₁ : BType u_3) [] (F₂ : Type u_4) [] (E₂ : BType u_5) [] [(x : B) → Zero (E₁ x)] [(x : B) → Zero (E₂ x)] [(x : B) → TopologicalSpace (E₁ x)] [(x : B) → TopologicalSpace (E₂ x)] [FiberBundle F₁ E₁] [FiberBundle F₂ E₂] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Trivialization F₂ Bundle.TotalSpace.proj} :

### Pullbacks of fiber bundles #

instance instForAllTopologicalSpacePullback {B : Type u} (E : BType w₁) {B' : Type w₂} (f : B'B) [(x : B) → TopologicalSpace (E x)] (x : B') :
theorem pullbackTopology_def {B : Type u_1} (F : Type u_2) (E : BType u_3) {B' : Type u_4} (f : B'B) [] [] :
= TopologicalSpace.induced Bundle.TotalSpace.proj inst✝
@[irreducible]
def pullbackTopology {B : Type u_1} (F : Type u_2) (E : BType u_3) {B' : Type u_4} (f : B'B) [] [] :

Definition of Pullback.TotalSpace.topologicalSpace, which we make irreducible.

Instances For
instance Pullback.TotalSpace.topologicalSpace {B : Type u} (F : Type v) (E : BType w₁) {B' : Type w₂} (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.

theorem Pullback.continuous_proj {B : Type u} (F : Type v) (E : BType w₁) {B' : Type w₂} [] [] (f : B'B) :
Continuous Bundle.TotalSpace.proj
theorem Pullback.continuous_lift {B : Type u} (F : Type v) (E : BType w₁) {B' : Type w₂} [] [] (f : B'B) :
theorem inducing_pullbackTotalSpaceEmbedding {B : Type u} (F : Type v) (E : BType w₁) {B' : Type w₂} [] [] (f : B'B) :
theorem Pullback.continuous_totalSpaceMk {B : Type u} (F : Type v) (E : BType w₁) {B' : Type w₂} [] [] [] [] [(x : B) → TopologicalSpace (E x)] [] {f : B'B} {x : B'} :
noncomputable def Trivialization.pullback {B : Type u} {F : Type v} {E : BType w₁} {B' : Type w₂} [] [] [] [] [(_b : B) → Zero (E _b)] {K : Type U} [] (e : Trivialization F Bundle.TotalSpace.proj) (f : K) :
Trivialization F Bundle.TotalSpace.proj

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

Instances For
noncomputable instance FiberBundle.pullback {B : Type u} {F : Type v} {E : BType w₁} {B' : Type w₂} [] [] [] [] [(_b : B) → Zero (E _b)] {K : Type U} [] [(x : B) → TopologicalSpace (E x)] [] (f : K) :
FiberBundle F (f *ᵖ E)