Alphabeta Math
LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)
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.

Fixed points are exactly the intersections of the graph with the diagonal

Statement

Let M be a smooth manifold and f:M→M a smooth map (Cr and smooth maps between smooth manifolds) with graph Γf={(x,f(x)):x∈M}⊆M×M (The graph of a smooth map is an embedded submanifold) and diagonal ΔM={(x,x):x∈M} (The diagonal ΔX⊆X×X, the diagonal map δX, and the pairing ⟨f,g⟩ of two maps, The diagonal is an embedded submanifold). Then for every x∈M, x∈Fix⁡(f)  ⟺  (x,f(x))∈Γf∩ΔM  ⟺  (x,x)∈Γf, so the graph map γf:M→M×M, γf(x)=(x,f(x)), satisfies γf−1(ΔM)=Fix⁡(f)={x∈M:f(x)=x}: fixed points of f are exactly the intersections of the graph with the diagonal.

Facts & Assumptions

Given: A smooth manifold M, a smooth map f:M→M, its graph Γf={(x,f(x)):x∈M} and the diagonal ΔM={(x,x):x∈M} of the product M×M; write Fix⁡(f)={x∈M:f(x)=x}.

[F1]

The graph Γf⊆M×M is an embedded submanifold of dimension dim⁡M, and (y,z)∈Γf holds exactly when z=f(y) (The graph of a smooth map is an embedded submanifold).

[F2]

ΔM={(x,x):x∈M} and the graph map γf, as the pairing ⟨idM,f⟩, satisfies γf−1[ΔM]={x∈M:idM(x)=f(x)} (The diagonal ΔX⊆X×X, the diagonal map δX, and the pairing ⟨f,g⟩ of two maps).

[F3]

The diagonal ΔM is an embedded submanifold of M×M (The diagonal is an embedded submanifold).

Proof

1.1givenF1F2F3

Let x∈M. By [F2], (x,f(x))∈ΔM holds exactly when x=f(x); by [F1], (x,x)∈Γf holds exactly when x=f(x); and (x,f(x))∈Γf always holds by the definition of the graph in [F1], while (x,x)∈ΔM holds exactly when x=x. Hence the three conditions x∈Fix⁡(f), (x,f(x))∈Γf∩ΔM and (x,x)∈Γf all say the same equation f(x)=x, so they are equivalent. The intersection is taken inside the product M×M, in which both factors are embedded submanifolds by [F1] and [F3].

2.1step 1.1F2given∎

The preimage of the diagonal under the graph map is γf−1[ΔM]={x∈M:γf(x)∈ΔM}={x∈M:(x,f(x))∈ΔM}, which by [F2] is {x∈M:x=f(x)}=Fix⁡(f); this is the same set whose elements are the points x with (x,x)∈Γf by step 1.1, so fixed points of f correspond exactly to the intersections Γf∩ΔM, through the map x↦(x,f(x))=(x,x).

Depends on

Used by

Dependency tree · two levels

17 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