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

## References #

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

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
• = Σ (x : B), E x
@[instance]
def bundle.total_space.inhabited {B : Type u_1} (E : B → Type u_2) [inhabited B] [inhabited (E (default B))] :
Equations
@[simp]
def bundle.proj {B : Type u_1} (E : B → Type u_2) :
→ B

bundle.proj E is the canonical projection total_space E → B on the base space.

Equations
@[simp]
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 topological_fiber_bundle_core.

Equations
@[instance]
def bundle.total_space.has_coe_t {B : Type u_1} (E : B → Type u_2) {x : B} :
has_coe_t (E x)
Equations
@[simp]
theorem bundle.coe_fst {B : Type u_1} (E : B → Type u_2) (x : B) (v : E x) :
v.fst = x
theorem bundle.to_total_space_coe {B : Type u_1} (E : B → Type u_2) {x : B} (v : E x) :
v = x, v⟩
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
@[instance]
def bundle.trivial.inhabited {B : Type u_1} {F : Type u_2} [inhabited F] {b : B} :
Equations
def bundle.trivial.proj_snd (B : Type u_1) (F : Type u_2) :
→ F

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

Equations
@[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), (E x)] (x : B) (r : R) (v : E x) :
(r v).snd = r v.snd
@[instance]
def bundle.trivial.add_comm_monoid {B : Type u_1} {F : Type u_3} (b : B)  :
Equations
• = _inst_2
@[instance]
def bundle.trivial.add_comm_group {B : Type u_1} {F : Type u_3} (b : B)  :
Equations
• = _inst_2
@[instance]
def bundle.trivial.module {B : Type u_1} {F : Type u_3} {R : Type u_4} [semiring R] (b : B) [ F] :
F b)
Equations
• = _inst_3