mathlib3 documentation

data.bundle

Bundle #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. Basic data structure to implement fiber bundles, vector bundles (maybe fibrations?), etc. This file should contain all possible results that do not involve any topology.

We represent a bundle E over a base space B as a dependent type E : B → Type*.

We define bundle.total_space F E to be the type of pairs ⟨b, x⟩, where b : B and x : E x. This type is isomorphic to Σ x, E x and uses an extra argument F for reasons explained below. In general, the constructions of fiber bundles we will make will be of this form.

Main Definitions #

bundle.total_space the total space of a bundle.
bundle.total_space.proj the projection from the total space to the base space.
bundle.total_space.mk the constructor for the total space.

Implementation Notes #

We use a custom structure for the total space of a bundle instead of using a type synonym for the canonical disjoint union Σ x, E x because the total space usually has a different topology and Lean 4 simp fails to apply lemmas about Σ x, E x to elements of the total space.
The definition of bundle.total_space has an unused argument F. The reason is that in some constructions (e.g., bundle.continuous_linear_map.vector_bundle) we need access to the atlas of trivializations of original fiber bundles to construct the topology on the total space of the new fiber bundle.

References #

https://en.wikipedia.org/wiki/Bundle_(mathematics)

@[ext]

structure bundle.total_space {B : Type u_1} (F : Type u_4) (E : B → Type u_5) :

Type (max u_1 u_5)

proj : B
snd : E self.proj

bundle.total_space E is the total space of the bundle. It consists of pairs (proj : B, snd : E proj).

Instances for bundle.total_space

theorem bundle.total_space.ext {B : Type u_1} {F : Type u_4} {E : B → Type u_5} (x y : bundle.total_space F E) (h : x.proj = y.proj) (h_1 : x.snd == y.snd) :

x = y

theorem bundle.total_space.ext_iff {B : Type u_1} {F : Type u_4} {E : B → Type u_5} (x y : bundle.total_space F E) :

x = y ↔ x.proj = y.proj ∧ x.snd == y.snd

@[protected, instance]

def bundle.total_space.inhabited {B : Type u_1} {F : Type u_2} (E : B → Type u_3) [inhabited B] [inhabited (E inhabited.default)] :

inhabited (bundle.total_space F E)

Equations

bundle.total_space.inhabited E = {default := {proj := inhabited.default _inst_1, snd := inhabited.default _inst_2}}

theorem bundle.total_space.mk_cast {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {x x' : B} (h : x = x') (b : E x) :

{proj := x', snd := cast _ b} = {proj := x, snd := b}

@[protected, instance]

def bundle.total_space.has_coe_t {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {x : B} :

has_coe_t (E x) (bundle.total_space F E)

Equations

bundle.total_space.has_coe_t = {coe := bundle.total_space.mk x}

@[simp]

theorem bundle.total_space.coe_proj {B : Type u_1} {F : Type u_2} {E : B → Type u_3} (x : B) (v : E x) :

@[simp]

theorem bundle.total_space.coe_snd {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {x : B} {y : E x} :

theorem bundle.total_space.coe_eq_mk {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {x : B} (v : E x) :

↑v = {proj := x, snd := v}

theorem bundle.total_space.eta {B : Type u_1} {F : Type u_2} {E : B → Type u_3} (z : bundle.total_space F E) :

{proj := z.proj, snd := z.snd} = z

@[nolint, reducible]

def bundle.trivial (B : Type u_1) (F : Type u_2) :

B → Type u_2

bundle.trivial B F is the trivial bundle over B of fiber F.

Equations

bundle.trivial B F = λ (_x : B), F

def bundle.total_space.trivial_snd (B : Type u_1) (F : Type u_2) :

bundle.total_space F (bundle.trivial B F) → F

The trivial bundle, unlike other bundles, has a canonical projection on the fiber.

Equations

bundle.total_space.trivial_snd B F = bundle.total_space.snd

def bundle.total_space.to_prod (B : Type u_1) (F : Type u_2) :

bundle.total_space F (λ (_x : B), F) ≃ B × F

A trivial bundle is equivalent to the product B × F.

Equations

bundle.total_space.to_prod B F = {to_fun := λ (x : bundle.total_space F (λ (_x : B), F)), (x.proj, x.snd), inv_fun := λ (x : B × F), {proj := x.fst, snd := x.snd}, left_inv := _, right_inv := _}

@[simp]

theorem bundle.total_space.to_prod_symm_apply_proj (B : Type u_1) (F : Type u_2) (x : B × F) :

(⇑((bundle.total_space.to_prod B F).symm) x).proj = x.fst

@[simp]

theorem bundle.total_space.to_prod_symm_apply_snd (B : Type u_1) (F : Type u_2) (x : B × F) :

(⇑((bundle.total_space.to_prod B F).symm) x).snd = x.snd

@[simp]

theorem bundle.total_space.to_prod_apply (B : Type u_1) (F : Type u_2) (x : bundle.total_space F (λ (_x : B), F)) :

⇑(bundle.total_space.to_prod B F) x = (x.proj, x.snd)

def bundle.pullback {B : Type u_1} {B' : Type u_4} (f : B' → B) (E : B → Type u_2) :

B' → Type u_2

The pullback of a bundle E over a base B under a map f : B' → B, denoted by pullback f E or f *ᵖ E, is the bundle over B' whose fiber over b' is E (f b').

Equations

f *ᵖ E = λ (x : B'), E (f x)

Instances for bundle.pullback

@[protected, instance]

def bundle.pullback.nonempty {B : Type u_1} {E : B → Type u_3} {B' : Type u_4} {f : B' → B} {x : B'} [nonempty (E (f x))] :

nonempty (f *ᵖ E x)

@[simp]

def bundle.pullback_total_space_embedding {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {B' : Type u_4} (f : B' → B) :

bundle.total_space F f *ᵖ E → B' × bundle.total_space F E

Natural embedding of the total space of f *ᵖ E into B' × total_space E.

Equations

bundle.pullback_total_space_embedding f = λ (z : bundle.total_space F f *ᵖ E), (z.proj, {proj := f z.proj, snd := z.snd})

def bundle.pullback.lift {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {B' : Type u_4} (f : B' → B) :

bundle.total_space F f *ᵖ E → bundle.total_space F E

The base map f : B' → B lifts to a canonical map on the total spaces.

Equations

bundle.pullback.lift f = λ (z : bundle.total_space F f *ᵖ E), {proj := f z.proj, snd := z.snd}

@[simp]

theorem bundle.pullback.lift_snd {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {B' : Type u_4} (f : B' → B) (ᾰ : bundle.total_space F f *ᵖ E) :

(bundle.pullback.lift f ᾰ).snd = ᾰ.snd

@[simp]

theorem bundle.pullback.lift_proj {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {B' : Type u_4} (f : B' → B) (ᾰ : bundle.total_space F f *ᵖ E) :

(bundle.pullback.lift f ᾰ).proj = f ᾰ.proj

@[simp]

theorem bundle.pullback.lift_mk {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {B' : Type u_4} (f : B' → B) (x : B') (y : E (f x)) :

bundle.pullback.lift f {proj := x, snd := y} = {proj := f x, snd := y}

@[simp]

theorem bundle.coe_snd_map_apply {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [Π (x : B), has_add (E x)] (x : B) (v w : E x) :

↑(v + w).snd = ↑v.snd + ↑w.snd

@[simp]

theorem bundle.coe_snd_map_smul {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {R : Type u_4} [Π (x : B), has_smul R (E x)] (x : B) (r : R) (v : E x) :

↑(r • v).snd = r • ↑v.snd