Local homology at a point with a Euclidean chart #
Let M be a T₁ space and x : M a point in the source of an open partial homeomorphism
φ : M → E to a real normed space, such as a chart of a topological manifold modelled on E.
The local homology of M at x is the relative singular homology Hₖ(M, M ∖ {x}). This
file computes it: it is the homology of (E, E ∖ {φ x}), so it vanishes in degree zero when
E ≠ 0, and in degree k + 1 it is the degree-k reduced homology of the unit sphere S of E.
When E has dimension n, Hₖ(M, M ∖ {x}) therefore vanishes for k ≠ n, and it is one copy of
the coefficients in degree n.
Local homology is the input to local orientations of manifolds: a local orientation of an
n-manifold at x is a generator of Hₙ(M, M ∖ {x}; ℤ), and the orientation local system and
fundamental classes are assembled from these groups.
The computation has three steps.
- Excision. For an open set
Ucontaining a closed setK, the inclusion(U, U ∖ K) ⟶ (X, X ∖ K)induces isomorphisms on relative homology (TopPair.isIso_singularHomologyMap_excisionMap_of_isClosed_subset), because the interiors ofUandX ∖ KcoverX. Applied to the source ofφinMand to its target inE, and combined with the homeomorphism of source and target, this identifiesHₖ(M, M ∖ {x})withHₖ(E, E ∖ {φ x})(TauCeti.singularHomologyComplSingletonIsoOfChart). - The connecting morphism. Since
Eis contractible, the reduced connecting morphism fromHₖ₊₁(E, E ∖ {y})to the degree-kreduced homology ofE ∖ {y}is an isomorphism. - Radial retraction.
E ∖ {y}is homotopy equivalent to the unit sphere ofE(TauCeti.complSingletonHomotopyEquivSphere), by radial projection aboutyfollowed by translation.
Main definitions and results #
TauCeti.singularHomologyComplSingletonIsoOfChart:Hₖ(M, M ∖ {x}) ≅ Hₖ(E, E ∖ {φ x}).TauCeti.singularHomologyComplSingletonIso:Hₖ₊₁(M, M ∖ {x})is isomorphic to the degree-kreduced homology ofS.TauCeti.isZero_singularHomology_complSingleton_zero:H₀(M, M ∖ {x}) = 0whenE ≠ 0.TauCeti.isZero_singularHomology_complSingleton_of_ne:Hₖ(M, M ∖ {x}) = 0fork ≠ dim E, for finite-dimensionalE.TauCeti.singularHomologyComplSingletonIsoOfFinrankEq:Hₙ₊₁(M, M ∖ {x}) ≅ Rwhendim E = n + 1.TauCeti.singularHomologyComplSingletonIsoOfFinrankEqZero:H₀(M, M ∖ {x}) ≅ Rwhendim E = 0, generated by the class of the point.TauCeti.singularHomologyComplSingletonFinrankIso:H_d(M, M ∖ {x}) ≅ Rford = dim E, uniformly ind.
Local homology along star-convex sets #
Local homology is locally constant: if K ⊆ φ.target is closed, bounded and star-convex about
φ x, and φ.symm '' K is closed in M (as when K is compact and M is Hausdorff), then the
inclusion (M, M ∖ φ.symm '' K) ⟶ (M, M ∖ {x}) induces isomorphisms on relative homology. For
convex K this holds at every point of φ.symm '' K, so the local homology groups at nearby
points are identified through Hₖ(M, M ∖ φ.symm '' K); this is how local orientations at nearby
points are compared. In E, both E ∖ K and E ∖ {φ x}
deformation retract onto a large sphere about φ x (StarConvex.complSphereHomotopyEquiv), and
the five lemma TopPair.isIso_singularHomologyMap_of_isIso compares the two pairs; excision
(TopPair.isIso_singularHomologyMap_ofSubsetMap_compl_iff) transports the comparison along φ.
TauCeti.isIso_singularHomologyMap_compl_of_starConvex:(E, E ∖ K) ⟶ (E, E ∖ {y})induces isomorphisms for boundedKstar-convex abouty ∈ K.TauCeti.isIso_singularHomologyMap_compl_of_chart:(M, M ∖ φ.symm '' K) ⟶ (M, M ∖ {x})induces isomorphisms for suchKstar-convex aboutφ x ∈ K.TauCeti.isZero_singularHomology_compl_symm_image_of_ne,TauCeti.singularHomologyComplSymmImageIsoOfFinrankEqandTauCeti.singularHomologyComplSymmImageIsoOfFinrankEqZero: henceHₖ(M, M ∖ φ.symm '' K)vanishes fork ≠ dim E, and is one copy of the coefficients whenk = dim E.
References #
- A. Hatcher, Algebraic Topology, Section 3.3, the local homology groups
Hₙ(M, M ∖ {x})and local orientations, where the comparison throughHₙ(M, M ∖ B)for a ballBdefines the topology of the orientation cover, and Section 2.1, Theorem 2.20 (excision).
The local homology of M at a point x in the source of an open partial homeomorphism
φ : M → E is that of E at φ x: excision onto the source of φ, the homeomorphism of the
source with the target, and excision onto the target give Hₖ(M, M ∖ {x}) ≅ Hₖ(E, E ∖ {φ x})
(TauCeti.singularHomologyMap_excisionMap_comp_singularHomologyComplSingletonIsoOfChart_hom).
Instances For
The isomorphism TauCeti.singularHomologyComplSingletonIsoOfChart commutes with the
excision maps from the source and target of φ and the homeomorphism between them.
The isomorphism TauCeti.singularHomologyComplSingletonIsoOfChart commutes with the
excision maps from the source and target of φ and the homeomorphism between them.
The inverse of TauCeti.singularHomologyComplSingletonIsoOfChart commutes with the excision
maps from the target and source of φ and the inverse homeomorphism between them.
The inverse of TauCeti.singularHomologyComplSingletonIsoOfChart commutes with the excision
maps from the target and source of φ and the inverse homeomorphism between them.
The local homology isomorphism of the identity chart of E is the identity.
Local homology at a point with a Euclidean chart. For x in the source of an open
partial homeomorphism φ : M → E, the local homology Hₖ₊₁(M, M ∖ {x}) is the degree-k
reduced homology of the unit sphere of E. It is
TauCeti.singularHomologyComplSingletonIsoOfChart, followed by the reduced connecting morphism
of the pair (E, E ∖ {φ x}), an isomorphism since E is contractible, and by
TauCeti.complSingletonHomotopyEquivSphere.
Instances For
TauCeti.singularHomologyComplSingletonIso is the chart isomorphism followed by the reduced
connecting morphism of (E, E ∖ {φ x}) and the map induced by
TauCeti.complSingletonHomotopyEquivSphere.
The inverse of TauCeti.singularHomologyComplSingletonIso is the map induced by the homotopy
inverse of TauCeti.complSingletonHomotopyEquivSphere, followed by the inverse of the reduced
connecting morphism of (E, E ∖ {φ x}) and the inverse of the chart isomorphism.
Local homology vanishes in degree zero at a point with a chart to a nonzero real normed
space: E is path connected and E ∖ {φ x} is nonempty.
Local homology vanishes outside the dimension: at a point with a chart to a real normed
space E of finite dimension n, the local homology Hₖ(M, M ∖ {x}) vanishes for k ≠ n.
Local homology of a zero-dimensional chart: at a point with a chart to a zero-dimensional
real normed space, the local homology H₀(M, M ∖ {x}) is one copy of the coefficients. Since E
is a point, E ∖ {φ x} is empty, so it is TauCeti.singularHomologyComplSingletonIsoOfChart
followed by the inverse of the quotient map from H₀(E) and by the augmentation of H₀(E).
Instances For
TauCeti.singularHomologyComplSingletonIsoOfFinrankEqZero sends the image of a class of
H₀(E) under the quotient map and the inverse of the chart isomorphism to its augmentation.
TauCeti.singularHomologyComplSingletonIsoOfFinrankEqZero sends the image of a class of
H₀(E) under the quotient map and the inverse of the chart isomorphism to its augmentation.
The generator of the local homology H₀(M, M ∖ {x}) of a zero-dimensional chart is the class
of the point φ x of E, carried by the quotient map and the inverse of the chart isomorphism.
Local homology in the top degree: at a point with a chart to a real normed space of
dimension n + 1, the local homology Hₙ₊₁(M, M ∖ {x}) is one copy of the coefficients. It is
TauCeti.singularHomologyComplSingletonIso followed by the map on reduced homology induced by the
homeomorphism of the unit sphere of E with TopCat.sphere n
(TauCeti.sphereHomeomorphOfFinrankEq and TauCeti.diskBoundaryHomeomorph), and by
TauCeti.reducedSingularHomologyTopCatSphereIso.
Instances For
TauCeti.singularHomologyComplSingletonIsoOfFinrankEq is
TauCeti.singularHomologyComplSingletonIso, followed by the map on reduced homology induced by the
homeomorphism of the unit sphere of E with TopCat.sphere n, and by
TauCeti.reducedSingularHomologyTopCatSphereIso.
The inverse of TauCeti.singularHomologyComplSingletonIsoOfFinrankEq is the inverse of
TauCeti.reducedSingularHomologyTopCatSphereIso, followed by the map on reduced homology induced
by the homeomorphism of TopCat.sphere n with the unit sphere of E, and by the inverse of
TauCeti.singularHomologyComplSingletonIso.
Local homology in the top degree, uniformly in the dimension: at a point with a chart to
a finite-dimensional real normed space E, the local homology H_d(M, M ∖ {x}) in degree
d = finrank ℝ E is one copy of the coefficients. It is
TauCeti.singularHomologyComplSingletonIsoOfFinrankEqZero when d = 0 and
TauCeti.singularHomologyComplSingletonIsoOfFinrankEq otherwise.
Instances For
Local homology is constant along star-convex sets #
Removing a bounded star-convex set does not change homology. If K contains y, is
star-convex about y and is bounded, then the inclusion (E, E ∖ K) ⟶ (E, E ∖ {y}) induces
isomorphisms on relative singular homology. Both E ∖ K and E ∖ {y} deformation retract onto a
sphere about y containing K in its interior (StarConvex.complSphereHomotopyEquiv), so the
inclusion induces isomorphisms on the homology of the subspaces, and the five lemma
TopPair.isIso_singularHomologyMap_of_isIso applies.
The point x lies in φ.symm '' K when φ x ∈ K, so the identity of M maps
M ∖ φ.symm '' K into M ∖ {x}.
Local homology is constant along a closed bounded star-convex set in a chart. Let
φ : M → E be an open partial homeomorphism from a topological space to a real normed space, such
as a chart of a topological manifold, and let K ⊆ φ.target be closed, bounded and star-convex
about φ x, where x ∈ φ.source and φ x ∈ K, such that φ.symm '' K is closed in M. Then the
inclusion (M, M ∖ φ.symm '' K) ⟶ (M, M ∖ {x}) induces isomorphisms on relative singular
homology. By excision onto the source and the target of φ, this reduces to the inclusion
(E, E ∖ K) ⟶ (E, E ∖ {φ x}) (TauCeti.isIso_singularHomologyMap_compl_of_starConvex).
When K is compact, it is closed and bounded, and if M is moreover Hausdorff then its image
φ.symm '' K is compact and hence closed; star-convexity and K ⊆ φ.target remain separate
hypotheses. For instance, all hypotheses hold for a closed ball about φ x contained in the
target of a chart of a finite-dimensional Hausdorff manifold.
Local homology along a closed bounded star-convex set vanishes outside the dimension:
for K as in TauCeti.isIso_singularHomologyMap_compl_of_chart and E of finite dimension n,
the relative homology Hₖ(M, M ∖ φ.symm '' K) vanishes for k ≠ n.
Local homology along a closed bounded star-convex set in the top degree: for K as in
TauCeti.isIso_singularHomologyMap_compl_of_chart and E of dimension n + 1, the relative
homology Hₙ₊₁(M, M ∖ φ.symm '' K) is one copy of the coefficients. It is the map to the local
homology Hₙ₊₁(M, M ∖ {x}) induced by the inclusion, followed by
TauCeti.singularHomologyComplSingletonIsoOfFinrankEq.
Instances For
TauCeti.singularHomologyComplSymmImageIsoOfFinrankEq is the map induced by the inclusion
(M, M ∖ φ.symm '' K) ⟶ (M, M ∖ {x}), followed by
TauCeti.singularHomologyComplSingletonIsoOfFinrankEq.
The inverse of TauCeti.singularHomologyComplSymmImageIsoOfFinrankEq is the inverse of
TauCeti.singularHomologyComplSingletonIsoOfFinrankEq, followed by the inverse of the map induced
by the inclusion (M, M ∖ φ.symm '' K) ⟶ (M, M ∖ {x}).
Local homology along a closed bounded star-convex set in degree zero: for K as in
TauCeti.isIso_singularHomologyMap_compl_of_chart and E of dimension 0, the relative homology
H₀(M, M ∖ φ.symm '' K) is one copy of the coefficients. It is the map to the local homology
H₀(M, M ∖ {x}) induced by the inclusion, followed by
TauCeti.singularHomologyComplSingletonIsoOfFinrankEqZero.
Instances For
TauCeti.singularHomologyComplSymmImageIsoOfFinrankEqZero is the map induced by the inclusion
(M, M ∖ φ.symm '' K) ⟶ (M, M ∖ {x}), followed by
TauCeti.singularHomologyComplSingletonIsoOfFinrankEqZero.
The inverse of TauCeti.singularHomologyComplSymmImageIsoOfFinrankEqZero is the inverse of
TauCeti.singularHomologyComplSingletonIsoOfFinrankEqZero, followed by the inverse of the map
induced by the inclusion (M, M ∖ φ.symm '' K) ⟶ (M, M ∖ {x}).