LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge 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.

Disjoint unions of framed cobordisms

Statement

Assume ${A C}_{ω}$ . Let $M$ be a closed smooth manifold and $k \geq 0$ . Let $(W_{N}, ε_{N}, Ψ_{N})$ and $(W_{L}, ε_{L}, Ψ_{L})$ be framed codimension- $k$ cobordisms in $M \times I$ , from $(N_{0}, φ_{0})$ to $(N_{1}, φ_{1})$ and from $(L_{0}, ψ_{0})$ to $(L_{1}, ψ_{1})$ , respectively. If their images are disjoint, then their union, with the combined framing and collar width $\min (ε_{N}, ε_{L})$ , is a framed cobordism from $(N_{0} ⊔ L_{0}, φ_{0} ⊔ ψ_{0})$ to $(N_{1} ⊔ L_{1}, φ_{1} ⊔ ψ_{1})$ .

Disjoint endpoint sets alone do not assert disjointness of the cobordisms. This lemma does not assert that arbitrary embedded framed cobordism classes in a fixed $M$ form a monoid. For finite disjoint sets of framed points, cardinality modulo two is additive, and, when $M$ is oriented, the sum of framing signs is additive.

Facts & Assumptions

Given: Two framed cobordisms as above with $W_{N} \cap W_{L} = \emptyset$ .

[F1]

A framed cobordism is a compact neat embedded submanifold with literal product ends of width $0 < ε < 1 / 2$ and a normal-quotient framing equal to the specified endpoint framing throughout each collar (Framed cobordism of framed submanifolds, Framings of a normal bundle, Neat submanifolds of a manifold with boundary).

[F2]

The ambient smooth manifold is Hausdorff; compact subsets are closed, and a finite union of compact sets is compact. Embeddedness and smoothness are local properties (Smooth manifolds and their smooth charts, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, Smooth embeddings, In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones).

Proof

technique · direct

1.1F1F2given

Each of $W_{N}, W_{L}$ is closed by compactness and the Hausdorff property. Thus every point of either has an ambient neighbourhood missing the other. On that neighbourhood $W = W_{N} \cup W_{L}$ is exactly the corresponding neat embedded submanifold. Therefore $W$ is a compact neat embedded submanifold, with boundary $(N_{0} ⊔ L_{0}) \times {0} ⊔ (N_{1} ⊔ L_{1}) \times {1}$ . The normal quotient restricts on each open-and-closed piece to its original normal quotient.

2.1F1step 1.1algebra∎

Set $ε = \min (ε_{N}, ε_{L}) \in (0, 1 / 2)$ . The product ends of the two pieces give product ends of $W$ with this width. Their framings paste smoothly on its disjoint open-and-closed pieces and restrict to the combined endpoint framings throughout those collars. Hence $(W, ε, Ψ_{N} ⊔ Ψ_{L})$ is the asserted framed cobordism. For disjoint finite sets, summing one per point, or the orientation sign per point, splits into the sums over the two sets; reducing cardinalities modulo two gives parity additivity. This includes either set being empty and rank-zero cobordisms.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

37 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

Daniel S. Freed, Bordism: Old and New (lecture notes, UT Austin, Fall 2012) (standard reference, not scraped)
John Milnor, Topology from the Differentiable Viewpoint (standard reference, not scraped)