Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Banach-Space Differential Calculus and Banach Manifolds

1 · Prerequisites

2 · Summary

This page supplies the nonlinear differential calculus that the linear operator theory of the preceding pages does not contain, and it does so in the Fréchet, not the Gâteaux, sense: over the real field throughout, a derivative is a bounded linear operator satisfying a uniform $o (∥ h ∥)$ remainder estimate. The opening definition fixes that convention, the uniqueness lemma makes the notation $D f (x)$ legitimate, and the sum, bounded-bilinear product and chain rules are proved at a single point at a time, with no continuity of any derivative assumed. The class $C^{k}$ is then defined recursively with derivatives valued in spaces of bounded operators under the operator norm, and the mean value estimate on a convex set is proved through the Hahn--Banach norming functional and the scalar mean value theorem — the one step on this page that spends the Axiom of Choice.

The first half closes with the two local existence theorems for maps between Banach spaces. The inverse function theorem normalises the derivative to the identity and runs the contraction argument on a closed ball: the inverse is constructed, shown Lipschitz, differentiated, and then shown to be of class $C^{k}$ by differentiating the identity $D g = i n v \circ D f \circ g$ and using the Neumann series for operator inversion. The implicit function theorem is the standard reduction of the equation $F (x, y) = 0$ to the inverse theorem applied to $(x, y) \mapsto (x, F (x, y))$ , followed by the derivative formula $D g = - D_{y} F^{- 1} D_{x} F$ along the graph.

The second half turns to manifolds: a $C^{k}$ Banach manifold is a Hausdorff, second-countable space with a $C^{k}$ atlas modelled on a real Banach space, and a map between such manifolds is $C^{k}$ when all its coordinate representatives are. Tangent vectors are defined as chart-coordinate velocities modulo the transition-derivative relation, the differential is defined through coordinate representatives, and the chart independence of both, together with functoriality, is proved from the chain rule. Split submanifolds are defined by the existence of charts that flatten them onto a slice $E_{0} \times {0}$ with $E_{0}$ complemented, and the regular value theorem is proved by applying the implicit function theorem in a complement of the kernel: its domain carries a maximal specified atlas, the kernel is printed as a complemented subspace in the hypothesis, and the closing remark explains why surjectivity alone cannot replace it.

The final block treats the infinite-dimensional transversality package: smooth Banach vector bundles and their sections, the vertical derivative at a zero of a section and its independence of the local trivialisation, the theorem that a section transverse to the zero section — vertical derivative onto with complemented kernel, on a domain with maximal specified atlas — has a split zero submanifold with tangent equal to that kernel, the definition of a Fredholm map between Banach manifolds with its pointwise index, the local finite-dimensional reduction of a Fredholm map to the normal form $(u, v) \mapsto (u, g (u, v))$ with finite-dimensional obstruction map $g$ . Two following draft remarks explicitly record Smale's external countable proper-localization and nowhere-dense critical-image results; they are the bounded backward prerequisites for the existing DT-4 Sard--Smale theorem and are not local proofs. The block ends with local constancy of the index, which makes the index constant on connected components.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Fréchet derivative between Banach spaces

Definition

