Fiber bundles

Stream: maths

[Yury G. Kudryashov]

I have several loosely related proposals about API of fiber bundles.

See below for an updated version

Fiber bundle structure on proj : Z → B

Currently, the only surviving file about maps proj : Z → B as fiber bundles is the file about docs#Trivialization. I think that we should restore at least the topological fiber bundle definition (as a typeclass or as a bundled proj map) so that we can talk about, e.g., Hopf fibration as a fiber bundle without choosing a bijection to the sigma type.

Also, I suggest that we reformulate the definition of docs#Trivialization in terms of fiberwise maps and add a custom toLocalHomeomorph making docs#Trivialization.coe_fst, docs#Trivialization.source_eq, and docs#Trivialization.target_eq into rfls.

Fiber bundles as sigma types

I had 2 suggestions, both of them turned out to be bad ideas.

As for fibder bundles as "a topology on the sigma type with a trivialization around each point", I suggest that we drop the axiomatic approach docs#FiberBundle and deal with docs#FiberBundleCore instead. The reason is simple: except for trivial examples like the trivial bundle, I don't know any way to construct a nice TopologicalSpace structure on the sigma type.

Also, we can use Prod instead of Sigma because all fibers are defeq anyway.

[Yury G. Kudryashov]

Of course, all these suggestions are for after port.

[Yury G. Kudryashov]

@Heather Macbeth @Floris van Doorn @Moritz Doll @Sebastien Gouezel @Patrick Massot @Oliver Nash :up:

[Sebastien Gouezel]

Yury G. Kudryashov said:

Also, we can use Prod instead of Sigma because all fibers are defeq anyway.

No, because in Riemannian manifolds you want to have different norms on each fibers, so they should be types of their own, and this is much more convenient with Sigma types.

[Yury G. Kudryashov]

Our fibers are type synonyms for the same type anyway.

[Yury G. Kudryashov]

With Prod we can continue using Fiber x everywhere but avoid HEq

[Sebastien Gouezel]

I think I don't understand what you want to do. For instance, in docs#TopologicalVectorSpace.linear, we express a bunch of properties of fibers using typeclasses, which is very handy in a Sigma type situation. I don't see how you would express this kind of things if we used products.

[Yury G. Kudryashov]

The docs leads to 404

[Sebastien Gouezel]

Sorry. Is docs#Pretrivialization.linear better?

To elaborate, when you have v : E x, then you can form ⟨x, v⟩ as an element of the total space, and Lean understands its type right away. Conversely, if you have z : TotalSpace E, then if you do a case on z you get a pair ⟨x, v⟩ where Lean already knows that v is in the fiber above x, with all its classes. In a product situation, I don't see how to obtain such a transparent way to go back and forth without confusing Lean.

[Yury G. Kudryashov]

Probably, you're right. Sigma types work better with cases etc.

[Yury G. Kudryashov]

About docs#Pretrivialization.IsLinear, I suggest that we drop it (as well as the rest of the axiomatic approach to bundles on sigma types) and use docs#FiberBundleCore + docs#VectorBundleCore instead.

[Yury G. Kudryashov]

(UPD: rethinking; possibly, this is not a very good idea)

[Yury G. Kudryashov]

If we drop it and reformulate constructions like prod in terms of FiberBundleCore, then fibers will unfold to products of model spaces, not of fibers.

[Yury G. Kudryashov]

So, scratch that.

[Yury G. Kudryashov]

Thank you!

[Yury G. Kudryashov]

As for the first suggestion, nothing in the definition of docs#FiberBundle needs the total space to be a sigma type. I think that we can have this definition for any type, then restrict to a sigma type for definition/lemmas that need it (and for vector bundles).

[Yury G. Kudryashov]

Updated proposal

Trivializations

• Redefine docs#Trivialization in terms of fiberwise maps (maps Z → F and B → F → Z with properties).
• Define Trivialization.toLocalHomeomorph with docs#Trivialization.coe_fst, docs#Trivialization.source_eq, and docs#Trivialization.target_eq true by definition.
• (?) Define a constructor from a LocalHomeomorph with extra assumptions.

Fiber bundle structure on proj : Z → B

• Generalize docs#FiberBundle to any map, not just Sigma.fst.
• docs#VectorBundle deals with FiberBundle for Sigma.fst.

Fiber bundles on docs#Bundle.TotalSpace

• (?) Make docs#Bundle.TotalSpace.proj semireducible.
• Alternatively, use an entirely new type instead of Sigma. We don't need much API about Sigma anyway and Lean 4 simp can't use, e.g., docs#Sigma.mk.inj_iff for elements of the docs#Bundle.TotalSpace.

[Floris van Doorn]

Yes, I like these suggestions.

I briefly tried the trivialization refactor in branch3#trivialization_definitional_fiberwise, but there I also changed Z to total_space E at the same time; I realize now that this was not necessary.

I'm happy with the FiberBundle suggestions.

We are definitely having a bit of a mess with Bundle.TotalSpace.proj vs Sigma.fst. The first thing that has to be done there is to remove the simp attribute from Bundle.TotalSpace.proj and instead make Bundle.TotalSpace.proj the simp-normal form (assuming we can do that without changing the behavior for ordinary sigma-types).

[Yury G. Kudryashov]

We can do it by using a new type instead of Sigma. I think that we don't need much of the API.

[Floris van Doorn]

Probably not too much, but we might still want some of the equivalences on Sigma. If you prefer a new structure, that's fine by me.

[Yury G. Kudryashov]

I'll complete the port first, then do the Trivialization refactor. Then we'll see.

[Yury G. Kudryashov]

I'm redefining bundle.total_space so that it depends on F. I'm trying to switch to a custom structure at the same time. The first field will be called proj. What is a good name for the second field?

[Yury G. Kudryashov]

Thinking about docs#Trivialization again, I tihnk that we should move to the docs#Bundle everywhere, make API as nice as we can get in this case, move everything about it to the Bundle namespace, then add abstract fiber bundles in a new namespace.

[Yury G. Kudryashov]

E.g., this way the inverse map can be from F to E x, not to Z.