Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-29
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.

A map from a disjoint union is smooth iff each restriction is smooth

Statement

Let X=⨆i∈IMi be a countable disjoint union of fixed-dimensional smooth manifolds with its canonical smooth structure, let N be a smooth manifold, and let F:X→N be a map. Then F is smooth if and only if each restriction

Fi:=F∘κi:Mi→N

to a summand is smooth.

Facts & Assumptions

Given: A countable disjoint union X=⨆i∈IMi with canonical injections κi:Mi→X, a smooth manifold N, and a map F:X→N.

[F1]

The disjoint union X is a smooth manifold whose smooth charts are the transported charts coming from the summands; in particular every point of X lies in exactly one summand and around that point there are smooth charts coming from that summand (Countable disjoint unions of fixed-dimensional smooth manifolds are smooth manifolds).

[F2]

A map between smooth manifolds is smooth exactly when it is continuous and its coordinate representatives are smooth near each point (Cr and smooth maps between smooth manifolds).

Proof

technique · direct
1.1givenF1F2L1choose

Assume F is smooth, and fix i∈I and p∈Mi with charts as below. [given, F1, F2, L1, choose] By [F2] it is continuous, so [L1] makes each restriction Fi=F∘κi continuous. Fix i∈I and p∈Mi. Choose a smooth chart (U,α) of Mi at p and a smooth chart (V,β) of N at Fi(p). The transported chart (κi[U],α∘κi−1) is a smooth chart of X at κi(p) by [F1].

1.2F1F2L1choose

Conversely assume every restriction Fi is smooth, and fix x∈X with charts as below. [F1, F2, L1, choose] Then [F2] makes each Fi continuous, so [L1] makes F continuous. Let x∈X. By [F1] there is a unique i∈I and a unique point p∈Mi with x=κi(p); choose a smooth chart (U,α) of Mi at p and a smooth chart (V,β) of N at F(x). The transported chart (κi[U],α∘κi−1) is smooth on X.

2.1F1F2step 1.1step 1.2

In the charts chosen in steps 1.1 and 1.2, the representative of the [F1, F2, step 1.1, step 1.2] restriction Fi is β∘Fi∘α−1=β∘F∘(α∘κi−1)−1. Under the hypothesis of step 1.1, the right-hand side is the representative of F in a transported source chart, so [F2] makes it smooth and therefore every Fi is smooth. Under the hypothesis of step 1.2, the same formula identifies the representative of F with β∘Fi∘α−1, which is smooth because Fi is. Hence [F2] makes F smooth at x, and therefore smooth everywhere.

3.1step 2.1∎

Step 2.1 proves both directions of the equivalence.

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