feat(topology/topological_fiber_bundle): topological fiber bundles #1421
Conversation
|
I have just realized that for the very definition of fiber bundles, there is a better (more structured) version which is more efficient later on. I will switch the PR to the new definition when it is ready (and when I have checked that it works well in the application I have in mind). |
sgouezel
added
blocked-by-other-PR
sgouezel
added
awaiting-review
| * In the trivial situation of the trivial bundle where there is only one chart and one | ||
| trivialization, this construction is defeq to the canonical construction (Σ x : B, F). In the case | ||
| of the tangent bundle of manifolds, this implies that on vector spaces the derivative and the | ||
| manifold derivative are defeq. |
There was a problem hiding this comment.
Is this last sentence now true? I remember it used to be a lie.
| are in fact no dependent type difficulties here! | ||
|
|
||
| For this construction, we should thus choose for each `x` one specific trivialization around it. We | ||
| include this choice in the definition of the fiber bundle, as it makes some constructions more |
There was a problem hiding this comment.
Here you are referring to topological_fiber_bundle_core, right?
| variable (F) | ||
|
|
||
| /-- A structure extending local homeomorphisms, defining a local trivialization of a projection | ||
| `proj : Z → B` with fiber `F`, as a local homeomorphism between `Z` and `B × F`. -/ |
There was a problem hiding this comment.
This docstring misses the important information enforced in target_eq.
| map_target := λp hp, | ||
| by simpa only [set.mem_preimage, and_true, set.mem_univ, set.mem_prod] using hp, | ||
| left_inv := begin | ||
| assume p hx, |
There was a problem hiding this comment.
Why not using rintros ⟨x, v⟩ hv?
| { simp [hx] } | ||
| end, | ||
| right_inv := begin | ||
| assume p hx, |
| (Z.local_triv i).symm.trans (Z.local_triv j) ≈ Z.triv_change i j := | ||
| Z.local_triv'_trans i j | ||
|
|
||
| /-- Extended version of the local trivialization, as a bundle trivialization -/ |
There was a problem hiding this comment.
What do you mean by "extended" here?
| begin | ||
| assume s hs, | ||
| rw mem_nhds_sets_iff at hs, | ||
| rcases hs with ⟨t, st, t_open, xt⟩, |
There was a problem hiding this comment.
For your readability toolbox: do you know you can replace the above two lines by:
obtain ⟨t, st, t_open, xt⟩ : ∃ t ⊆ s, is_open t ∧ proj x ∈ t,
from mem_nhds_sets_iff.1 hs,| continuous_to_fun := continuous_on.prod continuous_fst.continuous_on (Z.coord_change_continuous i j), | ||
| continuous_inv_fun := begin | ||
| have := continuous_on.prod continuous_fst.continuous_on (Z.coord_change_continuous j i), | ||
| rwa inter_comm at this |
There was a problem hiding this comment.
by simpa [inter_comm] using continuous_on.prod continuous_fst.continuous_on (Z.coord_change_continuous j i)?
| ext p, | ||
| simp only [set.mem_preimage, and_true, set.mem_inter_eq, set.mem_univ, | ||
| topological_fiber_bundle_core.local_triv'_fst, iff_self, set.mem_prod, and_self, | ||
| topological_fiber_bundle_core.mem_local_triv'_source] |
There was a problem hiding this comment.
This is finishing, you could leave simp.
There was a problem hiding this comment.
But that might make it substantially slower...?
There was a problem hiding this comment.
I'm approving this now (at @PatrickMassot 's suggestion) so it gets merged in time for the paper release. The remaining comments are just cosmetic. Feel free to return to them any time.
robertylewis
added
ready-to-merge
…eanprover-community#1421) * feat(topology/topological_fiber_bundle): topological fiber bundles * better definition of fiber bundles
Define topological fiber bundles, check that the first and second projections in a product are indeed fiber bundles, and most importantly give a way to construct fiber bundles from a structure registering how trivialization changes act on fibers.
This has already been discussed on Zulip (see for instance https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/Manifolds/near/174669060), and the version in this PR already takes the comments in the discussion into account.
Depends on #1549