On this page the scalar field is the field $R$ of real numbers: $X$ , $Y$ and $Z$ always denote real Banach spaces (Banach space) and $U \subseteq X$ always denotes an open subset of $X$ , in the metric topology of the norm (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

Let $f : U \to Y$ be a map and let $x \in U$ . For a bounded linear operator $T \in B (X, Y)$ (A bounded linear operator between normed spaces, The spaces (\mathcal B(X,Y)) and (\mathcal B(X)) of bounded linear operators) write

$r (h) : = f (x + h) - f (x) - T h (h \in X, x + h \in U) .$

Then $f$ is Fréchet differentiable at $x$ when there is $T \in B (X, Y)$ with

$\lim_{\begin{array}{c} h \to 0 \\ h \neq 0 \end{array}} \frac{∥ f (x + h) - f (x) - T h ∥}{∥ h ∥} = 0,$

the limit being taken over those $h$ with $x + h \in U$ . Such an operator $T$ is a Fréchet derivative of $f$ at $x$ , written $T = D f (x)$ , and $∥ T ∥$ is its operator norm (The operator norm as the least bound and as the unit-sphere or unit-ball supremum). When $f$ is Fréchet differentiable at every point of $U$ , $f$ is differentiable on $U$ and the derivative is the map $D f : U \to B (X, Y)$ , $x \mapsto D f (x)$ .

Remarks

The limit is a genuine two-sided limit. Since $U$ is open and $x \in U$ , there is $ρ > 0$ with $x + h \in U$ whenever $∥ h ∥ < ρ$ . The condition above is therefore a statement about a punctured neighbourhood of $0$ , and no one-sided or directional restriction is imposed on $h$ . The quantity displayed is defined for every $h \neq 0$ with $x + h \in U$ , and it is $0$ at $h = 0$ by convention only, which is why $h \neq 0$ is written out.
The $ε$ - $δ$ form. The displayed limit says exactly: for every real $ε > 0$ there is a real $δ > 0$ such that $∥ r (h) ∥ \leq ε ∥ h ∥ whenever ∥ h ∥ < δ and x + h \in U .$ This is the form used in every estimate on this page, and it is the form in which the remainder is written $r (h) = o (∥ h ∥)$ .
The derivative is unique when it exists, so the notation $D f (x)$ is unambiguous; this is proved as the next item on the page, The Fréchet derivative is unique.
Differentiability at $x$ implies continuity at $x$ . Take $ε = 1$ in the previous remark and let $∥ h ∥ < δ$ with $x + h \in U$ . Then $∥ f (x + h) - f (x) ∥ \leq ∥ T h ∥ + ∥ r (h) ∥ \leq (∥ T ∥ + 1) ∥ h ∥,$ so every $η > 0$ is met by $∥ f (x + h) - f (x) ∥ < η$ once $∥ h ∥ < \min {δ, η / (∥ T ∥ + 1)}$ (the case $∥ T ∥ + 1$ being positive); this is continuity of $f$ at $x$ in the $ε$ - $δ$ form (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form). No separate hypothesis of continuity is ever needed with differentiability.
Fréchet, not Gâteaux or directional. The derivative $T$ is required to be a bounded linear operator defined on all of $X$ , and the remainder is measured against $∥ h ∥$ uniformly over all directions. The weaker notions that test only $h = t v$ along single lines, or that require merely $∥ r (h) ∥ / ∥ h ∥ \to 0$ along each such line, are not used anywhere on this page: every statement below is about the Fréchet derivative, and the inverse and implicit function theorems in particular are proved for it.
Graphs and affine maps. A bounded linear $T \in B (X, Y)$ is differentiable at every $x \in X$ with $D T (x) = T$ , since the remainder vanishes identically; and the derivative of a constant map is $0$ . In particular an affine map $x \mapsto y_{0} + T (x - x_{0})$ has derivative $T$ everywhere. These instances are used without further comment.

LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

The Fréchet derivative is unique

Statement

Let $U \subseteq X$ be open in a real Banach space $X$ , let $f : U \to Y$ map to a real Banach space $Y$ , and let $x \in U$ . If $A, B \in B (X, Y)$ both satisfy the Fréchet remainder condition for $f$ at $x$ , that is

$\lim_{\begin{array}{c} h \to 0 \\ h \neq 0 \end{array}} \frac{∥ f (x + h) - f (x) - A h ∥}{∥ h ∥} = 0 and \lim_{\begin{array}{c} h \to 0 \\ h \neq 0 \end{array}} \frac{∥ f (x + h) - f (x) - B h ∥}{∥ h ∥} = 0,$

then $A = B$ .

Facts & Assumptions

Given: An open $U$ in a real Banach space $X$ , a map $f : U \to Y$ , a point $x \in U$ , and $A, B \in B (X, Y)$ satisfying the two remainder conditions. Write $r_{A} (h) : = f (x + h) - f (x) - A h$ and $r_{B} (h) : = f (x + h) - f (x) - B h$ .

[L1]

The remainder condition means: for every real $ε > 0$ there is a real $δ > 0$ such that $∥ r_{A} (h) ∥ \leq ε ∥ h ∥$ and $∥ r_{B} (h) ∥ \leq ε ∥ h ∥$ whenever $∥ h ∥ < δ$ and $x + h \in U$ (Fréchet derivative between Banach spaces).

[L2]

The norm satisfies the triangle inequality $∥ u + v ∥ \leq ∥ u ∥ + ∥ v ∥$ , absolute homogeneity $∥ λ u ∥ = ∣ λ ∣ ∥ u ∥$ for real $λ$ , and separation $∥ u ∥ = 0 \Rightarrow u = 0$ (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

[L3]

Since $U$ is open and $x \in U$ , there is a real $ρ > 0$ such that $x + h \in U$ whenever $∥ h ∥ < ρ$ (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

Proof

technique · direct

1.1

Fix $v \in X$ with $v \neq 0$ ; by [L3] there is $ρ > 0$ such that $x + h \in U$ whenever $∥ h ∥ < ρ$ , so $x + t v \in U$ for every real $t$ with $∣ t ∣ ∥ v ∥ < ρ$ , that is for every $t$ with $∣ t ∣ < ρ / ∥ v ∥$ .

L3algebra

2.1

For every real $t \neq 0$ with $∣ t ∣ < ρ / ∥ v ∥$ the two remainders at $h = t v$ satisfy $r_{A} (t v) - r_{B} (t v) = - (t A v - t B v)$ , hence $t (A - B) v = r_{B} (t v) - r_{A} (t v), ∥ (A - B) v ∥ \leq \frac{∥ r_{A} (t v) ∥ + ∥ r_{B} (t v) ∥}{∣ t ∣} .$

step 1.1L2algebra

3.1

For real $t$ with $0 < ∣ t ∣ < ρ / ∥ v ∥$ one has $∥ t v ∥ = ∣ t ∣ ∥ v ∥$ , so the right-hand side of [step 2.1] equals $∥ v ∥ (∥ r_{A} (t v) ∥ / ∥ t v ∥ + ∥ r_{B} (t v) ∥ / ∥ t v ∥)$ , and the two quotients tend to $0$ as $t \to 0$ by [L1] applied with $h = t v$ , since $∥ t v ∥ \to 0$ .

L1step 2.1algebra

3.2

Given a real $ε > 0$ , [L1] supplies $δ > 0$ with $∥ r_{A} (h) ∥ \leq ε ∥ h ∥$ and $∥ r_{B} (h) ∥ \leq ε ∥ h ∥$ for $∥ h ∥ < δ$ ; applying [step 2.1] to $h = t v$ with $0 < ∣ t ∣ < \min {ρ / ∥ v ∥, δ / ∥ v ∥}$ gives $∥ (A - B) v ∥ \leq 2 ∥ v ∥ ε$ . As $ε > 0$ was arbitrary, $∥ (A - B) v ∥ = 0$ , and [L2] gives $(A - B) v = 0$ .

L1step 2.1L2choose

4.1

The vector $v \neq 0$ was arbitrary, so $(A - B) v = 0$ for every nonzero $v$ ; for $v = 0$ linearity of $A - B$ gives $(A - B) 0 = 0$ as well. Hence $A - B = 0$ , that is $A = B$ .

step 3.2algebra∎

TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Chain sum product and composition rules for Banach derivatives

Statement

Let $U \subseteq X$ be open in a real Banach space $X$ , and let $Y$ , $Z$ , $W$ be real Banach spaces. Then:

Sum rule. If $f_{1}, f_{2} : U \to Y$ are Fréchet differentiable at $x \in U$ and $a, b \in R$ , then $a f_{1} + b f_{2}$ is Fréchet differentiable at $x$ with $D (a f_{1} + b f_{2}) (x) = a D f_{1} (x) + b D f_{2} (x)$ .
Bounded-bilinear product rule. If $f : U \to Y$ and $g : U \to Z$ are Fréchet differentiable at $x$ , and $B : Y \times Z \to W$ is bounded bilinear, then $U ∋ u \mapsto B (f (u), g (u))$ is Fréchet differentiable at $x$ and

$D (B (f, g)) (x) h = B (D f (x) h, g (x)) + B (f (x), D g (x) h) (h \in X) .$

Chain rule. If $f : U \to Y$ is Fréchet differentiable at $x$ , if $W_{0} \subseteq Y$ is an open set with $f [U] \subseteq W_{0}$ , and if $g : W_{0} \to Z$ is Fréchet differentiable at $f (x)$ , then $g \circ f$ is Fréchet differentiable at $x$ and $D (g \circ f) (x) = D g (f (x)) D f (x) .$

No continuity of any derivative map is assumed; these are pointwise statements about one $x$ at a time.

Facts & Assumptions

Given: An open $U \subseteq X$ in a real Banach space $X$ , real Banach spaces $Y, Z, W$ , and $x \in U$ . The three claims have separate map data:

For claim 1, $f_{1}, f_{2} : U \to Y$ are differentiable at $x$ and $a, b \in R$ .
For claim 2, $f : U \to Y$ and $g : U \to Z$ are differentiable at $x$ , and $B : Y \times Z \to W$ is bounded bilinear with a constant $C \geq 0$ as in [L3].
For claim 3, $f : U \to Y$ is differentiable at $x$ , $W_{0} \subseteq Y$ is open with $f [U] \subseteq W_{0}$ , and $g : W_{0} \to Z$ is differentiable at $f (x)$ .

The symbols $f, g$ are local to their respective claims. Throughout the proof, source increments $h$ satisfy $x + h \in U$ ; in claim 3 this guarantees $y + k (h) = f (x + h) \in W_{0}$ .

[L1]

Fréchet differentiability at $x$ with derivative $T$ means that for every real $ε > 0$ there is a real $δ > 0$ such that $∥ f (x + h) - f (x) - T h ∥ \leq ε ∥ h ∥$ for every $h$ with $∥ h ∥ < δ$ and $x + h \in U$ (Fréchet derivative between Banach spaces).

[L2]

The norm satisfies the triangle inequality $∥ u + v ∥ \leq ∥ u ∥ + ∥ v ∥$ , absolute homogeneity $∥ λ u ∥ = ∣ λ ∣ ∥ u ∥$ , and separation $∥ u ∥ = 0 \Rightarrow u = 0$ (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

[L3]

A bounded bilinear map $B$ has a real constant $C \geq 0$ with $∥ B (u, v) ∥ \leq C ∥ u ∥ ∥ v ∥$ for all $u, v$ , and is jointly continuous (A bounded bilinear map between normed spaces, For a bilinear map, boundedness is equivalent to joint continuity).

[L4]

Linear combinations of bounded linear operators with a common source and target are bounded linear. A composite of bounded linear operators is bounded linear, and $∥ S T ∥ \leq ∥ S ∥ ∥ T ∥$ ; the operator norm satisfies $∥ T u ∥ \leq ∥ T ∥ ∥ u ∥$ (Composition satisfies |ST|\le|S|,|T|, The operator norm as the least bound and as the unit-sphere or unit-ball supremum, The spaces (\mathcal B(X,Y)) and (\mathcal B(X)) of bounded linear operators).

[L5]

If two bounded linear operators satisfy the Fréchet remainder condition for the same map at the same point, they are equal (The Fréchet derivative is unique).

Proof

technique · direct

1.1

For claim 1, write $T : = a D f_{1} (x) + b D f_{2} (x)$ , a bounded linear operator by [L4], and $r (h) : = a f_{1} (x + h) + b f_{2} (x + h) - a f_{1} (x) - b f_{2} (x) - T h$ , which equals $a r_{1} (h) + b r_{2} (h)$ with $r_{j} (h) : = f_{j} (x + h) - f_{j} (x) - D f_{j} (x) h$ . Then $∥ r (h) ∥ / ∥ h ∥ \leq ∣ a ∣ ∥ r_{1} (h) ∥ / ∥ h ∥ + ∣ b ∣ ∥ r_{2} (h) ∥ / ∥ h ∥$ for $h \neq 0$ , and both terms tend to $0$ by [L1]; hence $a f_{1} + b f_{2}$ is differentiable at $x$ with derivative $T$ , which is claim 1.

L1L2L4algebra

1.2

For claim 2 define $L (h) : = B (D f (x) h, g (x)) + B (f (x), D g (x) h)$ for $h \in X$ . Since $D f (x)$ , $D g (x)$ are linear and $B$ is bilinear, $L$ is linear, and $∥ L (h) ∥ \leq C (∥ D f (x) ∥ ∥ g (x) ∥ + ∥ f (x) ∥ ∥ D g (x) ∥) ∥ h ∥$ by [L3] and [L4], so $L$ is a bounded linear operator $X \to W$ .

L3L4algebra

1.3

For claim 3 let $T : = D f (x)$ and $S : = D g (f (x))$ , write $y : = f (x)$ , $R (k) : = g (y + k) - g (y) - S k$ for $k \in Y$ with $y + k \in W_{0}$ , and $r (h) : = f (x + h) - f (x) - T h$ . Put $k (h) : = f (x + h) - f (x) = T h + r (h)$ ; then $g (f (x + h)) - g (f (x)) - S T h = S r (h) + R (k (h))$ identically in $h$ . Given a real $η > 0$ , apply [L1] for $g$ at $y$ with $ε : = η / (2 (∥ T ∥ + 1))$ to get $δ_{1} > 0$ with $∥ R (k) ∥ \leq \frac{η}{2 (∥ T ∥ + 1)} ∥ k ∥$ for $∥ k ∥ < δ_{1}$ , and apply [L1] for $f$ at $x$ with $ε : = 1$ and with $ε : = η / (2 (1 + ∥ S ∥))$ to get a single $δ_{2} > 0$ such that for $∥ h ∥ < δ_{2}$ both $∥ k (h) ∥ \leq (∥ T ∥ + 1) ∥ h ∥$ and $∥ r (h) ∥ \leq \frac{η}{2 (1 + ∥ S ∥)} ∥ h ∥$ hold (take the smaller of the two thresholds). Then for $∥ h ∥ < \min {δ_{2}, δ_{1} / (∥ T ∥ + 1)}$ one has $∥ R (k (h)) ∥ \leq \frac{η}{2} ∥ h ∥$ and $∥ S r (h) ∥ \leq ∥ S ∥ ∥ r (h) ∥ \leq \frac{η}{2} ∥ h ∥$ , so $∥ g (f (x + h)) - g (f (x)) - S T h ∥ \leq η ∥ h ∥$ . Hence the bounded linear operator $S T$ of [L4] satisfies the remainder condition for $g \circ f$ at $x$ , and by [L5] it is the derivative, which is claim 3.

L1L4L5algebra

2.1

For claim 2 put $Δ_{f} (h) : = f (x + h) - f (x)$ , $Δ_{g} (h) : = g (x + h) - g (x)$ , so that $Δ_{f} (h) = D f (x) h + r_{f} (h)$ and $Δ_{g} (h) = D g (x) h + r_{g} (h)$ with remainders $r_{f}, r_{g}$ as in [L1]. By bilinearity, expanding $B (f (x) + Δ_{f}, g (x) + Δ_{g})$ gives $B (f (x + h), g (x + h)) - B (f (x), g (x)) - L (h) = B (r_{f} (h), g (x)) + B (f (x), r_{g} (h)) + B (Δ_{f} (h), Δ_{g} (h)),$ because $B (Δ_{f}, g (x)) = B (D f (x) h, g (x)) + B (r_{f}, g (x))$ and likewise in the second variable, while the cross term is $B (Δ_{f}, Δ_{g})$ .

step 1.2L3algebra

3.1

For $∥ h ∥$ small, [L1] with $ε = 1$ gives $∥ Δ_{f} (h) ∥ \leq (∥ D f (x) ∥ + 1) ∥ h ∥$ and $∥ Δ_{g} (h) ∥ \leq (∥ D g (x) ∥ + 1) ∥ h ∥$ . Combining this with [step 2.1] and [L3], $∥ B (f (x + h), g (x + h)) - B (f (x), g (x)) - L (h) ∥ \leq C ∥ r_{f} (h) ∥ ∥ g (x) ∥ + C ∥ f (x) ∥ ∥ r_{g} (h) ∥ + C (∥ D f (x) ∥ + 1) (∥ D g (x) ∥ + 1) ∥ h ∥^{2} .$ Dividing by $∥ h ∥$ for $h \neq 0$ and letting $h \to 0$ , every term tends to $0$ by [L1], so the left-hand side is $o (∥ h ∥)$ and the bounded linear operator $L$ of [step 1.2] satisfies the remainder condition for $B (f, g)$ at $x$ ; by [L5] it is the derivative, which is claim 2.

step 1.2L1L3L5algebra

4.1

Claim 1 is [step 1.1], claim 2 is [step 3.1], and claim 3 is [step 1.3]; this is exactly the conjunction stated.

step 1.1step 1.3step 3.1∎

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

C k map between Banach spaces

Definition

Let $X$ and $Y$ be real Banach spaces and let $U \subseteq X$ be open. All derivatives below are Fréchet derivatives (Fréchet derivative between Banach spaces), and all continuity is with respect to the norm metrics (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form).

$f : U \to Y$ is of class $C^{0}$ when $f$ is continuous on $U$ .
$f$ is of class $C^{1}$ when $f$ is differentiable on $U$ and its derivative map $D f : U \to B (X, Y)$ is continuous for the operator norm on $B (X, Y)$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum, The spaces (\mathcal B(X,Y)) and (\mathcal B(X)) of bounded linear operators).
For $k \geq 1$ define the spaces of iterated derivative values by $B_{0} : = Y, B_{k} : = B (X, B_{k - 1}) .$ Each $B_{k}$ is a real Banach space for the operator norm, by induction on $k$ from If (Y) is Banach then (\mathcal B(X,Y)) is Banach. Then $f$ is of class $C^{k}$ when $f$ is of class $C^{k - 1}$ , the map $D^{k - 1} f : U \to B_{k - 1}$ is differentiable on $U$ , where $D^{0} f : = f$ , and the $k$ -th derivative $D^{k} f : U \to B_{k}$ is continuous for the operator norm on $B_{k}$ . We write $D^{k} f (x)$ for the value at $x$ .
$f$ is of class $C^{\infty}$ when $f$ is of class $C^{k}$ for every $k \geq 0$ .

For open sets $U \subseteq X$ and $V \subseteq Y$ , a map $f : U \to V$ is a $C^{k}$ diffeomorphism when it is a bijection, $f$ is of class $C^{k}$ and $f^{- 1} : V \to U$ is of class $C^{k}$ ; likewise with $C^{\infty}$ in place of $C^{k}$ .

Remarks

Currying and the joint norm. The space $B_{k}$ of the definition is canonically identified with the space of bounded $k$ -linear maps $X^{k} \to Y$ by currying, $T \leftrightarrow (h_{1}, \dots, h_{k}) \mapsto (\dots ((T h_{1}) h_{2}) \dots) h_{k}$ , and under this identification the operator norm on $B_{k}$ is the least constant $C$ with $∥ T (h_{1}, \dots, h_{k}) ∥ \leq C ∥ h_{1} ∥ \dots ∥ h_{k} ∥$ . Only the iterated-operator description is used on this page, so the identification is recorded as a reading convention rather than developed.
Continuity of the $k$ -th derivative is an operator-norm condition. It is the continuity of $x \mapsto D^{k} f (x)$ in the norm of $B_{k}$ ; this is strictly stronger than the pointwise continuity of each scalar or vector map $x \mapsto D^{k} f (x) (h_{1}, \dots, h_{k})$ for fixed $h_{i}$ . The definition uses the operator norm, exactly as the sources do, and the inverse function theorem below is proved for this notion.
$C^{1}$ has the chain rule, so the class is stable under composition for $k = 1$ . If $f : U \to V$ and $g : V \to W$ are of class $C^{1}$ with $V$ open, then $g \circ f$ is of class $C^{1}$ : it is differentiable by the chain rule (Chain sum product and composition rules for Banach derivatives), its derivative is $D (g \circ f) (x) = D g (f (x)) D f (x)$ , and this is continuous in $x$ because $x \mapsto (D g (f (x)), D f (x))$ is continuous and operator multiplication is a jointly continuous bilinear operation (For a bilinear map, boundedness is equivalent to joint continuity, Composition satisfies |ST|\le|S|,|T|). The corresponding statement for $C^{k}$ with $k \geq 2$ is an induction of the same shape, using the higher chain rule; it is not developed here because no item on this page beyond the $C^{1}$ statements consumes it, and nothing below asserts it.
Linear and affine maps. A bounded linear $T : X \to Y$ is of class $C^{\infty}$ on $X$ , all of whose derivatives equal $T$ at the first step and $0$ afterwards; constant maps are of class $C^{\infty}$ with derivative $0$ . Consequently a $C^{k}$ map followed or preceded by a bounded linear isomorphism between open sets is again of class $C^{k}$ , a reduction used in the inverse function theorem.
Where this definition is consumed. The inverse and implicit function theorems state their conclusions in this class of regularity, and the countable-base Banach manifolds defined later on this page use exactly this notion for their transition maps and coordinate representatives.

LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Banach mean value estimate on a convex set

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $U$ be an open convex subset of a real Banach space $X$ , let $f : U \to Y$ be Fréchet differentiable on $U$ with values in a real Banach space $Y$ , let $x, y \in U$ and let $M \geq 0$ be a real number with

$∥ D f (z) ∥ \leq M for every z \in [x, y] : = {x + t (y - x) : 0 \leq t \leq 1} \subseteq U .$

Then

$∥ f (y) - f (x) ∥ \leq M ∥ y - x ∥ .$

Facts & Assumptions

Given: An assumed AC, an open convex $U$ in a real Banach space $X$ , a differentiable $f : U \to Y$ into a real Banach space $Y$ , points $x, y \in U$ and a real $M \geq 0$ bounding $∥ D f ∥$ on the segment $[x, y]$ .

[L1]

Differentiability of $f$ at each $z \in U$ means $f (z + h) - f (z) - D f (z) h = o (∥ h ∥)$ for $h \to 0$ in the sense of the $ε$ - $δ$ remainder estimate (Fréchet derivative between Banach spaces).

[L2]

Since $U$ is convex and $x, y \in U$ , the point $γ (t) : = x + t (y - x)$ lies in $U$ for every real $t \in [0, 1]$ ; a convex set contains all convex combinations of its points with real coefficients in $[0, 1]$ (Convex sets and continuous real-hyperplane separation in a normed space).

[L3]

Under AC, every nonzero $w \in Y$ admits $φ \in Y^{*}$ with $∥ φ ∥ = 1$ and $φ (w) = ∥ w ∥$ (Every nonzero vector has a norming functional); here $Y^{*}$ is the dual space of bounded linear functionals (The dual space X^* of a normed space and its dual norm) and $∣ φ (v) ∣ \leq ∥ φ ∥ ∥ v ∥$ .

[L4]

The chain rule applies to maps between open domains when the image of the first map lies in the domain of the second (Chain sum product and composition rules for Banach derivatives). A bounded linear map is Fréchet differentiable everywhere with derivative equal to itself, and Fréchet differentiability implies continuity (Fréchet derivative between Banach spaces, Remarks).

[L5]

The mean value theorem: a real function continuous on $[0, 1]$ and differentiable on $(0, 1)$ has some $c \in (0, 1)$ with $g (1) - g (0) = g^{'} (c)$ (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

[L6]

The operator norm satisfies $∥ T u ∥ \leq ∥ T ∥ ∥ u ∥$ for all $u$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[L7]

Norm axioms: triangle inequality and absolute homogeneity (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms); the absolute value of a real number is its norm, so $∣ g^{'} (c) ∣ \leq M ∥ y - x ∥$ reads as $g^{'} (c) \geq - M ∥ y - x ∥$ and $g^{'} (c) \leq M ∥ y - x ∥$ .

Proof

technique · direct

1.1

If $x = y$ the estimate reads $∥ f (x) - f (x) ∥ \leq 0$ and holds; if $w : = f (y) - f (x) = 0$ it reads $0 \leq M ∥ y - x ∥$ and holds. Hence we may assume $x \neq y$ and $w \neq 0$ , and then [L3] provides a norming functional for this nonzero $w$ .

givenL7algebra

1.2

By [L3] fix $φ \in Y^{*}$ with $∥ φ ∥ = 1$ and $φ (w) = ∥ w ∥$ ; then $φ (f (y)) - φ (f (x)) = ∥ f (y) - f (x) ∥ \geq 0$ .

L3L7algebra

1.3

Define $γ : R \to X$ by $γ (t) : = x + t (y - x)$ and put $J : = γ^{- 1} [U] = {t \in R : γ (t) \in U} .$ By [L2], $[0, 1] \subseteq J$ . The set $J$ is open: if $t_{0} \in J$ , openness of $U$ gives $ρ > 0$ with $B (γ (t_{0}), ρ) \subseteq U$ , and $∣ t - t_{0} ∣ < ρ / ∥ y - x ∥$ implies $∥ γ (t) - γ (t_{0}) ∥ = ∣ t - t_{0} ∣ ∥ y - x ∥ < ρ$ (recall that $x \neq y$ ). Define the well-typed function $g : J \to R$ by $g (t) : = φ (f (γ (t)))$ .

L2def-metric-topologyL7construct

1.4

The map $γ$ is differentiable at every $t_{0} \in R$ with constant derivative $D γ (t_{0}) = (s \mapsto s (y - x))$ , because $γ (t_{0} + s) - γ (t_{0}) = s (y - x)$ exactly, so the remainder vanishes.

givenL7algebra

1.5

The restriction $γ ∣_{J} : J \to U$ is differentiable at every $t_{0} \in J$ with the derivative in [step 1.4]. Since $J$ and $U$ are open and $γ [J] \subseteq U$ , two applications of [L4], first to $f \circ γ ∣_{J}$ and then to the bounded linear functional $φ$ , show that $g$ is differentiable on $J$ with $g^{'} (t_{0}) = φ (D f (γ (t_{0})) (y - x)) .$ In particular $g$ is continuous on $J$ , hence its restriction to $[0, 1]$ is continuous there and differentiable on $(0, 1)$ .

L1L4step 1.3step 1.4algebra

2.1

For every $t_{0} \in [0, 1]$ the bound in the statement gives $∥ D f (γ (t_{0})) ∥ \leq M$ because $γ (t_{0}) \in [x, y]$ , so by [step 1.5], [L6] and $∥ φ ∥ = 1$ , $∣ g^{'} (t_{0}) ∣ = ∣ φ (D f (γ (t_{0})) (y - x)) ∣ \leq ∥ D f (γ (t_{0})) ∥ \cdot ∥ y - x ∥ \leq M ∥ y - x ∥ .$

step 1.5L6L7algebra

2.2

By [L5] applied to $g$ on the interval $[0, 1]$ , whose hypotheses were verified in [step 1.5], there is $c \in (0, 1)$ with $g (1) - g (0) = g^{'} (c)$ .

step 1.5L5

3.1

Combining [step 1.2], [step 1.3] and [step 1.5], $∥ f (y) - f (x) ∥ = φ (f (y)) - φ (f (x)) = g (1) - g (0) = g^{'} (c) = ∣ g^{'} (c) ∣ \leq M ∥ y - x ∥,$ the second equality because $g (1) - g (0) = ∥ f (y) - f (x) ∥ \geq 0$ forces $g^{'} (c) \geq 0$ .

step 1.2step 1.3step 2.1step 2.2L7algebra

4.1

The estimate is [step 3.1] under the assumptions made there, and [step 1.1] disposes of the two degenerate cases; hence it holds in general.

step 1.1step 3.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Inverse function theorem for Banach spaces

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $X$ , $Y$ be real Banach spaces, let $U \subseteq X$ be open, let $f : U \to Y$ be of class $C^{k}$ with $k \geq 1$ (C k map between Banach spaces), and let $a \in U$ . If $D f (a) : X \to Y$ is a bounded linear isomorphism — that is, $D f (a)$ is bijective and its inverse $D f (a)^{- 1} : Y \to X$ is bounded — then there are open sets $U_{0} \subseteq U$ with $a \in U_{0}$ and $V_{0} \subseteq Y$ with $f (a) \in V_{0}$ such that $f ∣_{U_{0}} : U_{0} \to V_{0}$ is a bijection and its inverse $g : = (f ∣_{U_{0}})^{- 1} : V_{0} \to U_{0}$ is of class $C^{k}$ , with

$D g (f (x)) = D f (x)^{- 1} for every x \in U_{0} .$

Facts & Assumptions

Given: AC, real Banach spaces $X, Y$ , an open $U \subseteq X$ , $a \in U$ , a $C^{k}$ map $f : U \to Y$ with $k \geq 1$ , and a bounded linear isomorphism $A : = D f (a) : X \to Y$ .

[L1]

$C^{k}$ means the recursive operator-norm condition of C k map between Banach spaces: $f$ is $C^{k - 1}$ , its $(k - 1)$ -st derivative exists as a differentiable map, and $D^{k} f$ is continuous; in particular $D f$ is continuous and every differentiable map is continuous.

[L2]

Mean value estimate: on an open convex set, a differentiable map whose derivative is bounded by $M$ on a segment is $M$ -Lipschitz along that segment (Banach mean value estimate on a convex set); applied under AC.

[L3]

A contraction of a nonempty complete metric space has exactly one fixed point in it (A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point).

[L4]

Neumann series: if $∥ R ∥ < 1$ then $I - R$ is invertible with $∥ (I - R)^{- 1} ∥ \leq (1 - ∥ R ∥)^{- 1}$ , and if $A$ is invertible with $∥ A^{- 1} E ∥ < 1$ then $A + E$ is invertible with $(A + E)^{- 1} = (I + A^{- 1} E)^{- 1} A^{- 1}$ and $∥ (A + E)^{- 1} ∥ \leq ∥ A^{- 1} ∥ (1 - ∥ A^{- 1} E ∥)^{- 1}$ (Neumann series and small perturbations of bounded inverses).

[L5]

Chain rule and its linear special case: a bounded linear map equals its own derivative at every point, so $D (L \circ F) (x) = L \circ D F (x)$ , and the derivative of a composite of differentiable maps is the composite of the derivatives (Chain sum product and composition rules for Banach derivatives).

[L6]

Operator norm and composition: $∥ T u ∥ \leq ∥ T ∥ ∥ u ∥$ and $∥ S T ∥ \leq ∥ S ∥ ∥ T ∥$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum, Composition satisfies |ST|\le|S|,|T|); a Banach space is complete (Banach space).

[L7]

A closed subset of a complete metric space is complete in the subspace metric (Closed subspaces of complete metric spaces are complete; the converse under countable choice, claim 2, in ZF); a closed ball $\overset{ˉ}{B} (a, r)$ is a closed subset of $X$ , being ${x : ∥ x - a ∥ \leq r}$ (Open ball, closed ball and sphere in a metric space).

[L8]

$D Φ (x)$ is characterised by the $ε$ - $δ$ remainder estimate of the Fréchet derivative (Fréchet derivative between Banach spaces).

Proof

technique · direct

1.1

(Affine changes of variable preserve the class.) Let $F$ be of class $C^{k}$ on an open set, let $τ (x) = x_{0} + x$ be a translation, and let $L \in B (Y, Z)$ . Then $F \circ τ$ is of class $C^{k}$ with $D^{j} (F \circ τ) (x) = D^{j} F (τ (x))$ , and $L \circ F$ is of class $C^{k}$ with $D^{j} (L \circ F) (x) = L \circ D^{j} F (x)$ , for every $j \leq k$ : by [L5] the first derivatives are $D (F \circ τ) (x) = D F (τ (x))$ and $D (L \circ F) (x) = L \circ D F (x)$ , and the induction step differentiates these identities, the derivative of the translation being the identity and that of the bounded linear postcomposition $S \mapsto L \circ S$ being itself, with $∥ L \circ S ∥ \leq ∥ L ∥ ∥ S ∥$ by [L6] ensuring continuity of the resulting expressions.

L1L5L6algebra

1.2

If $X = {0}$ , then the isomorphism $A : X \to Y$ forces $Y = {0}$ and the theorem is immediate with $U_{0} = U = {0}$ and $V_{0} = Y$ ; hence assume $X \neq {0}$ , so $∥ A^{- 1} ∥ > 0$ . Since $D f$ is continuous at $a$ by [L1], choose $ρ > 0$ such that $B (a, ρ) \subseteq U$ and $∥ D f (x) - A ∥ < \frac{1}{2 ∥ A^{- 1} ∥} (x \in B (a, ρ)) .$ Put $r : = ρ / 3$ . Then $\overset{ˉ}{B} (a, r) \subseteq B (a, 2 r) \subseteq B (a, ρ) \subseteq U$ , and $∥ A^{- 1} (D f (x) - A) ∥ \leq \frac{1}{2}$ on $B (a, 2 r)$ . Thus $D f (x)$ is invertible there by [L4], with $∥ D f (x)^{- 1} ∥ \leq 2 ∥ A^{- 1} ∥$ .

L1L4L6choose

2.1

Put $Φ : = A^{- 1} \circ f$ on $U$ ; by [L5], $D Φ (x) = A^{- 1} \circ D f (x)$ , so $Φ (a) = A^{- 1} f (a) = : b$ , $D Φ (a) = I_{X}$ , and $Φ$ is of class $C^{k}$ by [step 1.1]. Put also $Ψ (x) : = x - Φ (x)$ on $B (a, 2 r)$ ; then $D Ψ (x) = I_{X} - A^{- 1} D f (x) = - A^{- 1} (D f (x) - A)$ , so $∥ D Ψ (x) ∥ \leq ∥ A^{- 1} ∥ ∥ D f (x) - A ∥ < \frac{1}{2}$ for every $x \in B (a, 2 r)$ .

step 1.2L1L5L6algebra

3.1

For $x, z \in \overset{ˉ}{B} (a, r)$ their segment lies in $\overset{ˉ}{B} (a, r) \subset B (a, 2 r)$ , so [L2] applied to $Ψ$ on the open convex set $B (a, 2 r)$ gives $∥ Ψ (x) - Ψ (z) ∥ \leq \frac{1}{2} ∥ x - z ∥$ . Since $Φ (x) - Φ (z) = (x - z) - (Ψ (x) - Ψ (z))$ , also $∥ Φ (x) - Φ (z) ∥ \geq \frac{1}{2} ∥ x - z ∥$ . In particular, $Φ$ is injective on $B (a, r)$ .

step 1.2step 2.1L2algebra

4.1

Fix $y \in B (b, r / 4)$ and define $T_{y} (x) : = y + x - Φ (x) = y + Ψ (x)$ on $\overset{ˉ}{B} (a, r)$ . For $x \in \overset{ˉ}{B} (a, r)$ one has $T_{y} (x) - a = (y - b) + Ψ (x) - Ψ (a)$ because $a - Φ (a) = Ψ (a)$ , so [step 3.1] yields $∥ T_{y} (x) - a ∥ \leq ∥ y - b ∥ + \frac{1}{2} ∥ x - a ∥ < \frac{r}{4} + \frac{r}{2} < r$ ; thus $T_{y}$ maps $\overset{ˉ}{B} (a, r)$ into $B (a, r)$ , and it is a contraction with constant $\frac{1}{2}$ by [step 3.1]. By [L7] the closed ball is a nonempty complete metric space, so [L3] gives a unique fixed point $g (y) \in B (a, r)$ of $T_{y}$ , and $T_{y} (x) = x$ is equivalent to $Φ (x) = y$ ; hence $y$ has exactly one preimage under $Φ$ in $B (a, r)$ .

step 3.1L3L7algebra

5.1

The set $W : = B (a, r) \cap Φ^{- 1} (B (b, r / 4))$ is open and contains $a$ , and $Φ ∣_{W} : W \to B (b, r / 4)$ is a bijection with inverse $g$ : it is injective by [step 3.1], and surjective by [step 4.1], which for each $y \in B (b, r / 4)$ produces $g (y) \in B (a, r)$ with $Φ (g (y)) = y$ . Moreover $g$ is Lipschitz with constant $2$ : [step 3.1] gives $∥ g (y) - g (z) ∥ \leq ∥ Φ (g (y)) - Φ (g (z)) - (g (y) - g (z)) ∥ + ∥ y - z ∥ \leq \frac{1}{2} ∥ g (y) - g (z) ∥ + ∥ y - z ∥$ .

step 3.1step 4.1L1algebra

6.1

For $y \in B (b, r / 4)$ put $x : = g (y)$ ; by [step 1.2] and [L4] the operator $D Φ (x)$ is invertible with $∥ D Φ (x)^{- 1} ∥ \leq 2$ . Let $h$ be small with $y + h \in B (b, r / 4)$ and put $k : = g (y + h) - g (y)$ , so that $∥ k ∥ \leq 2 ∥ h ∥$ by [step 5.1] and $h = Φ (x + k) - Φ (x) = D Φ (x) k + r_{Φ} (k)$ with $∥ r_{Φ} (k) ∥ = o (∥ k ∥)$ by [L8]; applying $D Φ (x)^{- 1}$ gives $k - D Φ (x)^{- 1} h = - D Φ (x)^{- 1} r_{Φ} (k)$ , and $∥ D Φ (x)^{- 1} r_{Φ} (k) ∥ \leq 2 ∥ r_{Φ} (k) ∥$ , which is $o (∥ k ∥) = o (∥ h ∥)$ ; hence $g$ is differentiable at $y$ with $D g (y) = D Φ (x)^{- 1} = D f (g (y))^{- 1} A$ .

step 1.2step 5.1L4L6L8algebra

7.1

The derivative formula of [step 6.1] is continuous in $y$ : the map $y \mapsto D Φ (g (y))$ is continuous because $D Φ$ is continuous by [L1] and [step 2.1] and $g$ is continuous by [step 5.1]; inversion is continuous at each invertible operator, since for $∥ A^{- 1} E ∥ \leq \frac{1}{2}$ the bound $∥ (A + E)^{- 1} - A^{- 1} ∥ \leq ∥ (A + E)^{- 1} ∥ ∥ E ∥ ∥ A^{- 1} ∥ \leq 2 ∥ A^{- 1} ∥^{2} ∥ E ∥$ from [L4] and [L6] tends to $0$ with $∥ E ∥$ . Hence $g$ is of class $C^{1}$ .

step 5.1step 6.1L1L4L6algebra

8.1

(Higher regularity.) Inversion $i n v (A) : = A^{- 1}$ is of class $C^{\infty}$ on the open set of invertible operators in $B (X)$ : for $∥ A^{- 1} H ∥ < 1$ , [L4] gives $(A + H)^{- 1} = A^{- 1} - A^{- 1} H A^{- 1} + R (H)$ with $∥ R (H) ∥ \leq \frac{∥ A^{- 1} ∥^{3} ∥ H ∥^{2}}{1 - ∥ A^{- 1} H ∥}$ , whence $D i n v (A) H = - A^{- 1} H A^{- 1}$ ; that formula is continuous in $A$ by [L4] and [L6], and iterating the expansion differentiates it again, so $i n v$ is $C^{r}$ for every $r$ . Now let $k \geq 2$ and let $Φ$ be of class $C^{k}$ ; then $D Φ$ is of class $C^{k - 1}$ by [L1] and $D g = i n v \circ D Φ \circ g$ by [step 6.1] and [L5]. If $g$ is of class $C^{j - 1}$ for some $j$ with $2 \leq j \leq k$ , then $D g$ , a composite of $C^{j - 1}$ maps, is of class $C^{j - 1}$ and hence $g$ is of class $C^{j}$ ; the case $j = 1$ is [step 7.1], so induction gives $g$ of class $C^{k}$ .

step 7.1L1L4L5L6

9.1

Transfer to $f$ : by [step 5.1] the set $U_{0} : = W$ is an open neighbourhood of $a$ contained in $U$ , and $V_{0} : = f [U_{0}] = A [Φ [W]] = A [B (b, r / 4)]$ is an open neighbourhood of $f (a)$ ; the restriction $f ∣_{U_{0}}$ is a bijection onto $V_{0}$ with inverse $F (y) : = g (A^{- 1} y)$ , which is of class $C^{k}$ by [step 1.1] and [step 8.1] as a composite of the bounded linear map $A^{- 1}$ and the $C^{k}$ map $g$ .

step 5.1step 1.1step 8.1L6algebra

10.1

For $x \in U_{0}$ the map $F \circ f$ equals the identity near $x$ , so the chain rule [L5] differentiates it to $D F (f (x)) D f (x) = I_{X}$ ; multiplying on the right by $D f (x)^{- 1}$ gives $D F (f (x)) = D f (x)^{- 1}$ , which is the displayed derivative formula for the statement's inverse $g$ , here the map $F$ of [step 9.1].

step 9.1step 5.1L5algebra∎

TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Implicit function theorem for Banach spaces

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $X$ , $Y$ , $Z$ be real Banach spaces, let $U \subseteq X \times Y$ be open for the product metric, let $F : U \to Z$ be of class $C^{k}$ with $k \geq 1$ (C k map between Banach spaces), and let $(a, b) \in U$ with $F (a, b) = 0$ . Let $D_{X} F (a, b) : = D F (a, b) \circ i_{X}$ and $D_{Y} F (a, b) : = D F (a, b) \circ i_{Y}$ be the partial derivatives, where $i_{X} (x) : = (x, 0)$ and $i_{Y} (y) : = (0, y)$ . If $D_{Y} F (a, b) : Y \to Z$ is a bounded linear isomorphism, then there are open neighbourhoods $A \subseteq X$ of $a$ and $B \subseteq Y$ of $b$ and a unique map $g : A \to B$ of class $C^{k}$ such that

${(x, y) \in A \times B : F (x, y) = 0} = {(x, g (x)) : x \in A},$

and along the graph $D g$ satisfies $D g (x) = - D_{Y} F (x, g (x))^{- 1} D_{X} F (x, g (x)) (x \in A) .$ In particular $g (a) = b$ .

Facts & Assumptions

Given: AC, real Banach spaces $X, Y, Z$ , an open $U \subseteq X \times Y$ , a $C^{k}$ map $F : U \to Z$ with $k \geq 1$ , a point $(a, b) \in U$ with $F (a, b) = 0$ , and a bounded linear isomorphism $L : = D_{Y} F (a, b) : Y \to Z$ .

[L1]

Fréchet derivative, partial derivatives as restrictions of $D F$ to the coordinate axes, and the derivative of a bounded linear map (Fréchet derivative between Banach spaces); the product norm $∥ (x, y) ∥_{\max} = \max {∥ x ∥, ∥ y ∥}$ is a norm on $X \times Y$ (The standard product norms on a finite product of normed spaces).

[L2]

Chain rule and sum rule (Chain sum product and composition rules for Banach derivatives).

[L3]

Inverse function theorem: a $C^{k}$ map ( $k \geq 1$ ) between real Banach spaces whose derivative at a point is a bounded linear isomorphism restricts to a $C^{k}$ diffeomorphism between open neighbourhoods of that point and its image (Inverse function theorem for Banach spaces); AC is assumed there and here.

[L4]

Neumann perturbation: an operator close enough to an invertible one is invertible with a norm bound on its inverse (Neumann series and small perturbations of bounded inverses).

[L5]

$C^{k}$ for $k \geq 1$ includes differentiability and continuity of the derivative (C k map between Banach spaces).

[L6]

A closed subset of a complete metric space is complete; a Banach space is complete (Closed subspaces of complete metric spaces are complete; the converse under countable choice, Banach space).

[L7]

The operator norm satisfies $∥ T u ∥ \leq ∥ T ∥ ∥ u ∥$ and $∥ S T ∥ \leq ∥ S ∥ ∥ T ∥$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum, The spaces (\mathcal B(X,Y)) and (\mathcal B(X)) of bounded linear operators).

Proof

technique · direct

1.1

The product $X \times Y$ with the max norm is complete: a Cauchy sequence in $X \times Y$ has Cauchy coordinate sequences, which converge in the Banach spaces $X$ and $Y$ , and the coordinatewise limit is a limit in the product metric; similarly $X \times Z$ is complete. Hence these products are real Banach spaces, and $U$ is an open subset of the Banach space $X \times Y$ .

L1L6algebra

1.2

Define $Φ : U \to X \times Z$ by $Φ (x, y) : = (x, F (x, y))$ . Its first component is the (bounded, linear) projection $(x, y) \mapsto x$ , and its second is $F$ ; the derivative of a bounded linear map is the map itself by [L1], so $D Φ (a, b) (h, k) = (h, D_{X} F (a, b) h + D_{Y} F (a, b) k)$ , and $D Φ (a, b)$ is a bounded linear isomorphism with inverse $(u, w) \mapsto (u, L^{- 1} (w - D_{X} F (a, b) u))$ .

L1L7algebra

2.1

Since $F$ is of class $C^{k}$ , so is $Φ$ : for $k = 1$ this is the chain rule applied to the two components $x$ and $F$ , and for higher $k$ the same computation differentiates each component, the components of $D^{j} Φ$ being those of $D^{j} x$ and $D^{j} F$ for $j \leq k$ ; continuity of the top derivative is inherited from that of $D^{k} F$ together with the constant derivatives of the linear first component. Also $Φ (a, b) = (a, 0)$ .

step 1.2L2L5algebra

3.1

By [L3] applied to the $C^{k}$ map $Φ$ at $(a, b)$ , whose derivative is the isomorphism of [step 1.2], there are open sets $U_{0} ∋ (a, b)$ and $V_{0} ∋ (a, 0)$ such that $Φ ∣_{U_{0}} : U_{0} \to V_{0}$ is a bijection with $C^{k}$ inverse $Ψ : V_{0} \to U_{0}$ .

step 1.2step 2.1L3

4.1

Because $Φ$ preserves the first coordinate, so does $Ψ$ : if $(x, z) = Φ (x^{'}, y^{'})$ then $x = x^{'}$ , hence $Ψ (x, z) = (x, H (x, z))$ for the $C^{k}$ map $H : = {p r}_{2} \circ Ψ$ ; and $Ψ$ being an inverse of $Φ$ means $F (x, H (x, z)) = z$ for all $(x, z) \in V_{0}$ .

step 3.1algebra

5.1

Choose open $A \subseteq X$ and $B \subseteq Y$ with $A \times B \subseteq U_{0}$ and such that $(a, 0) \in A \times {0} \subseteq V_{0}$ : possible because $U_{0}$ and $V_{0}$ are open and contain $(a, b)$ respectively $(a, 0)$ , and the set ${x : (x, 0) \in V_{0}}$ is an open neighbourhood of $a$ . Shrinking $A$ if necessary we may also assume $g (A) \subseteq B$ : $g$ is continuous at $a$ with $g (a) = b \in B$ and $B$ is open, so some neighbourhood $A_{0}$ of $a$ satisfies $H (A_{0} \times {0}) \subseteq B$ , and we replace $A$ by $A \cap A_{0}$ . Define $g (x) : = H (x, 0)$ for $x \in A$ , so $g$ is of class $C^{k}$ with values in $B$ , $g (a) = b$ , and $F (x, g (x)) = 0$ for every $x \in A$ by [step 4.1].

step 4.1algebra

6.1

Conversely, if $(x, y) \in A \times B$ has $F (x, y) = 0$ , then $Φ (x, y) = (x, 0) \in V_{0}$ , so $(x, y) = Ψ (x, 0) = (x, g (x))$ by [step 4.1] and [step 5.1], and hence $y = g (x)$ . Thus the zero set of $F$ in $A \times B$ is exactly the graph of $g$ , which proves existence and uniqueness of $g$ on $A$ .

step 5.1step 4.1algebra

7.1

For $x \in A$ , differentiate the identity $F (x, g (x)) = 0$ using the chain rule [L2]: $D_{X} F (x, g (x)) + D_{Y} F (x, g (x)) D g (x) = 0$ ; the operator $D_{Y} F (x, g (x))$ is invertible for $x$ close to $a$ by continuity of $D_{Y} F$ at $(a, b)$ (from [L5]) and [L4], and shrinking $A$ if necessary we may assume this holds for all $x \in A$ ; then $D g (x) = - D_{Y} F (x, g (x))^{- 1} D_{X} F (x, g (x))$ , which with [step 6.1] is the displayed formula.

step 5.1step 6.1L2L4L5algebra∎

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Countable base Banach manifold and smooth map

Definition

Let $k \in N \cup {\infty}$ and let $E$ be a real Banach space (Banach space) with its norm topology (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

A chart on a topological space $M$ (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison) is a pair $(φ, U)$ in which $U \subseteq M$ is open and $φ : U \to φ [U] \subseteq E$ is a homeomorphism onto an open subset of $E$ (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological); $U$ is the domain of the chart and $φ$ its coordinate map.
Two charts $(φ, U)$ and $(ψ, V)$ of $M$ with $U \cap V \neq \emptyset$ are $C^{k}$ compatible when the transition map $ψ \circ φ^{- 1} : φ [U \cap V] \to ψ [U \cap V]$ and its inverse are of class $C^{k}$ (C k map between Banach spaces) as maps between open subsets of $E$ . Two charts with disjoint domains are declared compatible.
An atlas of class $C^{k}$ on $M$ is a family of pairwise $C^{k}$ compatible charts whose domains cover $M$ , and the space $M$ together with such an atlas is a $C^{k}$ Banach manifold modelled on $E$ — a Banach manifold for short — when additionally $M$ is Hausdorff (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not) and second countable (Second countability: an at most countable basis for the topology).

Thus every point of $M$ lies in the domain of a chart: $M$ is locally homeomorphic to open subsets of the Banach space $E$ , and the change of coordinates between any two charts in its specified atlas is a $C^{k}$ map. Henceforth a chart of the structured manifold $M$ means a member of that specified atlas; it does not mean an arbitrary local homeomorphism on the underlying topological space. The pair (Hausdorff, second countable) is part of the definition and is never dropped below.

Let $M$ be a $C^{k}$ Banach manifold modelled on $E$ and $N$ a $C^{k}$ Banach manifold modelled on $F$ , and let $f : M \to N$ be a map.

$f$ is of class $C^{k}$ when for every chart $(φ, U)$ in the specified atlas of $M$ and every chart $(ψ, V)$ in the specified atlas of $N$ the coordinate representative $ψ \circ f \circ φ^{- 1} : φ [U \cap f^{- 1} [V]] \to F$ has open domain $φ [U \cap f^{- 1} [V]] \subseteq E$ and is of class $C^{k}$ on that domain. Openness is part of the requirement, not an assumption about an arbitrary set map $f$ .
$f$ is smooth when it is of class $C^{\infty}$ .
A bijection $f : M \to N$ is a $C^{k}$ diffeomorphism when both $f$ and $f^{- 1}$ are of class $C^{k}$ ; likewise for $C^{\infty}$ .

Remarks

Chart independence of the class of a map is a chain-rule statement. If $(φ, U)$ , $(φ^{'}, U^{'})$ are charts of $M$ and $(ψ, V)$ , $(ψ^{'}, V^{'})$ are charts of $N$ from their specified atlases, then on the open set where both sides are defined, $ψ^{'} \circ f \circ φ^{' - 1}$ equals $(ψ^{'} \circ ψ^{- 1}) \circ (ψ \circ f \circ φ^{- 1}) \circ (φ \circ φ^{' - 1})$ , a composite of $C^{k}$ transition maps and the representative $ψ \circ f \circ φ^{- 1}$ . For $k = 1$ the class is therefore independent of the charts by the chain rule (Chain sum product and composition rules for Banach derivatives) — the composition of $C^{1}$ maps is $C^{1}$ because the chain rule expresses the derivative as a product of continuous operator-valued maps (C k map between Banach spaces) — and consequently $C^{1}$ -ness may be checked at each point with one pair of charts around it. Nothing below uses this independence for $k \geq 2$ , and the definition itself quantifies over all pairs from the specified atlases, so no higher-order chain rule is presupposed.
The model space is fixed. Charts take values in one Banach space $E$ , which may be infinite dimensional; a manifold with a finite-dimensional model space is the familiar finite-dimensional case. Two manifolds modelled on different Banach spaces are compared by maps whose coordinate representatives map open subsets of one model space into the other.
Open sets are the basic examples, when the model space is second countable. If $E$ is second countable, then an open subset $W$ of $E$ is a $C^{\infty}$ Banach manifold modelled on $E$ with the single chart $({i d}_{W}, W)$ : a basis of $E$ restricts to a basis of the subspace $W$ , and $W$ is Hausdorff because $E$ is. The hypothesis cannot be dropped: for $E = ℓ^{\infty}$ and $W = E$ the identity chart covers $E$ , but $E$ is not second countable — the uncountably many $0$ - $1$ sequences are pairwise at distance $1$ . Their radius- $1 / 3$ balls are pairwise disjoint. A countable basis would assign to each such sequence the least indexed basis member containing it and contained in its ball, giving an injection of the uncountable set of $0$ - $1$ sequences into $N$ , a contradiction. A map between open subsets of a second countable $E$ is of class $C^{k}$ as a map of manifolds exactly when it is of class $C^{k}$ in the sense of C k map between Banach spaces. All the local theorems of this page are statements about such open sets, transported to manifolds exactly through charts.
The Hausdorff and countability hypotheses are part of the definition. They are the standard hypotheses of the global theory: the countable base is what the later Sard–Smale and transversality development consumes, and the Hausdorff condition is what makes the local pieces of a manifold fit together as a space of points rather than a set with overlapping coordinate patches. No theorem on this page asserts anything for a non-Hausdorff or non-second-countable "manifold", and the four Euclidean-space local theorems above are unaffected by either hypothesis because they do not mention manifolds at all.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Tangent space and differential on a Banach manifold

Definition

Let $k \geq 1$ , let $M$ be a $C^{k}$ Banach manifold modelled on the real Banach space $E$ (Countable base Banach manifold and smooth map) and let $p \in M$ . Consider the set of pairs $(φ, v)$ in which $φ$ is a chart of $M$ whose domain contains $p$ and $v \in E$ , and declare

$(φ, v) \sim (ψ, w) : ⟺ w = D (ψ \circ φ^{- 1}) (φ (p)) v,$

the derivative being that of the transition map, a $C^{1}$ map between open subsets of $E$ (Fréchet derivative between Banach spaces). The tangent space to $M$ at $p$ is the quotient set

$T_{p} M : = {(φ, v) : p \in dom φ} / \sim,$

and the class of $(φ, v)$ is written $[φ, v]$ . For a chart $φ$ at $p$ the assignment $[φ, v] \mapsto v$ identifies $T_{p} M$ with $E$ ; the resulting real vector space structure is

$λ [φ, v] + μ [φ, w] : = [φ, λ v + μ w] (λ, μ \in R),$

and the differential of a $C^{1}$ map $f : M \to N$ between Banach manifolds (models $E$ and $F$ ) at $p$ is

$D f (p) ([φ, v]) : = [ψ, D (ψ \circ f \circ φ^{- 1}) (φ (p)) v] \in T_{f (p)} N,$

where $φ$ is any chart of $M$ at $p$ and $ψ$ any chart of $N$ at $f (p)$ for which the representative $ψ \circ f \circ φ^{- 1}$ is defined near $φ (p)$ . The well-definedness of the relation, of the vector space operations and of the differential, together with the identities below, is proved on this page as Banach manifold differentials are chart independent.

Remarks

Tangent vectors are velocities of curves. If $φ$ is a chart at $p$ and $v \in E$ , then the curve $γ (t) : = φ^{- 1} (φ (p) + t v)$ , defined for small real $t$ , lies in $M$ and satisfies $φ \circ γ (t) = φ (p) + t v$ , so its coordinate velocity at $0$ is $v$ ; the class $[φ, v]$ is exactly that velocity. Conversely every velocity of a curve through $p$ arises in this way. This is the reading used in the counterexample on the companion page, where a curve in a closed subspace produces a tangent vector of the subspace.
The differential is linear on tangent spaces. This is not part of the definition but follows from the chain rule: in a fixed chart at $p$ and a fixed chart at $f (p)$ the map $v \mapsto D (ψ \circ f \circ φ^{- 1}) (φ (p)) v$ is bounded linear, and the chart identifications are linear. The functoriality statements $D (i d) = i d$ and $D (g \circ f) = D g \circ D f$ are proved with the same computation.
The vector space structure does not depend on the chart. A change $φ \to ψ$ multiplies coordinate vectors by the transition derivative $D (ψ \circ φ^{- 1}) (φ (p))$ , which is a bounded linear isomorphism of $E$ with inverse $D (φ \circ ψ^{- 1}) (ψ (p))$ ; linearity of this change is exactly what makes the displayed operations independent of the chart chosen. The invertibility follows from the chain rule: the two transition maps are mutually inverse $C^{1}$ maps, so their composites are the identity on open sets and differentiating those identities exhibits each derivative as the inverse of the other. Both facts are recorded in the lemma below.
For an admissible open model the tangent space is the model space. If the norm topology of $E$ is second countable, $W \subseteq E$ is open, and $p \in W$ , then $W$ is a Banach manifold under the convention of Countable base Banach manifold and smooth map. The single chart $({i d}_{W}, W)$ makes $T_{p} W$ the set of classes $[{i d}_{W}, v]$ , which is canonically identified with $E$ ; under this identification $D f (p)$ of a map $f : W \to E$ is the Fréchet derivative of the coordinate representative, which here is $f$ itself. All computations on this page are performed through this identification.

LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Banach manifold differentials are chart independent

Statement

Let $k \geq 1$ , let $M$ be a $C^{k}$ Banach manifold modelled on $E$ (all manifolds below are $C^{k}$ and smooth maps are $C^{1}$ ), and use the tangent space, its vector space structure and the differential of Tangent space and differential on a Banach manifold. Then:

$\sim$ is an equivalence relation on the pairs $(φ, v)$ with $p \in dom φ$ .
The differential $D f (p) : T_{p} M \to T_{f (p)} N$ of a $C^{1}$ map $f : M \to N$ is well defined; more precisely, for any two choices of charts the resulting classes coincide, and the chart-based vector space operations on $T_{p} M$ are independent of the chart used.
$D ({i d}_{M}) (p) = {i d}_{T_{p} M}$ for every $p$ , and $D (g \circ f) (p) = D g (f (p)) \circ D f (p)$ whenever $f : M \to N$ and $g : N \to P$ are $C^{1}$ .

Facts & Assumptions

Given: $k \geq 1$ , $C^{k}$ Banach manifolds $M, N, P$ modelled on real Banach spaces $E, F, G$ , points $p \in M$ , and charts $φ, φ^{'}$ of $M$ at $p$ , $ψ, ψ^{'}$ of $N$ at $f (p)$ for the $C^{1}$ map $f : M \to N$ .

[L1]

Definition of tangent vectors, their chart identifications, the vector space operations and the differential, together with the fact that transition maps of a $C^{k}$ manifold are $C^{k}$ and hence $C^{1}$ (Tangent space and differential on a Banach manifold, Countable base Banach manifold and smooth map).

[L2]

Chain rule, sum rule and the derivative of the identity: for $C^{1}$ maps of open subsets of Banach spaces, $D (β \circ α) (x) = D β (α (x)) D α (x)$ , and $D (i d) (x) = I$ ; a bounded linear map is its own derivative (Chain sum product and composition rules for Banach derivatives, Fréchet derivative between Banach spaces).

[L3]

Chart representatives of $C^{1}$ maps between manifolds are $C^{1}$ on their open domains, and composites of the transition maps appearing below are defined on a neighbourhood of the relevant point, because chart domains and their images are open (Countable base Banach manifold and smooth map).

Proof

technique · direct

1.1

(Reflexivity and symmetry.) For a chart $φ$ at $p$ the transition $φ \circ φ^{- 1}$ is the identity on an open set containing $φ (p)$ , so $D (φ \circ φ^{- 1}) (φ (p)) = I$ by [L2] and $(φ, v) \sim (φ, v)$ . If $(φ, v) \sim (ψ, w)$ , then $w = D (ψ \circ φ^{- 1}) (φ (p)) v$ ; the two transition maps are mutually inverse $C^{1}$ maps on neighbourhoods of $φ (p)$ and $ψ (p)$ , so differentiating the identities $(φ \circ ψ^{- 1}) \circ (ψ \circ φ^{- 1}) = i d$ and $(ψ \circ φ^{- 1}) \circ (φ \circ ψ^{- 1}) = i d$ with [L2] gives $D (φ \circ ψ^{- 1}) (ψ (p)) w = v$ , that is $(ψ, w) \sim (φ, v)$ .

L1L2L3

2.1

(Transitivity.) If $(φ, v) \sim (ψ, w)$ and $(ψ, w) \sim (χ, u)$ , then on a neighbourhood of $φ (p)$ the identity $χ \circ φ^{- 1} = (χ \circ ψ^{- 1}) \circ (ψ \circ φ^{- 1})$ holds, and [L2] gives $D (χ \circ φ^{- 1}) (φ (p)) v = D (χ \circ ψ^{- 1}) (ψ (p)) D (ψ \circ φ^{- 1}) (φ (p)) v = D (χ \circ ψ^{- 1}) (ψ (p)) w = u$ , that is $(φ, v) \sim (χ, u)$ . Together with [step 1.1], this establishes the equivalence relation before any construction is asserted on its classes.

step 1.1L2L3

3.1

(The differential is well defined.) Let $f : M \to N$ be $C^{1}$ and let $(φ, ψ)$ , $(φ^{'}, ψ^{'})$ be two chart pairs at $p$ and $f (p)$ . On a neighbourhood of $φ^{'} (p)$ one has $ψ^{'} \circ f \circ φ^{' - 1} = (ψ^{'} \circ ψ^{- 1}) \circ (ψ \circ f \circ φ^{- 1}) \circ (φ \circ φ^{' - 1})$ ; if $(φ^{'}, v^{'}) \sim (φ, v)$ , that is $v = D (φ \circ φ^{' - 1}) (φ^{'} (p)) v^{'}$ , then [L2] gives $D (ψ^{'} \circ f \circ φ^{' - 1}) (φ^{'} (p)) v^{'} = D (ψ^{'} \circ ψ^{- 1}) (ψ (f (p))) [D (ψ \circ f \circ φ^{- 1}) (φ (p)) v]$ , which is precisely the relation $[ψ^{'}, D (ψ^{'} \circ f \circ φ^{' - 1}) (φ^{'} (p)) v^{'}] = [ψ, D (ψ \circ f \circ φ^{- 1}) (φ (p)) v]$ defining $\sim$ on the target manifold. Because [step 1.1] and [step 2.1] have already proved that $\sim$ is an equivalence relation, this comparison proves independence of both the representative and the chart pair.

step 1.1step 2.1L1L2L3

3.2

(The vector space operations are chart independent.) If $(φ, v) \sim (φ^{'}, v^{'})$ and $(φ, w) \sim (φ^{'}, w^{'})$ , then the shared transition derivative $T : = D (φ^{'} \circ φ^{- 1}) (φ (p))$ is linear with $v^{'} = T v$ , $w^{'} = T w$ ; hence $v^{'} + w^{'} = T (v + w)$ and $λ v^{'} = T (λ v)$ , that is $(φ, v + w) \sim (φ^{'}, v^{'} + w^{'})$ and $(φ, λ v) \sim (φ^{'}, λ v^{'})$ . Since $\sim$ is an equivalence relation by [step 1.1] and [step 2.1], these representative calculations define operations on the quotient classes.

step 1.1step 2.1L1L2algebra

4.1

(Functoriality.) The maps in this step are well defined on tangent classes by [step 3.1]. For the identity, $D ({i d}_{M}) (p) [φ, v] = [φ, D (φ \circ {i d}_{M} \circ φ^{- 1}) (φ (p)) v] = [φ, D (i d) (φ (p)) v] = [φ, v]$ by [L2]. For a composite, fix charts $φ$ at $p$ , $ψ$ at $f (p)$ and $ρ$ at $g (f (p))$ ; then $ρ \circ (g \circ f) \circ φ^{- 1} = (ρ \circ g \circ ψ^{- 1}) \circ (ψ \circ f \circ φ^{- 1})$ near $φ (p)$ , and applying [L2] to this identity of open-subset maps gives equality of the two well-defined maps $D (g \circ f) (p)$ and $D g (f (p)) \circ D f (p)$ on every class represented in the chart $φ$ .

step 3.1L1L2L3

5.1

Assertion 1 is [step 1.1] with [step 2.1]; assertion 2 is [step 3.1] and [step 3.2]; assertion 3 is [step 4.1].

step 1.1step 2.1step 3.1step 3.2step 4.1∎

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Split Banach submanifold

Definition

Let $k \geq 1$ , let $M$ be a $C^{k}$ Banach manifold modelled on the real Banach space $E$ (Countable base Banach manifold and smooth map), and let $S \subseteq M$ be a subset. Then $S$ is a split $C^{k}$ submanifold of $M$ when for every $p \in S$ there are

a chart $(φ, U)$ of $M$ with $p \in U$ , and
a decomposition $E = E_{0} \oplus E_{1}$ of the model space into two closed subspaces with bounded coordinate projections (A complemented closed subspace of a normed space, Linear subspace of a vector space),

such that

$φ [U \cap S] = φ [U] \cap (E_{0} \oplus {0}) .$

In other words, in the chart the submanifold is exactly the slice of the open set $φ [U]$ cut out by setting the $E_{1}$ -coordinate equal to zero. The subspace topology on $S$ (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace) carries the resulting componentwise $C^{k}$ structure: the charts $(φ ∣_{U \cap S}, U \cap S)$ take values in open subsets of the local space $E_{0}$ , and their transition maps are restrictions of the $C^{k}$ transition maps of $M$ . On an overlap, the derivative of such a transition map is a bounded linear isomorphism between the two local model spaces. Hence the isomorphism type of $E_{0}$ is locally constant on $S$ , and every connected component of $S$ is a $C^{k}$ Banach manifold modelled on one fixed representative of that type. Different components need not have isomorphic model spaces; without an additional uniform-model hypothesis, $S$ as a whole need not be modelled on one Banach space in the global convention of Countable base Banach manifold and smooth map.

For $p \in S$ the tangent space $T_{p} S$ is the tangent space of the component of $S$ containing $p$ , and the differential of the inclusion identifies it with a subspace of $T_{p} M$ .

Remarks

Splitness is a local condition, and the complement is part of the local data. The definition does not assert that an arbitrary closed subspace of a Banach space is a submanifold of it: the complement $E_{1}$ is produced along with the chart, and the companion page exhibits a closed subspace $c_{0}$ of $ℓ^{\infty}$ that is not complemented in it. For a closed subspace $E_{0} \leq E$ with $E$ second countable, the split charts with $M = E$ and $φ = i d$ exist exactly when $E_{0}$ is complemented in $E$ ; for $E = ℓ^{\infty}$ the ambient is not a Banach manifold in the library's sense, so the example separates closedness from complementedness at the level of Banach spaces rather than exhibiting a split-submanifold failure for a Banach manifold.
The local model can vary between components. For example, ${0} \cup (1, 2) \subseteq R$ satisfies the slice condition, with local model ${0}$ at the isolated point and $R$ on the interval. Thus it is split in the componentwise sense above, but it is not modelled on one fixed Banach space.
The tangent space of a split submanifold is complemented. In a chart at $p$ the tangent space of $S$ corresponds to $E_{0}$ and that of $M$ to $E$ , so the inclusion $T_{p} S \to T_{p} M$ is, in that chart, the inclusion of the complemented subspace $E_{0}$ into $E$ . This is why the regular value theorem below demands a complemented kernel rather than mere surjectivity of the derivative.
Automatic cases. If $E_{0}$ is finite dimensional or of finite codimension in $E$ , then every closed subspace of that kind is complemented, so the only obstruction to splitness in these cases is the local product structure of $S$ itself (Finite-dimensional subspaces are complemented). In particular finite-dimensional level sets of submersions are automatically split when the derivative is surjective.

TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Regular value theorem for Banach manifolds

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $M$ and $N$ be $C^{k}$ Banach manifolds with $k \geq 1$ (Countable base Banach manifold and smooth map), and assume that the specified $C^{k}$ atlas of $M$ is maximal: every $C^{k}$ chart compatible with all of its charts is already a member of that atlas. Let $f : M \to N$ be of class $C^{k}$ , let $q \in N$ and suppose that

$D f (p) : T_{p} M \to T_{q} N is surjective with complemented kernel for every p \in f^{- 1} (q) .$

Then $f^{- 1} (q)$ is a split $C^{k}$ submanifold of $M$ (Split Banach submanifold) and

$T_{p} (f^{- 1} (q)) = \ker D f (p) for every p \in f^{- 1} (q) .$

Facts & Assumptions

Given: AC, $C^{k}$ Banach manifolds $M, N$ with $k \geq 1$ , a maximal specified $C^{k}$ atlas on $M$ , a $C^{k}$ map $f : M \to N$ , a point $q \in N$ , and for every $p \in f^{- 1} (q)$ a surjective $D f (p)$ with complemented kernel.

[L1]

Tangents and differentials on Banach manifolds, the chart-independence of the differential, and functoriality (Tangent space and differential on a Banach manifold, Banach manifold differentials are chart independent); split submanifolds and their slices (Split Banach submanifold). A chart of a structured manifold means a member of its specified atlas; by the maximal-atlas hypothesis on $M$ , every $C^{k}$ chart compatible with that atlas is such a member (Countable base Banach manifold and smooth map).

[L2]

Implicit function theorem for $C^{k}$ maps between Banach spaces, $k \geq 1$ (Implicit function theorem for Banach spaces); it is applied under the assumed AC.

[L3]

A bounded bijection between Banach spaces has a bounded inverse under DC (Bounded inverse theorem), and AC supplies DC (AC supplies the countable and dependent choices used in Banach integration).

[L4]

A complemented closed subspace has a closed complement with bounded projections; a bounded linear isomorphism carries a complemented subspace onto a complemented subspace (A complemented closed subspace of a normed space).

[L5]

Chain rule and the derivative of the identity for maps between open subsets of Banach spaces (Chain sum product and composition rules for Banach derivatives, Fréchet derivative between Banach spaces).

Proof

technique · direct

1.1

Fix $p \in S : = f^{- 1} (q)$ and choose specified-atlas charts $φ_{0} : U \to E$ of $M$ at $p$ and $ψ : V \to F$ of $N$ at $q$ . Put $a : = φ_{0} (p)$ and $b : = ψ (q)$ . The translated coordinate map $φ : = φ_{0} - a$ is a $C^{k}$ chart compatible with the specified atlas of $M$ ; maximality therefore makes $φ$ a chart of the structured manifold, and $φ (p) = 0$ . Writing $L : = D f (p)$ , the recentered coordinate representative $\hat{f} (x) : = ψ (f (φ^{- 1} (x))) - b$ is $C^{k}$ on the open set $Ω : = φ [U \cap f^{- 1} [V]] \subseteq E$ , satisfies $\hat{f} (0) = 0$ , and has $D \hat{f} (0) = D ψ (q) \circ L \circ D φ (p)^{- 1} .$ Translations have identity derivative, so this follows from chart functoriality and the chain rule without requiring a translated target chart to belong to the atlas of $N$ .

L1L5

2.1

The kernel of $D \hat{f} (0)$ is $K : = D φ (p) [\ker L]$ , a complemented subspace of $E$ : the chart derivative $D φ (p)$ is a bounded linear isomorphism by [L1] and [L5] applied to $φ \circ φ^{- 1} = i d$ , and [L4] transports the given complement of $\ker L$ to a complement of $K$ ; moreover $D \hat{f} (0)$ is surjective, because $D ψ (q)$ and $D φ (p)$ are isomorphisms and $L$ is onto.

step 1.1L1L4L5

3.1

Fix a topological direct sum $E = K \oplus E_{1}$ with bounded projections $P_{K}$ , $P_{E_{1}}$ existing by [step 2.1] and [L4], and let $L_{1} : = D \hat{f} (0) ∣_{E_{1}} : E_{1} \to F$ . Then $L_{1}$ is a bounded linear bijection: it is injective because $\ker D \hat{f} (0) = K$ meets $E_{1}$ only in $0$ , and surjective because $D \hat{f} (0)$ is onto and agrees with $L_{1}$ on $E_{1}$ ; hence $L_{1}^{- 1}$ is bounded by [L3] and AC supplies the DC that [L3] assumes.

step 2.1L3L4algebra

4.1

Define $G : Ω^{'} \to F$ on the open set $Ω^{'} : = {(w, u) \in K \times E_{1} : w + u \in Ω}$ by $G (w, u) : = \hat{f} (w + u)$ . Then $G$ is $C^{k}$ , $G (0, 0) = 0$ , and its partial derivative in the second variable at $(0, 0)$ is $L_{1}$ , a bounded linear isomorphism by [step 3.1]; by [L2] there are open neighbourhoods $A \subseteq K$ of $0$ and $B \subseteq E_{1}$ of $0$ and a $C^{k}$ map $h : A \to B$ with ${(w, u) \in A \times B : \hat{f} (w + u) = 0} = {(w, h (w)) : w \in A} .$

step 3.1L2

5.1

The map $Θ (w, u) : = (w, u - h (w))$ is a homeomorphism of $A \times E_{1}$ onto itself with inverse $(w, v) \mapsto (w, v + h (w))$ , and both maps are $C^{k}$ . It carries the zero set ${(w, h (w)) : w \in A}$ of [step 4.1] onto the slice $A \times {0}$ . Let $U_{1} : = φ^{- 1} (A \times B)$ and define $Φ : = Θ \circ φ ∣_{U_{1}}$ . Its image $Θ (A \times B)$ is open, and $Φ$ is a $C^{k}$ chart compatible with every specified-atlas chart $χ$ : on each overlap the two transitions are $Φ \circ χ^{- 1} = Θ \circ φ \circ χ^{- 1}, χ \circ Φ^{- 1} = χ \circ φ^{- 1} \circ Θ^{- 1},$ restricted to open domains, hence are $C^{k}$ . Maximality of the specified atlas of $M$ now implies that $Φ$ is a chart of the structured manifold. Finally, $Φ [U_{1} \cap S] = Φ [U_{1}] \cap (K \oplus {0}),$ so $Φ$ is the split chart required by the library definition.

step 4.1L1L4L5algebra

6.1

In the charts $Φ$ and $ψ$ of [step 5.1], the coordinate representative of $f$ is $b + \hat{f} \circ Θ^{- 1}$ ; its derivative at $0$ is $D \hat{f} (0) \circ D Θ (0)^{- 1} = D \hat{f} (0)$ because $D Θ (0) = I$ . Indeed, $h (0) = 0$ and $D h (0) = 0$ , the latter by differentiating $G (w, h (w)) = 0$ at $w = 0$ with [L5], which gives $D_{K} G (0, 0) + L_{1} D h (0) = 0$ and $D_{K} G (0, 0) = D \hat{f} (0) ∣_{K} = 0$ . Consequently the kernel of the differential of $f$ at $p$ , computed in the charts $Φ$ and $ψ$ , is exactly the set of classes $[Φ, k]$ with $k \in K$ , which by [step 5.1] is the tangent space of $S$ at $p$ ; hence $T_{p} S = \ker D f (p)$ .

step 5.1L1L4L5algebra

7.1

Since $p \in S$ was arbitrary, [step 5.1] gives a split chart for $S$ at every one of its points, so $S$ is a split $C^{k}$ submanifold of $M$ , and [step 6.1] identifies its tangent space at each $p \in S$ with $\ker D f (p)$ .

step 5.1step 6.1∎

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Smooth Banach vector bundle and section

Definition

Let $M$ be a smooth ( $C^{\infty}$ ) Banach manifold modelled on the real Banach space $E$ (Countable base Banach manifold and smooth map) and let $F$ be a real Banach space whose norm topology is second countable (Banach space). This countability hypothesis makes the product $U \times F$ , with its product atlas, a Banach manifold in the library's second-countable convention.

A smooth Banach vector bundle over $M$ with fibre $F$ is a smooth Banach manifold $E$ together with a surjective smooth map $π : E \to M$ (Countable base Banach manifold and smooth map) such that:

every fibre $E_{p} : = π^{- 1} (p)$ , $p \in M$ , is a real vector space;
for every $p \in M$ there is an open neighbourhood $U$ of $p$ and a local trivialization, a diffeomorphism $Φ : π^{- 1} [U] \to U \times F$ satisfying ${p r}_{1} \circ Φ = π$ , whose restriction $Φ_{q} : = {p r}_{2} \circ Φ ∣_{E_{q}} : E_{q} \to F$ is a linear isomorphism for every $q \in U$ ;
cocycle condition: if $Φ$ over $U$ and $Ψ$ over $V$ are local trivializations, then on $π^{- 1} [U \cap V]$ , $Ψ \circ Φ^{- 1} (q, v) = (q, g (q) v)$ for a map $g : U \cap V \to B (F)$ into the bounded operators on $F$ (The spaces (\mathcal B(X,Y)) and (\mathcal B(X)) of bounded linear operators) whose representative in every base chart is $C^{\infty}$ in the Banach-space sense, and $g (q)$ is invertible for every $q \in U \cap V$ .

A smooth section of $π$ is a smooth map $s : M \to E$ with $π \circ s = {i d}_{M}$ . Its zeros are the points $p \in M$ with $s (p) = 0$ , the zero of the vector space $E_{p}$ . In a local trivialization $Φ$ over $U$ the section corresponds to the smooth map $σ : = {p r}_{2} \circ Φ \circ s : U \to F,$ and $s (p) = 0$ if and only if $σ (p) = 0$ .

At a zero $p$ of $s$ the vertical derivative of $s$ at $p$ is

$D^{v} s (p) : T_{p} M ⟶ E_{p}, D^{v} s (p) (ξ) : = Φ_{p}^{- 1} (D σ (p) ξ),$

where $Φ$ is any local trivialization around $p$ and $D σ (p)$ is the differential of the smooth manifold map $σ$ at $p$ , the target $F$ being read with its single identity chart; $ξ$ denotes a tangent vector in $T_{p} M$ .

Remarks

The vertical derivative is well defined. Let $Φ$ over $U$ and $Ψ$ over $V$ be local trivializations around the zero $p$ , with cocycle $g : U \cap V \to B (F)$ as above, and let $σ_{Φ} = {p r}_{2} \circ Φ \circ s$ , $σ_{Ψ} = {p r}_{2} \circ Ψ \circ s$ be the local representatives. Then $σ_{Ψ} (q) = g (q) σ_{Φ} (q)$ for $q \in U \cap V$ , and at the zero $p$ the product rule (Chain sum product and composition rules for Banach derivatives) applied to the composition of $q \mapsto (g (q), σ_{Φ} (q))$ with the bounded bilinear evaluation map $B (F) \times F \to F$ , $(T, v) \mapsto T v$ (A bounded bilinear map between normed spaces, For a bilinear map, boundedness is equivalent to joint continuity), gives

$D σ_{Ψ} (p) = g (p) D σ_{Φ} (p) + D g (p) σ_{Φ} (p) = g (p) D σ_{Φ} (p),$

the last term vanishing because $σ_{Φ} (p) = 0$ . Since $Ψ_{p} = g (p) \circ Φ_{p}$ as linear isomorphisms $E_{p} \to F$ , the two prescriptions give the same element of $E_{p}$ .

Fibrewise linear structure is intrinsic. The linear structure on $E_{p}$ is part of the data, and each trivialization restricts to a linear isomorphism on it. The transition maps are fibrewise bounded linear and depend smoothly on the base; the vector bundle axioms are not restated here as a list of identities because they are exactly the conditions 1–3 above.
The zero section. The assignment $p \mapsto 0 \in E_{p}$ is a smooth section, the zero section, whose vertical derivative at every point is the zero operator. Transversality of a section $s$ to the zero section is the condition that at every zero $p$ the map $D^{v} s (p)$ is surjective with complemented kernel (A complemented closed subspace of a normed space); it is the hypothesis of the next theorem on this page, where the zero set is straightened.
Ranks and dimension. Nothing is assumed about the dimension of $F$ or of $E$ beyond the second-countability convention above; the fibre may be infinite dimensional and second countable, which is exactly the case the infinite-dimensional transversality theorem below needs. When $\dim F < \infty$ and $D^{v} s (p)$ is onto, its kernel has finite codimension in $T_{p} M$ and is therefore automatically complemented, so the local condition of transversality reduces to surjectivity (Closed finite-codimensional subspaces are complemented).

TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

A transverse Banach bundle section has a split zero submanifold

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $π : E \to M$ be a smooth Banach vector bundle over a Banach manifold $M$ (Smooth Banach vector bundle and section), assume that the specified smooth atlas of $M$ is maximal among compatible smooth charts, and let $s : M \to E$ be a smooth section which is transverse to the zero section, meaning that at every zero $p$ of $s$ the vertical derivative $D^{v} s (p) : T_{p} M \to E_{p}$ is surjective with complemented kernel. Then the zero set $s^{- 1} (0)$ is a split smooth submanifold of $M$ and

$T_{p} (s^{- 1} (0)) = \ker D^{v} s (p) for every p \in s^{- 1} (0) .$

Facts & Assumptions

Given: AC, a smooth Banach vector bundle $π : E \to M$ , a maximal specified smooth atlas on $M$ , and a smooth section $s$ whose vertical derivative is onto with complemented kernel at every zero.

[L1]

The definition of the vertical derivative and its independence of the trivialization, including the transformation $D σ_{Ψ} (p) = g (p) D σ_{Φ} (p)$ at a zero (Smooth Banach vector bundle and section).

[L2]

Regular value theorem for Banach manifolds (Regular value theorem for Banach manifolds), applied under the assumed AC and its maximal-domain-atlas hypothesis: a $C^{k}$ map, $k \geq 1$ (including $k = \infty$ ), whose derivative at every point of a level set is onto with complemented kernel has that level set as a split $C^{k}$ submanifold with tangent equal to the kernel.

[L3]

Split submanifolds and their local character (Split Banach submanifold); tangents of open subsets of a Banach space are identified with the model space (Tangent space and differential on a Banach manifold); tensor and operator calculus as used for the transformation in [L1] (Chain sum product and composition rules for Banach derivatives).

Proof

technique · direct

1.1

Let $p$ be a zero of $s$ and let $Φ$ be a smooth local trivialization over an open neighbourhood $U$ of $p$ ; then $σ : = {pr}_{2} \circ Φ \circ s : U \to F$ is smooth and $σ^{- 1} (0) = s^{- 1} (0) \cap U$ . For every $q \in σ^{- 1} (0)$ , [L1] identifies $D σ (q) : T_{q} U \to F$ with $D^{v} s (q)$ followed by the fibre isomorphism $Φ_{q} : E_{q} \to F$ . Thus $D σ (q)$ is surjective with complemented kernel for every point of this local zero set. The atlas on $U$ formed by restrictions of charts of the maximal smooth atlas on $M$ is itself maximal: every compatible smooth chart on $U$ is also compatible with the atlas of $M$ (charts not meeting its domain are automatically compatible), and hence already belongs to that atlas.

L1L3

2.1

Apply [L2] with $k = \infty$ to the smooth map $σ : U \to F$ at the value $0$ . The domain carries the maximal smooth atlas verified in [step 1.1], and every point of $σ^{- 1} (0)$ has derivative onto with complemented kernel. Therefore $σ^{- 1} (0)$ is a split smooth submanifold of $U$ and $T_{q} (σ^{- 1} (0)) = \ker D σ (q)$ for every $q \in σ^{- 1} (0)$ .

step 1.1L2

3.1

Since $U$ is open in $M$ , the set $σ^{- 1} (0) = s^{- 1} (0) \cap U$ is a split submanifold of $M$ as well, with the same tangent spaces: splitness is local by [L3] and the local charts of $U$ are charts of $M$ .

step 2.1L3

4.1

The zeros of $s$ are covered by such neighbourhoods $U$ as $p$ ranges over $s^{- 1} (0)$ ; by [step 3.1] each point of $s^{- 1} (0)$ has a split chart in $M$ , so $s^{- 1} (0)$ is a split smooth submanifold of $M$ .

step 3.1L3

4.2

For the tangent description, fix a zero $p$ and two trivializations $Φ$ over $U$ and $Ψ$ over $V$ with $p \in U \cap V$ , and let $σ_{Φ}, σ_{Ψ}$ be the corresponding local representatives; [L1] gives $D σ_{Ψ} (p) = g (p) D σ_{Φ} (p)$ , where $g (p)$ is the invertible fibre isomorphism of the cocycle. Hence the kernels of $D σ_{Ψ} (p)$ and $D σ_{Φ} (p)$ coincide, and the kernel of $D^{v} s (p)$ is intrinsically characterised as the set of $ξ \in T_{p} M$ with $D σ_{Φ} (p) ξ = 0$ for one, equivalently every, trivialization around $p$ .

step 3.1L1L3

5.1

Combining [step 2.1] with [step 4.2]: for a zero $p$ , $T_{p} (s^{- 1} (0)) = \ker D σ_{Φ} (p) = \ker D^{v} s (p)$ , the first equality because $σ^{- 1} (0)$ is the zero set of the local representative and the tangent of a split submanifold is computed in its charts, the second by the trivialization-independence just proved.

step 2.1step 4.2L1L3∎

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Fredholm map between Banach manifolds

Definition

Let $M$ and $N$ be $C^{1}$ Banach manifolds (Countable base Banach manifold and smooth map) and let $f : M \to N$ be a $C^{1}$ map, so that $D f (p) : T_{p} M \to T_{f (p)} N$ is a bounded linear operator for every $p \in M$ (Tangent space and differential on a Banach manifold, A bounded linear operator between normed spaces). Then:

$f$ is Fredholm at $p$ when $D f (p)$ is a Fredholm operator, that is when $\ker D f (p)$ is finite dimensional, $ran D f (p)$ is closed in $T_{f (p)} N$ , and the cokernel $coker D f (p) = T_{f (p)} N / ran D f (p)$ is finite dimensional (Fredholm operator cokernel and index);
$f$ is a Fredholm map when it is Fredholm at every point of $M$ ;
the index of a Fredholm map at $p$ is the integer $ind D f (p) = \dim \ker D f (p) - \dim coker D f (p)$ , and $f$ has index $n$ when $ind D f (p) = n$ for every $p \in M$ .

The pointwise index is defined whenever $f$ is Fredholm at $p$ ; the phrase "has index $n$ " is a separate, global condition, and the local constancy of $p \mapsto ind D f (p)$ is a theorem below, not part of this definition.

Remarks

Well-definedness: chart changes conjugate the derivative. If $(φ, ψ)$ and $(φ^{'}, ψ^{'})$ are two chart pairs around $p$ and $f (p)$ , then the corresponding representatives of $f$ satisfy $ψ^{'} \circ f \circ φ^{' - 1} = (ψ^{'} \circ ψ^{- 1}) \circ (ψ \circ f \circ φ^{- 1}) \circ (φ \circ φ^{' - 1})$ , so their derivatives at the point in question are related by $D {\hat{f}}^{'} (x^{'}) = D (ψ^{'} \circ ψ^{- 1}) (ψ (f (p))) D \hat{f} (x) D (φ \circ φ^{' - 1}) (x^{'})$ , a conjugation by bounded linear isomorphisms (Banach manifold differentials are chart independent). Conjugation by isomorphisms preserves Fredholmness and the index: for bounded isomorphisms $U, V$ the composite $U T V$ is Fredholm exactly when $T$ is, and $ind (U T V) = ind T$ , because $ind (U T) = ind U + ind T$ , isomorphisms have index $0$ , and the same applies on the other side (Fredholm index is additive, Fredholm operator cokernel and index); that additivity theorem is proved under AC, which is therefore inherited by every use of the index made through charts.
Index and the Fredholm condition are local in the base. Both are properties of the single operator $D f (p)$ in the appropriate tangent spaces; neither involves any choice of charts, by the previous remark. In particular the index at $p$ may be read in any chart pair around $p$ and $f (p)$ .
Nonconstant index is possible a priori. The definition allows the pointwise index to jump, and the local-constancy proposition below is what rules that out for $C^{1}$ Fredholm maps. It is not built into the definition, because the proof needs the openness of the set of Fredholm operators in operator norm, a theorem about operators rather than about manifolds.
Finite-dimensional fibres. When the index is $\dim M - \dim N$ in the finite-dimensional model case one recovers the classical notion; the definition here is the infinite-dimensional one, in which neither tangent space need be finite dimensional and only the kernel and cokernel are required to be.

LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Local finite-dimensional reduction for a Fredholm map

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $f : M \to N$ be a $C^{k}$ Fredholm map with $k \geq 1$ between $C^{k}$ Banach manifolds (Fredholm map between Banach manifolds), and let $p \in M$ . Let $E$ and $F$ be the model spaces of $M$ and $N$ . Choose charts $φ$ at $p$ and $ψ$ at $f (p)$ , put $a : = φ (p)$ and $b : = ψ (f (p))$ , and use the recentered coordinate representative $\hat{f} (x) : = ψ (f (φ^{- 1} (a + x))) - b .$ Let $L : = D \hat{f} (0) : E \to F$ . Fix topological direct sums

$E = \ker L \oplus E_{1}, F = ran L \oplus C$

with bounded coordinate projections, in which $\ker L$ and $C ≅ coker L$ are finite dimensional (A complemented closed subspace of a normed space).

Then there are open neighbourhoods $U_{0} \subseteq ran L$ of $0$ , $A_{0} \subseteq \ker L$ of $0$ , a $C^{k}$ diffeomorphism $T$ from a neighbourhood of $p$ onto (an open subset of) $U_{0} \times A_{0}$ , and a $C^{k}$ map

$g : U_{0} \times A_{0} ⟶ C,$

such that, after the translation matching $p$ to $0$ and $f (p)$ to $0$ and the linear identification $F = ran L \oplus C$ , the map $f$ becomes the map

$(u, v) ⟼ (u, g (u, v)) (u \in U_{0}, v \in A_{0}),$

with first coordinate in $ran L$ and second coordinate in $C$ .

Thus, near $p$ , $f$ is $C^{k}$ -equivalent to a map that is the identity in the infinite-dimensional coordinate $u$ up to a finite-dimensional obstruction map $g$ defined on the product of an open subset of the range complement and an open subset of the finite-dimensional kernel. No constant-rank or constant-index claim is made, and $g$ depends on both variables.

Facts & Assumptions

Given: AC, $C^{k}$ Banach manifolds $M, N$ with $k \geq 1$ , a $C^{k}$ Fredholm map $f : M \to N$ , a point $p \in M$ , arbitrary specified-atlas charts $φ, ψ$ at $p, f (p)$ , their coordinate values $a, b$ , and a Fredholm splitting as in the statement for the recentered representative $\hat{f} (x) = ψ (f (φ^{- 1} (a + x))) - b$ and $L : = D \hat{f} (0) : E \to F$ .

[L1]

Fredholm maps, tangents and chart-independence of the differential (Fredholm map between Banach manifolds, Banach manifold differentials are chart independent, Tangent space and differential on a Banach manifold).

[L2]

Fredholm splitting: for a Fredholm operator $T : X \to Y$ between real Banach spaces there are a closed $X_{1}$ with $X = \ker T \oplus X_{1}$ , a finite-dimensional closed $Y_{0}$ with $Y = ran T \oplus Y_{0}$ , all four projections bounded, and $T ∣_{X_{1}} : X_{1} \to ran T$ is a bounded isomorphism; moreover $\dim_{R} Y_{0} = \dim_{R} coker T$ (Fredholm splitting and parametrix).

[L3]

A bounded bijection between Banach spaces has a bounded inverse under DC (Bounded inverse theorem), and AC supplies DC (AC supplies the countable and dependent choices used in Banach integration).

[L4]

Implicit function theorem for $C^{k}$ maps, $k \geq 1$ (Implicit function theorem for Banach spaces); applied under the assumed AC.

[L5]

Chain rule and the $C^{k}$ calculus of open subsets of Banach spaces (Chain sum product and composition rules for Banach derivatives, C k map between Banach spaces).

[L6]

Charts of the manifolds and their representative maps are $C^{k}$ ; the model spaces are real Banach spaces (Countable base Banach manifold and smooth map).

Proof

technique · direct

1.1

The set $Ω : = {x \in E : a + x \in φ [dom φ \cap f^{- 1} (dom ψ)]}$ is an open neighbourhood of $0$ . The recentered representative $\hat{f} (x) = ψ (f (φ^{- 1} (a + x))) - b$ is $C^{k}$ on $Ω$ , satisfies $\hat{f} (0) = 0$ , and has derivative $D \hat{f} (0) = L$ by definition. The source and target translations have identity derivative, so chart independence identifies $L$ with the tangent map $D f (p)$ up to the bounded chart isomorphisms; hence $L$ is Fredholm. No translated coordinate map is asserted to be a member of either specified atlas.

L1L5L6

2.1

Use the fixed splittings from the statement. The restriction $L_{1} : = L ∣_{E_{1}} : E_{1} \to ran L$ is bounded and injective because $E_{1} \cap \ker L = {0}$ ; it is surjective because writing any $x \in E$ as $x = v + x_{1}$ gives $L x = L x_{1}$ . The range is closed and hence Banach, and $C$ is finite dimensional with $\dim_{R} C = \dim_{R} coker L$ , as guaranteed by [L2].

step 1.1L2

3.1

By [L3] the inverse $L_{1}^{- 1} : ran L \to E_{1}$ is bounded; AC supplies the DC assumed by that theorem.

step 2.1L3

4.1

Write $K : = \ker L$ , $ρ : = {pr}_{ran L} \circ \hat{f}$ , and $c : = {pr}_{C} \circ \hat{f}$ on $Ω$ ; both component maps are $C^{k}$ by [L5]. On the open set $Ω^{'} : = {((w, y), x_{1}) \in (K \times ran L) \times E_{1} : w + x_{1} \in Ω}$ define $G ((w, y), x_{1}) : = ρ (w + x_{1}) - y$ . Its partial derivative in $x_{1}$ at the origin is $L_{1}$ , a bounded isomorphism by step 3.1. By [L4], after shrinking to a product $A_{0} \times U_{0} \subseteq K \times ran L$ , there are a neighbourhood $B \subseteq E_{1}$ and a $C^{k}$ map $θ : A_{0} \times U_{0} \to B$ such that $ρ (w + θ (w, u)) = u$ , uniquely among $x_{1} \in B$ .

step 2.1step 3.1L4L5

5.1

Coordinate diffeomorphism. The subset $T_{0} : = {(w, x_{1}) \in K \times B : w + x_{1} \in Ω, (w, ρ (w + x_{1})) \in A_{0} \times U_{0}}$ is an open neighbourhood of $(0, 0)$ . On it, the formula $S (w, x_{1}) : = (ρ (w + x_{1}), w)$ gives a map $S : T_{0} \to U_{0} \times A_{0}$ , and [step 4.1] shows that $S$ is bijective with $C^{k}$ inverse $(u, w) \mapsto (w, θ (w, u))$ ; hence $S$ is a $C^{k}$ diffeomorphism. Composing $S$ with the linear splitting $E = K \oplus E_{1}$ and with the ordinary translated coordinate map $x \mapsto φ (x) - a$ gives the asserted $C^{k}$ diffeomorphism $T$ from a neighbourhood of $p$ onto $U_{0} \times A_{0}$ . This construction uses the given atlas chart $φ$ but does not claim its translation is another atlas member.

step 4.1L5L6

6.1

Define $g : U_{0} \times A_{0} \to C$ by $g (u, w) : = c (w + θ (w, u))$ . It is $C^{k}$ , and for $(u, w) \in U_{0} \times A_{0}$ one has $\hat{f} (S^{- 1} (u, w)) = (u, g (u, w))$ under the fixed decomposition $F = ran L \oplus C$ .

step 4.1step 5.1L5

7.1

Returning through the given atlas charts $φ, ψ$ and undoing the affine translations by $a, b$ , [step 6.1] is exactly the asserted local normal form for the recentered representative and the fixed splittings; the kernel variable and obstruction target are finite dimensional by [L2].

step 2.1step 5.1step 6.1L1∎

RemarkRemark: Literature-sourcedProof: Not supplied‡ sources checked 2026-09-22‡ not proved hereOpen item page →

‡ Recorded, not proved here. This statement is included so the library can refer to it honestly, with a citation to the literature. It is not proved anywhere in this library: the track that would prove it has not been developed here yet.

Fredholm maps have countable proper local restrictions externally

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $f : M \to N$ be a $C^{h}$ map, $h \geq 1$ , between Hausdorff second-countable real Banach manifolds (Countable base Banach manifold and smooth map), and suppose every $D f (x)$ has closed range and finite-dimensional kernel and cokernel. There is a finite or countable family of closed subsets $(C_{j})_{j \in J}$ of $M$ , indexed by $J \subseteq N$ , whose interiors cover $M$ such that, for every $j \in J$ :

$C_{j}$ is contained in a Fredholm normal-form neighbourhood $W_{j}$ ;
$f ∣_{C_{j}} : C_{j} \to N$ is proper, meaning inverse images of compact sets are compact; and
$f (W_{j})$ lies in a target chart.

Here a Fredholm normal-form neighbourhood means source and target coordinates in which

f (u, v) = (u, g (u, v)),

with $u$ in a Banach range space, $v$ in a finite-dimensional kernel space, and $g$ valued in a finite-dimensional obstruction space, as in Local finite-dimensional reduction for a Fredholm map. The chart may be shrunk before choosing the subordinate closed proper restriction. No closed ball in an infinite-dimensional Banach space is asserted compact. If $M$ is empty, take $J = \emptyset$ ; no normal-form neighbourhood or target chart then needs to be chosen.

Remarks

This countable localization and local-properness package is recorded from Smale and is not proved locally here.

RemarkRemark: Literature-sourcedProof: Not supplied‡ sources checked 2026-09-22‡ not proved hereOpen item page →

Critical images of proper local Fredholm restrictions are nowhere dense externally

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $f : M \to N$ be a $C^{h}$ map of fixed Fredholm index $m$ between Hausdorff second-countable real Banach manifolds (Countable base Banach manifold and smooth map), where $h$ is a positive integer or $\infty$ and $h > \max {m, 0}$ . Suppose $W \subseteq M$ is open, $f (W)$ lies in a target chart, and on $W$ the map has Fredholm normal form

(u, v) ⟼ (u, g (u, v)),

where the kernel variable lies in a finite-dimensional space $K$ , the obstruction component lies in a finite-dimensional space $Q$ , and $\dim K - \dim Q = m$ (Local finite-dimensional reduction for a Fredholm map).

If $C \subseteq W$ is closed in $M$ and $f ∣_{C} : C \to N$ is proper, then

f (C \cap Crit (f))

is closed and nowhere dense in $N$ , where $Crit (f) = {x \in M : D f (x) is not surjective}$ and nowhere dense has the meaning in Nowhere dense, meagre, residual, and comeagre subsets of a topological space.

Remarks

This is the localized category consequence used in Smale's proof, not a separately numbered theorem there and not a local proof in this library.

PropositionStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

The index of a Fredholm map is locally constant

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $f : M \to N$ be a $C^{1}$ Fredholm map between Banach manifolds (Fredholm map between Banach manifolds). Then the function

$M ⟶ Z, p ⟼ ind D f (p),$

is locally constant, and consequently it is constant on every connected component of $M$ (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).

Facts & Assumptions

Given: AC, $C^{1}$ Banach manifolds $M, N$ and a $C^{1}$ Fredholm map $f : M \to N$ .

[L1]

Fredholm map: $D f (p)$ is Fredholm at every $p$ , its index is $\dim \ker - \dim coker$ , and chart changes conjugate the differential, so the index may be read in any chart pair (Fredholm map between Banach manifolds, Banach manifold differentials are chart independent).

[L2]

The Fredholm operators $X \to Y$ between Banach spaces form an open subset of $B (X, Y)$ : near a Fredholm $T$ every operator with the same index is Fredholm of that index (Fredholm index is locally constant); the index is additive under composition, and invertible operators have index $0$ (Fredholm index is additive).

[L3]

$C^{1}$ means that the derivative map is continuous in operator norm (C k map between Banach spaces).

[L4]

A map from a topological space to a discrete set that is locally constant is constant on each connected component: the preimages of the values are open, form a partition, and a connected space admits no partition into two disjoint nonempty open sets (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[L5]

Charts of the manifolds are homeomorphisms onto open subsets of the model spaces (Countable base Banach manifold and smooth map, Tangent space and differential on a Banach manifold).

Proof

technique · direct

1.1

Fix $p \in M$ and charts $φ$ of $M$ at $p$ and $ψ$ of $N$ at $f (p)$ , and write $x_{0} : = φ (p)$ ; the representative $\hat{f} : = ψ \circ f \circ φ^{- 1}$ is $C^{1}$ near $x_{0}$ and its derivative is continuous there by [L3].

L3L5

2.1

Conjugation identity: for $x$ near $x_{0}$ , writing $y : = φ^{- 1} (x)$ , the chain rule gives $D \hat{f} (x) = D ψ (f (y)) \circ D f (y) \circ D φ (y)^{- 1}$ ; here $D ψ (f (y))$ and $D φ (y)$ are bounded linear isomorphisms and depend continuously on $y$ by [L5] and the chain rule applied to $φ \circ φ^{- 1} = i d$ and $ψ \circ ψ^{- 1} = i d$ .

step 1.1L1L5

3.1

Since $D \hat{f} (x_{0})$ is Fredholm by [L1], [L2] supplies a real $δ > 0$ such that every bounded operator within distance $δ$ of $D \hat{f} (x_{0})$ is Fredholm with the same index; by continuity in [step 2.1] and [L3] there is a neighbourhood $V$ of $x_{0}$ with $∥ D \hat{f} (x) - D \hat{f} (x_{0}) ∥ < δ$ for $x \in V$ .

step 1.1step 2.1L2L3

4.1

Hence for every $x \in V$ the operator $D \hat{f} (x)$ is Fredholm with $ind D \hat{f} (x) = ind D \hat{f} (x_{0})$ ; translating through the conjugation identity of [step 2.1] and the index invariance recorded in [L1] and [L2] gives that $D f (y)$ is Fredholm with $ind D f (y) = ind D f (p)$ for every $y$ in the open neighbourhood $φ^{- 1} [V]$ of $p$ .

step 2.1step 3.1L1L2

5.1

Since $p$ was arbitrary, $p \mapsto ind D f (p)$ is locally constant; by [L4] it is constant on every connected component of $M$ .

step 4.1L4∎

RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-22Open item page →

Surjectivity alone does not imply a complemented kernel

Remarks

The regular value theorem of this page (Regular value theorem for Banach manifolds) separately requires the specified atlas of the domain manifold to be maximal and assumes that at every point of the level set the derivative is surjective with complemented kernel (A complemented closed subspace of a normed space). For general Banach spaces the second clause is not a consequence of the first, and it cannot be dropped:

Equivalent formulation. Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain). For a surjective bounded linear operator $L : X \to Y$ between Banach spaces, $\ker L$ is complemented in $X$ if and only if $L$ admits a bounded right inverse (Under Dependent Choice, a surjective bounded operator between Banach spaces has a bounded right inverse exactly when its kernel is complemented). Thus the hypothesis of the regular value theorem is exactly the requirement that the derivative admit a bounded right inverse along the level set.
Why surjectivity by itself is not enough, and where the failure is seen. The open mapping theorem makes $L$ open, but it does not supply a bounded linear right inverse. Without one, the fibres of the linear map are affine translates of a closed uncomplemented subspace and cannot be the split coordinate slices demanded by Split Banach submanifold. The companion page carries the standard witness: $c_{0}$ is a closed subspace of $ℓ^{\infty}$ that is not complemented in it, so the identity chart has no split-coordinate decomposition for the pair $(ℓ^{\infty}, c_{0})$ . Because $ℓ^{\infty}$ is not second countable, this is a Banach-space obstruction and not a counterexample involving a Banach manifold under this library's convention. It shows why complementability is a genuine extra linear hypothesis; it does not by itself exhibit a regular level set in the manifold category.
Automatic cases, and the ones that matter below. A closed subspace that is finite dimensional or of finite codimension is automatically complemented (Finite-dimensional subspaces are complemented, Closed finite-codimensional subspaces are complemented). In particular, if $L$ is a Fredholm operator (Fredholm operator cokernel and index) or if its target is finite dimensional, then surjectivity of $L$ implies that $\ker L$ is complemented, so the extra clause of the theorem is automatic in those cases. This is why the Fredholm-and-transversality results of this page can print the complemented-kernel hypothesis once and use it everywhere without further case distinctions, while the abstract theorem states it outright.
Bookkeeping. The equivalence in the first bullet is a Dependent Choice theorem, and the regular value theorem is proved under the Axiom of Choice (The Axiom of Choice), which supplies DC; it also has the independent structural hypothesis that the specified domain atlas is maximal. The counterexample on the companion page uses only the Axiom of Countable Choice, since the non-complementation it appeals to is proved at that strength.

5 · Examples, counterexamples and false statements

None yet.

Banach-Space Differential Calculus and Banach Manifolds

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Fréchet derivative between Banach spaces

Definition

Remarks

The Fréchet derivative is unique

Statement

Facts & Assumptions

Proof

Chain sum product and composition rules for Banach derivatives

Statement

Facts & Assumptions

Proof

C k map between Banach spaces

Definition

Remarks

Banach mean value estimate on a convex set

Statement

Facts & Assumptions

Proof

Inverse function theorem for Banach spaces

Statement

Facts & Assumptions

Proof

Implicit function theorem for Banach spaces

Statement

Facts & Assumptions

Proof

Countable base Banach manifold and smooth map

Definition

Remarks

Tangent space and differential on a Banach manifold

Definition

Remarks

Banach manifold differentials are chart independent

Statement

Facts & Assumptions

Proof

Split Banach submanifold

Definition

Remarks

Regular value theorem for Banach manifolds

Statement

Facts & Assumptions

Proof

Smooth Banach vector bundle and section

Definition

Remarks

A transverse Banach bundle section has a split zero submanifold

Statement

Facts & Assumptions

Proof

Fredholm map between Banach manifolds

Definition

Remarks

Local finite-dimensional reduction for a Fredholm map

Statement

Facts & Assumptions

Proof

Fredholm maps have countable proper local restrictions externally

Statement

Remarks

Critical images of proper local Fredholm restrictions are nowhere dense externally

Statement

Remarks

The index of a Fredholm map is locally constant

Statement

Facts & Assumptions

Proof

Surjectivity alone does not imply a complemented kernel

Remarks

5 · Examples, counterexamples and false statements

Sources