mathlib documentation

data.bundle

Bundle #

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 provide a type synonym of Σ x, E x as bundle.total_space E, to be able to endow it with a topology which is not the disjoint union topology sigma.topological_space. In general, the constructions of fiber bundles we will make will be of this form.

Main Definitions #

References #

source
def bundle.total_space {B : Type u_1} (E : B → Type u_2) :
Type (max u_1 u_2)

bundle.total_space E is the total space of the bundle Σ x, E x. This type synonym is used to avoid conflicts with general sigma types.

Equations
Instances for bundle.total_space
source
@[protected, instance]
def bundle.total_space.inhabited {B : Type u_1} (E : B → Type u_2) [inhabited B] [inhabited (E inhabited.default)] :
inhabited (bundle.total_space E)
Equations
source
@[simp, reducible]
def bundle.total_space.proj {B : Type u_1} {E : B → Type u_2} :
bundle.total_space E → B

bundle.total_space.proj is the canonical projection bundle.total_space E → B from the total space to the base space.

Equations
source
@[simp, reducible]
def bundle.total_space_mk {B : Type u_1} {E : B → Type u_2} (b : B) (a : E b) :
bundle.total_space E

Constructor for the total space of a bundle.

Equations
source
theorem bundle.total_space.proj_mk {B : Type u_1} {E : B → Type u_2} {x : B} {y : E x} :
(bundle.total_space_mk x y).proj = x
source
theorem bundle.sigma_mk_eq_total_space_mk {B : Type u_1} {E : B → Type u_2} {x : B} {y : E x} :
⟨x, y⟩ = bundle.total_space_mk x y
source
theorem bundle.total_space.mk_cast {B : Type u_1} {E : B → Type u_2} {x x' : B} (h : x = x') (b : E x) :
bundle.total_space_mk x' (cast _ b) = bundle.total_space_mk x b
source
theorem bundle.total_space.eta {B : Type u_1} {E : B → Type u_2} (z : bundle.total_space E) :
bundle.total_space_mk z.proj z.snd = z
source
@[protected, instance]
def bundle.total_space.has_coe_t {B : Type u_1} {E : B → Type u_2} {x : B} :
has_coe_t (E x) (bundle.total_space E)
Equations
source
@[simp]
theorem bundle.coe_fst {B : Type u_1} {E : B → Type u_2} (x : B) (v : E x) :
↑v.fst = x
source
@[simp]
theorem bundle.coe_snd {B : Type u_1} {E : B → Type u_2} {x : B} {y : E x} :
↑y.snd = y
source
theorem bundle.to_total_space_coe {B : Type u_1} {E : B → Type u_2} {x : B} (v : E x) :
↑v = bundle.total_space_mk x v
source
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
Instances for bundle.trivial
source
@[protected, instance]
def bundle.trivial.inhabited {B : Type u_1} {F : Type u_2} [inhabited F] {b : B} :
inhabited (bundle.trivial B F b)
Equations
source
def bundle.trivial.proj_snd (B : Type u_1) (F : Type u_2) :
bundle.total_space (bundle.trivial B F) → F

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

Equations
source
@[nolint]
def bundle.pullback {B : Type u_1} {B' : Type u_3} (f : B' → B) (E : B → Type u_2) (x : 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
source
@[simp]
def bundle.pullback_total_space_embedding {B : Type u_1} {E : B → Type u_2} {B' : Type u_3} (f : B' → B) :
bundle.total_space (f *ᵖ E) → B' × bundle.total_space E

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

Equations
source
def bundle.pullback.lift {B : Type u_1} {E : B → Type u_2} {B' : Type u_3} (f : B' → B) :
bundle.total_space (f *ᵖ E) → bundle.total_space E

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

Equations
source
@[simp]
theorem bundle.pullback.proj_lift {B : Type u_1} {E : B → Type u_2} {B' : Type u_3} (f : B' → B) (x : bundle.total_space (f *ᵖ E)) :
(bundle.pullback.lift f x).proj = f x.fst
source
@[simp]
theorem bundle.pullback.lift_mk {B : Type u_1} {E : B → Type u_2} {B' : Type u_3} (f : B' → B) (x : B') (y : E (f x)) :
bundle.pullback.lift f (bundle.total_space_mk x y) = bundle.total_space_mk (f x) y
source
theorem bundle.pullback_total_space_embedding_snd {B : Type u_1} {E : B → Type u_2} {B' : Type u_3} (f : B' → B) (x : bundle.total_space (f *ᵖ E)) :
(bundle.pullback_total_space_embedding f x).snd = bundle.pullback.lift f x
source
@[simp]
theorem bundle.coe_snd_map_apply {B : Type u_1} {E : B → Type u_2} [Π (x : B), add_comm_monoid (E x)] (x : B) (v w : E x) :
↑(v + w).snd = ↑v.snd + ↑w.snd
source
@[simp]
theorem bundle.coe_snd_map_smul {B : Type u_1} {E : B → Type u_2} [Π (x : B), add_comm_monoid (E x)] (R : Type u_3) [semiring R] [Π (x : B), module R (E x)] (x : B) (r : R) (v : E x) :
↑(r • v).snd = r • ↑v.snd
source
@[protected, instance]
def bundle.trivial.add_comm_monoid {B : Type u_1} {F : Type u_3} (b : B) [add_comm_monoid F] :
add_comm_monoid (bundle.trivial B F b)
Equations
source
@[protected, instance]
def bundle.trivial.add_comm_group {B : Type u_1} {F : Type u_3} (b : B) [add_comm_group F] :
add_comm_group (bundle.trivial B F b)
Equations
source
@[protected, instance]
def bundle.trivial.module {B : Type u_1} {F : Type u_3} {R : Type u_4} [semiring R] (b : B) [add_comm_monoid F] [module R F] :
module R (bundle.trivial B F b)
Equations