bundle of continuous linear maps

Stream: sphere eversion

[Heather Macbeth]

I'm having trouble getting the topology right for the construction of the vector bundle of continuous linear maps from E₁ to E₂, where E₁ is a vector bundle modelled on a topological (or normed if easier) vector space F₁ and E₂ is a vector bundle modelled on F₂.

I believe that to make the construction work, one needs to choose a topology on every space of operators A →L[𝕜] B, in such a way that the following two properties hold for all topological spaces B and all topological (or normed if easier) vector spaces F₁, F₂, F₃:

lemma pre (ε : B → (F₁ →L[𝕜] F₂)) (h : continuous (λ p : B × F₁, ε p.1 p.2)) :
  continuous (λ p : B × (F₂ →L[𝕜] F₃), p.2 ∘L ε p.1) :=

lemma post (ε : B → (F₂ →L[𝕜] F₃)) (h : continuous (λ p : B × F₂, ε p.1 p.2)) :
  continuous (λ p : B × (F₁ →L[𝕜] F₂), ε p.1 ∘L p.2) :=

(It may be that I have already assumed too much in reducing to these properties. But I think I can see my way to the end of the construction from here, if they work out.)

I tried proving these properties for (a) the operator norm topology, (b) the topology of pointwise convergence, and couldn't get them to work out, at least in the naive follow-one's-nose approach. In the case (a) I could reduce to a property which doesn't hold in general for (a) but does for (b), and in the case (b) I could reduce to a property which doesn't hold in general for (b) but does for (a)! See branch#vb-hom-toy .

Is there a clever way to make either (a) or (b) work? Is one of the other operator topologies more appropriate? Or did I assume too much in reducing to these two properties, perhaps there's a construction of the bundle which bypasses them?

cc @Moritz Doll @Sebastien Gouezel @Patrick Massot @Oliver Nash

[Heather Macbeth]

The only reference I know of for infinite-dimensional vector bundles is Lang's Differentiable Manifolds, and if I'm reading correctly he assumes more structure on them than mathlib does: namely a fixed collection of trivializations for the bundle, such that the coordinate changes B → (F ≃L[𝕜] F) for any pair of trivializations are continuous (wrt the operator norm topology) on the appropriate domain.

[Heather Macbeth]

