Bundle definitions rationale

Stream: general

[Dominic Steinitz]

I was expecting a vector bundle to be an extension of a fibre bundle (with the fibres being vector spaces and the coordinate change functions being linear on the fibres) but if I look at the definition here

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Topology/VectorBundle/Basic.lean#L472

then it seems to start from scratch. Here's the definition of a fibre bundle for comparison (well FiberBundelCore to be precise).

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Topology/FiberBundle/Basic.lean#L394

What's the rationale behind this?

I have a fibre bundle defined by FiberBundleCore and know that the fibres are vector spaces and that the coordinate change functions are linear. Maybe there is some theorem that says under those circumstances a FiberBundleCore is a VectorBundleCore but I have yet to find it.

Thanks :smile:

[Sébastien Gouëzel]

Vector bundles (not the core versions) are indeed defined as extensions of fiber bundles. On the other hand, the data you need to define vector bundles and fiber bundles are of a different nature: for vector bundles, you need continuous linear equivs that should depend continuously on the base point, while for fiber bundles you need partial homeomorphisms sending fibers to fibers. So if you defined VectorBundleCore as an extension of FiberBundleCore, you would have additional fields (the partial homeos) that you would need to define every time you create a VectorBundleCore -- while we know they're not necessary because they can be derived from the other fields. So it's more economical for the user to define things as we do.

On the other hand, nothing prevents you from constructing a function building a VectorBundleCore out of a FiberBundleCore. But note that the change of coordinates being linear in the fibers is not enough, you also need to check continuity with respect to the basepoint for the operator norm topology.

[Sébastien Gouëzel]

In fact, I think having a way to build a VectorBundleCore out of a FiberBundleCore plus some properties is definitely a good idea, and a gap in our current API.

[Dominic Steinitz]

Sébastien Gouëzel said:

In fact, I think having a way to build a VectorBundleCore out of a FiberBundleCore plus some properties is definitely a good idea, and a gap in our current API.

I need that and so am happy to attempt doing that but I will need some guidance.

[Dominic Steinitz]

How about this?

/-
Copyright (c) 2025 Dominic Steinitz. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Dominic Steinitz
-/
import Mathlib

set_option linter.style.longLine false
set_option linter.style.lambdaSyntax false
set_option linter.style.cdot false

open Bundle Topology Set

def VtoF
  {R : Type*} [NontriviallyNormedField R]
  {B : Type*} [TopologicalSpace B]
  {F : Type*} [NormedAddCommGroup F] [NormedSpace R F]
  {ι : Type*}
  (Z : VectorBundleCore R B F ι) : FiberBundleCore ι B F := {
  baseSet := Z.baseSet
  isOpen_baseSet := Z.isOpen_baseSet
  indexAt := Z.indexAt
  mem_baseSet_at := Z.mem_baseSet_at
  coordChange := fun i j b => Z.coordChange i j b
  coordChange_self := Z.coordChange_self
  continuousOn_coordChange := fun i j =>
    isBoundedBilinearMap_apply.continuous.comp_continuousOn
      ((Z.continuousOn_coordChange i j).prod_map continuousOn_id)
  coordChange_comp := Z.coordChange_comp
  }

def FtoV {R : Type*} [NontriviallyNormedField R]
  {B : Type*} [TopologicalSpace B]
  {F : Type*} [NormedAddCommGroup F] [NormedSpace R F]
  {ι : Type*}
  (Z : FiberBundleCore ι B F)
  (coordChangeLin : ∀ (i j : ι) (b : B), F →L[R] F)
  (h_coord_eq : ∀ i j b, ⇑(coordChangeLin i j b) = Z.coordChange i j b)
  (h_coord_cont : ∀ i j, ContinuousOn (fun b ↦ coordChangeLin i j b) (Z.baseSet i ∩ Z.baseSet j)) :
  VectorBundleCore R B F ι := {
    baseSet := Z.baseSet
    isOpen_baseSet := Z.isOpen_baseSet
    indexAt := Z.indexAt
    mem_baseSet_at := Z.mem_baseSet_at
    coordChange := coordChangeLin
    coordChange_self := by
      intros i b hb x
      rw [h_coord_eq]
      exact Z.coordChange_self i b hb x
    continuousOn_coordChange := by
      intro i j
      apply ContinuousOn.congr (h_coord_cont i j)
      intro b hb
      exact rfl
    coordChange_comp := by
      simp only [h_coord_eq]
      exact Z.coordChange_comp
  }