Identity up to isomorphism treated as identity in proof

Question

In the following corollary to the inverse mapping theorem by Serge Lang, Fundamentals of Differential Geometry, 1999, p.17-18, there are two things in the proof which I don't understand, the first step and the last one:

1. If there is an identity up to isomorphism between E and $ F_1 $ as established by $ f'(x_0) $, why can we limit our consideration in the proof to the actual identity? This I have seen several times in proofs, but I don't understand why it can be done here and what the precise circumstances have to be in a proof to allow for this.

2. I dont't see why the local inverse $ \big( \varphi'(0,0) \big)^{-1} $, which is called g at the end of the proof, satisfies the two requirements defined in the corollary for the map g used there.

Thanks for any help.

Notes: $E, F_1, F_2 $ are Banach spaces. "Morphism" means a $ C^p $-map with $ p \geq 1 $. "Local isomorphism" means a local $ C^p $-isomorphism (dt.: lokaler $ C^p $-Diffeomorphismus). "Toplinear isomorphism" means an isomorphism between topological vector spaces.

Maybe the following drawing is helpful:

Answer 1

The proof is indeed worded poorly wrt $\varphi'(0,0)$. It is also not necessary to do the identification $E=F_1$; the complication you get from considering them to be different is very manageable. Additionally using the word toplinear is a crime. Let me rewrite the proof with your two questions in mind:

Define $$\varphi: U\times F_2\to F_1\times F_2, \qquad (x,y)\mapsto f(x)+(0,y)$$ Then the derivative of $\varphi$ at $(x_0,0)$ is equal to $f'(x_0)+(0,\mathrm{id}_{F_2})$. Since $f'(x_0)$ is valued in $F_1$ and is a linear isomorphism you have that $\varphi'(x_0,0)$ is also a linear isomorphism.

By the inverse function theorem it follows that there is a neighbourhood $V\subseteq U\times F_2$ of $(x_0,0)$ so that $\varphi\lvert_V$ is a diffeomorphism (understood to imply $p$-times differentiable). Let $h$ denote the inverse of $\varphi\lvert_V$ and define $g:=(f'(x_0),\mathrm{id}_{F_2})\circ h$. As a composition of diffeomorphisms $g$ is a diffeomorphism. Let $U_1$ be the projection of $V$ onto the $E$ component.

Then for $x\in U_1$: $$g(f(x)) = (f'(x_0), \mathrm{id}_{F_2})\left[h(\varphi(x,0))\right]= (f'(x_0),\mathrm{id}_{F_2}) [(x,0)] = (f'(x_0)[x],0)$$ and $g\circ f$ is valued in $F_1\times\{0\}\subseteq F_1\times F_2$.