Possibly relevant (but I haven't read them in detail yet):
https://mathoverflow.net/questions/4943/vector-bundle-with-non-smoothly-varying-transition-functions
https://mathoverflow.net/questions/54550/the-third-axiom-in-the-definition-of-infinite-dimensional-vector-bundles-why

[Patrick Massot]

It definitely sounds like the mathlib definition doesn't assume enough to cover infinite dimension. This is not surprising at all. Nobody here is doing differential geometry in infinite dimension, and there are lots of subtle points.

[Sebastien Gouezel]

Yes, I agree with Patrick, we have overlooked that the conditions we impose are not strong enough in general. This shows (once again) that the good stress test for definitions is trying to prove nontrivial things with them!

[Heather Macbeth]

Heather Macbeth said:

a fixed collection of trivializations for the bundle, such that the coordinate changes B → (F ≃L[𝕜] F) for any pair of trivializations are continuous (wrt the operator norm topology) on the appropriate domain.

I think it would be possible to define a structure_groupoid for B × F, such that the property here is equivalent to has_groupoid for the given trivializations.

[Heather Macbeth]

This will mean that the vector bundle definition is no longer a Prop; it will have data. (We go from the existence of trivializations, to a choice of trivializations whose coordinate changes satisfy the above property.)

[Heather Macbeth]

So, currently we have the definition

class topological_vector_bundle : Prop :=
(total_space_mk_inducing [] : ∀ (b : B), inducing (total_space_mk E b))
(locally_trivial [] : ∀ b : B, ∃ e : trivialization R F E, b ∈ e.base_set)

and this could be changed to

class topological_vector_bundle :=
(total_space_mk_inducing [] : ∀ (b : B), inducing (total_space_mk E b))
(atlas []            : set (trivialization R F E))
(chart_at []         : B → trivialization R F E)
(mem_chart_source [] : ∀ b : B, b ∈ (chart_at b).base_set)
(chart_mem_atlas []  : ∀ b : B, chart_at b ∈ atlas)

which obviously extends charted_space (B × F) (total_space E).

[Heather Macbeth]

(Just noticed @Nicolò Cavalleri is not subscribed to this stream; fixed.)

[Sebastien Gouezel]

Are you saying that the better definition of topological vector bundle in Lang does not only depend on the topology and the vector space structure in the fibers, but that there is an additional choice to be made? If that's the way to go, then so be it!

[Heather Macbeth]

That's right, the additional choice is of a collection/"atlas" of trivializations, which are mutually-compatible in the sense that the associated co-ordinate changes B → (F ≃L[𝕜] F) are continuous (on the right subset of B), for the operator-norm topology on F ≃L[𝕜] F. At the moment we only know that the associated maps B × F → F are continuous, which I think is the same as saying that the co-ordinate changes are continuous for the topology of pointwise convergence on F ≃L[𝕜] F.

[Heather Macbeth]

Also, maybe later we'll want to assume that the co-ordinate changes B → (F ≃L[𝕜] F) are $C^k$ or smooth.

[Heather Macbeth]

I sketched out a new definition of topological vector bundle at branch#vb-groupoid, open to comments!

[Nicolò Cavalleri]

Ok probably I should have followed Lang too in the first place, I did not know either that the theory was different in infinite dimensions!

[Nicolò Cavalleri]

Heather Macbeth said:

That's right, the additional choice is of a collection/"atlas" of trivializations, which are mutually-compatible in the sense that the associated co-ordinate changes B → (F ≃L[𝕜] F) are continuous (on the right subset of B), for the operator-norm topology on F ≃L[𝕜] F. At the moment we only know that the associated maps B × F → F are continuous, which I think is the same as saying that the co-ordinate changes are continuous for the topology of pointwise convergence on F ≃L[𝕜] F.

At the moment the model space fiber F is not a normed space, but just a topological vector space. What do you you mean by operator-norm topology? Just the strong topology of linear continuous maps right?

[Nicolò Cavalleri]

Btw, another nice reference besides Lang on the infinite dimensional case which does not assume the vector spaces to be Banach is "The convenient setting of global analysis" by Kriegl and Michor!

[Heather Macbeth]

Nicolò Cavalleri said:

At the moment the model space fiber F is not a normed space, but just a topological vector space. What do you you mean by operator-norm topology? Just the strong topology of linear continuous maps right?

No, Lang actually assumes that the fibre model F is a Banach space. I believe the strong topology is the topology of pointwise convergence, right? That topology's not good enough -- it doesn't satisfy that evaluation and composition are continuous, I believe.

[Heather Macbeth]

Whereas the operator norm topology does: docs#is_bounded_bilinear_map_apply, docs#is_bounded_bilinear_map_comp

[Heather Macbeth]

Nicolò Cavalleri said:

Btw, another nice reference besides Lang on the infinite dimensional case which does not assume the vector spaces to be Banach is "The convenient setting of global analysis" by Kriegl and Michor!

Yes, I looked there yesterday; they assume the vector spaces are "convenient" (a definition we don't have, but it apparently admits an appropriate generalization of the operator norm topology), and they also make the further assumption we're discussing (fixed collection of trivializations, which are mutually-compatible in the sense that the associated co-ordinate changes B → (F ≃L[𝕜] F) are continuous).

[Nicolò Cavalleri]

Heather Macbeth said:

No, Lang actually assumes that the fibre model F is a Banach space. I believe the strong topology is the topology of pointwise convergence, right? That topology's not good enough -- it doesn't satisfy that evaluation and composition are continuous, I believe.

Sorry I thought you were referring to the current code not to Lang. And no by strong topology I do not mean pointwise convergence, I mean the topology of bounded convergence (like in Wiki: https://en.wikipedia.org/wiki/Topologies_on_spaces_of_linear_maps)

[Nicolò Cavalleri]

I'd guess what Michor and Kriegl do generalizes to TVSs with that topology

[Nicolò Cavalleri]

Btw my confusion originates from the fact that from the code you rewrote up to now you did not change TVS to normed spaces so my questions better reformulated would be what was your plan to extend Lang to topological vector spaces

[Heather Macbeth]

Nicolò Cavalleri said:

Btw my confusion originates from the fact that from the code you rewrote up to now you did not change TVS to normed spaces so my questions better reformulated would be what was your plan to extend Lang to topological vector spaces

I'm not sure what you mean by this. I assumed a Banach space fibre here, and so far (the construction isn't complete yet) have used that this implies that composition and inversion on F ≃L[𝕜] F are continuous.

[Heather Macbeth]

Nicolò Cavalleri said:

by strong topology I do not mean pointwise convergence, I mean the topology of bounded convergence (like in Wiki: https://en.wikipedia.org/wiki/Topologies_on_spaces_of_linear_maps)

Maybe @Moritz Doll can tell us how far we are from having this definition? (Or is it one of the things recently added?)

[Nicolò Cavalleri]

Heather Macbeth said:

I'm not sure what you mean by this. I assumed a Banach space fibre here, and so far (the construction isn't complete yet) have used that this implies that composition and inversion on F ≃L[𝕜] F are continuous.

I only looked at the file vector_bundle and I missed it, now things make sense! At any rate it would be cool to keep the TVS generality so to take into account Frechet vector bundles too, if the the strong topology for TVS is not too hard to implement

[Kevin Buzzard]

What do people actually use in practice? Are there people solving PDEs on manifolds who need all this generality and more, or is this just the mathlib "work in maximal generality for as long as possible" thing?

[Heather Macbeth]

Here's an example I remember offhand: all the "generic" statements in Morse theory. See Theorem 5.4 in these notes by Hutchings, and the applications (eg Prop 5.5) that follow.

[Kevin Buzzard]

Oh wow, is what we have general enough to define Banach manifolds?

[Heather Macbeth]

Sébastien's manifolds are Banach manifolds!

[Heather Macbeth]

class smooth_manifold_with_corners {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
  {E : Type*} [normed_group E] [normed_space 𝕜 E]
  {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
  (M : Type*) [topological_space M] [charted_space H M] extends
  has_groupoid M (cont_diff_groupoid ∞ I) : Prop

[Kevin Buzzard]

I had never internalised this; my mental model of them was always that "probably there are some assumptions which make things locally R^n somewhere". Thanks!

[Moritz Doll]

Heather Macbeth said:

Nicolò Cavalleri said:

by strong topology I do not mean pointwise convergence, I mean the topology of bounded convergence (like in Wiki: https://en.wikipedia.org/wiki/Topologies_on_spaces_of_linear_maps)

Maybe Moritz Doll can tell us how far we are from having this definition? (Or is it one of the things recently added?)

It is rather close, it depends of course on what kind of statements you need. I am more focusing on getting the polar topologies sorted out, but after that I can do topologies for linear maps.

[Moritz Doll]

there seem to be reasons to have manifolds over Fréchet spaces: https://www.ams.org/journals/bull/1982-07-01/S0273-0979-1982-15004-2/S0273-0979-1982-15004-2.pdf

[Moritz Doll]

(we don't have Fréchet spaces yet)

[Heather Macbeth]

Moritz Doll said:

It is rather close, it depends of course on what kind of statements you need. I am more focusing on getting the polar topologies sorted out, but after that I can do topologies for linear maps.

I'll push ahead with the normed version and keep track of what properties we need. My guess would be that one needs not too much to define topological vector bundles, but rather more (perhaps a whole rewrite of docs#cont_diff?) for smooth vector bundles.

[Nicolò Cavalleri]

Moritz Doll said:

there seem to be reasons to have manifolds over Fréchet spaces: https://www.ams.org/journals/bull/1982-07-01/S0273-0979-1982-15004-2/S0273-0979-1982-15004-2.pdf

I think Fréchet manifold also come up in deformation theory!

[Nicolò Cavalleri]

Heather Macbeth said:

Moritz Doll said:

It is rather close, it depends of course on what kind of statements you need. I am more focusing on getting the polar topologies sorted out, but after that I can do topologies for linear maps.

I'll push ahead with the normed version and keep track of what properties we need. My guess would be that one needs not too much to define topological vector bundles, but rather more (perhaps a whole rewrite of docs#cont_diff?) for smooth vector bundles.

I also think this! Indeed my comment was only referring to topological vector bundles: despite I think there could be reasons to have more generality in manifolds too the dimension of the refactor is clearly very different so I was suggesting that for vector bundles just cause it seemed doable besides useful

[Heather Macbeth]

I need to (or at least ought to) stop working on this for a few days, but if anyone would like to help pick off some sorries, the approach for the redefinition should now be fairly stable. See branch#redefine-vb. The sorries in topology/vector_bundle and topology/vector_bundle_hom should hopefully be correct and doable. Making the tangent bundle a vector bundle is now a fair bit of work, so geometry/manifold/tangent_bundle now has a ton of errors which I haven't looked through carefully yet.

[Heather Macbeth]

Alternatively, we could revert #8295, so temporarily no longer have a topological_vector_bundle instance for the tangent bundle. This would allow the rest of the refactor to go through faster.

[Patrick Massot]

I'll take a look at those sorries

[Heather Macbeth]

Thanks Patrick! Many should be one-liners, so hopefully not hard to make progress.

[Patrick Massot]

I removed the first two sorries in vector_bundle.lean.

[Patrick Massot]

@Heather Macbeth do we know that inversion is continuous on F →L[R] F?

[Heather Macbeth]

Yes, under the hypothesis of completeness.

[Heather Macbeth]

Somewhere in normed_space.units

[Patrick Massot]

We don't have any completeness assumption in that vector bundle file, right?

[Heather Macbeth]

docs#normed_ring.inverse_continuous_at together with docs#continuous_linear_map.to_ring_inverse

[Heather Macbeth]

Not yet, but feel free to add it, Lang assumes Banach.

[Patrick Massot]

Maybe it's because I don't understand what you were doing.

[Patrick Massot]

Could you take a look at the diff in https://github.com/leanprover-community/mathlib/commit/f969fdc27bf9b28057803b5723eb72373601e9d2

[Patrick Massot]

I'm changing the intermediate statements in that proof, but maybe I'm simply confused.

[Heather Macbeth]

In that proof in particular I didn't think very hard about the intermediate statements, so very likely you're right.

[Heather Macbeth]

The argument is, "we want a fact about continuity of transition between e and e', let's convert that to a fact about continuity of ε", right?

[Patrick Massot]

The issue is that what seems to come naturally is the continuity of ε composed with inversion

[Patrick Massot]

The remaining sorry in my proof is have : continuous_on (λ p : B × F, (p.1, (ε p.1).symm p.2)) (s ×ˢ (univ : set F)),

[Patrick Massot]

Note the (ε p.1).symm

[Heather Macbeth]

I wonder if I should have swapped e and e' right at the start? At

(continuous_coord_change : ∀ e e' ∈ trivialization_atlas,
  continuous_transitions R B F (by exact e.to_local_equiv.symm.trans e'.to_local_equiv))

that is (in the definition of topological_vector_bundle).

[Patrick Massot]

And I find this suspicious

[Patrick Massot]

That could be the explanation

[Patrick Massot]

Maybe there is some inconsistency between the definition of topological bundles and topological vector bundles

[Heather Macbeth]

There wasn't before, so if there is, I introduced it with that axiom :upside_down:

[Heather Macbeth]

Do you want to try changing it there and all the way down?

[Patrick Massot]

What would be the new version?

[Heather Macbeth]

(continuous_coord_change : ∀ e e' ∈ trivialization_atlas,
  continuous_transitions R B F (by exact e'.to_local_equiv.symm.trans e.to_local_equiv))

[Heather Macbeth]

(swap e and e')

[Heather Macbeth]

And likewise in topological_vector_bundle_core probably (?)

[Heather Macbeth]

Heather Macbeth said:

There wasn't before, so if there is, I introduced it with that axiom :upside_down:

(I guess it's also perfectly possible that both directions are truly needed ... if so, that would be where Lang's Banach hypothesis comes in, to make inversion continuous.)

[Patrick Massot]

Switching certainly make that proof much easier

[Patrick Massot]

see https://github.com/leanprover-community/mathlib/commit/de241ba3b61f8efc70fe15a51cc6dfd18267356c

[Heather Macbeth]

Great! Now to see whether the symm pops up somewhere else ... :)

[Patrick Massot]

That file is ok at least

[Patrick Massot]

But there is still a continuous_coord_change sorry at the very bottom

[Patrick Massot]

For product bundles

[Patrick Massot]

We really struggle with naming consistency for product-related stuff. Compare docs#continuous_linear_map.prod and docs#continuous_linear_equiv.prod

[Heather Macbeth]

I got a bit of time and did one sorry from the direct sum section.

[Patrick Massot]

I finished the direct sum construction. I didn't understand why you replace one of my proofs from yesterday by a much more complicated one so I reverted that change (adding one more supporting definition to my proof).

[Patrick Massot]

I also removed two sorries from vector_bundle_hom.lean, but I should do something else this afternoon.

[Patrick Massot]

In order to deal with the remaining sorries in that proof, we may need to fill more fundamental holes. I think we don't have a topology on continuous_linear_equiv, even if everything is normed. Do you confirm? What was your plan for those sorries?

[Heather Macbeth]

Patrick Massot said:

I finished the direct sum construction. I didn't understand why you replace one of my proofs from yesterday by a much more complicated one so I reverted that change (adding one more supporting definition to my proof).

It looked simpler but then I squeezed a simp :(

[Heather Macbeth]

Patrick Massot said:

In order to deal with the remaining sorries in that proof, we may need to fill more fundamental holes. I think we don't have a topology on continuous_linear_equiv, even if everything is normed. Do you confirm?

I agree, there's no topology on continuous_linear_equiv; do we need it though?

[Heather Macbeth]

I was hoping
Patrick Massot said:

Do you confirm? What was your plan for those sorries?

I didn't think it through yet but I was hoping it (the continuity) would be some abstract nonsense from the alternative expression as

 λ x, (Φ₂ (ε₂ x)).comp (Φ₁ (ε₁ x).symm)

[Heather Macbeth]

composition is jointly continuous, Φ₂ and Φ₁ are continuous-linear so continuous, ε₂ and ε₁ are continuous_on, and (aha)! linear_equiv.symm is continuous by the argument we were discussing before, if we assume completeness.

[Patrick Massot]

Heather Macbeth said:

Patrick Massot said:

I finished the direct sum construction. I didn't understand why you replace one of my proofs from yesterday by a much more complicated one so I reverted that change (adding one more supporting definition to my proof).

It looked simpler but then I squeezed a simp :(

Even without squeezing it was longer.

[Patrick Massot]

Anyway, I'll let you handle those two sorries, I have some proofreading to do and an overdue referee report to work on. But I think we can define a topology on M ≃SL[σ] M' using the embedding into (M →SL[σ] M') × (M' →SL[σ'] M) and prove we get a topological group, and then adapt your work on inversion to prove that inversion is continuous at a continuous linear map coming from an continuous linear equiv. We'll need all this one day anyway.

[Patrick Massot]

@Heather Macbeth I pushed a continuity proof. It is rather messy and uses temporary names but it type-checks.

[Patrick Massot]

But there are rather serious elaboration issues when manipulating spaces of continuous semilinear maps. A lot of statement take ages to elaborate. This has nothing to do with proofs, the statements are slow. @Floris van Doorn if you are bored you can have a look at this branch#redefine-vb, especially src/topology/vector_bundle_hom.lean

[Floris van Doorn]

I'm currently working on exists_loops, but I'll try to take a look later.

[Heather Macbeth]

Awesome! (I'll come back to this after the talk on Saturday, sorry for the absence.)

[Heather Macbeth]

What do you think of PR'ing this now like I was proposing, temporarily reverting the claim that the tangent bundle is a vector bundle?

[Patrick Massot]

There are still two sorries in the vector_bundle_hom file, but I hope they have no mathematical content

[Heather Macbeth]

@Patrick Massot I knocked off the second-last sorry, and I also found a way to drop the completeness hypothesis (by using the reverse of one of the transition functions, so the continuity of the inverse comes for free).

[Patrick Massot]

Great!

[Patrick Massot]

I got distracted by partitions of unity that were blocking two other quests, but I'll return to vector bundles soon (but probably not today).

[Heather Macbeth]

I proved the last sorry. The proof was

⟨_, ⟨e₁, he₁, e₂, he₂, rfl⟩, rfl⟩

[Heather Macbeth]

We have the bundle of continuous linear maps! I'm going to start PR'ing, not the construction itself, but some preliminary re-working of the vector bundle files which will make the later diffs easier to read.

[Patrick Massot]

There will also be a lot of cleanup to do in https://github.com/leanprover-community/mathlib/blob/c4b598d7068e23eba51174824c033ef7810d3c99/src/topology/vector_bundle_hom.lean#L220-L271

[Patrick Massot]

We probably miss lemmas stated as explained in https://leanprover-community.github.io/mathlib_docs/notes.html#continuity%20lemma%20statement

[Heather Macbeth]

@Patrick Massot I have been getting the refactor ready for PR, branch#redefine-vb-only (this is just the refactor, not the bundle of continuous linear maps). How do you feel about this version of the abstract-nonsense argument you had disliked when it wasn't given its own declaration?

[Heather Macbeth]

I was able to prove that the tangent bundle is a vector bundle under the stricter definition, but it's messy.

[Patrick Massot]

Indeed we clearly need continuous_linear_map.prod_mapL, at least in our current way to do things. I'm still a little worried that our setup requires so much work to get such easy continuity results.

[Patrick Massot]

And we'll need a docstring for this definition.

[Patrick Massot]

And of course we florised versions, as in:

variables {R₁ : Type u₁} [nondiscrete_normed_field R₁]
  {M₁ : Type u₂} [normed_group M₁] [normed_space R₁ M₁]
  {M₂ : Type u₃} [normed_group M₂] [normed_space R₁ M₂]
  {M₃ : Type u₄} [normed_group M₃] [normed_space R₁ M₃]
  {M₄ : Type u₅} [normed_group M₄] [normed_space R₁ M₄]
  {X : Type*} [topological_space X]

lemma continuous.prod_mapL {f : X → M₁ →L[R₁] M₂} {g : X → M₃ →L[R₁] M₄}
  (hf : continuous f) (hg : continuous g) : continuous (λ x, (f x).prod_map (g x)) :=
sorry

lemma continuous.prod_map_equivL
  {f : X → M₁ ≃L[R₁] M₂} {g : X → M₃ ≃L[R₁] M₄}
  (hf : continuous (λ x, (f x : M₁ →L[R₁] M₂))) (hg : continuous (λ x, (g x : M₃ →L[R₁] M₄))) :
    continuous (λ x, ((f x).prod (g x) : M₁ × M₃ →L[R₁] M₂ × M₄)) :=
sorry

lemma continuous_on.prod_mapL
  {f : X → M₁ →L[R₁] M₂} {g : X → M₃ →L[R₁] M₄} {s : set X}
  (hf : continuous_on f s) (hg : continuous_on g s) :
  continuous_on (λ x, (f x).prod_map (g x)) s :=
sorry

lemma continuous_on.prod_map_equivL
  {f : X → M₁ ≃L[R₁] M₂} {g : X → M₃ ≃L[R₁] M₄} {s : set X}
  (hf : continuous_on (λ x, (f x : M₁ →L[R₁] M₂)) s)
  (hg : continuous_on (λ x, (g x : M₃ →L[R₁] M₄)) s) :
  continuous_on (λ x, ((f x).prod (g x) : M₁ × M₃ →L[R₁] M₂ × M₄)) s :=
sorry

[Patrick Massot]

So that https://github.com/leanprover-community/mathlib/commit/5ffef8f3901241d54b35a1549f9f6af8aa677284#diff-79d90cc0e04ff77cc1545538bb22d0bb33304bc4b687d2e3912626f2585a91c6R1051-R1054 can become exact hε.prod_map_equivL hη

[Patrick Massot]

And now I'll go teaching.

[Patrick Massot]

@Heather Macbeth I opened #13165

[Heather Macbeth]

I finished cleaning up the refactor branch and opened #13175.

[Floris van Doorn]

I merged branch#vb-hom with master.

There are some diverging changes in the vector bundle and fiber bundle file, and for now I chose the changes of the library. This breaks some definitions in the hom file. On the other hand, we should be able to use some of the new additions to the library (like docs#topological_vector_bundle.trivialization.symm) to simplify some proofs.

[Floris van Doorn]

In this branch, the definition of docs#topological_fiber_prebundle is modified to not require a topology on the fibers. Do we indeed want to make that change?

[Heather Macbeth]

I think we should make that change, yes. This is the first use of topological_fiber_prebundle as far as I know, and it's not surprising that before that constructor had been used, we hadn't thought closely about what information would typically be available during the construction.

[Floris van Doorn]

Ok, that seems reasonable. I separated that change out in #14377.

[Floris van Doorn]

In branch#vb-hom-floris I finished the definition of the topological vector bundle of continuous linear maps.
I started a new branch, because I wanted to define many notions differently (using various new definitions on trivializations, such as docs#topological_vector_bundle.pretrivialization.symm and some others in #14484).
It depends on #14462 and #14484.

[Patrick Massot]

A bunch or PRes were merged so I created branch#vb-hom-again which sits on top of branch#vb-symmL which is currently borsed. The new vector_bundle/hom.lean has sorries in this branch but hopefully @Floris van Doorn will still have an easier time picking this up than rebasing on master.

[Floris van Doorn]

Thanks! I rebased on master and fixed the proofs. I'll clean up this branch and PR it today.

[Floris van Doorn]

@Heather Macbeth on branch#vb-hom you define trivialization.continuous_linear_map for any two trivializations of the original vector bundles, not just the ones in the trivialization_atlas of the original vector bundles.
It is easy to do it for the ones in the trivialization_atlas (using trivialization_of_mem_pretrivialization_atlas), but to what extend is it reasonable to do this for any trivialization? Don't we run into trouble if we have a trivialization which has a non-continuous coordinate change function w.r.t. the standard trivializations?

[Patrick Massot]

I don't understand what is the issue. I guess the vector bundle structure is defined using the relevant trivializations, but this particular declaration is more general, although it will be useless in the general case.

[Floris van Doorn]

The topology on the fibers is also defined using the relevant trivializations.
If you want to define the continuous linear map trivialization between two trivializations e1 and e2, I think you need that e1 and e2 have continuous coordinate change w.r.t. the trivializations in the atlas.

[Patrick Massot]

What do you mean by "If you want to define the continuous linear map trivialization"? Isn't it what Heather did?

[Floris van Doorn]

No, because the continuity proof depended on the lemma continuous_triv_change_continuous_linear_map (on branch#vb-hom) that contains sorries.

I defined the bundle of continuous linear maps, I proved the lemma continuous_on_continuous_linear_map_coord_change (on branch#vb-hom-floris or branch#vb-hom-again), where I needed the hypotheses that the trivializations are in the atlas. The conclusion of my lemma is also stronger: the coordinate change function as a function into the space of continuous linear maps is continuous. This is needed since we redefined vector bundles so that they have the correct definition for infinite-dimensional spaces.

And now I'm inquiring whether it is possible to define trivialization.continuous_linear_map without assuming that the original trivializations lie in the corresponding atlases, as Heather's code claimed to do. If this is possible, I might need to prove some weaker continuity condition for the coordinate change function, which doesn't require that the trivializations are in the atlas, but I don't know what condition we would need exactly. I hope this explains my question.

[Floris van Doorn]

I opened #14541 with the vector bundle of continuous linear maps, depending on #14535 and #14539

[Patrick Massot]

Thanks! Did you see that the linter is unhappy with #14541?