mathlib 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 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