PropositionStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

Products of smooth manifolds have a canonical product smooth structure

Statement

Let $(M, S)$ and $(N, T)$ be smooth manifolds of dimensions $m$ and $n$ . Then $M \times N$ with the product topology is a topological $(m + n)$ -manifold. If $A$ and $B$ are smooth atlases with $[A] = S$ and $[B] = T$ , then the set of product charts

$A \times B : = {(V \times W, φ \times ψ) : (V, φ) \in A, (W, ψ) \in B}$

is a smooth atlas on $M \times N$ , and the maximal atlas it generates is independent of the presenting atlases: it depends only on $S$ and $T$ . This maximal atlas is the product smooth structure of $M \times N$ .

Facts & Assumptions

Given: Smooth manifolds $(M, S)$ , $(N, T)$ of dimensions $m, n$ , with presenting atlases $A, B$ .

[F1]

A product of Hausdorff spaces is Hausdorff (Arbitrary products preserve $T_{0}$ , $T_{1}$ , and Hausdorffness).

[F2]

A topological space is second countable when its topology has an at most countable basis (Second countability: an at most countable basis for the topology).

[F3]

A finite power of an at most countable set is at most countable (Every finite power of an at most countable set is at most countable).

[F4]

The product topology on $\prod_{i} X_{i}$ has the products of one open set from each factor as a basis, and projections are as in The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space.

[F6]

A chart is a homeomorphism of an open domain onto an open subset of $R^{k}$ (Manifold charts, coordinate domains, and coordinate functions), and two charts are smoothly compatible when their domains are disjoint or both transition maps are smooth (Smoothly compatible charts and the smoothness of Euclidean transition maps).

[F7]

A smooth atlas is a set of pairwise smoothly compatible charts whose domains cover the manifold (Smooth atlases).

[L1]

Two atlases generate the same maximal atlas exactly when their union is a smooth atlas (Each smooth atlas is contained in a unique maximal smooth atlas).

[A1]

Under the identification of $R^{m} \times R^{n}$ with $R^{m + n}$ supplied by For $n \geq 1$ the product topology on $n$ copies of the usual topology of $R$ is the metric topology of $d_{\infty}$ on $R^{n}$ , and hence also of $d_{1}$ and $d_{2}$ , so $R^{n}$ as a product and $R^{n}$ as a metric space are one space, a map into the product is smooth exactly when both component maps are smooth, and the product of two homeomorphisms onto open sets is a homeomorphism onto the product of those open sets.

Proof

technique · direct

1.1

$M \times N$ is Hausdorff by [F1]. Second countability: choose at most countable bases $B_{M}$ and $B_{N}$ of $M$ and $N$ by [F2]; by [F4] the set ${U \times V : U \in B_{M}, V \in B_{N}}$ is a basis of the product topology, and it is at most countable by [F3], so $M \times N$ is second countable by [F2]. For $(p, q) \in M \times N$ take charts $(V, φ)$ at $p$ and $(W, ψ)$ at $q$ ; by [A1] the product $φ \times ψ : V \times W \to φ (V) \times ψ (W)$ is a homeomorphism between the open set $V \times W$ and the open subset $φ (V) \times ψ (W)$ of $R^{m + n}$ . Hence $M \times N$ is a topological $(m + n)$ -manifold.

givenF1F2F3F4F6A1

1.2

The transition between product charts of $A \times B$ is $(φ^{'} \times ψ^{'}) \circ (φ \times ψ)^{- 1} = (φ^{'} \circ φ^{- 1}) \times (ψ^{'} \circ ψ^{- 1})$ on the overlap image; the two factors are smooth by the compatibility clause of [F6] applied inside $A$ and $B$ , so [A1] makes the product transition smooth, and disjoint overlaps are covered by [F6]. Hence any two members are compatible, and [F7] makes $A \times B$ a smooth atlas.

givenF6F7A1

2.1

The members of $A \times B$ are charts on $M \times N$ by step 1.1, and their domains $V \times W$ cover $M \times N$ because the domains of $A$ cover $M$ and those of $B$ cover $N$ by [F7].

givenF7step 1.1

3.1

If $A^{'}$ , $B^{'}$ are other presentations of the same two structures, then $A \cup A^{'}$ and $B \cup B^{'}$ are smooth atlases by [L1], and the cross transitions of $(A \times B) \cup (A^{'} \times B^{'})$ are products of smooth transitions exactly as in step 1.2, so the union is a smooth atlas. Then [L1] gives $[A \times B] = [A^{'} \times B^{'}]$ , which is the claimed independence.

givenF6L1step 1.2∎

Depends on

Used by

The torus as a product smooth manifold Example
A map into a product is smooth iff its components are smooth Proposition
Restrictions, corestrictions, and products of smooth maps are smooth Proposition

Dependency tree · two levels

50 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

Rob van der Vorst, Introduction to differentiable manifolds, §2 (standard reference, not scraped)
Nigel Hitchin, Differentiable Manifolds, §2.3 (standard reference, not scraped)