LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22

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.

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∎

Depends on

Used by

Dependency tree · two levels

52 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Alberto Abbondandolo and Pietro Majer, Lectures on the Morse Complex — §2.11, Theorem 2.19 proof (standard reference, not scraped)