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 : B → Type u_5} (x : Bundle.TotalSpace F E) (y : Bundle.TotalSpace F E) : x = y ↔ x.proj = y.proj ∧ HEq x.snd y.snd

theorem Bundle.TotalSpace.ext {B : Type u_1} {F : Type u_4} {E : B → Type u_5} (x : Bundle.TotalSpace F E) (y : Bundle.TotalSpace F E) (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 : B → Type 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

instance Bundle.instInhabitedTotalSpace {B : Type u_1} {F : Type u_2} (E : B → Type u_3) [Inhabited B] [Inhabited (E default)] : Inhabited (Bundle.TotalSpace F E)

Equations

• Bundle.instInhabitedTotalSpace E = { default := { proj := default, snd := default } }

def Bundle.termπ__ : Lean.ParserDescr

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.

@[inline, reducible]

abbrev Bundle.TotalSpace.mk' {B : Type u_1} {E : B → Type u_3} (F : Type u_4) (x : B) (y : E x) : Bundle.TotalSpace F E

Equations

• Bundle.TotalSpace.mk' F x y = { proj := x, snd := y }

theorem Bundle.TotalSpace.mk_cast {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {x : B} {x' : B} (h : x = x') (b : E x) : Bundle.TotalSpace.mk' F x' (cast (_ : E x = E x') b) = { proj := x, snd := b }

@[simp]

theorem Bundle.TotalSpace.mk_inj {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {b : B} {y : E b} {y' : E b} : Bundle.TotalSpace.mk' F b y = Bundle.TotalSpace.mk' F b y' ↔ y = y'

theorem Bundle.TotalSpace.mk_injective {B : Type u_1} {F : Type u_2} {E : B → Type u_3} (b : B) : Function.Injective (Bundle.TotalSpace.mk b)

instance Bundle.instCoeTCTotalSpace {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {x : B} : CoeTC (E x) (Bundle.TotalSpace F E)

Equations

• Bundle.instCoeTCTotalSpace = { coe := Bundle.TotalSpace.mk x }

theorem Bundle.TotalSpace.eta {B : Type u_1} {F : Type u_2} {E : B → Type 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 : B → Type u_3} {p : Bundle.TotalSpace F E → Prop} : (∃ (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 : B → Type u_3} (b : B) : Set.range (Bundle.TotalSpace.mk b) = Bundle.TotalSpace.proj ⁻¹' {b}

def Bundle.«term_×ᵇ_» : Lean.TrailingParserDescr

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

Equations

• Bundle.«term_×ᵇ_» = Lean.ParserDescr.trailingNode `Bundle.term_×ᵇ_ 100 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×ᵇ ") (Lean.ParserDescr.cat `term 0))

@[reducible]

def Bundle.Trivial (B : Type u_4) (F : Type u_5) : B → Type u_5

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

Equations

• Bundle.Trivial B F x = F

def Bundle.TotalSpace.trivialSnd (B : Type u_4) (F : Type u_5) : Bundle.TotalSpace F (Bundle.Trivial B F) → F

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

Equations

• Bundle.TotalSpace.trivialSnd B F = Bundle.TotalSpace.snd

@[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.2

@[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.1

@[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)

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.

def Bundle.Pullback {B : Type u_1} {B' : Type u_4} (f : B' → B) (E : B → Type 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

• (f *ᵖ E) x = E (f x)

def Bundle.«term_*ᵖ_» : Lean.TrailingParserDescr

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

• Bundle.«term_*ᵖ_» = Lean.ParserDescr.trailingNode `Bundle.term_*ᵖ_ 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " *ᵖ ") (Lean.ParserDescr.cat `term 1023))

instance Bundle.instNonemptyPullback {B : Type u_1} {E : B → Type u_3} {B' : Type u_4} {f : B' → B} {x : B'} [Nonempty (E (f x))] : Nonempty ((f *ᵖ E) x)

Equations

• (_ : Nonempty ((f *ᵖ E) x)) = inst

def Bundle.pullbackTotalSpaceEmbedding {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {B' : Type u_4} (f : B' → B) : Bundle.TotalSpace F (f *ᵖ E) → B' × Bundle.TotalSpace F E

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

Equations

• Bundle.pullbackTotalSpaceEmbedding f z = (z.proj, { proj := f z.proj, snd := z.snd })

@[simp]

theorem Bundle.Pullback.lift_snd {B : Type u_1} {F : Type u_2} {E : B → Type 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 : B → Type u_3} {B' : Type u_4} (f : B' → B) : ∀ (a : Bundle.TotalSpace F (f *ᵖ E)), (Bundle.Pullback.lift f a).proj = f a.proj

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

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

Equations

• Bundle.Pullback.lift f z = { proj := f z.proj, snd := z.snd }

@[simp]

theorem Bundle.Pullback.lift_mk {B : Type u_1} {F : Type u_2} {E : B → Type 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 }