Local homology and invariance of dimension
This dependency-ordered branch contains the local-homology end of Hatcher §2.1, printed page 126. It is placed with computations and applications because its proof consumes the completed punctured-Euclidean retraction and sphere-homology calculation, while remaining part of the selected §2.1 source unit.
All four formalization leaves are complete.
For a space X and x : X, define the punctured topological pair
Hatcher.Relative.puncturedPair X x := (X, X \ {x}). If U : Set X is an
open neighborhood of x, and {x} is closed in X, define the canonical
pair morphism from the punctured pair in U to the punctured pair in X.
The main result
Hatcher.Relative.localHomologyOpenNeighborhoodMap_isIso states that this
canonical map induces an isomorphism on relative homology in every degree and
for every supported coefficient object under the explicit hypothesis
IsClosed ({x} : Set X) (or a T1Space X specialization). Also package the
pair isomorphism and induced homology isomorphism associated to a homeomorphism
carrying x to y.
This is Hatcher's local-homology observation following Theorem 2.26. Prove the open-neighborhood comparison with the completed excision API; do not replace the named inclusion-induced map by an arbitrary isomorphism.
Sources
Dependencies
Let P : TopPair have nonempty subspace and contractible ambient space. For
adjacent degrees i + 1 = n, construct the canonical isomorphism
H_n(P.fst, P.snd;R) ≅ H̃_i(P.snd;R)
whose forward map is the connecting morphism in the reduced long exact
sequence of the pair. Prove separately that H_0(P.fst,P.snd;R) is a zero
object. The main result is
Hatcher.Relative.contractibleAmbientRelativeHomologyIso; the degree-zero
statement is part of the same public review unit.
This packages the exact-sequence calculation used by Hatcher for punctured Euclidean space. It must retain the canonical connecting map rather than choosing an unrelated isomorphism.
Sources
Let d : ℕ, let
E := EuclideanSpace ℝ (Fin (d + 1)), and let x : E. For every coefficient
object R in the supported abelian target category, prove
Nonempty (H_(d+1)(E, E \ {x};R) ≅ R)
and prove that H_i(E,E \ {x};R) is a zero object whenever i ≠ d + 1.
The main result is Hatcher.Euclidean.localHomology with an integral
specialization matching Hatcher's displayed groups.
Translate x to the origin, use the radial strong deformation retraction of
punctured Euclidean space onto S^d, and combine the sphere calculation with
the contractible-ambient relative comparison. The theorem is intentionally
indexed by d + 1; dimension zero belongs to the final point-set split and is
not represented by a nonexistent negative sphere.
Sources
Dependencies
Hatcher, Theorem 2.26 (printed page 126). Let
U ⊆ EuclideanSpace ℝ (Fin m) and
V ⊆ EuclideanSpace ℝ (Fin n) be nonempty open sets. If their subtype
spaces are homeomorphic, then m = n.
The intended main result is
Hatcher.Euclidean.invarianceOfDimension_open. For positive dimensions,
choose a point of U, compare the local relative-homology groups through the
homeomorphism and the open-neighborhood theorem, and use the punctured
Euclidean calculation with integral coefficients to detect the unique nonzero
degree. The contradiction uses the nonzero object AddCommGrpCat.of ℤ; it is
not stated for an arbitrary coefficient object, which could be zero.
Handle dimension zero separately: a nonempty open subset of
zero-dimensional Euclidean space is subsingleton, while a nonempty open subset
in positive dimension contains two distinct points. Do not use m - 1, a
fictitious negative sphere, or the stronger invariance-of-domain theorem.
Sources
Prior art
Open Mathlib PR #36770 uses Brouwer's fixed-point theorem to prove invariance of domain and a conditional dimension theorem for whole finite-dimensional spaces. It is not present at the project pin and does not state this open-subset homological theorem.