Smooth Fiber Bundles

Stream: Is there code for X?

[Dominic Steinitz]

What might be the pitfalls to defining this?

import Mathlib

open Bundle

variable {n : WithTop ℕ∞} {𝕜 B B' F M : Type*} {E : B → Type*}

variable [NontriviallyNormedField 𝕜]
  {EB : Type*} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB]
  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [TopologicalSpace B] [ChartedSpace HB B]

  {EM : Type*} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM]
  {HM : Type*} [TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM}

  [TopologicalSpace M] [ChartedSpace HM M]

  [∀ x, AddCommMonoid (E x)] [∀ x, Module 𝕜 (E x)]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F]

variable [TopologicalSpace (TotalSpace F E)] [∀ x, TopologicalSpace (E x)] (F E)
variable [FiberBundle F E]

variable [ChartedSpace HM F]

variable (n IB) in
/-- A smooth fiber bundle is a topological fiber bundle where the coordinate changes
    between trivializations are smooth. The coordinate change maps
    `B × F → F` must be `C^n` with respect to the product smooth structure. -/
class ContMDiffFiberBundle : Prop where
  contMDiff_coordChange :
  ∀ (e e' : Trivialization F (π F E))
    [MemTrivializationAtlas e] [MemTrivializationAtlas e'],
    ContMDiffOn (IB.prod IM) IM n
      (fun (p : B × F) => e'.coordChange e p.1 p.2)
      ((e.baseSet ∩ e'.baseSet) ×ˢ Set.univ)

[Sébastien Gouëzel]

Isn't that equivalent to requiring IsManifold (IB.prod 𝓘(𝕜, F)) n (TotalSpace F E)? If that's indeed the case, we shouldn't add this definition because it would just add another way of saying the same thing, which is not a good idea in general.

[Dominic Steinitz]

Does that mean we should not have this: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Geometry/Manifold/VectorBundle/Basic.html#ContMDiffVectorBundle either?

[Sébastien Gouëzel]

No, that's different: the vector bundle definition requires that the change of coordinates, as a continuous linear map, depends smoothly on the base point. That's a subtle point in the definition of the vector bundle: it is not enough to require that the bundle is smooth as a manifold to ensure that the change of coordinates is smooth, and the latter is what you need to construct other bundles. (Note that in finite dimensional bundles the two points of view are equivalent, it's only the general case which is troublesome).

There is a story here: I hadn't noticed the subtlety, so I gave a first definition of smooth vector bundles in mathlib which was essentially your definition above. Then @Heather Macbeth noticed the issue (explained in a book by Lang) and she had to change everything to get to the better current definition, with @Floris van Doorn.

[Michael Rothgang]

To elabore more: for Banach space vector bundles, those two notions are not equivalent - and Banach vector bundles are important.

[Dominic Steinitz]

Vector bundles are fibre bundles where the fibres are vector spaces and the transition maps at a point are linear?

[Michael Rothgang]

yes-ish: you also need continuity of these maps in the base point.