Good pairs and quotient exact sequences
Hatcher §2.1, Theorem 2.13 and Proposition 2.22 (printed pages 114,
124, and 128). For a good pair (X,A), the quotient map identifies relative
homology with reduced homology of X/A. Transporting the reduced pair sequence
through this comparison gives the quotient long exact sequence, naturally in
maps of good pairs.
All fifteen leaves in the good-pair source unit are formalized locally and complete. The shared strong-deformation-retract background leaf listed below is also complete.
The point quotient is represented functorially as the TopCat pushout
X ⊔_A PUnit. The good-pair witness keeps Hatcher's exact neighborhood
hypothesis A ⊆ interior V; it does not assume that the chosen V is open.
The topology and homology bridges are decomposed separately so that the final
source-facing theorems use canonical quotient-induced maps.
Good pairs and point quotients
Package an inclusion i : C(A,Y), a retraction r : C(Y,A), the identity
r ∘ i = id, and a homotopy from id_Y to i ∘ r relative to the image of
i as Hatcher.StrongDeformationRetract i.
Expose the induced ContinuousMap.HomotopyEquiv and the elementary transport
of contractibility and path connectedness. This neutral topology interface is
already formalized in Hatcher/Topology/StrongDeformationRetract.lean; this
article gives the existing declaration its own reusable roadmap owner instead
of leaving it hidden inside the Mayer–Vietoris review unit.
Sources
Dependencies
For P : TopPair, define Hatcher.Relative.GoodPairData P to contain a
nonempty subspace, closedness of Set.range P.map, a set V : Set P.fst
with Set.range P.map ⊆ interior V, and a strong deformation retraction of
V onto the embedded subspace.
Define Hatcher.Relative.IsGoodPair P := Nonempty (GoodPairData P) and the
full subcategory of good pairs. Morphisms are ordinary morphisms of
topological pairs and do not preserve the chosen witness data. The neighborhood
field is not required to be open: this states Hatcher's hypothesis exactly.
Sources
Dependencies
For every P : TopPair, define the point quotient of its ambient space as the
TopCat pushout P.fst ⊔_{P.snd} PUnit. Package the pushout point as a pointed
topological pair.
The intended main declaration is
Hatcher.Relative.pointQuotientPairFunctor : TopPair ⥤ TopPair. Include the
ambient projection, collapsed point, induced quotient map for every morphism
of pairs, and the natural comparison
Hatcher.Relative.pointQuotientComparison : 𝟭 TopPair ⟶ pointQuotientPairFunctor.
Identify each target canonically with the existing pointedPair construction.
Formalized in Hatcher/Singular/PointQuotient.lean. The supporting API exposes
pointQuotientCollapse, pointQuotient, pointQuotientProjection,
pointQuotientPointInclusion, pointQuotientPoint, pointQuotientPair, and
pointQuotientMap. The target pair is defined using pointedPair, and
pointQuotientPair_map identifies its structure map with the pushout point
inclusion. The functor acts on every morphism of topological pairs, without a
good-pair hypothesis, and pointQuotientComparison is the natural map from a
pair to its pointed quotient. This node uses only the pushout universal
property; quotient-map, fibre, and complement topology remain in the next
node.
Sources
Dependencies
For a topological pair with nonempty subspace, prove that the ambient point-
quotient projection is a quotient map and that the inverse image of the
collapsed point is exactly Set.range P.map. When that range is closed, deduce
that the collapsed point is closed.
Construct the canonical homeomorphism
P.fst ∖ Set.range P.map ≃ₜ (X/A) ∖ {collapsedPoint}.
The intended completion target is
Hatcher.Relative.pointQuotientComplementHomeomorph, with the quotient-map
and fibre theorems as supporting results in the same review unit.
Formalized in Hatcher/Singular/PointQuotientTopology.lean. For nonempty
P.snd, pointQuotientProjection_isQuotientMap proves that the ambient
projection is a quotient map, and pointQuotientProjection_preimage_point
identifies its collapsed fibre with Set.range P.map.
pointQuotientPoint_isClosed transfers closedness of this range to the
collapsed point. Under the same closedness hypothesis,
pointQuotientComplementHomeomorph restricts the canonical projection to the
displayed homeomorphism; its simp lemma records that the forward map is
literally the quotient projection.
Sources
For h : Hatcher.Relative.GoodPairData P, let qV be the image of its chosen
neighborhood under the point-quotient projection. Prove saturation
q ⁻¹' qV = h.V, that the restricted map h.V → qV is a quotient map, and
that the collapsed point lies in interior qV.
The proof must use Set.range P.map ⊆ interior h.V; it may not assume
IsOpen h.V. Define the canonical neighborhood pairs and the maps needed by
the Proposition 2.22 diagram, together with the two deleted-subset-excision
closure hypotheses.
Formalized in Hatcher/Singular/GoodPairNeighborhoodQuotient.lean. The set
pointQuotientNeighborhood is the image of h.V, and
pointQuotientProjection_preimage_neighborhood proves its inverse image is
exactly h.V. The restricted continuous map
pointQuotientNeighborhoodProjection is surjective and a quotient map. Its
proof works with ambient open representatives of open subsets of h.V: each
representative either contains the entire collapsed range or avoids it, hence
is saturated for the global quotient projection. No openness assumption is
placed on h.V.
The theorem pointQuotientPoint_mem_interior_neighborhood obtains an open
neighborhood of the collapsed point by projecting interior h.V. The module
also supplies the two exact closure-in-interior hypotheses for deleted-subset
excision, packages (X/A,V/A) as pointQuotientNeighborhoodPair, and defines
the canonical maps from (X/A,A/A) and (X,V) into that pair.
Sources
Dependencies
Descend the chosen strong deformation retraction of V onto the embedded
subspace through the restricted quotient map V → qV. Construct a strong
deformation retraction of qV onto the collapsed point and expose its
homotopy equivalence.
The intended main declaration is
Hatcher.Relative.GoodPairData.pointQuotientNeighborhoodStrongDeformationRetract.
Continuity must follow from the quotient property proved for the source-exact,
not-necessarily-open neighborhood.
Formalized in
Hatcher/Singular/PointQuotientNeighborhoodContraction.lean. The chosen
deformation of V preserves the fibers of the restricted quotient: it fixes
all representatives in the collapsed subspace, while equality of two
noncollapsed representatives follows from the complement homeomorphism.
Joint continuity of the descended homotopy follows from
pointQuotientNeighborhoodProjection_isQuotientMap.continuous_lift_prod_right;
no openness assumption is made on V. The resulting strong deformation
retraction is relative to the canonical collapsed-point inclusion, and
pointQuotientNeighborhoodHomotopyEquiv exposes the corresponding homotopy
equivalence with that inclusion as its forward map.
Sources
Dependencies
For chosen good-pair data, package Hatcher's page-124 comparison diagram from
the pairs (X,A), (X,V), and (X ∖ A,V ∖ A) to their point-quotient
counterparts.
Define the pair map induced by the complement homeomorphism and prove both
canonical squares commute, including the neighborhood comparison identity
used in the final diagram chase. The intended main artifact is
Hatcher.Relative.GoodPairData.pointQuotientExcisionDiagram.
Formalized in Hatcher/Singular/GoodPairExcisionDiagram.lean. The source and
target complement pairs are packaged explicitly, and
pointQuotientComplementPairIso is induced by the canonical homeomorphism
off the collapsed subspace together with its restriction to the deleted
neighborhoods. The theorem neighborhood_pointQuotientComparison proves the
left square
neighborhoodPairHom ≫ neighborhoodPairToPointQuotientNeighborhoodPair =
pointQuotientComparison.app P ≫ pointQuotientPairToNeighborhoodPair,
while pointQuotientComplement_excisionSquare proves the right square with
the two canonical deletedSubsetPairHom maps. The main artifact packages
these two identities and the exact complement-pair isomorphism; no homology
isomorphism or diagram chase is asserted in this node.
Sources
Dependencies
Relative homology comparisons
Let f : P ⟶ Q be a morphism of topological pairs. If its ambient and
subspace maps induce ordinary homology isomorphisms in every degree, prove
that the canonical relative-homology map
(Hatcher.Relative.homologyFunctor R n).map f
is an isomorphism for every n, including degree zero. The intended main
theorem is Hatcher.Relative.homologyMap_isIso_of_components and should use
HomologicalComplex.HomologySequence.isIso_homologyMap_τ₃ rather than a new
diagram chase.
Dependencies
For good-pair data on (X,A), prove that the canonical map
H_n(X,A;R) → H_n(X,V;R)
is an isomorphism in every degree. The intended main declaration is an
IsIso instance for the exact map produced by
Hatcher.Relative.homologyFunctor.
Use the chosen deformation retraction to identify the subspace component and the componentwise relative-homology criterion. The canonical map, not an unspecified object isomorphism, is the endpoint.
Sources
For good-pair data, prove that the canonical map
H_n(X/A,A/A;R) → H_n(X/A,V/A;R)
is an isomorphism in every degree. The quotient-neighborhood contraction gives the required component homotopy equivalence; apply the componentwise relative-homology criterion and retain the canonical functorial map.
Formalized in
Hatcher/Singular/PointQuotientNeighborhoodHomology.lean. The ambient
component of pointQuotientPairToNeighborhoodPair is the identity on X/A,
while its subspace component is definitionally the forward map of
pointQuotientNeighborhoodHomotopyEquiv. Ordinary homology therefore sends
both components to isomorphisms, and homologyMap_isIso_of_components proves
that the exact canonical relative-homology map is an isomorphism for every
degree, including degree zero.
Sources
Prove that the canonical map
H_n(X,V;R) → H_n(X/A,V/A;R)
is an isomorphism. Compare both sides by deleted-subset excision and the
homeomorphism induced by the quotient map on complements. The intended main
declaration is an IsIso instance for the exact vertical map in the
complementary excision diagram.
Formalized in Hatcher/Singular/PointQuotientNeighborhoodExcision.lean. The
instance applies relative homology to the proved complementary-excision square.
Both canonical deleted-subset maps and the complement-pair homeomorphism induce
isomorphisms, so categorical cancellation proves that the exact map induced by
neighborhoodPairToPointQuotientNeighborhoodPair is an isomorphism in every
degree, including degree zero.
Sources
Hatcher, Proposition 2.22 (printed page 124). For every good pair and every
degree, prove that the exact canonical map induced by
Hatcher.Relative.pointQuotientComparison is an isomorphism
H_n(X,A;R) → H_n(X/A,A/A;R).
Compose it with Hatcher.Relative.pointedPairHomologyIso to define
Hatcher.Relative.goodPairRelativeHomologyIsoReducedPointQuotient :
H_n(X,A;R) ≅ H̃_n(X/A;R).
Its forward map must be definitionally or propositionally identified with the quotient-induced relative map followed by the pointed comparison.
Formalized in Hatcher/Singular/GoodPairPointQuotientHomology.lean. Applying
relative homology to the canonical neighborhood square identifies the desired
quotient map followed by the quotient-neighborhood comparison with the
composite of the original-neighborhood and neighborhood-quotient comparisons.
The three latter maps are isomorphisms, so categorical cancellation proves
that the exact map induced by pointQuotientComparison.app P is an
isomorphism in every degree, including degree zero. The proof is first given
for GoodPairData and then descends through IsGoodPair, without requiring
maps of pairs to preserve a chosen neighborhood witness.
The definition
Hatcher.Relative.goodPairRelativeHomologyIsoReducedPointQuotient composes
this exact quotient-induced isomorphism with pointedPairHomologyIso. Its
companion _hom theorem identifies the forward map exactly with the required
quotient-induced relative map followed by the pointed comparison.
Dependencies
Exactness and naturality
For a based continuous map, prove naturality of
Hatcher.Relative.pointedPairHomologyIso in every degree. Include naturality
of the reduced-pair projection and the degree-zero sequence map, so the result
does not silently omit the terminal endpoint.
The intended main theorem is
Hatcher.Relative.pointedPairHomologyIso_naturality. It is a general bridge,
not restricted to good pairs.
Sources
Dependencies
Restrict relative homology and reduced homology of the point quotient to the
full subcategory of good pairs. Package the Proposition 2.22 comparisons as a
natural isomorphism
Hatcher.Relative.goodPairPointQuotientRelativeHomologyNatIso.
Maps of good pairs are ordinary pair morphisms and need not preserve chosen
neighborhood witnesses. Prove the canonical identity saying that reduced-pair
projection followed by the comparison is exactly the map on reduced homology
induced by the ambient quotient q : X → X/A.
Formalized in Hatcher/Singular/GoodPairPointQuotientNaturality.lean.
Relative homology and reduced homology of the functorial point quotient are
restricted to the full subcategory Hatcher.Relative.GoodPair. The component
at a good pair is exactly
goodPairRelativeHomologyIsoReducedPointQuotient; naturality follows by
combining pointQuotientComparison.naturality with
pointedPairHomologyIso_naturality. Since morphisms of the full subcategory
carry only an underlying pair map, no chosen neighborhood or deformation
retraction is preserved.
The theorem
reducedPairProjection_comp_goodPairPointQuotientRelativeHomologyNatIso_hom_app
also identifies the displayed composite with
Hatcher.Reduced.homologyFunctor.map (pointQuotientProjection P.obj) in every
degree, including degree zero.
Sources
Dependencies
Hatcher, Theorem 2.13 (printed page 114). For a good pair (X,A), define
the adjacent six-term windows in the reduced sequence
H̃_n(A;R) → H̃_n(X;R) → H̃_n(X/A;R) →
H̃_m(A;R) → H̃_m(X;R) → H̃_m(X/A;R)
for m + 1 = n, and prove every position exact. Include overlap lemmas, the
terminal exact sequence ending H̃_0(X/A;R) → 0, endpoint glue, and a
long-exact package.
Both maps into quotient homology must literally be induced by the ambient
quotient q. Define the connecting map by transporting the reduced-pair
connecting morphism through the Proposition 2.22 comparison.
Formalized in
Hatcher/Singular/GoodPairPointQuotientExactSequence.lean. The definition
Hatcher.Relative.goodPairPointQuotientSequence writes both maps into
quotient homology literally as the maps induced by
pointQuotientProjection. The connecting morphism is the inverse of the
canonical Proposition 2.22 comparison followed by reducedPairConnecting.
Hatcher.Relative.goodPairPointQuotientSequence_exact proves every six-term
window exact by transport from the reduced-pair sequence. The same module
proves consecutive-window overlap, the exact terminal degree-zero sequence,
its glue to the degree-one/degree-zero window, and the combined theorem
Hatcher.Relative.goodPairPointQuotientLongExact.
Hatcher, §2.1 (printed page 128). Every map of good pairs induces the corresponding map between quotient exact sequences. Define the morphisms of six-term windows and prove every square commutes, including the connecting square, overlap compatibility, and the degree-zero endpoint.
The induced map X/A → Y/B comes from the point-quotient functor. The theorem
must not require the map of pairs to preserve chosen neighborhood or
deformation-retraction witnesses.
Formalized in
Hatcher/Singular/GoodPairPointQuotientSequenceNaturality.lean. The main
theorem Hatcher.Relative.goodPairPointQuotientConnecting_naturality
transports reduced-pair connecting naturality through the Proposition 2.22
natural isomorphism. The definitions
Hatcher.Relative.goodPairPointQuotientSequenceMap and
Hatcher.Relative.goodPairPointQuotientZeroSequenceMap package the six-term
and terminal degree-zero sequence maps. Their quotient components are exactly
the reduced-homology maps induced by pointQuotientMap f.hom; the module also
records both quotient squares, compatibility on all three terms shared by
successive windows, the final square to zero, and compatibility of the
terminal sequence with the degree-one/degree-zero window. All declarations
take an ordinary morphism in the full good-pair subcategory and use no chosen
good-pair witness data.