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 #

@[simp, reducible]
def bundle.total_space.proj {B : Type u_1} {E : B Type u_2} :

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

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

Constructor for the total space of a bundle.

Equations
theorem bundle.total_space.proj_mk {B : Type u_1} {E : B Type u_2} {x : B} {y : E x} :
theorem bundle.sigma_mk_eq_total_space_mk {B : Type u_1} {E : B Type u_2} {x : B} {y : E x} :
theorem bundle.total_space.mk_cast {B : Type u_1} {E : B Type u_2} {x x' : B} (h : x = x') (b : E x) :
theorem bundle.total_space.eta {B : Type u_1} {E : B Type u_2} (z : bundle.total_space E) :
@[protected, instance]
def bundle.total_space.has_coe_t {B : Type u_1} {E : B Type u_2} {x : B} :
Equations
@[simp]
theorem bundle.coe_fst {B : Type u_1} {E : B Type u_2} (x : B) (v : E x) :
v.fst = x
@[simp]
theorem bundle.coe_snd {B : Type u_1} {E : B Type u_2} {x : B} {y : E x} :
y.snd = y
theorem bundle.to_total_space_coe {B : Type u_1} {E : B Type u_2} {x : B} (v : E x) :
@[protected, instance]
def bundle.trivial.inhabited {B : Type u_1} {F : Type u_2} [inhabited F] {b : B} :
Equations

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

Equations
@[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
@[simp]
def bundle.pullback_total_space_embedding {B : Type u_1} {E : B Type u_2} {B' : Type u_3} (f : B' B) :

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

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

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

Equations
@[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)) :
@[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)) :
@[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
@[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
@[protected, instance]
Equations
@[protected, instance]
def bundle.trivial.add_comm_group {B : Type u_1} {F : Type u_3} (b : B) [add_comm_group F] :
Equations
@[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] :
Equations