Documentation

Mathlib.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 _→ Type _.

We provide a type synonym of Σ x, E x as Bundle.TotalSpace E, to be able to endow it with a topology which is not the disjoint union topology Sigma.TopologicalSpace. In general, the constructions of fiber bundles we will make will be of this form.

Main Definitions #

References #

def Bundle.TotalSpace {B : Type u_1} (E : BType u_2) :
Type (maxu_1u_2)

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

Equations
instance Bundle.instInhabitedTotalSpace {B : Type u_1} (E : BType u_2) [inst : Inhabited B] [inst : Inhabited (E default)] :
Equations
def Bundle.TotalSpace.proj {B : Type u_1} {E : BType u_2} :

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

Equations
  • Bundle.TotalSpace.proj = Sigma.fst

The canonical projection defining a bundle.

Equations
def Bundle.totalSpaceMk {B : Type u_1} {E : BType u_2} (b : B) (a : E b) :

Constructor for the total space of a bundle.

Equations
theorem Bundle.TotalSpace.proj_mk {B : Type u_1} {E : BType u_2} {x : B} {y : E x} :
theorem Bundle.sigma_mk_eq_totalSpaceMk {B : Type u_1} {E : BType u_2} {x : B} {y : E x} :
{ fst := x, snd := y } = Bundle.totalSpaceMk x y
theorem Bundle.TotalSpace.mk_cast {B : Type u_1} {E : BType u_2} {x : B} {x' : B} (h : x = x') (b : E x) :
Bundle.totalSpaceMk x' (cast (_ : E x = E x') b) = Bundle.totalSpaceMk x b
instance Bundle.instCoeTCTotalSpace {B : Type u_1} {E : BType u_2} {x : B} :
Equations
theorem Bundle.coe_fst {B : Type u_1} {E : BType u_2} (x : B) (v : E x) :
theorem Bundle.coe_snd {B : Type u_2} {E : BType u_1} {x : B} {y : E x} :
def Bundle.Trivial (B : Type u_1) (F : Type u_2) :
BType u_2

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

Equations
instance Bundle.instInhabitedTrivial {B : Type u_1} {F : Type u_2} [inst : Inhabited F] {b : B} :
Equations
  • Bundle.instInhabitedTrivial = { default := default }
def Bundle.Trivial.projSnd (B : Type u_1) (F : Type u_2) :

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

Equations
def Bundle.Pullback {B : Type u_1} {B' : Type u_2} (f : B'B) (E : BType u_3) (x : B') :
Type u_3

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

Equations

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

Equations
def Bundle.pullbackTotalSpaceEmbedding {B : Type u_1} {E : BType u_2} {B' : Type u_3} (f : B'B) :

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

Equations
def Bundle.Pullback.lift {B : Type u_1} {E : BType u_2} {B' : Type u_3} (f : B'B) :

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

Equations
@[simp]
theorem Bundle.Pullback.proj_lift {B : Type u_3} {E : BType u_2} {B' : Type u_1} (f : B'B) (x : Bundle.TotalSpace (f *ᵖ E)) :
@[simp]
theorem Bundle.Pullback.lift_mk {B : Type u_1} {E : BType u_2} {B' : Type u_3} (f : B'B) (x : B') (y : E (f x)) :
theorem Bundle.pullbackTotalSpaceEmbedding_snd {B : Type u_3} {E : BType u_2} {B' : Type u_1} (f : B'B) (x : Bundle.TotalSpace (f *ᵖ E)) :
@[simp]
theorem Bundle.coe_snd_map_apply {B : Type u_2} {E : BType u_1} [inst : (x : B) → AddCommMonoid (E x)] (x : B) (v : E x) (w : E x) :
@[simp]
theorem Bundle.coe_snd_map_smul {B : Type u_2} {E : BType u_1} [inst : (x : B) → AddCommMonoid (E x)] (R : Type u_3) [inst : Semiring R] [inst : (x : B) → Module R (E x)] (x : B) (r : R) (v : E x) :
(Bundle.totalSpaceMk x (r v)).snd = r (Bundle.totalSpaceMk x v).snd
instance Bundle.instAddCommGroupTrivial {B : Type u_1} {F : Type u_2} (b : B) [inst : AddCommGroup F] :
Equations
instance Bundle.instModuleTrivialInstAddCommMonoidTrivial {B : Type u_1} {F : Type u_2} {R : Type u_3} [inst : Semiring R] (b : B) [inst : AddCommMonoid F] [inst : Module R F] :
Equations