Composition of immersions is an immersion: infinite-dimensio

Stream: mathlib4

[Michael Rothgang]

I'm working on a mathlib-level definition of immersions of smooth manifolds. The correct definition is "f: M \to N is a C^k immersion if around each x : M, there are charts of M and N around x and f x, respectively, in which f looks like u\mapso (u,0)`.

In finite dimensions, this is equivalent to the familiar definition "f is an immersion iff each differential mfderiv I I' f x is injective. In infinite-dimensional (e.g. Banach) manifolds, mere injectivity is weaker than the property we want.

So far, so good. The question I'm struggling with is "is the composition of immersions an immersion"?
In finite dimensions, the answer is clearly yes (by the chain rule, the composition of injective maps is injective).
In infinite dimensions, I feel the answer should be yes. (For instance, if M is an embedded submanifold of N and N is an embedded submanifold of P, we'd like M to be an embedded submanifold of P --- so embedded "ought to be" stable under composition, and so should immersions.) But I find this much less obvious to prove.

Approach 1. Follow the definition; let x : M be arbitrary.
Since pick charts \phi near x and \psi near f x, and charts \psi' near f x and \chi near g (f x) such that

• f looks like the inclusion in charts \phi and \psi,
• g looks like the inclusion in charts \psi' and \chi.
  If \psi nad psi' were the same chart, we'd be very happy: but a priori, nothing forces them to be.

Approach 2. Looking at other textbooks, Lang (Fundamentals of differential geometry (1999)) proves that being an immersion at x is equivalent to the differential mfderiv I I' f x being a split continuous linear map (i.e., being injective, having closed range and the range admitting a closed complement). (See page 27; this uses the inverse function theorem.)
This looks like an approach which could prove composition. However, trying to formalise this in Lean gets me stuck also --- at trying to prove the sum of two closed submodules is closed. (See #23186, at this sorry.)

Thoughts about this are very appreciated. In case "being a submanifold" is no longer transitive in the Banach setting, that would at least be good to know.

[Michael Rothgang]

Further data points: Schmeding, Section 1.4 poses "the composition of submersions is a submersion" as an exercise, but makes no statement about immersions. (They work with locally convex spaces, which is a bit more general that mathlib's setting.)

[Sébastien Gouëzel]

If I read you correctly, you are asking the following question (which is now a pure linear-algebra question). Let A and B be two linear maps between Banach spaces which are injective, with closed range (equivalently, ||A x|| ≥ c ||x|| for a positive constant c), and with complemented range. Then is the same true for the composition of A and B?

[Michael Rothgang]

"Complemented range" might mean "closed complement".
I'm not exactly sure about that. I double-checked with another source: yes, closed is required. Makes more sense also.

[Michael Rothgang]

In fact, with just any complement, the result is not difficult.

[Sébastien Gouëzel]

I think the answer is yes. Injectivity and anti-Lipschitz compose obviously, so the question is the complemented range. Being complemented is the same as being the image of a continuous projection (or the kernel, it's equivalent). Let A : E -> F and B : F -> G. Let p_B : G -> range B be a continuous projection and p_A : F -> range E. Then B o p_A o B^{-1} o p_B should be a continuous projection on the range of B o A, if I'm not mistaken.

[Sébastien Gouëzel]

You can also write this by taking C_B a complement of the range of B, and C_Aa complement of the range of A. Then B(C_A) + C_B is a complement of the range of B o A, and the question is whether it's closed. In general, the sum of two closed subspaces has no reason to be closed, but here the two components live in the closed direct sum range B + C_B, so there is no problem.

[Sébastien Gouëzel]

(Because the norm on range B + C_B is equivalent to the max of the norms of the components, where the inequality ||(x, y)|| ≤ max ||x|| ||y|| is obvious, and the other one comes from the continuity of the projections on range B and C_B respectively)

[Michael Rothgang]

Thanks! I also think, B o p_A o B^{-1} o p_B should be a projection, so that would work.

[Michael Rothgang]

Sébastien Gouëzel said:

You can also write this by taking C_B a complement of the range of B, and C_Aa complement of the range of A. Then B(C_A) + C_B is a complement of the range of B o A, and the question is whether it's closed. In general, the sum of two closed subspaces has no reason to be closed, but here the two components live in the closed direct sum range B + C_B, so there is no problem.

That was what I had tried, and I got stuck at "why is the sum of the complements closed".

[Christian Merten]

For approach 1: Can't you restrict to an open neighbourhood of f x inside the intersection of the two charts around f x?

[Sébastien Gouëzel]

Here is a proof by hand that B(C_A) + C_B is closed.

[Sébastien Gouëzel]

Take a sequence (u_n) in B(C_A) + C_B which is converging. By continuity of the projections, their components x_n and y_n in range B and C_B both converge. As B is antilipschitz, B^{-1}(x_n) is also converging. As all of them belong to C_A, which is closed, B^{-1} x_n converges to a point in C_A. Therefore, by continuity of B, the sequence x_n = B (B^{-1} x_n) converges to a limit in B(C_A). Finally, u_n = x_n + y_n is converging to a point which is the sum of a point in B(C_A) and a point in C_B, qed.

[Michael Rothgang]

Thanks a lot! I will digest this, and complete my PR accordingly.