Local degree and the sum over a finite fiber
Hatcher §2.2, printed pages 135–136. This milestone orients the relative homology at a point of a positive-dimensional sphere, defines local degree at an isolated preimage, and proves Proposition 2.30: global degree is the sum of the local degrees over a finite fiber.
The proof keeps Hatcher's actual maps visible. A reusable sigma-pair API gives the direct sum of the local relative groups, disjoint open neighborhoods give the finite-puncture excision comparison, and naturality sends the oriented sphere class to the sum of its local classes.
Twelve of the twenty formalization leaves below are formalized locally. Eight remain; the current ready frontier is relative chains of sigma pairs, the finite-fiber pair map on local classes, and the local-homeomorphism calculation.
Coproduct and excision infrastructure
For P : ι → TopPair, define Hatcher.Relative.sigmaPair P. Its ambient
space is Σ i, (P i).fst, its subspace is Σ i, (P i).snd, and its structure
map applies (P i).map in the same summand. The main artifact is
Hatcher.Relative.sigmaPair.
For every i, also expose the canonical morphism
Hatcher.Relative.sigmaPairι P i : P i ⟶ sigmaPair P and prove formulas for
the structure map and its ambient and subspace components, both as morphisms
and on elements. Make the generic construction the implementation core while
preserving the existing sigmaPointedPair and sigmaPointedPairι names as
definitional wrappers. Publish named exact compatibility equalities for the
pointed object and every summand inclusion; do not maintain two independent
implementations or supply only an object isomorphism with no summand triangle.
The construction requires no Nonempty ι hypothesis and includes the empty
family.
The canonical summand map is Hatcher.Relative.sigmaPairι. The structure-map
and summand-component formulas are
Hatcher.Relative.sigmaPair_map_apply,
Hatcher.Relative.sigmaPairι_fst,
Hatcher.Relative.sigmaPairι_fst_apply,
Hatcher.Relative.sigmaPairι_snd, and
Hatcher.Relative.sigmaPairι_snd_apply.
The existing pointed constructions are definitional wrappers. Their named
exact compatibility equalities are
Hatcher.Relative.sigmaPointedPair_eq_sigmaPair and
Hatcher.Relative.sigmaPointedPairι_eq_sigmaPairι.
Sources
For a family P : ι → TopPair, construct the chain-complex isomorphism
∐ i, C_*(P i; R) ≅ C_*(sigmaPair P; R).
The main artifact is
Hatcher.Relative.relativeChainComplexSigmaPairIso. Its forward morphism
must restrict on each summand to the relative-chain map induced by
sigmaPairι P i.
Expose the underlying canonical map as
Hatcher.Relative.relativeChainComplexSigmaPairMap, identify the isomorphism's
forward morphism with it, and name the component equation
Hatcher.Relative.ι_relativeChainComplexSigmaPairIso_hom.
Refactor the completed singular-simplex sigma argument and the cokernel
comparison used by relativeChainComplexSigmaIso; preserve that pointed
declaration as an exact compatibility specialization rather than maintaining
a second proof. Preserve every existing pointed declaration and component
theorem for downstream consumers.
Keep the existing minimal assumptions: {ι : Type w}, P : ι → TopPair.{w},
an arbitrary preadditive coefficient category with HasCoproducts.{w}, and no
Abelian, AB4OfSize, or Nonempty ι hypothesis.
Sources
Dependencies
Assume the coefficient category has exact coproducts of the size of ι, via
Mathlib's AB4OfSize interface. Construct
∐ i, H_k(P i; R) ≅ H_k(sigmaPair P; R).
The main artifact is Hatcher.Relative.relativeHomologySigmaPairIso. Its
forward map must satisfy the component formula
Sigma.ι _ i ≫ iso.hom = H_k(sigmaPairι P i).
Expose the underlying canonical map as
Hatcher.Relative.relativeHomologySigmaPairMap, identify the isomorphism's
forward morphism with it, and name the component theorem
Hatcher.Relative.ι_relativeHomologySigmaPairIso_hom. Also provide
Hatcher.Relative.relativeIntegralHomologySigmaPairIso for universe-zero
integral pairs with no extra call-site hypotheses.
Make every existing pointed map, isomorphism, component theorem, and integral
isomorphism an exact compatibility specialization rather than a parallel
proof.
The integral finite-family instance used by Proposition 2.30 must require no
additional hypotheses at call sites. Preserve the empty-index case and use the
same universe for ι and the family of topological pairs, matching the chain
API.
Sources
Let U : ι → Set X be pairwise disjoint open subsets. Construct the canonical
homeomorphism
(Σ i, U i) ≃ₜ ⋃ i, U i
which forgets the summand tag. The main artifact is
Hatcher.Topology.sigmaSubtypeHomeomorphUnion. Its forward map and inverse on
a point lying in U i must have explicit computation lemmas.
The forward computation is
Hatcher.Topology.sigmaSubtypeHomeomorphUnion_apply_mk, and the inverse
computation is
Hatcher.Topology.sigmaSubtypeHomeomorphUnion_symm_apply_mk.
The proof may use openness to show that the inverse is continuous and pairwise disjointness to show the index is unique. Empty summands and an empty index type remain valid.
Sources
Dependencies
For F : Set X, write Hatcher.Relative.deletedPair X F for
(X, X \ F) and define
Hatcher.Relative.deletedPairWithin F W as the pair inside W obtained by
deleting the preimage of F, represented as
TopPair.ofSubset (Subtype.val ⁻¹' Fᶜ). If F is closed, W is open, and
F ⊆ W,
define the canonical morphism
Hatcher.Relative.deletedPairOpenNeighborhoodPairHom F W and its induced
homology map Hatcher.Relative.deletedPairOpenNeighborhoodMap F W R n.
The main theorem
Hatcher.Relative.deletedPairOpenNeighborhoodMap_isIso says that this map
induces an isomorphism on relative homology in every degree. Include a named
deletedPairOpenNeighborhoodMap_isIso_of_finite specialization in a
T1Space, using that finite sets are closed. Publish ambient and
proof-term-insensitive subspace component formulas for the pair map. No
nonemptiness hypothesis is permitted; in particular F = ∅ remains valid.
For F = {x}, construct the canonical source-pair isomorphism from the
punctured pair of W to deletedPairWithin {x} W. Name the induced homology
isomorphism and prove at pair and homology level that its forward map followed
by the deleted-pair neighborhood map is the completed
localHomologyOpenNeighborhoodMap; do not claim a generally ill-typed literal
equality between their source objects.
The pair objects, canonical pair map, induced homology map, and component
formulas are Hatcher.Relative.deletedPair,
Hatcher.Relative.deletedPairWithin,
Hatcher.Relative.deletedPairOpenNeighborhoodPairHom,
Hatcher.Relative.deletedPairOpenNeighborhoodMap,
Hatcher.Relative.deletedPairOpenNeighborhoodPairHom_fst_apply, and
Hatcher.Relative.deletedPairOpenNeighborhoodPairHom_snd_apply_coe. The
cover comparison is Hatcher.Relative.deletedPairWithinCoverIso with
factorization Hatcher.Relative.deletedPairWithinCoverIso_hom_comp; the
finite specialization is
Hatcher.Relative.deletedPairOpenNeighborhoodMap_isIso_of_finite.
The correctly directed singleton pair and homology isomorphisms are
Hatcher.Relative.puncturedPairIsoDeletedPairWithinSingleton and
Hatcher.Relative.puncturedPairHomologyIsoDeletedPairWithinSingleton, with
their _hom_comp theorems recording the two commuting equations.
Sources
Dependencies
Let U i be pairwise disjoint open subsets of X and choose x i ∈ U i.
The sigma pair of the punctured neighborhood pairs has ambient space
Σ i, U i and deletes one point in each summand. Construct the canonical pair
isomorphism from this sigma pair to the union ⋃ i, U i with the range of the
points x i deleted.
The main artifact is
Hatcher.Relative.sigmaPuncturedPairIsoDeletedUnion. Its ambient component is
sigmaSubtypeHomeomorphUnion, and its component formula identifies each
sigmaPairι with the ordinary inclusion of (U i,U i-{x i}) into the deleted
union pair.
Represent the target subspace as the preimage
Subtype.val ⁻¹' (Set.range x)ᶜ inside ⋃ i, U i, so it aligns with the later
deletedPairWithin API. Name both the sigma punctured source pair and deleted
union target pair. Construct the subspace homeomorphism without assuming that
the punctured sets are open; no T1Space X hypothesis belongs here.
Expose the direct local inclusion
Hatcher.Relative.puncturedNeighborhoodDeletedUnionPairHom, ambient and
proof-term-insensitive subspace component formulas, and the exact triangle
sigmaPairι i ≫ sigmaPuncturedPairIsoDeletedUnion.hom =
puncturedNeighborhoodDeletedUnionPairHom i.
The definitions require no Nonempty ι hypothesis and include the empty
family.
The named source and target are Hatcher.Relative.sigmaPuncturedPair and
Hatcher.Relative.deletedUnionPair. The subspace homeomorphism is
Hatcher.Relative.sigmaPuncturedSubspaceHomeomorphDeletedUnion, with a
proof-term-insensitive forward formula. The main pair isomorphism exposes its
ambient morphism and apply equations. The direct inclusion and its component
formulas are Hatcher.Relative.puncturedNeighborhoodDeletedUnionPairHom and
the associated _fst_apply and _snd_apply_coe theorems; the exact
reassociated summand triangle is
Hatcher.Relative.sigmaPairι_comp_sigmaPuncturedPairIsoDeletedUnion_hom.
Sources
Dependencies
Local degree
For 0 < n and y : TopCat.sphere n, define
Hatcher.Sphere.integralSphereLocalFundamentalClass n hn y
with type
AddCommGrpCat.of ℤ ⟶ H_n(puncturedPair (TopCat.sphere n) y; ℤ).
It is the completed ordered reduced sphere class followed by
Hatcher.Relative.reducedPairProjection.
The main artifact is the associated isomorphism
Hatcher.Sphere.integralSphereLocalHomologyIso :
H_n(Sⁿ,Sⁿ-{y};ℤ) ≅ AddCommGrpCat.of ℤ, whose inverse is exactly this
class. Prove that both the ordered reduced sphere class and, by contractibility
of the punctured sphere, reducedPairProjection are isomorphisms. Pin the sign
by proving that the ordinary ordered class followed by the inverse
positive-degree reduced-to-ordinary comparison and then
reducedPairProjection (puncturedPair Sⁿ y) is exactly the local class.
For every open neighborhood U of x, also define the transported source
class localClass(U,x) : ℤ ⟶ H_n(U,U-{x};ℤ) as the unique class whose image
under the canonical open-neighborhood isomorphism is the global local class.
Prove this transported
class is an isomorphism. For nested open neighborhoods V ⊆ U containing
x, define the canonical morphism of punctured neighborhood pairs, prove that
it composes with the U → Sⁿ inclusion to the V → Sⁿ inclusion, and prove
the oriented restriction equation
localClass(V,x) ≫ H_n(V → U) = localClass(U,x).
The ordered local class and its orientation isomorphism are formalized as
Hatcher.Sphere.integralSphereLocalFundamentalClass and
Hatcher.Sphere.integralSphereLocalHomologyIso; the inverse and sign
compatibility equations are
Hatcher.Sphere.integralSphereLocalHomologyIso_inv and
Hatcher.Sphere.integralSphereFundamentalClass_to_local.
The transported neighborhood class is
Hatcher.Sphere.integralSphereNeighborhoodFundamentalClass. Its ambient-map,
isomorphism, and restriction laws are
Hatcher.Sphere.integralSphereNeighborhoodFundamentalClass_map,
Hatcher.Sphere.integralSphereNeighborhoodFundamentalClass_isIso, and
Hatcher.Sphere.integralSphereNeighborhoodFundamentalClass_restrict.
The underlying canonical nested-neighborhood maps and their composition law
are
Hatcher.Relative.localHomologyOpenNeighborhoodRestrictionPairHom,
Hatcher.Relative.localHomologyOpenNeighborhoodRestrictionMap, and
Hatcher.Relative.localHomologyOpenNeighborhoodRestrictionMap_comp.
Sources
For a sphere map f and points x and y, define
Hatcher.Sphere.LocalDegreeNeighborhood f x y to package an open set U,
membership x ∈ U, the equality f x = y, and the assertion that a point of
U mapping to y equals x. Define
Hatcher.Sphere.IsolatedPreimage f x y as the nonemptiness of this structure.
The main artifact is Hatcher.Sphere.LocalDegreeNeighborhood.pairHom, the
canonical morphism
(U, U \ {x}) ⟶ (Sⁿ, Sⁿ \ {y})
induced by the restriction of f. Prove its ambient and punctured-subspace
component formulas without exposing subtype proof terms. Provide
Hatcher.Sphere.LocalDegreeNeighborhood.restrict for a smaller open set
containing x, and show that every packaged neighborhood supplies an
IsolatedPreimage witness. The generic morphism between nested punctured
neighborhood pairs belongs to the local-orientation node and is not duplicated
here.
The isolation proposition, witness conversion, and restriction operation are
Hatcher.Sphere.IsolatedPreimage,
Hatcher.Sphere.LocalDegreeNeighborhood.isolatedPreimage, and
Hatcher.Sphere.LocalDegreeNeighborhood.restrict. The pair-map component
formulas are
Hatcher.Sphere.LocalDegreeNeighborhood.pairHom_fst_apply and
Hatcher.Sphere.LocalDegreeNeighborhood.pairHom_snd_apply_coe.
Sources
For 0 < n and a LocalDegreeNeighborhood N of x over y, transport the
ordered source local class supplied by the local-orientation node through the
homology map induced by N.pairHom. Conjugate by the ordered target local
orientation and evaluate at 1 to define
Hatcher.Sphere.neighborhoodLocalDegree n hn N : ℤ.
First define the conjugated endomorphism
Hatcher.Sphere.neighborhoodLocalDegreeEndomorphism n hn N : ℤ ⟶ ℤ and prove
that it is AddCommGrpCat.asHom of the local degree. The composition order is
source neighborhood class, induced pair map, then the target local-homology
orientation isomorphism. Do not assume that the induced pair map is an
isomorphism.
The main theorem
Hatcher.Sphere.localFundamentalClass_map_eq_neighborhoodLocalDegree is the
class equation saying that the induced local map sends the transported source
class to the target class multiplied by neighborhoodLocalDegree:
localClass(N) ≫ H_n(N.pairHom) =
AddCommGrpCat.asHom (neighborhoodLocalDegree n hn N) ≫ localClass(y).
Mark this equation for reassociation so later finite-fiber compositions use the exact induced map without unfolding the conjugated endomorphism.
The conjugated endomorphism, its value at 1, and its scalar characterization
are Hatcher.Sphere.neighborhoodLocalDegreeEndomorphism,
Hatcher.Sphere.neighborhoodLocalDegree, and
Hatcher.Sphere.neighborhoodLocalDegreeEndomorphism_eq_asHom. The class
equation is
Hatcher.Sphere.localFundamentalClass_map_eq_neighborhoodLocalDegree.
Sources
Let N be a local-degree neighborhood and let M be a second such
neighborhood whose open set is contained in that of N. The inclusion of the
punctured pair of M into the punctured pair of N induces an isomorphism on
relative homology and makes the two local pair maps commute.
Name the pair-level triangle
Hatcher.Sphere.LocalDegreeNeighborhood.restrictionPairHom_comp_pairHom and
its induced homology equation
Hatcher.Sphere.LocalDegreeNeighborhood.restrictionMap_comp_pairHom_map.
Also expose a sphere-specific IsIso wrapper for the restriction map. The two
neighborhoods are arbitrary witnesses for the same f, x, and y; M need
not be definitionally produced by N.restrict.
The main theorem Hatcher.Sphere.neighborhoodLocalDegree_eq_of_subset states
neighborhoodLocalDegree n hn M = neighborhoodLocalDegree n hn N.
Prove the equality from the two oriented class equations and the naturality of the open-neighborhood comparison, not by unfolding a choice of inverse.
The pair and homology triangles are
Hatcher.Sphere.LocalDegreeNeighborhood.restrictionPairHom_comp_pairHom and
Hatcher.Sphere.LocalDegreeNeighborhood.restrictionMap_comp_pairHom_map.
The sphere-specific isomorphism wrapper is
Hatcher.Sphere.LocalDegreeNeighborhood.restrictionMap_isIso, and shrinking
invariance is Hatcher.Sphere.neighborhoodLocalDegree_eq_of_subset.
Sources
Dependencies
The intersection of any two local-degree neighborhoods is again an open
local-degree neighborhood contained in both. Use shrinking invariance to prove
that their neighborhood local degrees agree. Expose this data as
Hatcher.Sphere.LocalDegreeNeighborhood.inter, its left and right subset
lemmas, and the arbitrary-neighborhood theorem
Hatcher.Sphere.neighborhoodLocalDegree_eq.
Define Hatcher.Sphere.localDegree n hn f x y h for
h : IsolatedPreimage f x y by choosing one witness. The main theorem
Hatcher.Sphere.localDegree_eq_neighborhoodLocalDegree identifies this public
integer with the value from every packaged neighborhood. Publish an explicit
proof-irrelevance theorem for two isolation witnesses and the reassociated,
choice-free local fundamental-class equation
Hatcher.Sphere.localFundamentalClass_map_eq_localDegree, stated against an
arbitrary packaged neighborhood.
The theorem must make local degree proof-irrelevant in the
IsolatedPreimage witness and independent of all open-neighborhood data. A
classical chosen witness may appear inside the definition, but no chosen
neighborhood accessor or implementation choice appears in the public theorem
signatures.
The common refinement and its containment lemmas are
Hatcher.Sphere.LocalDegreeNeighborhood.inter,
Hatcher.Sphere.LocalDegreeNeighborhood.inter_U_subset_left, and
Hatcher.Sphere.LocalDegreeNeighborhood.inter_U_subset_right. Arbitrary
packaged neighborhoods are compared by
Hatcher.Sphere.neighborhoodLocalDegree_eq. The public degree, comparison,
proof-irrelevance, and choice-free class equation are
Hatcher.Sphere.localDegree,
Hatcher.Sphere.localDegree_eq_neighborhoodLocalDegree,
Hatcher.Sphere.localDegree_proof_irrel, and
Hatcher.Sphere.localFundamentalClass_map_eq_localDegree.
Sources
Suppose a local-degree neighborhood U maps homeomorphically onto an open
neighborhood V of y. The induced map of local relative groups is an
isomorphism, so its integer multiplier is a unit.
Package this hypothesis as
Hatcher.Sphere.LocalDegreeNeighborhood.LocalHomeomorphData N, containing
the open target neighborhood, a homeomorphism N.U ≃ₜ V, and the exact
pointwise equation identifying that homeomorphism with the restriction of
f. Define its punctured-pair isomorphism, prove that its forward map followed
by inclusion of V into the target punctured sphere is exactly N.pairHom,
and deduce that the actual homology map induced by N.pairHom is an
isomorphism.
Name LocalHomeomorphData.pairIso, its reassociated pair triangle, and
LocalHomeomorphData.pairHom_homologyMap_isIso. First prove a
chosen-neighborhood ±1 theorem from the isomorphism of the conjugated
endomorphism, then state the public theorem for an arbitrary isolation witness
and compare it with N via localDegree_eq_neighborhoodLocalDegree.
The main theorem
Hatcher.Sphere.localDegree_eq_one_or_neg_one_of_localHomeomorph says that
the local degree is 1 or -1. As a source-facing specialization, for
e : Sⁿ ≃ₜ Sⁿ, x : Sⁿ, and any isolation witness at x over e x, prove
the ordered equality
Hatcher.Sphere.localDegree_homeomorph_eq_degree with
Hatcher.Sphere.degree n hn (TopCat.isoOfHomeo e).hom.
Construct the canonical full-sphere neighborhood for e, prove its pair-map
factorization through puncturedPairIso e rfl, and name the signed naturality
equation sending the ordered local class at x to the global-degree multiple
of the ordered local class at e x. The global equality must hold for every
supplied isolation witness, not just the canonical one.
The equality must respect the ordered orientation fixed by the completed degree development; an unsigned statement that only proves the local map is an isomorphism is not sufficient.
Sources
Dependencies
Finite fibers
For f : Sⁿ → Sⁿ, y : Sⁿ, and a finite set-theoretic fiber
f ⁻¹' {y}, define the named subtype set Hatcher.Sphere.fiber f y, its
membership lemma, and a local-installation
Hatcher.Sphere.finiteFiberFintype hfinite; do not install a global instance
that hides the finiteness witness. Use
Set.Finite.t2_separation to choose an open neighborhood of every fiber point
so that the neighborhoods are pairwise disjoint.
The main artifact Hatcher.Sphere.finiteFiberNeighborhoods f y hfinite
packages these sets, their openness and center membership, pairwise
disjointness, and the resulting LocalDegreeNeighborhood at every fiber
point. Expose named projections for the sets, openness, center membership, and
pairwise disjointness. Also prove that their union is open, contains the entire
fiber, and is empty when the fiber is empty.
As neutral supporting data, define Hatcher.Sphere.finiteFiberPairMap, the
canonical map (Sⁿ,Sⁿ-fiber f y) ⟶ (Sⁿ,Sⁿ-{y}) induced by f, and record its
ambient and subspace formulas. This definition is independent of the chosen
separated neighborhoods and of a finiteness proof.
The construction is noncomputable but its stated properties may not depend on an enumeration or a decidable equality chosen by callers. It must also support the empty fiber, with an empty family and empty union.
The fiber API is Hatcher.Sphere.fiber, Hatcher.Sphere.mem_fiber, and
Hatcher.Sphere.finiteFiberFintype. The chosen data has type
Hatcher.Sphere.FiniteFiberNeighborhoods; its named set, openness, center,
disjointness, union, containment, and empty-fiber declarations are in the
namespace of that structure. The neutral pair map and its formulas are
Hatcher.Sphere.finiteFiberPairMap,
Hatcher.Sphere.finiteFiberPairMap_fst,
Hatcher.Sphere.finiteFiberPairMap_fst_apply, and
Hatcher.Sphere.finiteFiberPairMap_snd_apply_coe.
Sources
For the chosen finite-fiber neighborhoods, compose the canonical pair
isomorphism from their sigma pair to the deleted union pair with the inclusion
of that open union into the sphere pair obtained by deleting the full fiber.
Call the resulting morphism
Hatcher.Sphere.finitePuncturePairHom.
Name the finite wrapper
Hatcher.Sphere.finitePunctureSigmaPairIsoDeletedUnion, whose target is
literally deletedPairWithin (fiber f y) D.union, and the direct local
inclusion Hatcher.Sphere.finitePunctureNeighborhoodPairHom D i into
deletedPair Sⁿ (fiber f y). The pair map itself depends only on the chosen
separated-neighborhood data D; only the homology-isomorphism theorem takes
the explicit proof that the fiber is finite.
The main theorem Hatcher.Sphere.finitePuncturePairHom_homology_isIso states
that this morphism induces an isomorphism on relative integral homology in
every degree. Prove the component equation saying that
sigmaPairι followed by this map is the direct inclusion of the corresponding
punctured neighborhood pair into the finite-puncture sphere pair, and name
that exact triangle. The target must be the literal deleted-fiber pair, not an
abstract isomorphic object. No positivity, Fintype, or nonemptiness premise
is required; the empty fiber is included.
Sources
Compose the relative-homology sigma-pair isomorphism with the homology
isomorphism induced by finitePuncturePairHom. The main artifact
Hatcher.Sphere.finitePunctureHomologyIso has type
∐ x : fiber f y, H_n(U_x, U_x - {x}; ℤ)
≅ H_n(Sⁿ, Sⁿ - fiber f y; ℤ).
Prove the exact component formula: the xth coproduct injection followed by
the forward isomorphism is the homology map induced by inclusion of the xth
local punctured pair into the finite-puncture pair. Also expose the inverse
component maps used to test equality of morphisms into the finite coproduct.
Define Hatcher.Sphere.finitePunctureHomologyIso D hfinite k by composing
relativeIntegralHomologySigmaPairIso for the named local-pair family with the
isomorphism induced by finitePuncturePairHom D. Name the reassociated
component theorem
Hatcher.Sphere.ι_finitePunctureHomologyIso_hom.
Expose
Hatcher.Sphere.finitePunctureHomologyProjection D hfinite k i as the inverse
isomorphism followed by the ith finite-biproduct projection, together with a
hom-ext theorem for maps into finite-puncture homology. Install all Fintype,
DecidableEq, and finite-biproduct instances internally from hfinite; none
belongs in a public signature. The construction works in every degree and for
an empty fiber without branching.
Sources
For a fiber point x, inclusion of complements defines Hatcher's projection
p_x : H_n(Sⁿ,Sⁿ-fiber f y) → H_n(Sⁿ,Sⁿ-{x}).
Name the underlying pair map
Hatcher.Sphere.finitePunctureProjectionPairHom, its induced integral map
Hatcher.Sphere.finitePunctureProjectionMap, and their component formulas.
Also prove the reusable generic lemma that a relative-homology map is zero
when its ambient component factors through the target subspace; do not claim
that the pair morphism itself is zero.
The main theorem Hatcher.Sphere.finitePunctureProjection_comp_summand says
that, under finitePunctureHomologyIso, composing p_x with the zth
summand is the local-neighborhood inclusion when z = x and is zero when
z ≠ x.
State separate reassociated diagonal and off-diagonal component theorems. For
the off-diagonal factorization, use pairwise disjointness and the fact that the
center x lies in its own chosen neighborhood.
For the off-diagonal case, prove the reusable supporting lemma that a map of
relative pairs induces the zero map when its ambient component factors through
the target subspace. Apply it because the zth disjoint neighborhood misses
x. Package the resulting finite biproduct projection formula, with all
DecidableEq and finite-biproduct instances kept internal.
Normalize Hatcher's projection by the inverse open-neighborhood local-homology
map and identify it exactly with
finitePunctureHomologyIso.inv ≫ Sigma.π _ x. The point-indexed formulas are
vacuous for an empty fiber and require no Nonempty hypothesis.
Sources
Use Hatcher.Sphere.finitePunctureFundamentalClass from the global-degree
fiber-square node; do not redefine the class.
Define the named source-coproduct class
Hatcher.Sphere.finitePunctureLocalFundamentalClassSum D hfinite n hn as the
finite sum of each transported neighborhood class followed by its coproduct
injection. Prove that postcomposing it with the ith finite-biproduct
projection recovers exactly the ith transported class.
The main theorem Hatcher.Sphere.finitePunctureFundamentalClass_eq_sum says
that this class is the image, under finitePunctureHomologyIso, of the finite
sum of the transported oriented local classes in the coproduct summands.
First prove that the finite-puncture class followed by the geometric
projection to x is the ordered local class at x, using
reducedPairProjection_naturality for the identity ambient map. Combine this
with the projection-matrix normalization and
finitePunctureHomology_hom_ext; keep every finite/biproduct instance
internal.
For each fiber point, prove first that projection to the pair punctured only
at that point sends the finite-puncture class to the ordered local class and
kills all other summands. Then use the finite biproduct extensionality
principle. This theorem is the formal version of Hatcher's equation
j(1) = (1,…,1) = ∑ᵢ kᵢ(1).
The empty fiber requires no branch or Nonempty hypothesis: the source sum
and component family are empty, and hom-ext supplies the equality.
Sources
Use the canonical pair morphism
(Sⁿ, Sⁿ - fiber f y) ⟶ (Sⁿ, Sⁿ - {y})
defined with the finite-fiber data. For each fiber point, its composite with the inclusion of the chosen local punctured pair is the pair map used to define local degree.
Work parametrically with arbitrary D : FiniteFiberNeighborhoods f y rather
than hardwiring the noncomputable constructor. Name the exact pair triangle
Hatcher.Sphere.finitePuncturePairHomComponent_comp_finiteFiberPairMap, using
the direct inclusion finitePunctureNeighborhoodPairHom D i. The canonical
isolation witness on the right is (D.neighborhood i).isolatedPreimage.
The main theorem Hatcher.Sphere.finiteFiberPairMap_localClass states that
the full local-to-finite-to-target homology composite sends the transported
oriented class of the ith local summand to
AddCommGrpCat.asHom (localDegree n hn f x y hx) ≫
integralSphereLocalFundamentalClass n hn y.
The local integer must be the neighborhood-independent public local degree,
using localDegree_eq_neighborhoodLocalDegree for the neighborhoods supplied
by D. Mark both the pair triangle and class equation for reassociation. The
proof must rewrite the actual pair composite; no new isomorphism or scalar
cancellation is needed.
Sources
Define Hatcher.Sphere.finitePunctureFundamentalClass n f y from ℤ to the
degree-n relative homology of (Sⁿ,Sⁿ-fiber f y) as the ordered reduced
sphere class followed by reducedPairProjection. This definition needs
neither a positivity nor a finiteness witness. The finite-fiber pair map
induced by f takes this class to the global-degree multiple of the target
local class.
The main theorem Hatcher.Sphere.finiteFiberFundamentalClass_map identifies
the multiplier exactly:
finitePunctureFundamentalClass ≫ H.map finiteFiberPairMap =
AddCommGrpCat.asHom (degree n hn f) ≫
integralSphereLocalFundamentalClass n hn y.
Prove the square by naturality of reducedPairProjection and the completed
positive-degree comparison between reduced and ordinary homology, using the
morphism-level equation finiteFiberPairMap_fst = f. The theorem itself needs
no fiber-finiteness hypothesis. The sign must therefore be the ordered global
degree, not merely some integer with the same absolute value.
The projected class and the signed lower-square equation are
Hatcher.Sphere.finitePunctureFundamentalClass and
Hatcher.Sphere.finiteFiberFundamentalClass_map. The latter is marked for
reassociation and neither declaration depends on a fiber-finiteness witness.
Sources
Let 0 < n, let f : TopCat.sphere n ⟶ TopCat.sphere n, and let
y : TopCat.sphere n. If hfinite : (f ⁻¹' {y}).Finite, install the finite
fiber subtype's Fintype from hfinite; every fiber point is then an isolated
preimage and the following finite sum is defined.
The main theorem Hatcher.Sphere.degree_eq_sum_localDegree is Hatcher's
Proposition 2.30:
degree n hn f = ∑ x : fiber f y, localDegree n hn f x y (isolated x).
Name the canonical witness
Hatcher.Sphere.finiteFiberIsolatedPreimage f y hfinite i. First prove the
working theorem
Hatcher.Sphere.degree_eq_sum_localDegree_of_neighborhoods parametrically for
arbitrary D : FiniteFiberNeighborhoods f y, then obtain the source-facing
theorem by taking D := finiteFiberNeighborhoods f y hfinite. Install
finiteFiberFintype hfinite only inside these theorem propositions and proofs.
Apply the finite-fiber pair map to the orientation-sum equation and rewrite
each summand with finiteFiberPairMap_localClass. Naturality of
reducedPairProjection and the completed degree class equation identify the
same composite with the global-degree multiple of the target local class.
Distribute postcomposition over the finite sum, rewrite each term with the
local summand theorem, cancel the target local orientation isomorphism at
morphism level, and only then evaluate the resulting equality of integer
endomorphisms at 1.
The statement includes the empty fiber; in that case the sum is zero and the
result agrees with the completed nonsurjective-degree theorem. No Nonempty
hypothesis or separate empty-fiber proof is used.
Boundary
This milestone stops after Proposition 2.30. Examples 2.31–2.32, suspension invariance in Proposition 2.33, cellular homology, the Hopf converse, and Theorem 2.27 remain deferred.