[Merged by Bors] - feat(topology/vector_bundle): definition of topological vector bundle #4658

Nicknamen · 2020-10-17T16:10:29Z

Topological vector bundles

In this file we define topological vector bundles.

Let B be the base space. In our formalism, a topological vector bundle is by definition the type
bundle.total_space E where E : B → Type* is a function associating to
x : B the fiber over x. This type bundle.total_space E is just a type synonym for
Σ (x : B), E x, with the interest that one can put another topology than on Σ (x : B), E x
which has the disjoint union topology.

To have a topological vector bundle structure on bundle.total_space E,
one should addtionally have the following data:

F should be a topological vector space over a field 𝕜;
There should be a topology on bundle.total_space E, for which the projection to E is
a topological fiber bundle with fiber F (in particular, each fiber E x is homeomorphic to F);
For each x, the fiber E x should be a topological vector space over 𝕜, and the injection
from E x to bundle.total_space F E should be an embedding;
The most important condition: around each point, there should be a bundle trivialization which
is a continuous linear equiv in the fibers.

If all these conditions are satisfied, we register the typeclass
topological_vector_bundle 𝕜 F E. We emphasize that the data is provided by other classes, and
that the topological_vector_bundle class is Prop-valued.

The point of this formalism is that it is unbundled in the sense that the total space of the bundle
is a type with a topology, with which one can work or put further structure, and still one can
perform operations on topological vector bundles (which are yet to be formalized). For instance,
assume that E₁ : B → Type* and E₂ : B → Type* define two topological vector bundles over 𝕜
with fiber models F₁ and F₂ which are normed spaces. Then one can construct the vector bundle of
continuous linear maps from E₁ x to E₂ x with fiber E x := (E₁ x →L[𝕜] E₂ x) (and with the
topology inherited from the norm-topology on F₁ →L[𝕜] F₂, without the need to define the strong
topology on continuous linear maps between general topological vector spaces). Let
vector_bundle_continuous_linear_map 𝕜 F₁ E₁ F₂ E₂ (x : B) be a type synonym for E₁ x →L[𝕜] E₂ x.
Then one can endow
bundle.total_space (vector_bundle_continuous_linear_map 𝕜 F₁ E₁ F₂ E₂)
with a topology and a topological vector bundle structure.

Similar constructions can be done for tensor products of topological vector bundles, exterior
algebras, and so on, where the topology can be defined using a norm on the fiber model if this
helps.

Coauthored-by: Sebastien Gouezel sebastien.gouezel@univ-rennes1.fr

Nicknamen · 2021-03-10T12:15:51Z

Thank you very much! This is very cool! I mean, I was very uncertain about how good is it to use tactic mode inside a definition, since I always had problems with that, but, if you think that's not a problem in later proofs, this was a bit the best I could hope for, inasmuch requiring the least in definitions and getting the most out of "vector_bundle_trivialization.at"! As you said probably it is best to try to prove some simple results (I was thinking like trying to develop a bit the theory of sections)... Do you think there is anything else important to include in this PR?

sgouezel · 2021-03-10T20:19:53Z

I don't think anything else needs to be added to the PR. I can certainly not merge it myself, since I've changed the file too much, so we need to wait and see if other maintainers are happy with the design or want to modify it.

src/topology/vector_bundle.lean

Applied easy suggestions Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

semorrison · 2021-03-26T03:24:06Z

bors merge

