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

We define Bundle.TotalSpace F E to be the type of pairs ⟨b, x⟩, where b : B and x : E b. This type is isomorphic to Σ x, E x and uses an extra argument F for reasons explained below. In general, the constructions of fiber bundles we will make will be of this form.

Main Definitions #

Implementation Notes #

References #

structure Bundle.TotalSpace {B : Type u_1} (F : Type u_4) (E : BType u_5) :
Type (max u_1 u_5)

Bundle.TotalSpace F E is the total space of the bundle. It consists of pairs (proj : B, snd : E proj).

theorem Bundle.TotalSpace.ext {B : Type u_1} {F : Type u_4} {E : BType u_5} {x y : Bundle.TotalSpace F E} (proj : x.proj = y.proj) (snd : HEq x.snd y.snd) :
x = y
instance Bundle.instInhabitedTotalSpaceOfDefault {B : Type u_1} {F : Type u_2} (E : BType u_3) [Inhabited B] [Inhabited (E default)] :
Equations

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

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev Bundle.TotalSpace.mk' {B : Type u_1} {E : BType u_3} (F : Type u_4) (x : B) (y : E x) :
Equations
theorem Bundle.TotalSpace.mk_cast {B : Type u_1} {F : Type u_2} {E : BType u_3} {x x' : B} (h : x = x') (b : E x) :
Bundle.TotalSpace.mk' F x' (cast b) = { proj := x, snd := b }
@[simp]
theorem Bundle.TotalSpace.mk_inj {B : Type u_1} {F : Type u_2} {E : BType u_3} {b : B} {y y' : E b} :
theorem Bundle.TotalSpace.mk_injective {B : Type u_1} {F : Type u_2} {E : BType u_3} (b : B) :
instance Bundle.instCoeTCTotalSpace {B : Type u_1} {F : Type u_2} {E : BType u_3} {x : B} :
Equations
theorem Bundle.TotalSpace.eta {B : Type u_1} {F : Type u_2} {E : BType u_3} (z : Bundle.TotalSpace F E) :
{ proj := z.proj, snd := z.snd } = z
@[simp]
theorem Bundle.TotalSpace.exists {B : Type u_1} {F : Type u_2} {E : BType u_3} {p : Bundle.TotalSpace F EProp} :
(∃ (x : Bundle.TotalSpace F E), p x) ∃ (b : B) (y : E b), p { proj := b, snd := y }
@[simp]
theorem Bundle.TotalSpace.range_mk {B : Type u_1} {F : Type u_2} {E : BType u_3} (b : B) :
Set.range (Bundle.TotalSpace.mk b) = Bundle.TotalSpace.proj ⁻¹' {b}

Notation for the direct sum of two bundles over the same base.

Equations
@[reducible]
def Bundle.Trivial (B : Type u_4) (F : Type u_5) :
BType u_5

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

Equations

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

Equations
def Bundle.TotalSpace.toProd (B : Type u_4) (F : Type u_5) :
(Bundle.TotalSpace F fun (x : B) => F) B × F

A trivial bundle is equivalent to the product B × F.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Bundle.TotalSpace.toProd_symm_apply_snd (B : Type u_4) (F : Type u_5) (x : B × F) :
((Bundle.TotalSpace.toProd B F).symm x).snd = x.snd
@[simp]
theorem Bundle.TotalSpace.toProd_apply (B : Type u_4) (F : Type u_5) (x : Bundle.TotalSpace F fun (x : B) => F) :
(Bundle.TotalSpace.toProd B F) x = (x.proj, x.snd)
@[simp]
theorem Bundle.TotalSpace.toProd_symm_apply_proj (B : Type u_4) (F : Type u_5) (x : B × F) :
((Bundle.TotalSpace.toProd B F).symm x).proj = x.fst
def Bundle.Pullback {B : Type u_1} {B' : Type u_4} (f : B'B) (E : BType u_5) :
B'Type u_5

The pullback of a bundle E over a base B under a map f : B' → B, denoted by Bundle.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, denoted by Bundle.Pullback f E or f *ᵖ E, is the bundle over B' whose fiber over b' is E (f b').

Equations
instance Bundle.instNonemptyPullback {B : Type u_1} {E : BType u_3} {B' : Type u_4} {f : B'B} {x : B'} [Nonempty (E (f x))] :
Nonempty ((f *ᵖ E) x)
Equations
  • = inst
def Bundle.pullbackTotalSpaceEmbedding {B : Type u_1} {F : Type u_2} {E : BType u_3} {B' : Type u_4} (f : B'B) :

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

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

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

Equations
@[simp]
theorem Bundle.Pullback.lift_snd {B : Type u_1} {F : Type u_2} {E : BType u_3} {B' : Type u_4} (f : B'B) (a✝ : Bundle.TotalSpace F (f *ᵖ E)) :
(Bundle.Pullback.lift f a✝).snd = a✝.snd
@[simp]
theorem Bundle.Pullback.lift_proj {B : Type u_1} {F : Type u_2} {E : BType u_3} {B' : Type u_4} (f : B'B) (a✝ : Bundle.TotalSpace F (f *ᵖ E)) :
(Bundle.Pullback.lift f a✝).proj = f a✝.proj
@[simp]
theorem Bundle.Pullback.lift_mk {B : Type u_1} {F : Type u_2} {E : BType u_3} {B' : Type u_4} (f : B'B) (x : B') (y : E (f x)) :
Bundle.Pullback.lift f (Bundle.TotalSpace.mk' F x y) = { proj := f x, snd := y }