Mayer–Vietoris sequences
Hatcher §2.2, printed pages 149–150. This milestone constructs the ordinary and reduced Mayer–Vietoris sequences for two subspaces whose interiors cover the ambient space. It uses the already formalized small-chain equivalence from Proposition 2.21, so the chain complex of chains supported in one cover member can replace the full singular chain complex.
The source fixes the signs: the intersection map is x ↦ (x,-x), the union
map is (x,y) ↦ x+y, and the connecting map sends a small cycle represented
as x+y to the class of ∂x=-∂y. The reduced version comes from augmenting
the same short exact sequence.
Ordinary sequence
For subsets A B : Set X and coefficients R, let
C_*^{A+B}(X;R) be the chain complex of the simplicial subcomplex generated
by singular simplices whose images lie in A or in B. Construct the short
complex
C_*(A ∩ B;R) → C_*(A;R) ⊞ C_*(B;R) → C_*^{A+B}(X;R).
The first map is the biproduct lift of the two inclusion-induced chain maps,
with the source convention x ↦ (x,-x). The second is the biproduct descent
of the two canonical maps into the small-cover complex, so it acts as
(x,y) ↦ x+y. Their composite is zero.
The main artifact is
Hatcher.MayerVietoris.chainComplexShortComplex. Supporting declarations
should expose smallCoverChains and the canonical maps from the intersection
to each member and from each member to the small-cover complex. The
construction is defined for arbitrary A and B; the interior-cover
hypothesis is needed only when comparing small-cover homology with the
homology of X.
Sources
For arbitrary subsets A B : Set X, the Mayer–Vietoris chain complex is
short exact:
0 → C_*(A ∩ B;R) → C_*(A;R) ⊞ C_*(B;R)
→ C_*^{A+B}(X;R) → 0.
The main theorem is
Hatcher.MayerVietoris.chainComplexShortComplex_shortExact. Its proof maps
the simplicial-set pushout square for the binary small-cover subcomplex
through the singular-chain functor. Pushout exactness supplies exactness and
epimorphy, while projection onto the A component proves that the signed
intersection map is monic. This categorical argument is the coproduct-basis
splitting in invariant form and preserves the source signs from the preceding
node.
Use a coefficient-general abelian category with the coproducts required by
singular chains. The proof may adapt the Sigma-basis splitting technique
used in relative dévissage, but the theorem must concern the canonical maps
defined in the preceding node.
Sources
Let A B : Set X satisfy Hatcher.Excision.CoverCondition A B. For every
pair of adjacent degrees m + 1 = n, the canonical sequence
H_n(A ∩ B;R) → H_n(A;R) ⊞ H_n(B;R) → H_n(X;R)
→ H_m(A ∩ B;R) → H_m(A;R) ⊞ H_m(B;R) → H_m(X;R)
is exact. The first map is (i_A*, -i_B*), the second is the sum of the two
inclusion-induced maps, and the third is the Mayer–Vietoris connecting map.
The degree-zero map H_0(A;R) ⊞ H_0(B;R) → H_0(X;R) is an epimorphism.
The main theorem is Hatcher.MayerVietoris.sequence_exact. Supporting public
declarations are intersectionMap, unionMap, connecting, sequence, and
unionMap_zero_epi. Construct an isomorphism from the generic homology
sequence of the chain short complex to this source-facing sequence. Use the
additivity of the homology functor for the middle term and the homology
isomorphism induced by the small-chain homotopy equivalence for the ambient
term.
Also record Hatcher.MayerVietoris.connecting_eq: if a small representative
of a class is written z = x+y, with x supported in A and y supported
in B, then its image under the connecting map is represented by
∂x=-∂y in A ∩ B. A coefficient-general generalized-element formulation,
parallel to Hatcher.Relative.pairConnecting_eq, is acceptable.
The implementation first identifies the range subcomplexes in the canonical
chain-level short exact sequence with the singular chains of the actual
subspaces. It then transports the generic six-term homology sequence through
the additive homology functor's biproduct comparison and the small-chain
homotopy equivalence. The public maps retain Hatcher's signs. The theorem
connecting_eq uses a generalized element xy of the two-summand chain
object: its hypotheses say that xy represents the small cycle and that its
boundary is the signed image of a cycle in the intersection, which is the
coefficient-general form of ∂x = -∂y.
Sources
Dependencies
Reduced sequence
For any family of subsets, augment the small singular chain complex by
restricting the ordinary singular-chain augmentation. When the interiors of
the family cover X, the canonical inclusion into the augmented singular
chain complex of X is a chain-homotopy equivalence.
The main artifact is
Hatcher.Excision.smallAugmentedChainInclusionHomotopyEquiv. Supporting
declarations should expose smallAugmentedChainComplex and its canonical
inclusion without a cover hypothesis. Under SmallSimplicesCondition, shift
the existing small-chain homotopy equivalence through ChainComplex.augment,
use the identity on the inserted coefficient object, and verify the
augmentation compatibility. The fact that every vertex is small for an
interior cover supplies the degree-zero identity.
This is project bridge infrastructure rather than a separately stated result of Hatcher. It connects the formalized Proposition 2.21 to Hatcher's instruction to augment the Mayer–Vietoris chain sequence.
Sources
Dependencies
For arbitrary subsets A B : Set X, augment the binary-cover chain short
complex. Its successor degrees are the ordinary Mayer–Vietoris chain
sequence, while its inserted coefficient degree is
0 → R → R ⊞ R → R → 0,
with maps (𝟙_R,-𝟙_R) and codiagonal addition. The resulting short complex
of augmented chain complexes is short exact.
The main theorem is
Hatcher.MayerVietoris.augmentedChainComplexShortComplex_shortExact.
The supporting declarations augmentedChainComplexIntersectionMap and
augmentedChainComplexUnionMap have the displayed signed and codiagonal
components in degree zero and reuse the ordinary maps in every successor
degree. They form augmentedChainComplexShortComplex.
The middle complex augments the ordinary biproduct of the two member chain
complexes by their componentwise augmentations. Short exactness is proved
degreewise: the inserted coefficient sequence has the explicit splitting
with retraction biprod.fst and section biprod.inr, while each successor
degree is the corresponding evaluation of the ordinary short exact
Mayer–Vietoris chain complex.
For later passage to reduced homology,
Hatcher.MayerVietoris.augmentedSubspaceChainIso identifies the augmented
singular chains of a subspace with the corresponding supported-chain
complex, naturally for subset inclusions, and
Hatcher.MayerVietoris.augmentedMiddleChainsIso identifies the custom middle
term with the biproduct of the two singly augmented member complexes.
Sources
Let A B : Set X satisfy Hatcher.Excision.CoverCondition A B. For adjacent
degrees m + 1 = n, the sequence
H̃_n(A ∩ B;R) → H̃_n(A;R) ⊞ H̃_n(B;R) → H̃_n(X;R)
→ H̃_m(A ∩ B;R) → H̃_m(A;R) ⊞ H̃_m(B;R) → H̃_m(X;R)
is exact, with the same inclusion maps and signs as the ordinary sequence. The connecting morphism is induced by the augmented chain short complex.
The main theorem is Hatcher.MayerVietoris.reducedSequence_exact.
Supporting declarations should include reducedIntersectionMap,
reducedUnionMap, reducedConnecting, and reducedSequence. Transport the
generic augmented homology sequence using the augmented small-chain
homotopy equivalence and the additive homology functor's biproduct
comparison.
If A ∩ B is nonempty, also define the terminal sequence
H̃_0(A ∩ B;R) → H̃_0(A;R) ⊞ H̃_0(B;R) → H̃_0(X;R) → 0
and prove Hatcher.MayerVietoris.reducedZeroSequence_exact. Package the
adjacent windows and terminal statement as
Hatcher.MayerVietoris.reducedLongExact. The nonemptiness hypothesis is
essential for this source-facing endpoint: without it, augmented degree-zero
homology records the suppressed degree-minus-one term.
Sources
Dependencies
Boundary
This core milestone ends with exact ordinary and reduced binary interior-cover sequences. The separate sphere-homology milestone now covers the conditional neighborhood-retract extension and Example 2.46. The general CW-neighborhood construction, the Klein-bottle and mapping-torus examples, naturality for a new category of cover maps, degree, and cellular homology remain excluded here.