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 #

source
ink
def Bundle.TotalSpace {B : Type u_1} (E : B → Type 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
source
ink
instance Bundle.instInhabitedTotalSpace {B : Type u_1} (E : B → Type u_2) [inst : Inhabited B] [inst : Inhabited (E default)] :
Inhabited (Bundle.TotalSpace E)
Equations
source
ink
def Bundle.TotalSpace.proj {B : Type u_1} {E : B → Type u_2} :
Bundle.TotalSpace E → B

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
source
ink
def Bundle.termπ_ :
Lean.ParserDescr

The canonical projection defining a bundle.

Equations
source
ink
def Bundle.totalSpaceMk {B : Type u_1} {E : B → Type u_2} (b : B) (a : E b) :
Bundle.TotalSpace E

Constructor for the total space of a bundle.

Equations
source
ink
theorem Bundle.TotalSpace.proj_mk {B : Type u_1} {E : B → Type u_2} {x : B} {y : E x} :
Bundle.TotalSpace.proj (Bundle.totalSpaceMk x y) = x
source
ink
theorem Bundle.sigma_mk_eq_totalSpaceMk {B : Type u_1} {E : B → Type u_2} {x : B} {y : E x} :
{ fst := x, snd := y } = Bundle.totalSpaceMk x y
source
ink
theorem Bundle.TotalSpace.mk_cast {B : Type u_1} {E : B → Type 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
source
ink
theorem Bundle.TotalSpace.eta {B : Type u_1} {E : B → Type u_2} (z : Bundle.TotalSpace E) :
Bundle.totalSpaceMk (Bundle.TotalSpace.proj z) z.snd = z
source
ink
instance Bundle.instCoeTCTotalSpace {B : Type u_1} {E : B → Type u_2} {x : B} :
CoeTC (E x) (Bundle.TotalSpace E)
Equations
source
ink
theorem Bundle.coe_fst {B : Type u_1} {E : B → Type u_2} (x : B) (v : E x) :
(Bundle.totalSpaceMk x v).fst = x
source
ink
theorem Bundle.coe_snd {B : Type u_2} {E : B → Type u_1} {x : B} {y : E x} :
(Bundle.totalSpaceMk x y).snd = y
source
ink
def Bundle.«term_×ᵇ_» :
Lean.TrailingParserDescr

The direct sum of two bundles.

Equations
source
ink
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
source
ink
instance Bundle.instInhabitedTrivial {B : Type u_1} {F : Type u_2} [inst : Inhabited F] {b : B} :
Inhabited (Bundle.Trivial B F b)
Equations
  • Bundle.instInhabitedTrivial = { default := default }
source
ink
def Bundle.Trivial.projSnd (B : Type u_1) (F : Type u_2) :
Bundle.TotalSpace (Bundle.Trivial B F) → F

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

Equations
source
ink
def Bundle.Pullback {B : Type u_1} {B' : Type u_2} (f : B' → B) (E : B → Type 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
source
ink
def Bundle.«term_*ᵖ_» :
Lean.TrailingParserDescr

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
source
ink
def Bundle.pullbackTotalSpaceEmbedding {B : Type u_1} {E : B → Type u_2} {B' : Type u_3} (f : B' → B) :
Bundle.TotalSpace (f *ᵖ E) → B' × Bundle.TotalSpace E

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

Equations
source
ink
def Bundle.Pullback.lift {B : Type u_1} {E : B → Type u_2} {B' : Type u_3} (f : B' → B) :
Bundle.TotalSpace (f *ᵖ E) → Bundle.TotalSpace E

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

Equations
source
ink
@[simp]
theorem Bundle.Pullback.proj_lift {B : Type u_3} {E : B → Type u_2} {B' : Type u_1} (f : B' → B) (x : Bundle.TotalSpace (f *ᵖ E)) :
Bundle.TotalSpace.proj (Bundle.Pullback.lift f x) = f x.fst
source
ink
@[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.totalSpaceMk x y) = Bundle.totalSpaceMk (f x) y
source
ink
theorem Bundle.pullbackTotalSpaceEmbedding_snd {B : Type u_3} {E : B → Type u_2} {B' : Type u_1} (f : B' → B) (x : Bundle.TotalSpace (f *ᵖ E)) :
(Bundle.pullbackTotalSpaceEmbedding f x).snd = Bundle.Pullback.lift f x
source
ink
@[simp]
theorem Bundle.coe_snd_map_apply {B : Type u_2} {E : B → Type u_1} [inst : (x : B) → AddCommMonoid (E x)] (x : B) (v : E x) (w : E x) :
(Bundle.totalSpaceMk x (v + w)).snd = (Bundle.totalSpaceMk x v).snd + (Bundle.totalSpaceMk x w).snd
source
ink
@[simp]
theorem Bundle.coe_snd_map_smul {B : Type u_2} {E : B → Type 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
source
ink
instance Bundle.instAddCommMonoidTrivial {B : Type u_1} {F : Type u_2} (b : B) [inst : AddCommMonoid F] :
AddCommMonoid (Bundle.Trivial B F b)
Equations
source
ink
instance Bundle.instAddCommGroupTrivial {B : Type u_1} {F : Type u_2} (b : B) [inst : AddCommGroup F] :
AddCommGroup (Bundle.Trivial B F b)
Equations
source
ink
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] :
Module R (Bundle.Trivial B F b)
Equations