Alphabeta Math
PropositionStatement: 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.

The index of a Fredholm map is locally constant

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let f:M→N be a C1 Fredholm map between Banach manifolds (Fredholm map between Banach manifolds). Then the function

M⟶Z,p⟼ind⁡Df(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, C1 Banach manifolds M,N and a C1 Fredholm map f:M→N.

[L1]

Fredholm map: Df(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→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]

C1 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.1L3L5

Fix p∈M and charts φ of M at p and ψ of N at f(p), and write x0:=φ(p); the representative f^:=ψ∘f∘φ−1 is C1 near x0 and its derivative is continuous there by [L3].

2.1step 1.1L1L5

Conjugation identity: for x near x0, writing y:=φ−1(x), the chain rule gives Df^(x)=Dψ(f(y))∘Df(y)∘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 φ∘φ−1=id and ψ∘ψ−1=id.

3.1step 1.1step 2.1L2L3

Since Df^(x0) is Fredholm by [L1], [L2] supplies a real δ>0 such that every bounded operator within distance δ of Df^(x0) is Fredholm with the same index; by continuity in [step 2.1] and [L3] there is a neighbourhood V of x0 with ∥Df^(x)−Df^(x0)∥<δ for x∈V.

4.1step 2.1step 3.1L1L2

Hence for every x∈V the operator Df^(x) is Fredholm with ind⁡Df^(x)=ind⁡Df^(x0); translating through the conjugation identity of [step 2.1] and the index invariance recorded in [L1] and [L2] gives that Df(y) is Fredholm with ind⁡Df(y)=ind⁡Df(p) for every y in the open neighbourhood φ−1[V] of p.

5.1step 4.1L4∎

Since p was arbitrary, p↦ind⁡Df(p) is locally constant; by [L4] it is constant on every connected component of M.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

49 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