-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(topology/vector_bundle): definition of topological vector bundle #4658
Conversation
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? |
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. |
Applied easy suggestions Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
b82c674
to
eaef82e
Compare
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>
Build failed: |
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>
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>
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>
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>
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>
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 typebundle.total_space E
whereE : B → Type*
is a function associating tox : B
the fiber overx
. This typebundle.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𝕜
;bundle.total_space E
, for which the projection toE
isa topological fiber bundle with fiber
F
(in particular, each fiberE x
is homeomorphic toF
);x
, the fiberE x
should be a topological vector space over𝕜
, and the injectionfrom
E x
tobundle.total_space F E
should be an embedding;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, andthat the
topological_vector_bundle
class isProp
-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*
andE₂ : B → Type*
define two topological vector bundles over𝕜
with fiber models
F₁
andF₂
which are normed spaces. Then one can construct the vector bundle ofcontinuous linear maps from
E₁ x
toE₂ x
with fiberE x := (E₁ x →L[𝕜] E₂ x)
(and with thetopology inherited from the norm-topology on
F₁ →L[𝕜] F₂
, without the need to define the strongtopology 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 forE₁ 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