…#4658) # Topological vector bundles In this file we define topological vector bundles. Let `B` be the base space. In our formalism, a topological vector bundle is by definition the type `bundle.total_space E` where `E : B → Type*` is a function associating to `x : B` the fiber over `x`. This type `bundle.total_space E` is just a type synonym for `Σ (x : B), E x`, with the interest that one can put another topology than on `Σ (x : B), E x` which has the disjoint union topology. To have a topological vector bundle structure on `bundle.total_space E`, one should addtionally have the following data: * `F` should be a topological vector space over a field `𝕜`; * There should be a topology on `bundle.total_space E`, for which the projection to `E` is a topological fiber bundle with fiber `F` (in particular, each fiber `E x` is homeomorphic to `F`); * For each `x`, the fiber `E x` should be a topological vector space over `𝕜`, and the injection from `E x` to `bundle.total_space F E` should be an embedding; * The most important condition: around each point, there should be a bundle trivialization which is a continuous linear equiv in the fibers. If all these conditions are satisfied, we register the typeclass `topological_vector_bundle 𝕜 F E`. We emphasize that the data is provided by other classes, and that the `topological_vector_bundle` class is `Prop`-valued. The point of this formalism is that it is unbundled in the sense that the total space of the bundle is a type with a topology, with which one can work or put further structure, and still one can perform operations on topological vector bundles (which are yet to be formalized). For instance, assume that `E₁ : B → Type*` and `E₂ : B → Type*` define two topological vector bundles over `𝕜` with fiber models `F₁` and `F₂` which are normed spaces. Then one can construct the vector bundle of continuous linear maps from `E₁ x` to `E₂ x` with fiber `E x := (E₁ x →L[𝕜] E₂ x)` (and with the topology inherited from the norm-topology on `F₁ →L[𝕜] F₂`, without the need to define the strong topology on continuous linear maps between general topological vector spaces). Let `vector_bundle_continuous_linear_map 𝕜 F₁ E₁ F₂ E₂ (x : B)` be a type synonym for `E₁ x →L[𝕜] E₂ x`. Then one can endow `bundle.total_space (vector_bundle_continuous_linear_map 𝕜 F₁ E₁ F₂ E₂)` with a topology and a topological vector bundle structure. Similar constructions can be done for tensor products of topological vector bundles, exterior algebras, and so on, where the topology can be defined using a norm on the fiber model if this helps. Coauthored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

bors · 2021-03-26T05:00:48Z

Build failed:

Lint style

src/topology/vector_bundle.lean

semorrison · 2021-03-26T06:04:57Z

bors merge

…#4658) # Topological vector bundles In this file we define topological vector bundles. Let `B` be the base space. In our formalism, a topological vector bundle is by definition the type `bundle.total_space E` where `E : B → Type*` is a function associating to `x : B` the fiber over `x`. This type `bundle.total_space E` is just a type synonym for `Σ (x : B), E x`, with the interest that one can put another topology than on `Σ (x : B), E x` which has the disjoint union topology. To have a topological vector bundle structure on `bundle.total_space E`, one should addtionally have the following data: * `F` should be a topological vector space over a field `𝕜`; * There should be a topology on `bundle.total_space E`, for which the projection to `E` is a topological fiber bundle with fiber `F` (in particular, each fiber `E x` is homeomorphic to `F`); * For each `x`, the fiber `E x` should be a topological vector space over `𝕜`, and the injection from `E x` to `bundle.total_space F E` should be an embedding; * The most important condition: around each point, there should be a bundle trivialization which is a continuous linear equiv in the fibers. If all these conditions are satisfied, we register the typeclass `topological_vector_bundle 𝕜 F E`. We emphasize that the data is provided by other classes, and that the `topological_vector_bundle` class is `Prop`-valued. The point of this formalism is that it is unbundled in the sense that the total space of the bundle is a type with a topology, with which one can work or put further structure, and still one can perform operations on topological vector bundles (which are yet to be formalized). For instance, assume that `E₁ : B → Type*` and `E₂ : B → Type*` define two topological vector bundles over `𝕜` with fiber models `F₁` and `F₂` which are normed spaces. Then one can construct the vector bundle of continuous linear maps from `E₁ x` to `E₂ x` with fiber `E x := (E₁ x →L[𝕜] E₂ x)` (and with the topology inherited from the norm-topology on `F₁ →L[𝕜] F₂`, without the need to define the strong topology on continuous linear maps between general topological vector spaces). Let `vector_bundle_continuous_linear_map 𝕜 F₁ E₁ F₂ E₂ (x : B)` be a type synonym for `E₁ x →L[𝕜] E₂ x`. Then one can endow `bundle.total_space (vector_bundle_continuous_linear_map 𝕜 F₁ E₁ F₂ E₂)` with a topology and a topological vector bundle structure. Similar constructions can be done for tensor products of topological vector bundles, exterior algebras, and so on, where the topology can be defined using a norm on the fiber model if this helps. Coauthored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

bors · 2021-03-26T11:55:23Z

Pull request successfully merged into master.

Build succeeded:

