TheoremStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck passaudited 2026-09-14

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.

Excision and Mayer–Vietoris with local coefficients

Statement

Let $L$ be one local system on $X$ .

If $Z \subseteq A \subseteq X$ and $\overline{Z} \subseteq {int}_{X} (A)$ , inclusion induces excision isomorphisms in both local homology and local cohomology between $(X ∖ Z, A ∖ Z)$ and $(X, A)$ , using the restrictions of $L$ .
For an open cover $X = U \cup V$ , there are natural exact sequences $\dots \to H_{n} (U \cap V; L) \to H_{n} (U; L) \oplus H_{n} (V; L) \to H_{n} (X; L) \to \dots$ and $\dots \to H^{n} (X; L) \to H^{n} (U; L) \oplus H^{n} (V; L) \to H^{n} (U \cap V; L) \to \dots,$ where all systems are restrictions and the middle difference map in cohomology is $u ∣_{U \cap V} - v ∣_{U \cap V}$ .

The same conclusions hold for the standard excisive-cover condition after replacing the cover by interiors. A local system given only on a subspace is not silently assumed to extend to $X$ .

Facts & Assumptions

Given: The subspaces or ordered open cover in the relevant clause, and one ambient local system $L$ on $X$ .

[F1]

Homology and cohomology with local coefficients gives intrinsic simplex-wise chain and cochain complexes.

[F2]

A short exact sequence of chain complexes in an abelian category induces its long exact homology sequence (The long exact sequence in homology).

[F3]

A short exact sequence of cochain complexes in an abelian category induces its long exact cohomology sequence (The long exact sequence in cohomology).

[F4]

Excision for singular homology, Excision for singular cohomology, Mayer–Vietoris sequence in singular homology, and Mayer vietoris sequence in singular cohomology supply the ordinary small-chain patterns and sign conventions.

Proof

technique · direct

1.1

Define local barycentric subdivision $S$ on a simplex $σ$ by transporting its first-vertex coefficient along the affine segment in $Δ^{n}$ to each subdivided first vertex. Define the standard barycentric prism $T$ with the same transports. All face cancellations are literal except for routes across an affine triangle; those give the same local-system map because they are endpoint-fixed homotopic inside $Δ^{n}$ . Thus $S$ is a chain map and $\partial T + T \partial = 1 - S$ . Both operators preserve the image of each simplex, and $T$ preserves every small-chain subcomplex.

For a cover $U$ whose interiors cover $X$ , let $C_{*}^{U}$ be generated by simplices contained in one member. Set $D_{m} = \sum_{0 \leq i < m} T S^{i}$ . For each singular simplex $σ$ , choose the least integer $m (σ)$ for which $S^{m (σ)} σ$ is $U$ -small; existence follows from the Lebesgue-number argument on its compact domain. Put $D σ = D_{m (σ)} σ$ and

$ρ σ = S^{m (σ)} σ + D_{m (σ)} \partial σ - D \partial σ .$

Every face $τ$ of $σ$ has $m (τ) \leq m (σ)$ . Hence the difference $D_{m (σ)} \partial σ - D \partial σ$ consists only of terms $T S^{i} τ$ with $i \geq m (τ)$ and is small. The identity $\partial D_{m} + D_{m} \partial = 1 - S^{m}$ now gives $\partial D + D \partial = 1 - ι ρ$ , so $ρ$ is a chain map to $C_{*}^{U}$ ; for a small simplex $m = 0$ , whence $ρ ι = 1$ . This is a genuine chain-homotopy inverse, with no uniform subdivision power and no selection beyond least integers. The entire formula commutes with local coefficient transport because each affine path lies in its original simplex. Precomposition with $ρ, D$ proves the dual cochain homotopy equivalence for any coefficient fibers. This is Hatcher's small-chain construction with the local transports just checked. [F1, F4]

2.1

Put $B = X ∖ Z$ . Since $\overline{Z} \subseteq int A$ , the interiors of $A$ and $B$ cover $X$ . Apply Step 1.1 to the small complex generated by simplices in $A$ or $B$ . Its operators preserve $C_{*} (A; L)$ because every term stays in the image of its original simplex, so they descend to the quotient by $C_{*} (A; L)$ . The quotient of the small complex is canonically $C_{*} (B; L) / C_{*} (A \cap B; L)$ : its remaining basis consists exactly of simplices in $B$ but not $A$ . Thus inclusion $(B, A \cap B) \to (X, A)$ is a chain-homotopy equivalence on relative local chains. Dualizing that actual equivalence gives the restriction equivalence on relative local cochains. Taking (co)homology proves both excision isomorphisms with the restricted ambient system.

F1F4step 1.1

2.2

Let $C_{*}^{U, V} (X; L)$ be the local subcomplex generated by simplices lying in $U$ or $V$ . There is a degreewise exact sequence $0 \to C_{*} (U \cap V; L) \overset{c \mapsto (c, - c)}{\to} C_{*} (U; L) \oplus C_{*} (V; L) \overset{(a, b) \mapsto a + b}{\to} C_{*}^{U, V} (X; L) \to 0$ . Step 1.1 makes the last complex chain-homotopy equivalent to the full complex. The long exact sequence of [F2] gives the homology Mayer–Vietoris sequence with the signs displayed in [F4].

F1F2F4step 1.1

2.3

Dually, let $C_{U, V}^{q} (X; L)$ be the product of the first-vertex fibers over singular $q$ -simplices whose images lie in $U$ or in $V$ , with the intrinsic coboundary from [F1]. Compatible restrictions give $0 \to C_{U, V}^{*} (X; L) \to C^{*} (U; L) \oplus C^{*} (V; L) \overset{(u, v) \mapsto u - v}{\to} C^{*} (U \cap V; L) \to 0$ . Surjectivity of the last map follows by extending a simplex function on $U \cap V$ by zero on simplices of $U$ not contained in the intersection. The small-cochain complex computes full cohomology by step 1.1, and [F3] gives the cohomology sequence with the difference convention from [F4].

F1F3F4step 1.1

3.1

Subdivision, restriction, addition, difference, and the connector representative formulas commute with maps carrying the ordered cover into another ordered cover and with correctly directed coefficient morphisms. This proves naturality. Replacing an excisive cover by interiors gives the stated extension. Empty intersections, $U = X$ , zero systems, degree zero, disconnected spaces, and degenerate simplices are covered by the same exact sequences. All subdivisions of a given finite chain are finite and explicitly defined, so no AC is used.

step 1.1step 2.1step 2.2step 2.3∎

Depends on

Used by

Dependency tree · two levels

29 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

Hatcher, Algebraic Topology, Proposition 2.21 and §3.H, pp.123–124 and 332–334 (standard reference, not scraped)
Davis and Kirk, Lecture Notes in Algebraic Topology, Chapter 5 §4, pp.107–109 (standard reference, not scraped)