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₁ : TopologicalSpace B] [t₂ : TopologicalSpace F] :

TopologicalSpace (TotalSpace F (Trivial B F))

Equations

Bundle.Trivial.topologicalSpace B F = TopologicalSpace.induced Bundle.TotalSpace.proj t₁ ⊓ TopologicalSpace.induced (Bundle.TotalSpace.trivialSnd B F) t₂

source

theorem Bundle.Trivial.isInducing_toProd (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] :

Topology.IsInducing ⇑(TotalSpace.toProd B F)

source

def Bundle.Trivial.homeomorphProd (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] :

TotalSpace F (Trivial B F) ≃ₜ B × F

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

Equations

Bundle.Trivial.homeomorphProd B F = (Bundle.TotalSpace.toProd B F).toHomeomorphOfIsInducing ⋯

Instances For

source

@[simp]

theorem Bundle.Trivial.homeomorphProd_apply (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] (x : TotalSpace F fun (x : B) => F) :

(homeomorphProd B F) x = (x.proj, x.snd)

source

@[simp]

theorem Bundle.Trivial.homeomorphProd_symm_apply_proj (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] (x : B × F) :

((homeomorphProd B F).symm x).proj = x.1

source

@[simp]

theorem Bundle.Trivial.homeomorphProd_symm_apply_snd (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] (x : B × F) :

((homeomorphProd B F).symm x).snd = x.2

source

def Bundle.Trivial.trivialization (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] :

Trivialization F TotalSpace.proj

Local trivialization for trivial bundle.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Bundle.Trivial.trivialization_baseSet (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] :

(trivialization B F).baseSet = Set.univ

source

@[simp]

theorem Bundle.Trivial.trivialization_apply (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] (a : TotalSpace F (Trivial B F)) :

↑(trivialization B F) a = (a.proj, a.snd)

source

@[simp]

theorem Bundle.Trivial.trivialization_source (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] :

(trivialization B F).source = Set.univ

source

@[simp]

theorem Bundle.Trivial.trivialization_symm_apply_proj (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] (a : B × F) :

(↑(trivialization B F).symm a).proj = a.1

source

@[simp]

theorem Bundle.Trivial.trivialization_target (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] :

(trivialization B F).target = Set.univ

source

@[simp]

theorem Bundle.Trivial.trivialization_symm_apply_snd (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] (a : B × F) :

(↑(trivialization B F).symm a).snd = a.2

source

@[simp]

theorem Bundle.Trivial.trivialization_symm_apply (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] [Zero F] (b : B) (f : F) :

(trivialization B F).symm b f = f

source

@[simp]

theorem Bundle.Trivial.toOpenPartialHomeomorph_trivialization_symm_apply (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] (v : B × F) :

↑(trivialization B F).symm v = { proj := v.1, snd := v.2 }

source

instance Bundle.Trivial.fiberBundle (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] :

FiberBundle F (Trivial B F)

Fiber bundle instance on the trivial bundle.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem Bundle.Trivial.fiberBundle_trivializationAt' (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] (x✝ : B) :

FiberBundle.trivializationAt' x✝ = trivialization B F

source

@[simp]

theorem Bundle.Trivial.fiberBundle_trivializationAtlas' (B : Type u_1) (F : Type u_2) [TopologicalSpace B] [TopologicalSpace F] :

FiberBundle.trivializationAtlas' = {trivialization B F}

source

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

e = trivialization B F

Fibrewise product of two bundles #

source

instance FiberBundle.Prod.topologicalSpace {B : Type u_1} (F₁ : Type u_2) (E₁ : B → Type u_3) (F₂ : Type u_4) (E₂ : B → Type u_5) [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] :

TopologicalSpace (Bundle.TotalSpace (F₁ × F₂) fun (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 TotalSpace F₁ E₁ × TotalSpace F₂ E₂.

Equations

One or more equations did not get rendered due to their size.

source

theorem FiberBundle.Prod.isInducing_diag {B : Type u_1} (F₁ : Type u_2) (E₁ : B → Type u_3) (F₂ : Type u_4) (E₂ : B → Type u_5) [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] :

Topology.IsInducing fun (p : Bundle.TotalSpace (F₁ × F₂) fun (x : B) => E₁ x × E₂ x) => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })

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 an inducing map.

source

def Trivialization.Prod.toFun' {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [TopologicalSpace F₂] {E₂ : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) :

