[Merged by Bors] - refactor(topology/{fiber,vector}_bundle): make `vector_bundle` a mixin #17505

hrmacbeth · 2022-11-13T00:38:46Z

Previously, is_fiber_bundle* was a propositional typeclass on a function p : Z → B, stating the existence of local trivializations covering Z. Then vector_bundle* was a class with data on a type E : X → Type* (with the projection from Σ x : B, E x to B playing the role of p), giving a fixed atlas of fibrewise-linear local trivializations.

We change this definition so that
(i) the data is all held in fiber_bundle, with vector_bundle a mixin stating fibrewise-linearity
(ii) only sigma-types can be fiber bundles, not general topological spaces

This allows bundles to carry instances of typeclasses in which the scalar field, R, does not appear as a parameter. Notably, we would like a vector bundle over R with fibre F over base B to be a charted_space (B × F), with the trivializations providing the charts. This would be a dangerous instance for typeclass inference, because R does not appear as a parameter in charted_space (B × F). But if the data of the trivializations is held in fiber_bundle, then a fibre bundle with fibre F over base B can be a charted_space (B × F), and this is safe for typeclass inference.

We expect that this refector will also streamline constructions of fibre bundles with similar underlying structure (e.g., the same bundle being both a real and complex vector bundle).

Here is the relevant Zulip discussion.

*We take the opportunity to rename topological_{fiber,vector}_bundle to {fiber,vector}_bundle, since in the upcoming definition of smooth bundles, smoothness will be another mixin for fiber_bundle.

Co-authored-by: Floris van Doorn fpvdoorn@gmail.com

I tried to do things "in place" as much as possible, to make the diff a bit clearer, so there will be a follow-up PR moving around all the lemmas and instances which used to apply to vector bundles and now apply to fiber bundles.

sgouezel

LGTM, thanks!
bors d+

sgouezel · 2022-11-13T08:56:12Z

src/topology/fiber_bundle/basic.lean


-* `is_trivial_topological_fiber_bundle F p` : Prop saying that the map `p : Z → B` between
-  topological spaces is a trivial topological fiber bundle, i.e., there exists a homeomorphism
+* `is_trivial_fiber_bundle F p` : Prop saying that the map `p : Z → B` between


I understand that this one was already there, but now it does not fit in the framework of fiber bundles since Z is not a Sigma type in general. Maybe use a different name to emphasize this, like is_homeomorphic_trivial_fiber_bundle, or something like that? Or ditch it completely? (Is it really useful?)

I will keep it (renamed) for this PR, but maybe @urkud can comment on whether he thinks it should survive. I think he authored the only file that uses it, analysis.complex.re_im_topology (where it is used to abstract slightly the proofs that re and im are quotient maps).

sgouezel · 2022-11-13T09:02:34Z

src/topology/fiber_bundle/basic.lean

-∀ x : B, ∃e : trivialization F proj, x ∈ e.base_set
+class fiber_bundle :=
+(total_space_mk_inducing [] : ∀ (b : B), inducing (@total_space_mk B E b))
+(trivialization_atlas [] : set (trivialization F (π E)))


Now that trivializations are only used in a Sigma type situation, instead of parameterizing them by the projection I wonder if we shouldn't parameterize them just by the type, i.e., write trivialization F E instead of trivialization F (π E). Probably in another PR if you think it's a good idea, though.

For myself I'm not sure. It's certainly more elegant to have the trivialization concept be adapted to the definition chosen for fibre bundles. But the more general trivializations are still (as of this PR) used in a couple of places:

for is_trivial_fiber_bundle as we are discussing in the other comment

to say that a covering map admits local trivializations

@fpvandoorn, what do you think? I think you were in favour of keeping the more general version before.

I still think it's nice to have some tools that allow you to say things similar to 𝕊³ is a fiber bundle over 𝕊². Even if we don't allow this exact statement for fiber bundles, it might be useful to keep allowing it for trivializations...

src/topology/vector_bundle/basic.lean

bors · 2022-11-13T09:13:18Z

✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

hrmacbeth · 2022-11-15T19:01:33Z

bors r+

