coordinate changes in a topological vector bundle

Stream: maths

[Floris van Doorn]

In #13175 the field continuous_coord_change was added to docs#topological_vector_bundle, defined in terms of docs#continuous_transitions.
I'm a bit confused by the definition of continuous_transitions. isn't the s in continuous_transitions just e.base_set ∩ e'.base_set? If so, is there a reason to not be more explicit in the definition of continuous_transitions?

pinging @Heather Macbeth @Patrick Massot.

[Floris van Doorn]

Oh, I'm now looking at docs#topological_vector_bundle.continuous_on_coord_change and there the s is given explicitly.

[Sebastien Gouezel]

I had started working on a branch branch#gouezel_pullback to clean up a little bit #8545. I've just seen you've started on the same lines. Along this work, I noticed the same on continuous_transitions, and I started refactoring it to include the set. I'm not done with the refactor, but if you want to pick up anything from this branch don't hesitate to do so.

[Floris van Doorn]

Interesting. I think our cleanup went into different directions, but I'll see what I can incorporate.
I just finished the proof of continuous_coord_change for pullback, but a refactor of continuous_transitions would still be helpful.

[Patrick Massot]

I also noticed while working on Hom bundles that this spelling with a mysterious set s was a bit weird.

[Patrick Massot]

And I'm very happy to read that two people were working on this pull-back stuff while I was attending a student talk and then supervising a written exam.

[Kevin Buzzard]

In 2017 I noticed that the definition of compact also had a weird s in, but Johannes Hoelzl assured me it was a good idea...

[Floris van Doorn]

I pushed a version that I think compiles, with a complete proof (it might still have linter errors).
It would still be nice to use your simplified definition of the topology on the pullback bundle. If you want, you can change that, or otherwise I'll change that at some point.

[Heather Macbeth]

Floris van Doorn said:

In #13175 the field continuous_coord_change was added to docs#topological_vector_bundle, defined in terms of docs#continuous_transitions.
I'm a bit confused by the definition of continuous_transitions. isn't the s in continuous_transitions just e.base_set ∩ e'.base_set? If so, is there a reason to not be more explicit in the definition of continuous_transitions?

pinging Heather Macbeth Patrick Massot.

@Floris van Doorn @Sebastien Gouezel I was thinking of defining, later, the structure groupoid for B × F consisting of elements satisfying continuous_transitions. The elements of this structure groupoid would have type local_equiv (B × F) (B × F) (in fact, local_homeomorph) rather than type pretrivialization -- they don't "know" their own base set.

[Heather Macbeth]

I haven't tried to define (eg) smooth vector bundles yet, but I had an idea that this groupoid approach might be useful there.

[Heather Macbeth]

Hopefully, with API like docs#topological_vector_bundle.continuous_on_coord_change, it's not too painful to work with.

[Floris van Doorn]

But currently, every time you define a topological_vector_bundle you have to prove that (e.base_set ∩ e'.base_set) ×ˢ (univ : set F) is the source of e.to_local_equiv.symm.trans e'.to_local_equiv.

I think it's better to be more explicit, and put

∃ ε : B → (F ≃L[R] F), continuous_on (λ b, (ε b : F →L[R] F)) s
    ∧ ∀ b ∈ s, ∀ v : F, e (b, v) = (b, ε b v)

as a field, where s = e.base_set ∩ e'.base_set.
Maybe we can even go crazier, and put ε in topological_vector_bundle as a data field? Or will that give the wrong notion of equality on topological_vector_bundle?

[Floris van Doorn]

If we change the definition of topological_vector_bundle, we can still obtain a continuous_transition from a topological_vector_bundle, of course.

[Heather Macbeth]

Floris van Doorn said:

But currently, every time you define a topological_vector_bundle you have to prove that (e.base_set ∩ e'.base_set) ×ˢ (univ : set F) is the source of e.to_local_equiv.symm.trans e'.to_local_equiv.

Yes, that's true. In the two examples we have already (direct sum and hom-bundle), Patrick and I had to invoke mfld_set_tac for this bookkeeping. I have no objection to either of the revised versions you suggest!

[Floris van Doorn]

I incorporated a bunch of @Sebastien Gouezel's improvements into #8545, which is now ready for review.

[Floris van Doorn]

I've started on changing the field continuous_coord_change in branch#continuous_coord_change.

[Floris van Doorn]

#14462
I think the proofs that coordinate changes are continuous are nicer/simpler with the new definitions.
There is a downside: you now have to show that the coordinate change of your new vector bundle somehow relates to the coordinate change of the existing vector bundle (e.g. the coordinate change on the product vector bundle is a prod_map of the existing coordinate changes).