(Bundle.TotalSpace (F₁ × F₂) fun (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

Trivialization.Prod.toFun' e₁ e₂ p = (p.proj, (↑e₁ { proj := p.proj, snd := p.snd.1 }).2, (↑e₂ { proj := p.proj, snd := p.snd.2 }).2)

Instances For

source

theorem Trivialization.Prod.continuous_to_fun {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [TopologicalSpace F₂] {E₂ : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] {e₁ : Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Trivialization F₂ Bundle.TotalSpace.proj} :

ContinuousOn (toFun' e₁ e₂) (Bundle.TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))

source

noncomputable def Trivialization.Prod.invFun' {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [TopologicalSpace F₂] {E₂ : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] (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 : 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

Trivialization.Prod.invFun' e₁ e₂ p = { proj := p.1, snd := (e₁.symm p.1 p.2.1, e₂.symm p.1 p.2.2) }

Instances For

source

theorem Trivialization.Prod.left_inv {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [TopologicalSpace F₂] {E₂ : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] {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 : B) => E₁ x × E₂ x} (h : x ∈ Bundle.TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet)) :

invFun' e₁ e₂ (toFun' e₁ e₂ x) = x

source

theorem Trivialization.Prod.right_inv {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [TopologicalSpace F₂] {E₂ : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] {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) :

toFun' e₁ e₂ (invFun' e₁ e₂ x) = x

source

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

ContinuousOn (invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ Set.univ)

source

noncomputable def Trivialization.prod {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [TopologicalSpace F₂] {E₂ : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] (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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

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

(e₁.prod e₂).target = (e₁.baseSet ∩ e₂.baseSet) ×ˢ Set.univ

source

@[simp]

theorem Trivialization.prod_symm_apply_snd {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [TopologicalSpace F₂] {E₂ : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] (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₂) :

(↑(e₁.prod e₂).symm p).snd = (e₁.symm p.1 p.2.1, e₂.symm p.1 p.2.2)

source

@[simp]

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

(e₁.prod e₂).source = Bundle.TotalSpace.proj ⁻¹' e₁.baseSet ∩ Bundle.TotalSpace.proj ⁻¹' e₂.baseSet

source

@[simp]

theorem Trivialization.prod_symm_apply_proj {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [TopologicalSpace F₂] {E₂ : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] (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₂) :

(↑(e₁.prod e₂).symm p).proj = p.1

source

@[simp]

theorem Trivialization.prod_apply {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [TopologicalSpace F₂] {E₂ : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) [(x : B) → Zero (E₁ x)] [(x : B) → Zero (E₂ x)] (a✝ : Bundle.TotalSpace (F₁ × F₂) fun (x : B) => E₁ x × E₂ x) :

↑(e₁.prod e₂) a✝ = Prod.toFun' e₁ e₂ a✝

source

@[simp]

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

(e₁.prod e₂).baseSet = e₁.baseSet ∩ e₂.baseSet

source

@[deprecated Trivialization.prod_baseSet (since := "2025-06-19")]

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

(e₁.prod e₂).baseSet = e₁.baseSet ∩ e₂.baseSet

Alias of Trivialization.prod_baseSet.

source

theorem Trivialization.prod_symm_apply {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_2} [TopologicalSpace F₁] {E₁ : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [TopologicalSpace F₂] {E₂ : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] (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₂) :

↑(e₁.prod e₂).symm (x, w₁, w₂) = { proj := x, snd := (e₁.symm x w₁, e₂.symm x w₂) }

source

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

The product of two fiber bundles is a fiber bundle.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem FiberBundle.prod_trivializationAt' {B : Type u_1} [TopologicalSpace B] (F₁ : Type u_2) [TopologicalSpace F₁] (E₁ : B → Type u_3) [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] (F₂ : Type u_4) [TopologicalSpace F₂] (E₂ : B → Type u_5) [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(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₂] (b : B) :

trivializationAt' b = (trivializationAt F₁ E₁ b).prod (trivializationAt F₂ E₂ b)

source

@[simp]

theorem FiberBundle.prod_trivializationAtlas' {B : Type u_1} [TopologicalSpace B] (F₁ : Type u_2) [TopologicalSpace F₁] (E₁ : B → Type u_3) [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] (F₂ : Type u_4) [TopologicalSpace F₂] (E₂ : B → Type u_5) [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(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₂] :

trivializationAtlas' = {e : Trivialization (F₁ × F₂) Bundle.TotalSpace.proj | ∃ (e₁ : Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Trivialization F₂ Bundle.TotalSpace.proj) (_ : MemTrivializationAtlas e₁) (_ : MemTrivializationAtlas e₂), e = e₁.prod e₂}

source

instance instMemTrivializationAtlasProdProd {B : Type u_1} [TopologicalSpace B] (F₁ : Type u_2) [TopologicalSpace F₁] (E₁ : B → Type u_3) [TopologicalSpace (Bundle.TotalSpace F₁ E₁)] (F₂ : Type u_4) [TopologicalSpace F₂] (E₂ : B → Type u_5) [TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [(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} [MemTrivializationAtlas e₁] [MemTrivializationAtlas e₂] :

MemTrivializationAtlas (e₁.prod e₂)

Pullbacks of fiber bundles #

source

instance instTopologicalSpacePullback {B : Type u} (E : B → Type w₁) {B' : Type w₂} (f : B' → B) [(x : B) → TopologicalSpace (E x)] (x : B') :

TopologicalSpace ((f *ᵖ E) x)

Equations

instTopologicalSpacePullback E f = inferInstanceAs ((x : B') → TopologicalSpace (E (f x)))

source

@[irreducible]

def pullbackTopology {B : Type u_1} (F : Type u_2) (E : B → Type u_3) {B' : Type u_4} (f : B' → B) [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] :

TopologicalSpace (Bundle.TotalSpace F (f *ᵖ E))

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

Equations

pullbackTopology F E f = TopologicalSpace.induced Bundle.TotalSpace.proj inst✝¹ ⊓ TopologicalSpace.induced (Bundle.Pullback.lift f) inst✝

Instances For

source

theorem pullbackTopology_def {B : Type u_1} (F : Type u_2) (E : B → Type u_3) {B' : Type u_4} (f : B' → B) [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] :

pullbackTopology F E f = TopologicalSpace.induced Bundle.TotalSpace.proj inst✝ ⊓ TopologicalSpace.induced (Bundle.Pullback.lift f) inst✝¹

source

instance Pullback.TotalSpace.topologicalSpace {B : Type u} (F : Type v) (E : B → Type w₁) {B' : Type w₂} (f : B' → B) [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] :

TopologicalSpace (Bundle.TotalSpace 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.TotalSpace.topologicalSpace F E f = pullbackTopology F E f

source

theorem Pullback.continuous_proj {B : Type u} (F : Type v) (E : B → Type w₁) {B' : Type w₂} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] (f : B' → B) :

Continuous Bundle.TotalSpace.proj

source

theorem Pullback.continuous_lift {B : Type u} (F : Type v) (E : B → Type w₁) {B' : Type w₂} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] (f : B' → B) :

Continuous (Bundle.Pullback.lift f)

source

theorem inducing_pullbackTotalSpaceEmbedding {B : Type u} (F : Type v) (E : B → Type w₁) {B' : Type w₂} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] (f : B' → B) :

Topology.IsInducing (Bundle.pullbackTotalSpaceEmbedding f)

source

theorem Pullback.continuous_totalSpaceMk {B : Type u} (F : Type v) (E : B → Type w₁) {B' : Type w₂} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] {f : B' → B} {x : B'} :

Continuous (Bundle.TotalSpace.mk x)

source

noncomputable def Trivialization.pullback {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(_b : B) → Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass K B' B] (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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Trivialization.pullback_symm_apply_snd {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(_b : B) → Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass K B' B] (e : Trivialization F Bundle.TotalSpace.proj) (f : K) (y : B' × F) :

(↑(e.pullback f).symm y).snd = e.symm (f y.1) y.2

source

@[simp]

theorem Trivialization.pullback_symm_apply_proj {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(_b : B) → Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass K B' B] (e : Trivialization F Bundle.TotalSpace.proj) (f : K) (y : B' × F) :

(↑(e.pullback f).symm y).proj = y.1

source

@[simp]

theorem Trivialization.pullback_baseSet {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(_b : B) → Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass K B' B] (e : Trivialization F Bundle.TotalSpace.proj) (f : K) :

(e.pullback f).baseSet = ⇑f ⁻¹' e.baseSet

source

@[simp]

theorem Trivialization.pullback_target {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(_b : B) → Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass K B' B] (e : Trivialization F Bundle.TotalSpace.proj) (f : K) :

(e.pullback f).target = (⇑f ⁻¹' e.baseSet) ×ˢ Set.univ

source

@[simp]

theorem Trivialization.pullback_source {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(_b : B) → Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass K B' B] (e : Trivialization F Bundle.TotalSpace.proj) (f : K) :

(e.pullback f).source = Bundle.Pullback.lift ⇑f ⁻¹' e.source

source

@[simp]

theorem Trivialization.pullback_apply {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(_b : B) → Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass K B' B] (e : Trivialization F Bundle.TotalSpace.proj) (f : K) (z : Bundle.TotalSpace F (⇑f *ᵖ E)) :

↑(e.pullback f) z = (z.proj, (↑e (Bundle.Pullback.lift (⇑f) z)).2)

source

noncomputable instance FiberBundle.pullback {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(_b : B) → Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass K B' B] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (f : K) :

FiberBundle F (⇑f *ᵖ E)

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem FiberBundle.pullback_trivializationAtlas' {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(_b : B) → Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass K B' B] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (f : K) :

trivializationAtlas' = {ef : Trivialization F Bundle.TotalSpace.proj | ∃ (e : Trivialization F Bundle.TotalSpace.proj) (_ : MemTrivializationAtlas e), ef = e.pullback f}

source

@[simp]

theorem FiberBundle.pullback_trivializationAt' {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [TopologicalSpace B'] [TopologicalSpace (Bundle.TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [(_b : B) → Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass K B' B] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (f : K) (x : B') :

trivializationAt' x = (trivializationAt F E (f x)).pullback f

Documentation

Mathlib.Topology.FiberBundle.Constructions

Standard constructions on fiber bundles #

Tags #

The trivial bundle #

Fibrewise product of two bundles #

Pullbacks of fiber bundles #