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.
Smooth singular mayer vietoris sequence
Statement
For an ordered two-open cover of a smooth manifold, possibly with boundary, smooth singular cohomology has a natural Mayer–Vietoris sequence The maps before the connector are restriction and difference; the connector is positive lift-differential, with the small-complex cohomology identified by the actual inclusion. Naturality holds for smooth maps preserving the ordered cover. Negative groups vanish and the sequence begins with .
Facts & Assumptions
Given: The ordered open cover. Write , and for its cover-small subcomplex.
The ordinary two-open dual sequence is proved by gluing functions on the simplex bases and zero extension (Short exact two open singular cochain mayer vietoris sequence).
Smooth chains form a subcomplex and smooth cochains are its real dual (Smooth singular chain and cochain complexes).
Subdivision and its homotopy preserve smooth chains and do not enlarge simplex images (Barycentric subdivision and prism preserve smooth singular chains).
The ordinary small-chain inverse is constructed from least subdivision depths and the identity (The cover-small inclusion is a chain homotopy equivalence).
Every finite chain becomes cover-small after sufficiently many subdivisions (Finite chains eventually become cover-small).
Short exact cochain sequences give long exact cohomology sequences (The long exact sequence in cohomology).
Proof
For a smooth simplex , let be the least nonnegative integer such that is small; [F5] supplies existence. Set on vertices and recursively . Each maximum is finite, faces have smaller dimension, and [F3] ensures all face and subdivision chains remain smooth. A small simplex has , by induction on its faces.
Define , so by telescoping [F4]. Set and , extending on the supplied smooth basis. Then . On a simplex, . For each face , its correction is the signed sum ; every term is smooth and small because is small and preserve that property. Thus lands in .
With and , the identities are and , since vanishes on small simplices and their faces. Dualizing these actual equations gives : the cochain homotopy is precomposition with . This proves the needed equivalence within smooth chains, independently of any smooth/continuous comparison theorem.
The smooth bases for and , viewed in , have intersection precisely the smooth overlap basis. To check the corestriction clause, restrict any extension of an overlap-valued simplex to the open inverse image of , which contains its simplex. Thus the argument [F1] applies to these bases: restrictions inject the small dual into the pair of cochains, agreeing pairs glue uniquely by priority-U values, and maps to under difference. Signed face restrictions make both arrows cochain maps. Apply [F6] to this explicitly exact smooth row and identify its first cohomology through from step 3.1. This proves the sequence and initial injection.
For clarity, lift an overlap cocycle to a pair ; its differential equals for a unique small cocycle . The connector is . Changing the lift by changes by ; changing by and adding the differential of a lift of leaves unchanged. For a smooth ordered-cover map, postcomposition preserves each small smooth basis and commutes with inclusions and signed arrows. The image of is a lift of the image of , proving connector naturality, and the natural inclusion square transports it through .
Negative degrees have zero terms; at degree zero all vertices are small, , and no negative primitive exists. Empty opens and overlap give zero terms; when the row is diagonal then difference, with connector zero by the lift . This includes one-point and empty manifolds. Degenerate simplices have the same face recursion; no quotient discards them. Least integers, finite maxima and prescribed zero values give all constructions without AC, including boundary targets.
Depends on
- Short exact two open singular cochain mayer vietoris sequence
- Smooth singular chain and cochain complexes
- Barycentric subdivision and prism preserve smooth singular chains
- The cover-small inclusion is a chain homotopy equivalence
- The long exact sequence in cohomology
- Finite chains eventually become cover-small
Used by
Dependency tree · two levels
25 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
- DG-16 design; Hatcher/Park control (standard reference, not scraped)