Vault structure

Every Markdown file in the blueprint, as the vault holds them. Chapters come from directories, so the shape of this tree is the shape of the book.

blueprint/vault rootREADME.mdprosecoverage/README.mdproseroadmap/README.md Algebraic Topology (Hatcher) roadmaparticleready to stateappendix/README.md Appendixarticleready to stateclassical-cw-bridge/README.md Classical CW bridge supportarticleready to stateclassical-cell-arrow-iso.md Classical and standard cells have isomorphic attaching arrowsdeffully provedcompact-subset-bounded-skeleton.md Compact subsets lie in a bounded skeletontheoremfully provedsuccessor-skeleton-quotient.md A successor classical skeleton has the cell-attachment quotient topologytheoremfully provedclassical-skeleton-cell-attachment.md Classical skeleton inclusions are abstract cell attachmentsdeffully provedcompact-subspace-finite-subcomplex.md Compact subsets lie in finite subcomplexespropositionfully provedcohomology/README.md Cohomologyarticleready to statecohomology-groups/README.md Cohomology groupsarticlenot readycup-product/README.md Cup productarticlenot readypoincare-duality/README.md Poincaré dualityarticlenot readyfundamental-group/README.md The fundamental grouparticleready to statebasic-constructions/README.md Basic constructionsarticleready to stateaffine-path-homotopy.md Straight-line homotopy between pathsdeffully provedborsuk-ulam-sphere.md Borsuk–Ulam for the two-spheretheoremfully provedbrouwer-disc.md Brouwer's fixed point theorem for the disctheoremfully provedchange-of-basepoint.md A path induces change of basepointdefin mathlibcircle-covering.md The real line covers the circletheoremfully provedconvex-trivial-fundamental-group.md Convex sets have trivial fundamental grouptheoremin mathlibeuclidean-two-not-homeomorphic.md Euclidean two-space is distinguished by dimensiontheoremfully provedfundamental-group-circle.md The fundamental group of the circletheoremfully provedfundamental-group-law.md Path concatenation gives the fundamental-group lawtheoremfully provedfundamental-theorem-algebra.md The fundamental theorem of algebratheoremfully provedhomotopic-maps-fundamental-group.md Homotopic maps differ by basepoint changetheoremfully provedhomotopy-equivalence-fundamental-group.md A homotopy equivalence induces a fundamental-group isomorphismdeffully provedloop-in-open-cover.md A loop splits across an open covertheoremfully provedno-retraction-disc.md The circle is not a retract of the disctheoremfully provedpath-homotopy-equivalence.md Path homotopy is an equivalence relationtheoremin mathlibproduct-fundamental-group.md The fundamental group of a productdeffully provedretractions-fundamental-group.md Retractions and deformation retracts on the fundamental grouptheoremfully provedsimply-connected-unique-path-classes.md Simply connected spaces have unique path-homotopy classestheoremin mathlibsphere-simply-connected.md Higher spheres are simply connectedtheoremfully provedthree-closed-sets-antipodal.md Three closed sets covering the sphere contain an antipodal pairtheoremfully provedtorus-fundamental-group.md The fundamental group of the torusdeffully provedwinding-number.md Winding number of a loop in the circledeffully provedcovering-spaces/README.md Covering spacesarticleready to statebased-connected-cover.md Pointed connected covering spacesstructurefully provedclosed-lift-image.md The induced subgroup consists of loops with closed liftspropositionfully provedcover-basepoint-conjugacy.md Changing the lifted basepoint conjugates the image subgrouptheoremfully provedcovering-injective-path-classes.md Covering maps inject path-homotopy classeslemmain mathlibdeck-transformations/README.md Deck transformations and quotient actionsarticleready to statecovering-space-action.md Covering-space actions give quotient coveringstheoremfully proveddeck-group-calculation.md The deck group is the normalizer quotientdeffully proveddeck-realization.md A deck transformation is determined by one lifted pointtheoremfully proveddeck-transformation-group.md Deck transformations and normal coversdefin mathlibnormalizer-to-deck-exactness.md The normalizer map is surjective with kernel the covering subgrouptheoremfully provednormalizer-to-deck.md The normalizer acts by deck transformationsdeffully provedorbit-quotient-deck-group.md Orbit quotients are normal and have the expected deck groupdeffully provedorbit-quotient-fundamental-group.md The orbit-quotient fundamental group recovers the acting groupdeffully provedhomotopy-lifting.md Homotopies lift uniquely through a covering mappropositionfully provedlifting-criterion.md A map lifts exactly when its fundamental group lands in the covering subgrouppropositionfully provedlocally-path-connected-total-space.md Local path-connectedness ascends along a coveringlemmafully provedmonodromy-action.md The fundamental group acts on a covering fiberdefin mathlibpointed-cover-classification.md Pointed connected covers are classified by subgroupsdeffully provedpointed-cover-rigidity.md Equal image subgroups characterize pointed cover isomorphismpropositionfully provedsheet-index.md Sheets are cosets of the induced subgroupdeffully provedsubgroup-cover-image.md The subgroup cover realizes the chosen subgrouppropositionfully provedsubgroup-cover-is-covering.md The subgroup projection is a path-connected coveringtheoremfully provedsubgroup-cover-space.md The covering space associated to a subgroupdeffully provedunique-lifting.md A lift is determined by one pointtheoremin mathlibuniversal-cover/README.md The path-class universal coverarticleready to statenullhomotopic-open-basis.md Small nullhomotopy neighborhoods form a basislemmafully provedsemilocally-simply-connected.md Semilocally simply-connected spacesclassfully proveduniversal-cover-basis.md The sets U[γ] form the universal-cover basistheoremfully proveduniversal-cover-is-covering.md The endpoint map is a coveringtheoremfully proveduniversal-cover-path-connected.md The path-class cover is path-connectedinstancefully proveduniversal-cover-path-space.md The path-class universal-cover spacedeffully proveduniversal-cover-simply-connected.md The path-class cover is simply-connectedtheoremfully proveduniversal-cover-initial.md A simply-connected cover maps uniquely to every pointed connected covertheoremfully provedunpointed-cover-classification.md Connected covers are classified by conjugacy classesdeffully provedvan-kampen/README.md Van Kampen's theoremarticleready to stateattach-higher-cells-fundamental-group.md Attaching higher cells preserves the fundamental groupdeffully provedattach-two-cells-fundamental-group.md Attaching 2-cells adds the attaching relationsdeffully provedattaching-spheres-generate-intersection.md The attaching-sphere pieces generate the intersection grouptheoremfully provedbinary-van-kampen-pushout.md Binary van Kampen is a group pushoutdeffully provedcell-attachment-cover-model.md An open-cover model for attached cellslemmafully provedcell-attachment-support/README.md Cell-attachment supportarticleready to stateabstract-cell-attachment-indexed-model.md Every abstract cell attachment has an indexed cone modeldeffully provedauxiliary/README.md Hatcher's auxiliary cell-attachment coverarticleready to stateauxiliary-attachment-retract.md The strip enlargement retracts onto the attached spacedeffully provedauxiliary-base-cover-retract.md The base-side auxiliary cover retracts onto the original spacedeffully provedauxiliary-cell-attachment-open-cover.md Hatcher's binary cover of the strip enlargementtheoremfully provedauxiliary-cell-attachment-space.md The strip-enlarged cell-attachment spacedeffully provedauxiliary-cover-basepoint-transport.md The auxiliary cover basepoint transports to the original basepointdeffully provedauxiliary-overlap-attaching-map.md Overlap meridians recover the attaching loopstheoremfully provedauxiliary-overlap-open-cover.md The auxiliary overlap has an indexed open covertheoremfully provedauxiliary-overlap-piece-sphere.md Each overlap piece has the homotopy type of its attaching spheredeffully provedauxiliary-upper-cover-contractible.md The strip-connected upper cover is contractibletheoremfully provedbinary-cover-contractible-piece.md A binary cover with a contractible second piecedeffully provedbinary-cover-trivial-piece-quotient.md A binary cover with a trivial second fundamental groupdeffully provedcircle-degree-map.md The degree-n circle map sends the generator to the degree-n looptheoremfully provedcircle-well-pointed.md The circle is well-pointed at onetheoremfully provedcone-disk-homeomorphism.md The cone on a disk boundary is the diskdeffully provedcyclic-relation-quotient.md The degree-n circle relation gives the cyclic groupdeffully proveddisk-boundary-two-circle.md The boundary of the two-disk is the circledeffully provedempty-cell-attachment-iso.md An attachment with no cells is an isomorphismdeffully provedhigher-cell-attachment-path-components.md Higher-cell attachments preserve path componentstheoremfully provedindexed-basic-cell-attachment.md An indexed cone attachment is a standard cell attachmentdeffully provedindexed-cone-open-cover.md An indexed family of cones has a two-set open covertheoremfully provedindexed-cone-pushout.md An indexed family of cone attachments is a topological pushouttheoremfully provedpath-connected-two-skeleton.md The 2-skeleton of a path-connected CW complex is path-connectedtheoremfully provedsingle-basic-cell-attachment.md A single cone attachment is a standard cell attachmentdeffully provedsingle-cone-base-retract.md The base-side cone cover retracts onto the original spacedeffully provedsingle-cone-intersection.md The single-cone cover intersection has the homotopy type of its boundarydeffully provedsingle-cone-open-cover.md A single cone attachment has a two-set open covertheoremfully provedsingle-cone-pushout.md A single cone attachment is a topological pushouttheoremfully provedsingle-cone-upper-contractible.md The cone-side cover member is contractibletheoremfully provedcover-factorization.md Cover factorizations of a loopstructurefully provedcover-group-presentation.md The group presentation associated to an open coverdeffully provedcover-map-relations.md Overlap relations vanish under the cover maptheoremfully provedevery-group-fundamental-group.md Every group is a fundamental groupcorollaryfully provedevery-group-presentation.md Every group admits a generators-and-relations presentationtheoremfully provedfactorization-moves.md Elementary factorization moves preserve the quotient classtheoremfully provedfinite-skeleton-fundamental-group.md Finite skeleta above dimension two have the same fundamental groupdeffully provedhomotopic-factorizations.md Homotopic factorizations have the same quotient classtheoremfully provedhomotopy-cover-decomposition.md A homotopy admits a threefold-incidence cover decompositiontheoremfully provedpointed-wedge.md The pointed wedge of a family of spacesdeffully provedpresentation-complex/README.md Presentation-complex supportarticleready to statecircle-one-cell-quotient.md Collapsing the boundary of a one-disk gives the circledeffully provedcyclic-presentation-complex.md The cyclic presentation complexdeffully proveddisk-boundary-fundamental-group-representative.md Every fundamental-group element has a based disk-boundary representativedeffully provedempty-cell-attachment-constructor.md The identity attaches an empty family of cellsdeffully provedeventually-constant-cell-sequence.md Eventually constant cell sequences form abstract CW complexesdeffully provedpoint-zero-cell-attachment.md A point is one standard zero-celldeffully provedpointed-wedge-path-connected.md Pointed wedges of path-connected spaces are path-connectedinstancefully provedpointed-wedge-universal-property.md Continuous maps out of a pointed wedgedeffully provedpresentation-complex-cw-structure.md The presentation complex is an abstract two-dimensional CW complexdeffully provedpresentation-complex-fundamental-group.md The presentation complex has the presented fundamental groupdeffully provedpresentation-complex-realization.md Presented groups have two-dimensional presentation complexestheoremfully provedrelator-cell-attachment.md Free-group relators form a standard two-cell attachmentdeffully provedwedge-circles-one-skeleton.md A wedge of circles is an indexed one-cell attachmentdeffully provedtwo-skeleton-fundamental-group.md The 2-skeleton determines the fundamental groupdeffully provedvan-kampen-kernel.md The kernel is generated by overlap relationstheoremfully provedvan-kampen-quotient.md Van Kampen's quotient isomorphismdeffully provedvan-kampen-surjective.md The van Kampen cover map is surjectivetheoremfully provedwedge-circles-free-group.md The fundamental group of a wedge of circlesdeffully provedwedge-fundamental-group.md The fundamental group of a wedgedeffully provedwell-pointed-wedge-cover.md The standard cover of a well-pointed wedgetheoremfully provedhomology/README.md Homologyarticleready to statecomputations-and-applications/README.md Computations and applicationsarticleready to statedegree/README.md Degree foundations and applicationsarticleready to stateantipodal-degree.md The antipodal map has degree determined by dimensiontheoremfully provedbasic-degree-properties.md The formal properties of degreetheoremfully provedcoordinate-reflection-degree.md A sphere reflection has degree minus onetheoremfully proveddouble-simplex-swap-class.md Swapping the double simplex negates its fundamental classtheoremfully provedfixed-point-free-degree.md A fixed-point-free sphere map has antipodal degreetheoremfully provedfree-even-sphere-action.md Only the antipodal group acts freely on an even spheretheoremfully provedintegral-sphere-orientation.md The ordered class orients ordinary sphere homologydeffully provednonsurjective-degree-zero.md A nonsurjective sphere map has degree zerotheoremfully provednonzero-tangent-field-iff-odd.md A sphere has a nonvanishing tangent field exactly in odd dimensiontheoremfully provedodd-sphere-tangent-field.md Odd spheres have a nonvanishing tangent fielddeffully provedpunctured-sphere-stereographic.md A punctured sphere is Euclidean spacedeffully provedsphere-action-degree-character.md Degree gives a character of a sphere actiondeffully provedsphere-coordinate-sign-changes.md Coordinate sign changes on the spheretheoremfully provedsphere-degree-definition.md Degree is the multiplier of the ordered sphere classtheoremfully provedtangent-field-parity-obstruction.md A nonvanishing tangent field forces odd dimensiontheoremfully provedtangent-vector-field-data.md Tangent vector fields and normalizationstructurefully provedlocal-degree/README.md Local degree and the sum over a finite fiberarticleready to statedegree-local-sum-formula.md Degree is the sum of the local degreestheoremplanneddeleted-pair-open-neighborhood.md Deleted-pair homology is local on an open neighborhoodtheoremfully proveddisjoint-open-union-homeomorphism.md A disjoint open family is homeomorphic to its sigma typedeffully proveddisjoint-punctured-pair-iso.md Disjoint punctured neighborhoods form the deleted union pairdeffully provedfinite-fiber-local-map.md The finite-fiber pair map acts by the local degreestheoremfully provedfinite-fiber-neighborhoods.md A finite sphere-map fiber has disjoint isolated neighborhoodsdeffully provedfinite-puncture-homology-coproduct.md Finite-puncture homology is the coproduct of the local groupsdefplannedfinite-puncture-orientation-sum.md The finite-puncture class is the sum of the local classestheoremplannedfinite-puncture-pair-excision.md The disjoint local pairs excise to the finite-puncture pairtheoremfully provedfinite-puncture-projection-matrix.md Finite-puncture projections have the diagonal matrixtheoremplannedglobal-degree-fiber-square.md The finite-fiber pair map carries the global degreetheoremfully provedhomeomorphism-local-degree.md A local homeomorphism has local degree plus or minus onetheoremready to stateisolated-preimage-neighborhood.md An isolated preimage gives a map of punctured pairsstructurefully provedlocal-degree-shrinking.md Local degree is unchanged when the neighborhood shrinkstheoremfully provedlocal-degree-well-defined.md Local degree is independent of its neighborhoodtheoremfully provedneighborhood-local-degree.md Local degree on a chosen isolated neighborhoodtheoremfully provedrelative-chains-sigma-pair.md Relative chains commute with coproducts of arbitrary pairsdefready to staterelative-homology-sigma-pair.md Relative homology commutes with coproducts of arbitrary pairsdefplannedsigma-topological-pair.md The coproduct of a family of topological pairsdeffully provedsphere-local-orientation.md The ordered sphere class orients local homologydeffully provedlocal-homology-and-dimension/README.md Local homology and invariance of dimensionarticleready to statecontractible-ambient-relative-homology.md Relative homology in a contractible ambient spacedeffully provedinvariance-of-dimension-open-sets.md Homeomorphic nonempty Euclidean open sets have equal dimensiontheoremfully provedlocal-homology-open-neighborhood.md Local homology is unchanged on an open neighborhoodtheoremfully provedpunctured-euclidean-local-homology.md Local homology of positive-dimensional Euclidean spacetheoremfully provedmayer-vietoris/README.md Mayer–Vietoris sequencesarticleready to stateaugmented-binary-cover-chain-short-exact-sequence.md Augmented binary-cover chains form a short exact sequencetheoremfully provedbinary-cover-chain-complex.md The binary-cover Mayer–Vietoris chain complexdeffully provedbinary-cover-chain-short-exact-sequence.md Binary-cover chains form a short exact sequencetheoremfully provedbinary-cover-mayer-vietoris-sequence.md The binary-cover Mayer–Vietoris sequencetheoremfully provedreduced-binary-cover-mayer-vietoris-sequence.md The reduced binary-cover Mayer–Vietoris sequencetheoremfully provedsmall-augmented-chain-inclusion-homotopy-equivalence.md Small augmented chains include by a chain-homotopy equivalencedeffully provedpost-excision-applications/README.md Post-excision applicationsarticleready to statecontractible-subspace-relative-reduced-homology.md A contractible subspace identifies reduced and relative homologydeffully provedcw-subcomplex-excision.md Excision holds for a union of CW subcomplexescorollaryfully provedcw-subcomplex-neighborhood/README.md CW-subcomplex regular neighborhoodsarticleready to statecell-boundary-collar.md The radial collar of a cell boundarydeffully provedregular-neighborhood-strong-deformation-retract.md A regular neighborhood strongly deformation retracts onto its subcomplexdeffully provedregular-neighborhood-system.md A common regular-neighborhood system for subcomplexesstructurefully provedsubcomplex-intersection.md Intersections of CW subcomplexesdeffully provedsubcomplex-neighborhood-cover.md Subcomplex decompositions admit compatible neighborhoodstheoremfully proveddouble-simplex-fundamental-class.md The double-simplex difference generates reduced homologytheoremfully proveddouble-simplex-fundamental-cycle.md The ordered difference of the two simplices is a cycledeffully proveddouble-simplex-relative-comparison.md The first simplex computes homology relative to the secondtheoremfully proveddouble-simplex-sphere-homeomorphism.md The double simplex is a spheredeffully provedmapping-cone-cover-relative-homology.md The mapping-cone cover has the relative homology of the original pairinstancefully provedmapping-cone-model.md The mapping cone of a topological pairdeffully provedmapping-cone-relative-reduced-homology.md Relative homology is reduced homology of the mapping conedeffully provedpointed-wedge-point-quotient.md The pointed wedge is the point quotient of the sigma pairdeffully provedrelative-homology-coproduct.md Relative homology commutes with exact coproductsdeffully provedrelative-simplex-fundamental-class.md The identity simplex generates relative simplex homologytheoremfully provedsigma-good-pair.md A nonempty coproduct of pointed good pairs is goodtheoremfully provedsigma-pointed-pair.md The coproduct pair of a family of pointed spacesdeffully provedsingular-relative-chains-coproduct.md Relative singular chains commute with topological coproductsdeffully provedstandard-simplex-boundary-good-pairs.md Standard-simplex boundary and horn pairs are gooddeffully provedstandard-simplex-boundary-horn.md The boundary and zero horn of a standard topological simplexdeffully provedstandard-simplex-disk-pair-homeomorphism.md The standard simplex pair is homeomorphic to the disk pairdeffully provedstandard-simplex-zero-face-point-quotient.md The zero face identifies the two simplex point quotientsdeffully provedstandard-simplex-zero-face-relative-homology.md The zero face induces an isomorphism in relative homologytheoremfully provedstandard-simplex-zero-horn-retraction.md A standard simplex strongly deformation retracts onto its zero horndeffully provedtriple-connecting-cycle-formula.md The triple connecting map sends a relative cycle to its boundarytheoremfully provedwedge-reduced-homology.md Reduced homology of a wedge is the direct sum of the summandscorollaryfully provedsphere-homology/README.md Mayer–Vietoris transport, sphere homology, and Brouwerarticleready to statebrouwer-fixed-point-disk.md Brouwer's fixed-point theorem for diskstheoremfully provedclosed-ball-radial-deformation-retract.md A closed ball strongly deformation retracts from Euclidean spacedeffully provedcontractible-space-reduced-homology.md Reduced homology of a contractible space vanishestheoremfully proveddisk-boundary-no-retraction.md The boundary sphere is not a retract of the disktheoremfully provedfixed-point-free-disk-map-retraction.md A fixed-point-free disk map produces a boundary retractiontheoremfully provedhomotopy-equivalence-reduced-homology-iso.md A homotopy equivalence induces reduced-homology isomorphismsdeffully provedordinary-neighborhood-mayer-vietoris.md The ordinary neighborhood-retract Mayer–Vietoris sequencetheoremfully provedpunctured-space-radial-deformation-retract.md A sphere strongly deformation retracts from punctured Euclidean spacedeffully provedreduced-homology-homotopy-invariance.md Homotopic maps induce the same reduced-homology maptheoremfully provedreduced-neighborhood-mayer-vietoris.md The reduced neighborhood-retract Mayer–Vietoris sequencetheoremfully provedsphere-hemisphere-neighborhood-cover.md The hemispheres have compatible neighborhood deformation retractionsdeffully provedsphere-hemisphere-stereographic-models.md Stereographic models for hemispheres and the equatordeffully provedsphere-reduced-homology-recurrence.md The reduced homology of spheres satisfies the suspension recurrencetheoremfully provedsphere-reduced-homology.md Reduced homology of spherestheoremfully provedzero-sphere-reduced-homology.md Reduced homology of the zero-spheretheoremfully provedzero-sphere-two-point-homeomorphism.md The zero-sphere is a two-point spacedeffully provedformal-viewpoint/README.md The formal viewpointarticlenot readysimplicial-and-singular/README.md Simplicial and singular homologyarticleready to statechain-homotopy-invariance.md Chain-homotopic maps induce the same homology maplemmain mathlibchain-map-homology.md A chain map induces a map on homologydefin mathlibhomotopy-equivalence-homology-iso.md A homotopy equivalence induces homology isomorphismsdeffully provedpoint-homology.md Homology of a pointtheoremfully provedrelative-homology/README.md Relative homology and exact sequencesarticleready to stateaugmented-singular-chain-complex.md The augmented singular chain complexdeffully provedgood-pair-quotient/README.md Good pairs and quotient exact sequencesarticleready to stategood-pair-data.md Good pairs and neighborhood deformation retractsstructurefully provedgood-pair-excision-diagram.md The complementary excision diagramdeffully provedgood-pair-neighborhood-quotient.md Restricting the quotient to a good-pair neighborhoodtheoremfully provedgood-pair-neighborhood-relative-homology.md Enlarging to the chosen neighborhood preserves relative homologyinstancefully provedgood-pair-point-quotient-exact-sequence.md The good-pair quotient exact sequencetheoremfully provedgood-pair-point-quotient-relative-homology.md Good-pair relative homology is reduced quotient homologytheoremfully provedgood-pair-point-quotient-sequence-naturality.md Naturality of the good-pair quotient sequencetheoremfully provedgood-pair-quotient-comparison-naturality.md The good-pair quotient comparison is naturaldeffully provedpoint-quotient-functor.md Functorial point quotients of topological pairsdeffully provedpoint-quotient-neighborhood-contraction.md The quotient neighborhood contracts to its pointdeffully provedpoint-quotient-neighborhood-excision.md The neighborhood quotient map preserves relative homologyinstancefully provedpoint-quotient-neighborhood-relative-homology.md Enlarging the quotient point preserves relative homologyinstancefully provedpoint-quotient-projection-topology.md Topology of the point-quotient projectiondeffully provedpointed-relative-reduced-homology-naturality.md The pointed relative-to-reduced comparison is naturaltheoremfully provedrelative-homology-map-isomorphism-criterion.md Componentwise isomorphisms imply a relative isomorphismtheoremfully provedstrong-deformation-retract.md Strong deformation retractsstructurefully provedpair-long-exact-sequence-naturality.md The pair long exact sequence is naturaltheoremfully provedpair-long-exact-sequence.md The long exact sequence of a pairtheoremfully provedpointed-relative-reduced-homology.md Relative homology at a basepoint is reduced homologydeffully provedpointed-zeroth-homology-splitting.md Zeroth homology splits into reduced homology and the coefficient objectdeffully provedreduced-pair-long-exact-sequence-naturality.md The reduced pair long exact sequence is naturaltheoremfully provedreduced-pair-long-exact-sequence.md The reduced long exact sequence of a nonempty pairtheoremfully provedreduced-positive-degree-comparison.md Reduced and ordinary homology agree in positive degreesdeffully provedreduced-singular-homology.md Reduced singular homologydeffully provedrelative-homology-homotopy-invariance.md Homotopic maps of pairs induce the same relative-homology maptheoremfully provedrelative-singular-chain-homotopy.md A homotopy of pairs gives a relative chain homotopydeffully provedrelative-singular-homology.md Relative singular chains and homologydeffully provedshort-exact-homology-sequence.md A short exact sequence gives an exact homology sequencetheoremin mathlibsimplicial-pair-relative-homology.md Relative homology of a simplicial-set pairdefin mathlibsingular-pair-functor.md The singular set of a topological pairdeffully provedsmall-chains-and-excision/README.md Small chains and excisionarticleready to stateaffine-barycentric-subdivision.md Affine barycentric subdivision is compatible with facestheoremfully provedaffine-chain-subdivision-homotopy.md Affine-chain subdivision is homotopic to the identitydeffully provedbarycentric-subdivision-diameter.md Barycentric subdivision contracts simplex diametertheoremfully provedbinary-cover-excision-chain-equivalence.md The binary-cover excision chain map is a homotopy equivalencetheoremfully provedbinary-cover-excision-homology-isomorphism.md Binary-cover excision induces homology isomorphismsinstancefully proveddeleted-subset-excision-homology-isomorphism.md Deleted-subset excision induces homology isomorphismsinstancefully provedeventually-small-singular-simplices.md Iterated subdivision eventually makes every singular simplex smalltheoremfully provedrelative-chain-union-devissage.md Relative excision reduces to the union subcomplextheoremfully provedsingular-chain-subdivision-homotopy.md Singular-chain subdivision is naturally homotopic to the identitydeffully provedsmall-chain-inclusion-homotopy-equivalence.md Small singular chains include by a chain-homotopy equivalencedeffully provedtopological-triple.md Topological triples and their mapsstructurefully provedtriple-chain-short-exact-sequence.md Relative chains of a triple form a short exact sequencetheoremfully provedtriple-long-exact-sequence-naturality.md The triple long exact sequence is naturaltheoremfully provedtriple-long-exact-sequence.md The long exact sequence of a tripletheoremfully provedsingular-chain-complex.md The singular chain complexdefin mathlibsingular-homology-homotopy-invariance.md Homotopic maps induce the same singular-homology maplemmain mathlibsingular-homology.md Singular homologydefin mathlibtopological-homotopy-chain-homotopy.md A topological homotopy gives a singular-chain homotopydefin mathlibtotally-disconnected-higher-homology.md Higher homology vanishes for totally disconnected spaceslemmain mathlibzeroth-homology-components.md Zeroth homology is free on path componentsdefin mathlibhomotopy-theory/README.md Homotopy theoryarticleready to stateconnections-with-cohomology/README.md Connections with cohomologyarticlenot readyelementary-methods/README.md Elementary methods of calculationarticlenot readyhomotopy-groups/README.md Homotopy groupsarticlenot readyunderlying-geometric-notions/README.md Some underlying geometric notionsarticlenot ready