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

• Bundle.TotalSpace the total space of a bundle.
• Bundle.TotalSpace.proj the projection from the total space to the base space.
• Bundle.TotalSpace.mk the constructor for the total space.

## Implementation Notes #

• We use a custom structure for the total space of a bundle instead of using a type synonym for the canonical disjoint union Σ x, E x because the total space usually has a different topology and Lean 4 simp fails to apply lemmas about Σ x, E x to elements of the total space.

• The definition of Bundle.TotalSpace has an unused argument F. The reason is that in some constructions (e.g., Bundle.ContinuousLinearMap.vectorBundle) we need access to the atlas of trivializations of original fiber bundles to construct the topology on the total space of the new fiber bundle.

## References #

• https://en.wikipedia.org/wiki/Bundle_(mathematics)
theorem Bundle.TotalSpace.ext_iff {B : Type u_1} {F : Type u_4} {E : BType u_5} (x : ) (y : ) :
x = y x.proj = y.proj HEq x.snd y.snd
theorem Bundle.TotalSpace.ext {B : Type u_1} {F : Type u_4} {E : BType u_5} (x : ) (y : ) (proj : x.proj = y.proj) (snd : HEq x.snd y.snd) :
x = y
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).

• proj : B

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

• snd : E self.proj
Instances For
instance Bundle.instInhabitedTotalSpaceOfDefault {B : Type u_1} {F : Type u_2} (E : BType u_3) [] [Inhabited (E default)] :
Equations
• = { default := { proj := default, snd := default } }

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.
Instances For
@[reducible, inline]
abbrev Bundle.TotalSpace.mk' {B : Type u_1} {E : BType u_3} (F : Type u_4) (x : B) (y : E x) :
Equations
• = { proj := x, snd := y }
Instances For
theorem Bundle.TotalSpace.mk_cast {B : Type u_1} {F : Type u_2} {E : BType u_3} {x : B} {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 : E b} {y' : E b} :
= y = y'
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} :
CoeTC (E x) ()
Equations
• Bundle.instCoeTCTotalSpace = { coe := }
theorem Bundle.TotalSpace.eta {B : Type u_1} {F : Type u_2} {E : BType u_3} (z : ) :
{ 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 : } :
(∃ (x : ), 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) :
= Bundle.TotalSpace.proj ⁻¹' {b}

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

Equations
Instances For
@[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
Instances For
def Bundle.TotalSpace.trivialSnd (B : Type u_4) (F : Type u_5) :
F

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

Equations
• = Bundle.TotalSpace.snd
Instances For
@[simp]
theorem Bundle.TotalSpace.toProd_apply (B : Type u_4) (F : Type u_5) (x : Bundle.TotalSpace F fun (x : B) => F) :
() x = (x.proj, x.snd)
@[simp]
theorem Bundle.TotalSpace.toProd_symm_apply_snd (B : Type u_4) (F : Type u_5) (x : B × F) :
(().symm x).snd = x.2
@[simp]
theorem Bundle.TotalSpace.toProd_symm_apply_proj (B : Type u_4) (F : Type u_5) (x : B × F) :
(().symm x).proj = x.1
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.
Instances For
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
Instances For

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
Instances For
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) :
Bundle.TotalSpace F (f *ᵖ E)B' ×

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

Equations
• = (z.proj, { proj := f z.proj, snd := z.snd })
Instances For
@[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)), ().proj = f a.proj
@[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)), ().snd = a.snd
def Bundle.Pullback.lift {B : Type u_1} {F : Type u_2} {E : BType u_3} {B' : Type u_4} (f : B'B) :
Bundle.TotalSpace F (f *ᵖ E)

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

Equations
• = { proj := f z.proj, snd := z.snd }
Instances For
@[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)) :
= { proj := f x, snd := y }