Small chains and excision
Hatcher §2.1 (pages 119–124), Proposition 2.21 and Theorem 2.20. The approved scope is decomposed into ten formalizable leaves. This page remains a non-dispatchable container; the linked leaves, rather than this overview, are the proof units.
All ten leaves are complete, including the binary-cover and deleted-subset
IsIso endpoints on relative homology.
The target first proves that singular chains subordinate to a family of subsets whose interiors cover a space include into all singular chains by a chain-homotopy equivalence. It then derives excision for a binary cover and the equivalent deleted-subset formulation using the canonical maps of pairs.
Affine geometry
For an affine map from a real standard simplex into a convex space, define the barycentric subsimplex indexed by a permutation of the vertices and its iterates. The vertices are the images of barycenters of the nested faces in the corresponding complete flag.
The main theorem, intended as
Hatcher.Excision.affineSubdivisionIter_face, says that every iterated
barycentric subdivision of a face is itself a face of an iterated barycentric
subdivision of the original affine simplex. The same review unit supplies the
single-step face identity and the permutation/sign bookkeeping later needed to
prove that subdivision commutes with the chain boundary.
These definitions are local compatibility scaffolding for Hatcher's geometric construction; the geometric affine-subdivision API is absent from the pinned Mathlib version.
Sources
For an affine n-simplex s in a real normed space and any choice σ of
k successive barycentric subsimplices, the main theorem, intended as
Hatcher.Excision.affineSubdivisionIter_diameter_le, gives the bound
diam (affineSubdivisionIter s σ) ≤ (n / (n + 1))^k · diam s.
In particular, when n > 0, repeated subdivision makes every resulting
simplex arbitrarily small. The proof packages Hatcher's estimate from the
barycenter of a simplex to its vertices and iterates it uniformly over all
permutation-indexed subsimplices.
Sources
Subdivision and small chains
For a convex real space Y, universes w, v, and u, an ambient category
C : Type u with [Category.{v} C], [Preadditive C],
[HasCoproducts.{w} C], and a coefficient object R : C, construct the
barycentric subdivision endomorphism of the affine-simplex chain complex.
Construct its cone homotopy from the identity, naturally with respect to
affine maps.
The main artifact, intended as
Hatcher.Excision.affineChainHomotopyIdSubdivision, is this chain homotopy.
The subdivision map, cone operator, signed sum over permutation-indexed
subsimplices, and corresponding iterated formula are supporting declarations
in the same review unit. This is the categorical version of Hatcher's augmented
linear-chain construction on pages 121–122.
Sources
For X : TopCat.{w}, {C : Type u}, [Category.{v} C], [Preadditive C],
[HasCoproducts.{w} C], and R : C, transfer affine barycentric subdivision
of the standard simplex along every singular simplex. This gives a natural
chain endomorphism of X's singular chain complex, together with all finite
iterates.
The main artifact, intended as
Hatcher.Excision.singularChainHomotopyIdSubdivisionIter, is a chain homotopy
from the identity to every iterated subdivision map. Supporting declarations
give the one-step homotopy, naturality under continuous maps, the signed
subsimplex formula, face compatibility, and the fact that every subdivided
simplex has image contained in the original simplex's image. These support
properties are what later make subdivision and its homotopies preserve
subspaces.
Sources
Dependencies
Let U : ι → Set X be a family whose interiors cover X. Define the
simplicial subcomplex of the singular set generated by simplices whose images
lie in one U i, and say that a simplex is small after k subdivisions when
every permutation-indexed subsimplex of that iterate belongs to this
subcomplex.
The main theorem, intended as
Hatcher.Excision.exists_iteratedSubdivision_mem_smallSubcomplex, says that
every singular simplex is small after some finite number of subdivisions.
Apply the pinned compact-space Lebesgue-number lemma to the inverse-image cover
of the standard simplex and combine it with the diameter-decay estimate. The
subdivision depth is allowed to depend on the simplex.
Sources
Dependencies
Hatcher, Proposition 2.21 (pages 119–124). For a family of subsets whose
interiors cover X, the canonical inclusion from the subordinate singular
chain complex into the full singular chain complex is a chain-homotopy
equivalence. State the categorical form for X : TopCat.{w}, {C : Type u},
[Category.{v} C] [Preadditive C] [HasCoproducts.{w} C], and R : C;
Hatcher's integral version is the specialization to AddCommGrpCat.of ℤ.
The main artifact, intended as
Hatcher.Excision.smallChainInclusionHomotopyEquiv, must have that canonical
inclusion as its forward map. Choose the least subdivision depth m(σ) for
each simplex, prove that faces require no greater depth, form Hatcher's
variable-depth homotopy, and define the corrected retraction
ρ = 1 - ∂D - D∂. Verify that ρ lands in the subordinate subcomplex,
that ρ ∘ ι = id, and that ι ∘ ρ is homotopic to the identity. A
homology-isomorphism statement may
be recorded as a corollary, but it is not a substitute for the chain-level
main result.
Sources
Dependencies
Relative excision
Let f : P ⟶ Q be a morphism of simplicial-set pairs whose ambient component
is monic, and let Z be a subcomplex of Q.right. Work with
{C : Type u}, [Category.{v} C], [Preadditive C],
[HasCoproducts.{w} C], and R : C.
The main theorem, intended as
Hatcher.Excision.relativeChainMap_homotopyEquivalence_iff, assumes
Z = range(Q.hom) ⊔ range(f.right)
and
range(f.left ≫ Q.hom) = range(Q.hom) ⊓ range(f.right).
It says that the relative chain map induced by f is a chain-homotopy
equivalence exactly when the chain map induced by Z.ι is one. Specializing
to two subcomplexes A and B of a simplicial set X gives the canonical map
C_*(B;R) / C_*(A ∩ B;R) → C_*(X;R) / C_*(A;R)
and reduces its homotopy-equivalence property to that of the inclusion
A ⊔ B → X.
The degreewise split short complex behind this theorem is the categorical form of Hatcher's chain isomorphism
C_*(B;R) / C_*(A ∩ B;R) ≅ C_*^{A+B}(X;R) / C_*(A;R).
Sources
Dependencies
Let A and B be subsets of X with
interior A ∪ interior B = Set.univ. This review unit exposes the supporting
public predicate Hatcher.Excision.CoverCondition A B and, for
h : CoverCondition A B, the canonical map
Hatcher.Excision.coverPairHom h of topological pairs
(B, A ∩ B) → (X, A).
For {C : Type u}, [Category.{v} C], [Preadditive C],
[HasCoproducts.{w} C], and R : C, the main theorem, intended as
Hatcher.Excision.coverChainMap_homotopyEquivalence, says that the image of
coverPairHom h under Hatcher.Relative.chainComplexFunctor R is a
chain-homotopy equivalence. These two supporting declarations are why the
homology endpoint has a statement dependency on this review unit.
Use the existing Hatcher.Relative.singularPairFunctor; do not introduce a
second conversion from topological pairs to simplicial-set pairs. The proof
identifies the binary small-simplices subcomplex with the union of the two
subcomplexes, applies Proposition 2.21, and transports the result through the
relative-chain dévissage theorem.
Sources
Hatcher, Theorem 2.20 (pages 119 and 124), binary-cover form. If
interior A ∪ interior B = Set.univ, write
h : Hatcher.Excision.CoverCondition A B for this hypothesis. Then for every
degree n the canonical map
H_n(B, A ∩ B;R) → H_n(X,A;R)
induced by inclusion is an isomorphism. The intended main declaration
Hatcher.Excision.coverHomologyMap_isIso is an IsIso instance for the exact
morphism
(Hatcher.Relative.homologyFunctor R n).map
(Hatcher.Excision.coverPairHom h).
State the result for {C : Type u}, [Category.{v} C], [Preadditive C],
[HasCoproducts.{w} C], [CategoryWithHomology C], and R : C. Hatcher's
integral theorem is its specialization to AddCommGrpCat.of ℤ. Derive the
instance from the chain-level homotopy equivalence using the pinned
HomologicalComplex.homotopyEquivalences_le_quasiIso and
HomotopyEquiv.toHomologyIso machinery; do not replace the canonical map by
an unspecified isomorphism.
Sources
Dependencies
Hatcher, Theorem 2.20 (page 119), deleted-subset form. Let A Z : Set X
and suppose closure Z ⊆ interior A, which in particular implies Z ⊆ A.
For every degree n, the canonical inclusion of pairs induces an isomorphism
H_n(X ∖ Z, A ∖ Z;R) → H_n(X,A;R).
State the result for {C : Type u}, [Category.{v} C], [Preadditive C],
[HasCoproducts.{w} C], [CategoryWithHomology C], and R : C.
Define the proof-independent canonical map
Hatcher.Excision.deletedSubsetPairHom A Z from the pair built from
A ∖ Z ↪ X ∖ Z to TopPair.ofSubset A. The intended main declaration
Hatcher.Excision.deletedSubsetHomologyMap_isIso is an IsIso instance for
the exact morphism
(Hatcher.Relative.homologyFunctor R n).map
(Hatcher.Excision.deletedSubsetPairHom A Z).
Since this canonical morphism is proof-independent, the named instance takes
the hypothesis as [Fact (closure Z ⊆ interior A)]. The companion theorem
Hatcher.Excision.deletedSubsetHomologyMap_isIso_of_closure_subset_interior
accepts the same hypothesis as an ordinary explicit argument.
The proof specializes binary-cover excision to B = Zᶜ. It must record a
definitional equality or named equality between deletedSubsetPairHom A Z
and coverPairHom for the induced cover condition, together with the ambient
identities A ∩ Zᶜ = A ∖ Z and
interior (Zᶜ) = (closure Z)ᶜ; these turn the closure hypothesis into the
required interior-cover condition. The theorem is about subset pairs, not the
stronger arbitrary-embedding criterion found in implementation prior art.
Dependencies
Boundary
This milestone ends at the canonical relative-homology excision isomorphisms. It excludes Proposition 2.22, the good-pair quotient comparison, Theorem 2.13, sphere applications, Mayer–Vietoris, the simplicial–singular comparison, and §2.2.