#17505) Previously, `is_fiber_bundle`* was a propositional typeclass on a function `p : Z → B`, stating the existence of local trivializations covering `Z`. Then `vector_bundle`* was a class with data on a type `E : X → Type*` (with the projection from `Σ x : B, E x` to `B` playing the role of `p`), giving a fixed atlas of fibrewise-linear local trivializations. We change this definition so that (i) the data is all held in `fiber_bundle`, with `vector_bundle` a mixin stating fibrewise-linearity (ii) only sigma-types can be fiber bundles, not general topological spaces This allows bundles to carry instances of typeclasses in which the scalar field, `R`, does not appear as a parameter. Notably, we would like a vector bundle over `R` with fibre `F` over base `B` to be a `charted_space (B × F)`, with the trivializations providing the charts. This would be a dangerous instance for typeclass inference, because `R` does not appear as a parameter in `charted_space (B × F)`. But if the data of the trivializations is held in `fiber_bundle`, then a *fibre* bundle with fibre `F` over base `B` can be a `charted_space (B × F)`, and this is safe for typeclass inference. We expect that this refector will also streamline constructions of fibre bundles with similar underlying structure (e.g., the same bundle being both a real and complex vector bundle). [Here](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Smooth.20vector.20bundles/near/306023372) is the relevant Zulip discussion. *We take the opportunity to rename `topological_{fiber,vector}_bundle` to `{fiber,vector}_bundle`, since in the upcoming definition of smooth bundles, smoothness will be another mixin for `fiber_bundle`. Co-authored-by: Floris van Doorn [fpvdoorn@gmail.com](mailto:fpvdoorn@gmail.com)

bors · 2022-11-15T22:05:37Z

Build failed (retrying...):

Run tests

#17505) Previously, `is_fiber_bundle`* was a propositional typeclass on a function `p : Z → B`, stating the existence of local trivializations covering `Z`. Then `vector_bundle`* was a class with data on a type `E : X → Type*` (with the projection from `Σ x : B, E x` to `B` playing the role of `p`), giving a fixed atlas of fibrewise-linear local trivializations. We change this definition so that (i) the data is all held in `fiber_bundle`, with `vector_bundle` a mixin stating fibrewise-linearity (ii) only sigma-types can be fiber bundles, not general topological spaces This allows bundles to carry instances of typeclasses in which the scalar field, `R`, does not appear as a parameter. Notably, we would like a vector bundle over `R` with fibre `F` over base `B` to be a `charted_space (B × F)`, with the trivializations providing the charts. This would be a dangerous instance for typeclass inference, because `R` does not appear as a parameter in `charted_space (B × F)`. But if the data of the trivializations is held in `fiber_bundle`, then a *fibre* bundle with fibre `F` over base `B` can be a `charted_space (B × F)`, and this is safe for typeclass inference. We expect that this refector will also streamline constructions of fibre bundles with similar underlying structure (e.g., the same bundle being both a real and complex vector bundle). [Here](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Smooth.20vector.20bundles/near/306023372) is the relevant Zulip discussion. *We take the opportunity to rename `topological_{fiber,vector}_bundle` to `{fiber,vector}_bundle`, since in the upcoming definition of smooth bundles, smoothness will be another mixin for `fiber_bundle`. Co-authored-by: Floris van Doorn [fpvdoorn@gmail.com](mailto:fpvdoorn@gmail.com)

bors · 2022-11-16T01:16:36Z

Pull request successfully merged into master.

Build succeeded:

