Mathlib.Data.Bundle

Module docstring

{"# 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) "}

Bundle.TotalSpace structure

(F : Type*) (E : B → Type*)

Full source

/-- `Bundle.TotalSpace F E` is the total space of the bundle. It consists of pairs
`(proj : B, snd : E proj)`.
-/
@[ext]
structure TotalSpace (F : Type*) (E : B → Type*) where
  /-- `Bundle.TotalSpace.proj` is the canonical projection `Bundle.TotalSpace F E → B` from the
  total space to the base space. -/
  proj : B
  snd : E proj

Total space of a bundle

Informal description

The structure `Bundle.TotalSpace F E` represents the total space of a bundle with base space `B` and fibers `E b` for each `b : B`. It consists of pairs `(b, x)` where `b : B` and `x : E b`.

Bundle.instInhabitedTotalSpaceOfDefault instance

[Inhabited B] [Inhabited (E default)] : Inhabited (TotalSpace F E)

Full source

instance [Inhabited B] [Inhabited (E default)] : Inhabited (TotalSpace F E) :=
  ⟨⟨default, default⟩⟩

Nonempty Total Space of a Bundle with Nonempty Base and Fiber

Informal description

For any base space $B$ with a distinguished element and any fiber bundle $E : B \to \text{Type}^*$ where the fiber over the distinguished element is nonempty, the total space $\text{TotalSpace}(F, E)$ is nonempty.

Bundle.termπ__ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
scoped notation:max "π " F':max E':max => Bundle.TotalSpace.proj (F := F') (E := E')

Total space of a fiber bundle

Informal description

Given a base space $B$ and a fiber bundle $E : B \to \text{Type}^*$ (where for each $b \in B$, $E(b)$ represents the fiber over $b$), the total space $\text{TotalSpace}(F, E)$ is defined as the collection of all pairs $(b, x)$ where $b \in B$ and $x \in E(b)$. This structure is used to represent the entire fiber bundle, including all fibers over all points in the base space. The unused parameter $F$ is included for technical reasons related to constructing topologies in certain bundle constructions.

Bundle.TotalSpace.mk' abbrev

(F : Type*) (x : B) (y : E x) : TotalSpace F E

Full source

abbrev TotalSpace.mk' (F : Type*) (x : B) (y : E x) : TotalSpace F E := ⟨x, y⟩

Constructor for the total space of a bundle

Informal description

Given a type `F`, a base space `B`, and a fiber `E x` over each point `x : B`, the function `mk'` constructs an element of the total space `TotalSpace F E` as the pair `(x, y)` where `x : B` and `y : E x`.

Bundle.TotalSpace.mk_cast theorem

{x x' : B} (h : x = x') (b : E x) : .mk' F x' (cast (congr_arg E h) b) = TotalSpace.mk x b

Full source

theorem TotalSpace.mk_cast {x x' : B} (h : x = x') (b : E x) :
    .mk' F x' (cast (congr_arg E h) b) = TotalSpace.mk x b := by subst h; rfl

Equality of Total Space Constructions under Base Point Equality

Informal description

For any points $x, x'$ in the base space $B$ with $x = x'$, and any element $b$ in the fiber $E_x$, the construction of the total space element via `mk'` at $x'$ with the cast of $b$ along the equality $x = x'$ is equal to the total space element constructed at $x$ with $b$. That is, $\text{mk'}(x', \text{cast}(\text{congr\_arg}\, E\, h)\, b) = \text{mk}(x, b)$.

Bundle.TotalSpace.mk_inj theorem

