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.

Reversing a cobordism gives symmetry

Statement

If $(W, θ_{0}, θ_{1})$ is a bordism from a closed smooth manifold $M_{0}$ to a closed smooth manifold $M_{1}$ (Unoriented smooth cobordism of closed manifolds), then swapping the two boundary parts and the two collar parametrisations yields a bordism from $M_{1}$ to $M_{0}$ .

In the oriented theory, if $M_{0}$ and $M_{1}$ are oriented and $(W, θ_{0}, θ_{1})$ with an orientation of $W$ is an oriented bordism from $M_{0}$ to $M_{1}$ (Oriented smooth cobordism), then the same manifold with the opposite orientation, again with the two boundary parts and the two collar parametrisations interchanged, is an oriented bordism from $M_{1}$ to $M_{0}$ : the induced boundary orientations match $- M_{1}$ on the incoming face and $M_{0}$ on the outgoing face.

Facts & Assumptions

Given: A bordism $(W, θ_{0}, θ_{1})$ from $M_{0}$ to $M_{1}$ with boundary decomposition $\partial W = (\partial W)_{0} ⊔ (\partial W)_{1}$ and collars $θ_{0} : [0, 1) \times M_{0} \to W$ , $θ_{1} : (- 1, 0] \times M_{1} \to W$ ; in the oriented case, orientations $o_{0}, o_{1}$ and an orientation of $W$ with induced boundary orientations $- o_{0}$ on $(\partial W)_{0}$ and $o_{1}$ on $(\partial W)_{1}$ .

[F1]

A bordism is data $(W, θ_{0}, θ_{1})$ with a decomposition of $\partial W$ into open and closed parts and smooth embeddings $θ_{i}$ onto open collar neighbourhoods with $θ_{i} ({0} \times M_{i}) = (\partial W)_{i}$ (Unoriented smooth cobordism of closed manifolds, Immersions and embeddings for manifolds with boundary).

[F2]

An oriented bordism additionally carries an orientation of $W$ whose induced boundary orientation is $- o_{0}$ on the incoming face and $o_{1}$ on the outgoing face; the opposite orientation $- M$ of an oriented manifold reverses every determinant ray pointwise (Oriented smooth cobordism, Oriented smooth manifolds and oriented charts).

[F3]

The induced boundary orientation is defined by the outward-normal-first rule: an outward vector followed by a positive basis of the boundary is a positive basis of the ambient tangent space; it is independent of the chosen outward vector field (Induced boundary orientation, Boundary orientation is independent of the outward vector field).

[F4]

The reflection $s \mapsto - s$ is a diffeomorphism of $[0, 1)$ onto $(- 1, 0]$ and of $(- 1, 0]$ onto $[0, 1)$ (Diffeomorphisms and local diffeomorphisms of manifolds, Orientation-preserving parametrizations).

Proof

1.1F1F4

(The dual bordism.) Keep the manifold $W$ and swap the roles of the two boundary parts, setting $(\partial W^{'})_{0} : = (\partial W)_{1}$ and $(\partial W^{'})_{1} : = (\partial W)_{0}$ ; these are again open and closed in $\partial W$ and cover it. Define $θ_{0}^{'} : [0, 1) \times M_{1} \to W, θ_{0}^{'} (s, x) : = θ_{1} (- s, x), θ_{1}^{'} : (- 1, 0] \times M_{0} \to W, θ_{1}^{'} (s, x) : = θ_{0} (- s, x) .$ The reflection $s \mapsto - s$ maps $[0, 1)$ onto $(- 1, 0]$ and $(- 1, 0]$ onto $[0, 1)$ by [F4], so the composites are defined; each $θ_{i}^{'}$ is a smooth embedding, being a composite of the smooth embedding $θ_{1 - i}$ with a diffeomorphism of the interval factor, and its image is the same open collar neighbourhood as that of $θ_{1 - i}$ . Moreover $θ_{0}^{'} ({0} \times M_{1}) = θ_{1} ({0} \times M_{1}) = (\partial W)_{1} = (\partial W^{'})_{0}$ and $θ_{1}^{'} ({0} \times M_{0}) = (\partial W)_{0} = (\partial W^{'})_{1}$ . By [F1], $(W, θ_{0}^{'}, θ_{1}^{'})$ is a bordism from $M_{1}$ to $M_{0}$ . No choice is used.

2.1F2F3step 1.1

(The oriented dual.) Suppose now that $M_{0}, M_{1}$ are oriented and $W$ carries an orientation making $(W, θ_{0}, θ_{1})$ an oriented bordism from $M_{0}$ to $M_{1}$ . Keep the swapped data of step 1.1 and give $W$ the opposite orientation. By [F3], the induced boundary orientation of a face is computed from the ambient orientation by the outward-normal-first rule, so reversing the ambient orientation reverses the induced orientation of every boundary face: for a face with induced orientation $μ$ under one orientation of $W$ , the same face has induced orientation $- μ$ under the opposite orientation. Hence the new incoming face $(\partial W^{'})_{0} = (\partial W)_{1}$ carries $- o_{1} = - M_{1}$ and the new outgoing face $(\partial W^{'})_{1} = (\partial W)_{0}$ carries $- (- o_{0}) = o_{0} = M_{0}$ . By [F2], $(W, θ_{0}^{'}, θ_{1}^{'})$ with the opposite orientation is an oriented bordism from $M_{1}$ to $M_{0}$ .

3.1F1F2step 1.1step 2.1∎

(Assembly.) Step 1.1 gives symmetry of the unoriented cobordism relation; step 2.1 gives symmetry of the oriented relation with the reversed orientation on the dual bordism and the required boundary signs $- M_{1}$ incoming and $M_{0}$ outgoing. The constructions are explicit and use no choice principle.

Depends on

Used by

Smooth cobordism is an equivalence relation Theorem

Dependency tree · two levels

24 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 and James Stasheff, Characteristic Classes (original pagination) (standard reference, not scraped)