…#4658) # Topological vector bundles In this file we define topological vector bundles. Let `B` be the base space. In our formalism, a topological vector bundle is by definition the type `bundle.total_space E` where `E : B → Type*` is a function associating to `x : B` the fiber over `x`. This type `bundle.total_space E` is just a type synonym for `Σ (x : B), E x`, with the interest that one can put another topology than on `Σ (x : B), E x` which has the disjoint union topology. To have a topological vector bundle structure on `bundle.total_space E`, one should addtionally have the following data: * `F` should be a topological vector space over a field `𝕜`; * There should be a topology on `bundle.total_space E`, for which the projection to `E` is a topological fiber bundle with fiber `F` (in particular, each fiber `E x` is homeomorphic to `F`); * For each `x`, the fiber `E x` should be a topological vector space over `𝕜`, and the injection from `E x` to `bundle.total_space F E` should be an embedding; * The most important condition: around each point, there should be a bundle trivialization which is a continuous linear equiv in the fibers. If all these conditions are satisfied, we register the typeclass `topological_vector_bundle 𝕜 F E`. We emphasize that the data is provided by other classes, and that the `topological_vector_bundle` class is `Prop`-valued. The point of this formalism is that it is unbundled in the sense that the total space of the bundle is a type with a topology, with which one can work or put further structure, and still one can perform operations on topological vector bundles (which are yet to be formalized). For instance, assume that `E₁ : B → Type*` and `E₂ : B → Type*` define two topological vector bundles over `𝕜` with fiber models `F₁` and `F₂` which are normed spaces. Then one can construct the vector bundle of continuous linear maps from `E₁ x` to `E₂ x` with fiber `E x := (E₁ x →L[𝕜] E₂ x)` (and with the topology inherited from the norm-topology on `F₁ →L[𝕜] F₂`, without the need to define the strong topology on continuous linear maps between general topological vector spaces). Let `vector_bundle_continuous_linear_map 𝕜 F₁ E₁ F₂ E₂ (x : B)` be a type synonym for `E₁ x →L[𝕜] E₂ x`. Then one can endow `bundle.total_space (vector_bundle_continuous_linear_map 𝕜 F₁ E₁ F₂ E₂)` with a topology and a topological vector bundle structure. Similar constructions can be done for tensor products of topological vector bundles, exterior algebras, and so on, where the topology can be defined using a norm on the fiber model if this helps. Coauthored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>

The definition of topological vector bundle in #4658 was (inadvertently) a nonstandard definition, which agreed in finite dimension with the usual definition but not in infinite dimension. Specifically, it omitted the compatibility condition that for a vector bundle over `B` with model fibre `F`, the transition function `B → F ≃L[R] F` associated to any pair of trivializations be continuous, with respect to to the norm topology on `F →L[R] F`. (The transition function is automatically continuous with respect to the topology of pointwise convergence, which is why this works in finite dimension. The discrepancy between these conditions in infinite dimension turns out to be a [classic](https://mathoverflow.net/questions/4943/vector-bundle-with-non-smoothly-varying-transition-functions/4997#4997) [gotcha](https://mathoverflow.net/questions/54550/the-third-axiom-in-the-definition-of-infinite-dimensional-vector-bundles-why/54706#54706).) We refactor to add this compatibility condition to the definition of topological vector bundle, and to verify this condition in the existing examples of topological vector bundles (construction via a cocycle, direct sum of vector bundles, tangent bundle). Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Patrick Massot <patrickmassot@free.fr>

Nicknamen added 30 commits July 4, 2020 13:46

recreated the problem

03df6e2

Proved that continuous functions are an algebra

80b9cab

Merge branch 'master' into continuous_functions_algebra

d8ad078

Solving a conflict appeared in sheaves

56d2716

Corrected a mistake in the documentation

da64672

Solved a DANGEROUS INSTANCE problem

53b8e04

Forgot to remove #lint

fee8ca8

Making lint happy

dc6197b

Trying again to make lint happy

b807d94

Algebra structure over continuous bundled functions

4652e8a

Trying to merge

20866d7

Having problems with the merging

99cee94

Updated the code following smooth manifolds PR

ac6c3ba

Merge branch 'master' into Lie_groups

c8f1304

Merge branch 'master' into continuous_functions_algebra

f31adad

Merge branch 'continuous_functions_algebra' into continuous_bundled_map

fd3efc7

Added some documentation

a9bdde6

Merge branch 'Lie_groups' into smooth_map

1c3e998

Begun writing smooth_functions

f91678e

Merge branch 'master' into Lie_groups

46af74b

Added some documentation

f5abebf

Trying to show to Wojtek the excessive memory consumption

5288ed0

Merge branch 'master' into continuous_functions_algebra

3f5fa6d

Forgot to save files before last commit.

ee83faa

Merge branch 'master' into continuous_functions_algebra

37a21d4

Merge branch 'continuous_functions_algebra' into has_continuous_mul

629ad00

Merge branch 'has_continuous_mul' into continuous_bundled_map

ee812a2

Added some further documentation

283dd6e

Merge branch 'continuous_bundled_map' into smooth_map

3a3011d

Merge branch 'continuous_bundled_map' into Lie_groups

fcb4714

lint

09fa837