Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-31
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 graph of a smooth map is an embedded submanifold

Statement

Let F:M→N be smooth. Its graph

ΓF:={(p,F(p)):p∈M}⊆M×N

is an embedded submanifold of M×N of dimension dim⁡M.

Facts & Assumptions

Given: A smooth map F:M→N.

[L1]

The diagonal ΔN⊆N×N is an embedded submanifold (The diagonal is an embedded submanifold).

[L2]

A regular level set is an embedded submanifold (A regular level set is an embedded submanifold).

[L3]

Products of smooth manifolds carry canonical product structures (Products of smooth manifolds have a canonical product smooth structure).

Proof

technique · direct
1.1L1L3given

Consider the map G:M×N→N×N defined by G(p,q)=(F(p),q). In product charts on M×N and N×N, its representative has the form (u,v)↦(F^(u),v), so G is smooth. The graph satisfies ΓF=G−1(ΔN).

1.2L1L3givenconstruct

Fix (p,F(p))∈ΓF. Choose a chart ψ:V→Ω⊆Rn on N at F(p). By [L3], the product chart ψ×ψ identifies a neighbourhood of (F(p),F(p)) in N×N with Ω×Ω, and in these coordinates the diagonal from [L1] is the set {(a,b):a=b}. The difference map D:Ω×Ω→Rn, D(a,b)=b−a, is a smooth submersion with zero fibre exactly that diagonal slice.

2.1step 1.1step 1.2construct

Choose a chart φ:U→Λ on M at p with F(U)⊆V, and define H:=D∘(ψ×ψ)∘G∘(φ×ψ)−1:Λ×Ω→Rn. Then H(u,v)=v−F^(u), so the Jacobian of H has block form [−DF^(u)In] and is surjective at every point. Its zero fibre is exactly the graph in these coordinates. Thus 0 is a regular value of H.

3.1L2step 2.1∎

By [L2], the zero fibre of H is an embedded codimension-n submanifold of M×N near (p,F(p)). Since (p,F(p)) was arbitrary, ΓF is an embedded submanifold. Its ambient dimension is dim⁡M+n, so its dimension is dim⁡M.

Depends on

Used by

Dependency tree · two levels

19 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