The PR #17505 was a big refactor but left declarations in place. This PR proposes a reorganization to clean up: - new file `topology.fiber_bundle.is_homeomorphic_trivial_bundle` for the legacy `is_homeomorphic_trivial_fiber_bundle` construction (see [discussion](#17505 (comment))) - new file `topology.fiber_bundle.constructions` covering the trivial, fibrewise-product and pullback fiber bundles. The trivial-bundle material was previously split between `topology.{fiber,vector}_bundle.basic`, the prod material was previously in `topology.vector_bundle.prod`, the pullback material was previously in `topology.vector_bundle.pullback` - new file `topology.vector_bundle.constructions` covering the trivial, direct-sum and pullback vector bundles. The trivial-bundle material was previously in `topology.vector_bundle.basic`, the prod material was previously in `topology.vector_bundle.prod`, the pullback material was previously in `topology.vector_bundle.pullback` - delete files `topology.vector_bundle.prod` and `topology.vector_bundle.pullback`, whose material has all been moved elsewhere - delete construction `trivialization.comap`, which was morally (though not literally) a duplicate of `trivialization.pullback` - cleaner proof of `trivialization.prod.open_source`, removing a spurious dependence on an ambient fiber bundle structure - updated and augmented docs

hrmacbeth added 15 commits November 11, 2022 22:49

test ci

b1d1cd0

fix

fde36e8

cleanup

47656f5

a little more on trivial predicate

5d14eba

long line

8334a5e

clean up diff

831df16

further cleanup

4bbb66a

weaken typeclasses in prod

f29f0f4

fix hom

806736b

drop open

535220d

fix tangent bundle

ad6ed03

fix cont_mdiff_mfderiv

8ea4adf

fix mfderiv

58d6acd

lint, tests

da29f81

lint

bc4ea98

hrmacbeth added awaiting-review The author would like community review of the PR t-differential-geometry Manifolds, etc. labels Nov 13, 2022

hrmacbeth requested a review from sgouezel November 13, 2022 00:39

sgouezel reviewed Nov 13, 2022

View reviewed changes

leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Nov 13, 2022

hrmacbeth added 3 commits November 15, 2022 11:23

implementation note in module docstring

4ef17b5

rename is_trivial_fiber_bundle

2fd395e

long lines

2bcc216

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Nov 15, 2022

bors bot changed the title ~~refactor(topology/{fiber,vector}_bundle): make vector_bundle a mixin~~ [Merged by Bors] - refactor(topology/{fiber,vector}_bundle): make vector_bundle a mixin Nov 16, 2022

bors bot closed this Nov 16, 2022

bors bot deleted the new-fiber-bundle branch November 16, 2022 01:16

hrmacbeth mentioned this pull request Nov 16, 2022

[Merged by Bors] - chore(topology/{fiber,vector}_bundle/*): reorganize files #17559

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(topology/{fiber,vector}_bundle): make `vector_bundle` a mixin #17505

[Merged by Bors] - refactor(topology/{fiber,vector}_bundle): make `vector_bundle` a mixin #17505

hrmacbeth commented Nov 13, 2022 •

edited

sgouezel left a comment

sgouezel Nov 13, 2022

hrmacbeth Nov 13, 2022

sgouezel Nov 13, 2022

hrmacbeth Nov 13, 2022

fpvandoorn Nov 17, 2022

bors bot commented Nov 13, 2022

hrmacbeth commented Nov 15, 2022

bors bot commented Nov 15, 2022

bors bot commented Nov 16, 2022

[Merged by Bors] - refactor(topology/{fiber,vector}_bundle): make vector_bundle a mixin #17505

[Merged by Bors] - refactor(topology/{fiber,vector}_bundle): make vector_bundle a mixin #17505

Conversation

hrmacbeth commented Nov 13, 2022 • edited

sgouezel left a comment

Choose a reason for hiding this comment

sgouezel Nov 13, 2022

Choose a reason for hiding this comment

hrmacbeth Nov 13, 2022

Choose a reason for hiding this comment

sgouezel Nov 13, 2022

Choose a reason for hiding this comment

hrmacbeth Nov 13, 2022

Choose a reason for hiding this comment

fpvandoorn Nov 17, 2022

Choose a reason for hiding this comment

bors bot commented Nov 13, 2022

hrmacbeth commented Nov 15, 2022

bors bot commented Nov 15, 2022

bors bot commented Nov 16, 2022

[Merged by Bors] - refactor(topology/{fiber,vector}_bundle): make `vector_bundle` a mixin #17505

[Merged by Bors] - refactor(topology/{fiber,vector}_bundle): make `vector_bundle` a mixin #17505

hrmacbeth commented Nov 13, 2022 •

edited