{b : B} {y y' : E b} : mk' F b y = mk' F b y' ↔ y = y'

Full source

@[simp 1001, mfld_simps 1001]
theorem TotalSpace.mk_inj {b : B} {y y' : E b} : mk'mk' F b y = mk' F b y' ↔ y = y' := by
  simp [TotalSpace.ext_iff]

Injectivity of Total Space Construction at a Fixed Base Point

Informal description

For any point $b$ in the base space $B$ and any two elements $y, y'$ in the fiber $E_b$, the equality $\text{mk'}(F, b, y) = \text{mk'}(F, b, y')$ holds if and only if $y = y'$.

Bundle.TotalSpace.mk_injective theorem

(b : B) : Injective (mk b : E b → TotalSpace F E)

Full source

theorem TotalSpace.mk_injective (b : B) : Injective (mk b : E b → TotalSpace F E) := fun _ _ ↦
  mk_inj.1

Injectivity of Fiber Inclusion into Total Space at Fixed Base Point

Informal description

For any point $b$ in the base space $B$ of a bundle with total space $\text{TotalSpace}\,F\,E$, the map $\text{mk}_b : E(b) \to \text{TotalSpace}\,F\,E$ sending $x \mapsto (b, x)$ is injective. That is, for any $x, y \in E(b)$, if $(b, x) = (b, y)$, then $x = y$.

Bundle.instCoeTCTotalSpace instance

{x : B} : CoeTC (E x) (TotalSpace F E)

Full source

instance {x : B} : CoeTC (E x) (TotalSpace F E) :=
  ⟨TotalSpace.mk x⟩

Canonical Inclusion of Fiber into Total Space

Informal description

For any bundle $E$ over a base space $B$ and any point $x \in B$, there is a canonical inclusion map from the fiber $E(x)$ to the total space of the bundle $\text{TotalSpace}\,F\,E$.

Bundle.TotalSpace.eta theorem

(z : TotalSpace F E) : TotalSpace.mk z.proj z.2 = z

Full source

theorem TotalSpace.eta (z : TotalSpace F E) : TotalSpace.mk z.proj z.2 = z := rfl

Total Space Reconstruction Identity: $\text{mk}(z.\text{proj}, z.2) = z$

Informal description

For any element $z$ of the total space $\text{TotalSpace}\,F\,E$ of a bundle, the pair constructed from the projection of $z$ to the base space and the fiber component of $z$ is equal to $z$ itself. In other words, if $z = (b, x)$ where $b \in B$ and $x \in E(b)$, then $\text{TotalSpace.mk}\,b\,x = z$.

Bundle.TotalSpace.exists theorem

{p : TotalSpace F E → Prop} : (∃ x, p x) ↔ ∃ b y, p ⟨b, y⟩

Full source

@[simp]
theorem TotalSpace.exists {p : TotalSpace F E → Prop} : (∃ x, p x) ↔ ∃ b y, p ⟨b, y⟩ :=
  ⟨fun ⟨x, hx⟩ ↦ ⟨x.1, x.2, hx⟩, fun ⟨b, y, h⟩ ↦ ⟨⟨b, y⟩, h⟩⟩

Existence in Total Space of a Bundle

Informal description

For any predicate $p$ on the total space $\text{TotalSpace}\,F\,E$ of a bundle, there exists an element $x$ in the total space satisfying $p(x)$ if and only if there exists a base point $b \in B$ and an element $y \in E(b)$ such that $p$ holds for the pair $\langle b, y \rangle$.

Bundle.TotalSpace.range_mk theorem

(b : B) : range ((↑) : E b → TotalSpace F E) = π F E ⁻¹' { b }

Full source

@[simp]
theorem TotalSpace.range_mk (b : B) : range ((↑) : E b → TotalSpace F E) = π F Eπ F E ⁻¹' {b} := by
  apply Subset.antisymm
  · rintro _ ⟨x, rfl⟩
    rfl
  · rintro ⟨_, x⟩ rfl
    exact ⟨x, rfl⟩

Fiber Inclusion Range Equals Preimage of Base Point

Informal description

For any point $b$ in the base space $B$ of a bundle with total space $\text{TotalSpace}\,F\,E$, the range of the inclusion map from the fiber $E(b)$ to the total space is equal to the preimage of the singleton set $\{b\}$ under the projection map $\pi : \text{TotalSpace}\,F\,E \to B$.

Bundle.term_×ᵇ_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for the direct sum of two bundles over the same base. -/
notation:100 E₁ " ×ᵇ " E₂ => fun x => E₁ x × E₂ x

Direct sum of bundles over the same base

Informal description

The notation $ E_1 \times_b E_2 $ denotes the direct sum of two bundles $ E_1 $ and $ E_2 $ over the same base space $ B $, where for each point $ x \in B $, the fiber is the product $ E_1(x) \times E_2(x) $.

Bundle.Trivial definition

(B : Type*) (F : Type*) : B → Type _

Full source

/-- `Bundle.Trivial B F` is the trivial bundle over `B` of fiber `F`. -/
@[reducible, nolint unusedArguments]
def Trivial (B : Type*) (F : Type*) : B → Type _ := fun _ => F

Trivial bundle

Informal description

The trivial bundle over a base space $B$ with fiber $F$ is the bundle where each fiber over any point $b \in B$ is simply $F$ itself. In other words, it is the constant bundle where the fiber does not vary with the base point.

Bundle.TotalSpace.trivialSnd definition

(B : Type*) (F : Type*) : TotalSpace F (Bundle.Trivial B F) → F

Full source

/-- The trivial bundle, unlike other bundles, has a canonical projection on the fiber. -/
def TotalSpace.trivialSnd (B : Type*) (F : Type*) : TotalSpace F (Bundle.Trivial B F) → F :=
  TotalSpace.snd

Projection to fiber in trivial bundle

Informal description

The function maps a point $(b, x)$ in the total space of the trivial bundle over base space $B$ with fiber $F$ to its second component $x \in F$.

Bundle.TotalSpace.toProd definition

(B F : Type*) : (TotalSpace F fun _ : B => F) ≃ B × F

Full source

/-- A trivial bundle is equivalent to the product `B × F`. -/
@[simps (config := { attrs := [`mfld_simps] })]
def TotalSpace.toProd (B F : Type*) : (TotalSpace F fun _ : B => F) ≃ B × F where
  toFun x := (x.1, x.2)
  invFun x := ⟨x.1, x.2⟩
  left_inv := fun ⟨_, _⟩ => rfl
  right_inv := fun ⟨_, _⟩ => rfl

Equivalence between total space of trivial bundle and product space

Informal description

The equivalence between the total space of a trivial bundle with fiber $F$ over base space $B$ and the product space $B \times F$. Specifically, it maps a pair $(b, x)$ in the total space to $(b, x)$ in $B \times F$, and vice versa, with both compositions being identity maps.

Bundle.Pullback definition

(f : B' → B) (E : B → Type*) : B' → Type _

Full source

/-- 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')`. -/
def Pullback (f : B' → B) (E : B → Type*) : B' → Type _ := fun x => E (f x)

Pullback bundle

Informal description

Given a bundle $ E $ over a base space $ B $ and a map $ f \colon B' \to B $, the pullback bundle $ f^*E $ over $ B' $ is defined such that the fiber over each point $ b' \in B' $ is $ E(f(b')) $. In other words, the pullback bundle $ f^*E $ is the bundle over $ B' $ obtained by composing the original bundle $ E $ with the map $ f $.

Bundle.term_*ᵖ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation f " *ᵖ " E:arg => Pullback f E

Pullback bundle notation

Informal description

The notation `f *ᵖ E` represents the pullback bundle of a bundle `E : B → Type*` along a map `f : B' → B`. This constructs a new bundle over `B'` where the fiber over each point `b' : B'` is the fiber of `E` over `f(b')`.

Bundle.instNonemptyPullback instance

{f : B' → B} {x : B'} [Nonempty (E (f x))] : Nonempty ((f *ᵖ E) x)

Full source

instance {f : B' → B} {x : B'} [Nonempty (E (f x))] : Nonempty ((f *ᵖ E) x) :=
  ‹Nonempty (E (f x))›

Nonemptiness of Pullback Bundle Fibers

Informal description

For any bundle $E$ over a base space $B$, map $f \colon B' \to B$, and point $x \in B'$, if the fiber $E(f(x))$ is nonempty, then the fiber $(f^*E)(x)$ of the pullback bundle is also nonempty.

Bundle.pullbackTotalSpaceEmbedding definition

(f : B' → B) : TotalSpace F (f *ᵖ E) → B' × TotalSpace F E

Full source

/-- Natural embedding of the total space of `f *ᵖ E` into `B' × TotalSpace F E`. -/
@[simp]
def pullbackTotalSpaceEmbedding (f : B' → B) : TotalSpace F (f *ᵖ E) → B' × TotalSpace F E :=
  fun z => (z.proj, TotalSpace.mk (f z.proj) z.2)

Embedding of pullback bundle total space into base-product space

Informal description

The natural embedding of the total space of the pullback bundle $ f^*E $ into the product space $ B' \times \text{TotalSpace } F E $. Specifically, it maps a point $ (b', x) $ in the total space of $ f^*E $ to the pair $ (b', (f(b'), x)) $, where $ (f(b'), x) $ is a point in the total space of the original bundle $ E $.

Bundle.Pullback.lift definition

(f : B' → B) : TotalSpace F (f *ᵖ E) → TotalSpace F E

Full source

/-- The base map `f : B' → B` lifts to a canonical map on the total spaces. -/
@[simps (config := { attrs := [`mfld_simps] })]
def Pullback.lift (f : B' → B) : TotalSpace F (f *ᵖ E) → TotalSpace F E := fun z => ⟨f z.proj, z.2⟩

Lift from pullback bundle to original bundle

Informal description

Given a map $ f \colon B' \to B $ between base spaces, the function `Bundle.Pullback.lift f` maps a point $(b', x)$ in the total space of the pullback bundle $ f^*E $ to the point $(f(b'), x)$ in the total space of the original bundle $ E $. In other words, it lifts a point from the pullback bundle's total space to the original bundle's total space by applying $ f $ to the base point while keeping the fiber element unchanged.

Bundle.Pullback.lift_mk theorem

(f : B' → B) (x : B') (y : E (f x)) : Pullback.lift f (.mk' F x y) = ⟨f x, y⟩

Full source

@[simp, mfld_simps]
theorem Pullback.lift_mk (f : B' → B) (x : B') (y : E (f x)) :
    Pullback.lift f (.mk' F x y) = ⟨f x, y⟩ :=
  rfl

Lift of Pullback Bundle Point Equals Original Bundle Point

Informal description

For any map $f \colon B' \to B$ between base spaces, any point $x \in B'$, and any element $y \in E(f(x))$ in the fiber over $f(x)$, the lift of the point $(x, y)$ in the total space of the pullback bundle $f^*E$ equals the point $(f(x), y)$ in the total space of the original bundle $E$. In other words, the following equality holds: \[ \text{Pullback.lift } f \left( (x, y) \right) = (f(x), y). \]