## Stream: sphere eversion

### Topic: bundle of continuous linear maps

#### Heather Macbeth (Mar 19 2022 at 00:35):

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 (Mar 19 2022 at 03:29):

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 (Mar 19 2022 at 03:35):

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 (Mar 19 2022 at 09:31):

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 (Mar 19 2022 at 16:37):

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 (Mar 19 2022 at 18:18):

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 (Mar 19 2022 at 18:21):

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 (Mar 19 2022 at 18:37):

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 (Mar 19 2022 at 18:39):

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

#### Sebastien Gouezel (Mar 19 2022 at 19:40):

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 (Mar 19 2022 at 20:51):

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 (Mar 19 2022 at 20:52):

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

#### Heather Macbeth (Mar 20 2022 at 04:53):

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

#### Nicolò Cavalleri (Mar 20 2022 at 11:25):

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 (Mar 20 2022 at 12:15):

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 (Mar 20 2022 at 12:24):

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 (Mar 20 2022 at 16:16):

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 (Mar 20 2022 at 16:17):

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

#### Heather Macbeth (Mar 20 2022 at 16:19):

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 (Mar 20 2022 at 16:46):

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 (Mar 20 2022 at 16:47):

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

#### Nicolò Cavalleri (Mar 20 2022 at 16:53):

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 (Mar 20 2022 at 17:12):

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 (Mar 20 2022 at 17:17):

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 (Mar 20 2022 at 17:57):

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 (Mar 20 2022 at 18:04):

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 (Mar 20 2022 at 18:15):

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 (Mar 20 2022 at 18:24):

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

#### Heather Macbeth (Mar 20 2022 at 18:25):

Sébastien's manifolds are Banach manifolds!

#### Heather Macbeth (Mar 20 2022 at 18:26):

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 (Mar 20 2022 at 18:28):

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 (Mar 20 2022 at 18:29):

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 (Mar 20 2022 at 18:38):

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 (Mar 20 2022 at 18:41):

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

#### Heather Macbeth (Mar 20 2022 at 18:49):

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 (Mar 20 2022 at 18:52):

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 (Mar 20 2022 at 18:54):

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 (Mar 21 2022 at 18:24):

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 (Mar 21 2022 at 18:38):

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 (Mar 21 2022 at 19:39):

I'll take a look at those sorries

#### Heather Macbeth (Mar 21 2022 at 19:41):

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

#### Patrick Massot (Mar 21 2022 at 21:31):

I removed the first two sorries in vector_bundle.lean.

#### Patrick Massot (Mar 22 2022 at 10:28):

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

#### Heather Macbeth (Mar 22 2022 at 10:28):

Yes, under the hypothesis of completeness.

#### Heather Macbeth (Mar 22 2022 at 10:28):

Somewhere in normed_space.units

#### Patrick Massot (Mar 22 2022 at 10:29):

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

#### Heather Macbeth (Mar 22 2022 at 10:30):

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

#### Patrick Massot (Mar 22 2022 at 10:31):

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

#### Patrick Massot (Mar 22 2022 at 10:31):

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

#### Patrick Massot (Mar 22 2022 at 10:32):

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

#### Heather Macbeth (Mar 22 2022 at 10:35):

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

#### Heather Macbeth (Mar 22 2022 at 10:37):

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 (Mar 22 2022 at 10:37):

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

#### Patrick Massot (Mar 22 2022 at 10:38):

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 (Mar 22 2022 at 10:38):

Note the (ε p.1).symm

#### Heather Macbeth (Mar 22 2022 at 10:39):

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 (Mar 22 2022 at 10:39):

And I find this suspicious

#### Patrick Massot (Mar 22 2022 at 10:39):

That could be the explanation

#### Patrick Massot (Mar 22 2022 at 10:40):

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

#### Heather Macbeth (Mar 22 2022 at 10:40):

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

#### Heather Macbeth (Mar 22 2022 at 10:41):

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

#### Patrick Massot (Mar 22 2022 at 10:41):

What would be the new version?

#### Heather Macbeth (Mar 22 2022 at 10:42):

(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 (Mar 22 2022 at 10:42):

(swap e and e')

#### Heather Macbeth (Mar 22 2022 at 10:42):

And likewise in topological_vector_bundle_core probably (?)

#### Heather Macbeth (Mar 22 2022 at 10:47):

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 (Mar 22 2022 at 10:48):

Switching certainly make that proof much easier

#### Heather Macbeth (Mar 22 2022 at 10:52):

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

#### Patrick Massot (Mar 22 2022 at 10:53):

That file is ok at least

#### Patrick Massot (Mar 22 2022 at 10:53):

But there is still a continuous_coord_change sorry at the very bottom

#### Patrick Massot (Mar 22 2022 at 10:54):

For product bundles

#### Patrick Massot (Mar 22 2022 at 12:52):

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

#### Heather Macbeth (Mar 23 2022 at 01:30):

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

#### Patrick Massot (Mar 23 2022 at 09:57):

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 (Mar 23 2022 at 10:58):

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

#### Patrick Massot (Mar 23 2022 at 11:00):

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 (Mar 23 2022 at 11:22):

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 (Mar 23 2022 at 11:23):

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 (Mar 23 2022 at 11:26):

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 (Mar 23 2022 at 11:28):

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 (Mar 23 2022 at 11:47):

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 (Mar 23 2022 at 11:51):

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 (Mar 25 2022 at 14:27):

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

#### Patrick Massot (Mar 25 2022 at 14:30):

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 (Mar 25 2022 at 15:19):

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

#### Heather Macbeth (Mar 25 2022 at 15:48):

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

#### Heather Macbeth (Mar 25 2022 at 15:49):

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 (Mar 25 2022 at 16:02):

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

#### Heather Macbeth (Mar 29 2022 at 07:25):

@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).

Great!

#### Patrick Massot (Mar 29 2022 at 07:34):

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 (Mar 29 2022 at 20:07):

I proved the last sorry. The proof was

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


#### Heather Macbeth (Mar 29 2022 at 20:08):

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 (Mar 29 2022 at 20:12):

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 (Mar 29 2022 at 20:13):

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

#### Heather Macbeth (Apr 04 2022 at 06:12):

@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 (Apr 04 2022 at 06:14):

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

#### Patrick Massot (Apr 04 2022 at 06:42):

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 (Apr 04 2022 at 06:43):

And we'll need a docstring for this definition.

#### Patrick Massot (Apr 04 2022 at 07:11):

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 (Apr 04 2022 at 07:13):

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

#### Patrick Massot (Apr 04 2022 at 07:14):

And now I'll go teaching.

#### Patrick Massot (Apr 04 2022 at 14:00):

@Heather Macbeth I opened #13165

#### Heather Macbeth (Apr 05 2022 at 04:28):

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

#### Floris van Doorn (May 24 2022 at 17:05):

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 (May 24 2022 at 17:06):

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 (May 24 2022 at 18:16):

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 (May 25 2022 at 10:51):

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

#### Floris van Doorn (May 31 2022 at 17:31):

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 (Jun 02 2022 at 14:38):

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 (Jun 03 2022 at 09:07):

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

#### Floris van Doorn (Jun 03 2022 at 12:06):

@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 (Jun 03 2022 at 13:17):

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 (Jun 03 2022 at 13:31):

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 (Jun 03 2022 at 13:58):

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

#### Floris van Doorn (Jun 03 2022 at 14:10):

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 (Jun 04 2022 at 10:28):

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

#### Patrick Massot (Jun 05 2022 at 14:53):

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

Last updated: Dec 20 2023 at 11:08 UTC