Full theorem dependency graph

Project map

303 nodes · 565 dependencies. Arrows point from a prerequisite to what depends on it; dashed arrows are needed only by proofs. What the colours mean

in mathlib18Upstreamed into Mathlib.fully proved243Proved, and every prerequisite is fully proved too.ready to state29Prerequisites are stated, so this can be written down.not ready8Needs more blueprint work before it can be attempted.planned5Described in the blueprint only.

graph LR n0("Appendix"):::can_state n1("Classical CW bridge support"):::can_state n2["Classical and standard cells have isomorphic attaching arrows"]:::fully_proved n3("Compact subsets lie in finite subcomplexes"):::fully_proved n4("Compact subsets lie in a bounded skeleton"):::fully_proved n5("A successor classical skeleton has the cell-attachment quotient topology"):::fully_proved n6["Classical skeleton inclusions are abstract cell attachments"]:::fully_proved n7("Cohomology"):::can_state n8("Cohomology groups"):::not_ready n9("Cup product"):::not_ready n10("Poincaré duality"):::not_ready n11("The fundamental group"):::can_state n12("Basic constructions"):::can_state n13["Straight-line homotopy between paths"]:::fully_proved n14("The real line covers the circle"):::fully_proved n15["Winding number of a loop in the circle"]:::fully_proved n16("The fundamental group of the circle"):::fully_proved n17("A loop splits across an open cover"):::fully_proved n18("Higher spheres are simply connected"):::fully_proved n19("Borsuk–Ulam for the two-sphere"):::fully_proved n20("The circle is not a retract of the disc"):::fully_proved n21("Brouwer's fixed point theorem for the disc"):::fully_proved n22("Path homotopy is an equivalence relation"):::mathlib n23("Path concatenation gives the fundamental-group law"):::fully_proved n24["A path induces change of basepoint"]:::mathlib n25("Simply connected spaces have unique path-homotopy classes"):::mathlib n26("Convex sets have trivial fundamental group"):::mathlib n27("Euclidean two-space is distinguished by dimension"):::fully_proved n28("The fundamental theorem of algebra"):::fully_proved n29("Homotopic maps differ by basepoint change"):::fully_proved n30["A homotopy equivalence induces a fundamental-group isomorphism"]:::fully_proved n31["The fundamental group of a product"]:::fully_proved n32("Retractions and deformation retracts on the fundamental group"):::fully_proved n33("Three closed sets covering the sphere contain an antipodal pair"):::fully_proved n34["The fundamental group of the torus"]:::fully_proved n35("Covering spaces"):::can_state n36["Pointed connected covering spaces"]:::fully_proved n37["The fundamental group acts on a covering fiber"]:::mathlib n38("The induced subgroup consists of loops with closed lifts"):::fully_proved n39("Changing the lifted basepoint conjugates the image subgroup"):::fully_proved n40("Covering maps inject path-homotopy classes"):::mathlib n41("Deck transformations and quotient actions"):::can_state n42["Deck transformations and normal covers"]:::mathlib n43("A lift is determined by one point"):::mathlib n44("Covering-space actions give quotient coverings"):::fully_proved n45("A map lifts exactly when its fundamental group lands in the covering subgroup"):::fully_proved n46("Local path-connectedness ascends along a covering"):::fully_proved n47("Equal image subgroups characterize pointed cover isomorphism"):::fully_proved n48("A deck transformation is determined by one lifted point"):::fully_proved n49["The normalizer acts by deck transformations"]:::fully_proved n50("The normalizer map is surjective with kernel the covering subgroup"):::fully_proved n51["The deck group is the normalizer quotient"]:::fully_proved n52["Orbit quotients are normal and have the expected deck group"]:::fully_proved n53["The orbit-quotient fundamental group recovers the acting group"]:::fully_proved n54("Homotopies lift uniquely through a covering map"):::fully_proved n55["Semilocally simply-connected spaces"]:::fully_proved n56["The path-class universal-cover space"]:::fully_proved n57["The covering space associated to a subgroup"]:::fully_proved n58("Small nullhomotopy neighborhoods form a basis"):::fully_proved n59("The sets U[γ] form the universal-cover basis"):::fully_proved n60("The endpoint map is a covering"):::fully_proved n61["The path-class cover is path-connected"]:::fully_proved n62("The subgroup projection is a path-connected covering"):::fully_proved n63("The subgroup cover realizes the chosen subgroup"):::fully_proved n64["Pointed connected covers are classified by subgroups"]:::fully_proved n65["Sheets are cosets of the induced subgroup"]:::fully_proved n66("The path-class universal cover"):::can_state n67("A simply-connected cover maps uniquely to every pointed connected cover"):::fully_proved n68("The path-class cover is simply-connected"):::fully_proved n69["Connected covers are classified by conjugacy classes"]:::fully_proved n70("Van Kampen's theorem"):::can_state n71("A single cone attachment has a two-set open cover"):::fully_proved n72("An indexed family of cones has a two-set open cover"):::fully_proved n73("An indexed family of cone attachments is a topological pushout"):::fully_proved n74["The cone on a disk boundary is the disk"]:::fully_proved n75["An indexed cone attachment is a standard cell attachment"]:::fully_proved n76["Every abstract cell attachment has an indexed cone model"]:::fully_proved n77["The strip-enlarged cell-attachment space"]:::fully_proved n78["The strip enlargement retracts onto the attached space"]:::fully_proved n79("Hatcher's binary cover of the strip enlargement"):::fully_proved n80["The base-side cone cover retracts onto the original space"]:::fully_proved n81["The base-side auxiliary cover retracts onto the original space"]:::fully_proved n82("The cone-side cover member is contractible"):::fully_proved n83("The strip-connected upper cover is contractible"):::fully_proved n84["The auxiliary cover basepoint transports to the original basepoint"]:::fully_proved n85("The auxiliary overlap has an indexed open cover"):::fully_proved n86["The single-cone cover intersection has the homotopy type of its boundary"]:::fully_proved n87["Each overlap piece has the homotopy type of its attaching sphere"]:::fully_proved n88("An open-cover model for attached cells"):::fully_proved n89["An attachment with no cells is an isomorphism"]:::fully_proved n90["The group presentation associated to an open cover"]:::fully_proved n91("The van Kampen cover map is surjective"):::fully_proved n92("The attaching-sphere pieces generate the intersection group"):::fully_proved n93("Overlap relations vanish under the cover map"):::fully_proved n94["Cover factorizations of a loop"]:::fully_proved n95("Elementary factorization moves preserve the quotient class"):::fully_proved n96("A homotopy admits a threefold-incidence cover decomposition"):::fully_proved n97("Homotopic factorizations have the same quotient class"):::fully_proved n98("The kernel is generated by overlap relations"):::fully_proved n99["Van Kampen's quotient isomorphism"]:::fully_proved n100["Binary van Kampen is a group pushout"]:::fully_proved n101["A binary cover with a contractible second piece"]:::fully_proved n102["Attaching higher cells preserves the fundamental group"]:::fully_proved n103["The boundary of the two-disk is the circle"]:::fully_proved n104("Overlap meridians recover the attaching loops"):::fully_proved n105["A binary cover with a trivial second fundamental group"]:::fully_proved n106["Attaching 2-cells adds the attaching relations"]:::fully_proved n107("Cell-attachment support"):::can_state n108("Hatcher's auxiliary cell-attachment cover"):::can_state n109("The degree-n circle map sends the generator to the degree-n loop"):::fully_proved n110("The circle is well-pointed at one"):::fully_proved n111["The degree-n circle relation gives the cyclic group"]:::fully_proved n112("Higher-cell attachments preserve path components"):::fully_proved n113("The 2-skeleton of a path-connected CW complex is path-connected"):::fully_proved n114("A single cone attachment is a topological pushout"):::fully_proved n115["A single cone attachment is a standard cell attachment"]:::fully_proved n116("Every group admits a generators-and-relations presentation"):::fully_proved n117["Every fundamental-group element has a based disk-boundary representative"]:::fully_proved n118["The pointed wedge of a family of spaces"]:::fully_proved n119("The standard cover of a well-pointed wedge"):::fully_proved n120["The fundamental group of a wedge"]:::fully_proved n121["The fundamental group of a wedge of circles"]:::fully_proved n122["Free-group relators form a standard two-cell attachment"]:::fully_proved n123["Pointed wedges of path-connected spaces are path-connected"]:::fully_proved n124["The presentation complex has the presented fundamental group"]:::fully_proved n125["A point is one standard zero-cell"]:::fully_proved n126["Continuous maps out of a pointed wedge"]:::fully_proved n127["Collapsing the boundary of a one-disk gives the circle"]:::fully_proved n128["A wedge of circles is an indexed one-cell attachment"]:::fully_proved n129["The identity attaches an empty family of cells"]:::fully_proved n130["Eventually constant cell sequences form abstract CW complexes"]:::fully_proved n131["The presentation complex is an abstract two-dimensional CW complex"]:::fully_proved n132("Presented groups have two-dimensional presentation complexes"):::fully_proved n133("Every group is a fundamental group"):::fully_proved n134["Finite skeleta above dimension two have the same fundamental group"]:::fully_proved n135("Presentation-complex support"):::can_state n136["The cyclic presentation complex"]:::fully_proved n137["The 2-skeleton determines the fundamental group"]:::fully_proved n138("Homology"):::can_state n139("Computations and applications"):::can_state n140("Degree foundations and applications"):::can_state n141["Topological triples and their maps"]:::fully_proved n142["A chain map induces a map on homology"]:::mathlib n143["Relative homology of a simplicial-set pair"]:::mathlib n144["The singular set of a topological pair"]:::fully_proved n145["The singular chain complex"]:::mathlib n146["Singular homology"]:::mathlib n147["Relative singular chains and homology"]:::fully_proved n148["The boundary and zero horn of a standard topological simplex"]:::fully_proved n149["The augmented singular chain complex"]:::fully_proved n150["Reduced singular homology"]:::fully_proved n151["The ordered difference of the two simplices is a cycle"]:::fully_proved n152["Strong deformation retracts"]:::fully_proved n153["A standard simplex strongly deformation retracts onto its zero horn"]:::fully_proved n154["Good pairs and neighborhood deformation retracts"]:::fully_proved n155["Standard-simplex boundary and horn pairs are good"]:::fully_proved n156["Functorial point quotients of topological pairs"]:::fully_proved n157["The zero face identifies the two simplex point quotients"]:::fully_proved n158("A short exact sequence gives an exact homology sequence"):::mathlib n159("The long exact sequence of a pair"):::fully_proved n160["Reduced and ordinary homology agree in positive degrees"]:::fully_proved n161["Zeroth homology splits into reduced homology and the coefficient object"]:::fully_proved n162("The reduced long exact sequence of a nonempty pair"):::fully_proved n163["Zeroth homology is free on path components"]:::mathlib n164("Higher homology vanishes for totally disconnected spaces"):::mathlib n165("Homology of a point"):::fully_proved n166["Relative homology at a basepoint is reduced homology"]:::fully_proved n167["Topology of the point-quotient projection"]:::fully_proved n168("Restricting the quotient to a good-pair neighborhood"):::fully_proved n169("Componentwise isomorphisms imply a relative isomorphism"):::fully_proved n170("Chain-homotopic maps induce the same homology map"):::mathlib n171["A topological homotopy gives a singular-chain homotopy"]:::mathlib n172("Homotopic maps induce the same singular-homology map"):::mathlib n173["A homotopy equivalence induces homology isomorphisms"]:::fully_proved n174["Enlarging to the chosen neighborhood preserves relative homology"]:::fully_proved n175("Affine barycentric subdivision is compatible with faces"):::fully_proved n176["Affine-chain subdivision is homotopic to the identity"]:::fully_proved n177["Singular-chain subdivision is naturally homotopic to the identity"]:::fully_proved n178("Barycentric subdivision contracts simplex diameter"):::fully_proved n179("Iterated subdivision eventually makes every singular simplex small"):::fully_proved n180["Small singular chains include by a chain-homotopy equivalence"]:::fully_proved n181("Relative excision reduces to the union subcomplex"):::fully_proved n182("The binary-cover excision chain map is a homotopy equivalence"):::fully_proved n183["Binary-cover excision induces homology isomorphisms"]:::fully_proved n184["Deleted-subset excision induces homology isomorphisms"]:::fully_proved n185["The complementary excision diagram"]:::fully_proved n186["The quotient neighborhood contracts to its point"]:::fully_proved n187["Enlarging the quotient point preserves relative homology"]:::fully_proved n188["The neighborhood quotient map preserves relative homology"]:::fully_proved n189("Good-pair relative homology is reduced quotient homology"):::fully_proved n190("The pair long exact sequence is natural"):::fully_proved n191("The reduced pair long exact sequence is natural"):::fully_proved n192("The pointed relative-to-reduced comparison is natural"):::fully_proved n193["The good-pair quotient comparison is natural"]:::fully_proved n194("The zero face induces an isomorphism in relative homology"):::fully_proved n195("Relative chains of a triple form a short exact sequence"):::fully_proved n196("The long exact sequence of a triple"):::fully_proved n197("The triple connecting map sends a relative cycle to its boundary"):::fully_proved n198["A homotopy of pairs gives a relative chain homotopy"]:::fully_proved n199("Homotopic maps of pairs induce the same relative-homology map"):::fully_proved n200("The identity simplex generates relative simplex homology"):::fully_proved n201("The first simplex computes homology relative to the second"):::fully_proved n202("Homotopic maps induce the same reduced-homology map"):::fully_proved n203["A homotopy equivalence induces reduced-homology isomorphisms"]:::fully_proved n204("Reduced homology of a contractible space vanishes"):::fully_proved n205["A contractible subspace identifies reduced and relative homology"]:::fully_proved n206("The double-simplex difference generates reduced homology"):::fully_proved n207("Swapping the double simplex negates its fundamental class"):::fully_proved n208["The standard simplex pair is homeomorphic to the disk pair"]:::fully_proved n209["The double simplex is a sphere"]:::fully_proved n210("Coordinate sign changes on the sphere"):::fully_proved n211["The ordered class orients ordinary sphere homology"]:::fully_proved n212("Degree is the multiplier of the ordered sphere class"):::fully_proved n213("The formal properties of degree"):::fully_proved n214("A sphere reflection has degree minus one"):::fully_proved n215("The antipodal map has degree determined by dimension"):::fully_proved n216("A fixed-point-free sphere map has antipodal degree"):::fully_proved n217["Degree gives a character of a sphere action"]:::fully_proved n218("Only the antipodal group acts freely on an even sphere"):::fully_proved n219["Stereographic models for hemispheres and the equator"]:::fully_proved n220["A punctured sphere is Euclidean space"]:::fully_proved n221("A nonsurjective sphere map has degree zero"):::fully_proved n222["Tangent vector fields and normalization"]:::fully_proved n223("A nonvanishing tangent field forces odd dimension"):::fully_proved n224["Odd spheres have a nonvanishing tangent field"]:::fully_proved n225("A sphere has a nonvanishing tangent field exactly in odd dimension"):::fully_proved n226("Local degree and the sum over a finite fiber"):::can_state n227["The ordered sphere class orients local homology"]:::fully_proved n228["The coproduct pair of a family of pointed spaces"]:::fully_proved n229["The coproduct of a family of topological pairs"]:::fully_proved n230["Relative singular chains commute with topological coproducts"]:::fully_proved n231["Relative chains commute with coproducts of arbitrary pairs"]:::can_state n232["Relative homology commutes with exact coproducts"]:::fully_proved n233["Relative homology commutes with coproducts of arbitrary pairs"]:::planned n234("Local homology is unchanged on an open neighborhood"):::fully_proved n235("Deleted-pair homology is local on an open neighborhood"):::fully_proved n236["A disjoint open family is homeomorphic to its sigma type"]:::fully_proved n237["Disjoint punctured neighborhoods form the deleted union pair"]:::fully_proved n238["An isolated preimage gives a map of punctured pairs"]:::fully_proved n239["A finite sphere-map fiber has disjoint isolated neighborhoods"]:::fully_proved n240("The disjoint local pairs excise to the finite-puncture pair"):::fully_proved n241["Finite-puncture homology is the coproduct of the local groups"]:::planned n242("Finite-puncture projections have the diagonal matrix"):::planned n243("The finite-fiber pair map carries the global degree"):::fully_proved n244("The finite-puncture class is the sum of the local classes"):::planned n245("Local degree on a chosen isolated neighborhood"):::fully_proved n246("Local degree is unchanged when the neighborhood shrinks"):::fully_proved n247("Local degree is independent of its neighborhood"):::fully_proved n248("The finite-fiber pair map acts by the local degrees"):::fully_proved n249("Degree is the sum of the local degrees"):::planned n250("A local homeomorphism has local degree plus or minus one"):::can_state n251("Local homology and invariance of dimension"):::can_state n252["Relative homology in a contractible ambient space"]:::fully_proved n253["The binary-cover Mayer–Vietoris chain complex"]:::fully_proved n254("Binary-cover chains form a short exact sequence"):::fully_proved n255("The binary-cover Mayer–Vietoris sequence"):::fully_proved n256("The ordinary neighborhood-retract Mayer–Vietoris sequence"):::fully_proved n257["A sphere strongly deformation retracts from punctured Euclidean space"]:::fully_proved n258["Small augmented chains include by a chain-homotopy equivalence"]:::fully_proved n259("Augmented binary-cover chains form a short exact sequence"):::fully_proved n260("The reduced binary-cover Mayer–Vietoris sequence"):::fully_proved n261("The reduced neighborhood-retract Mayer–Vietoris sequence"):::fully_proved n262["A closed ball strongly deformation retracts from Euclidean space"]:::fully_proved n263["The hemispheres have compatible neighborhood deformation retractions"]:::fully_proved n264("The reduced homology of spheres satisfies the suspension recurrence"):::fully_proved n265["The zero-sphere is a two-point space"]:::fully_proved n266("Reduced homology of the zero-sphere"):::fully_proved n267("Reduced homology of spheres"):::fully_proved n268("Local homology of positive-dimensional Euclidean space"):::fully_proved n269("Homeomorphic nonempty Euclidean open sets have equal dimension"):::fully_proved n270("Mayer–Vietoris sequences"):::can_state n271("Post-excision applications"):::can_state n272["Intersections of CW subcomplexes"]:::fully_proved n273["The radial collar of a cell boundary"]:::fully_proved n274["A common regular-neighborhood system for subcomplexes"]:::fully_proved n275["A regular neighborhood strongly deformation retracts onto its subcomplex"]:::fully_proved n276("Subcomplex decompositions admit compatible neighborhoods"):::fully_proved n277("Excision holds for a union of CW subcomplexes"):::fully_proved n278("CW-subcomplex regular neighborhoods"):::can_state n279["The mapping cone of a topological pair"]:::fully_proved n280["The mapping-cone cover has the relative homology of the original pair"]:::fully_proved n281["Relative homology is reduced homology of the mapping cone"]:::fully_proved n282["The pointed wedge is the point quotient of the sigma pair"]:::fully_proved n283("A nonempty coproduct of pointed good pairs is good"):::fully_proved n284("Reduced homology of a wedge is the direct sum of the summands"):::fully_proved n285("Mayer–Vietoris transport, sphere homology, and Brouwer"):::can_state n286("The boundary sphere is not a retract of the disk"):::fully_proved n287("A fixed-point-free disk map produces a boundary retraction"):::fully_proved n288("Brouwer's fixed-point theorem for disks"):::fully_proved n289("The formal viewpoint"):::not_ready n290("Simplicial and singular homology"):::can_state n291("Relative homology and exact sequences"):::can_state n292("Good pairs and quotient exact sequences"):::can_state n293("The good-pair quotient exact sequence"):::fully_proved n294("Naturality of the good-pair quotient sequence"):::fully_proved n295("Small chains and excision"):::can_state n296("The triple long exact sequence is natural"):::fully_proved n297("Homotopy theory"):::can_state n298("Connections with cohomology"):::not_ready n299("Elementary methods of calculation"):::not_ready n300("Homotopy groups"):::not_ready n301("Algebraic Topology (Hatcher) roadmap"):::can_state n302("Some underlying geometric notions"):::not_ready n2 --> n5 n2 --> n6 n4 -.-> n113 n4 -.-> n137 n5 --> n6 n6 -.-> n113 n6 -.-> n134 n3 -.-> n4 n19 --> n33 n14 -.-> n16 n14 --> n15 n16 --> n19 n16 --> n27 n16 --> n28 n16 --> n20 n16 --> n34 n16 --> n106 n16 -.-> n104 n16 --> n109 n16 --> n111 n16 --> n103 n16 --> n121 n23 --> n24 n17 --> n18 n17 -.-> n91 n20 --> n21 n22 --> n23 n22 --> n25 n31 --> n34 n32 --> n106 n32 -.-> n101 n25 -.-> n26 n18 --> n19 n18 --> n27 n18 -.-> n102 n15 --> n16 n36 --> n51 n36 --> n48 n36 --> n49 n36 --> n64 n36 --> n47 n36 --> n67 n36 --> n69 n38 -.-> n39 n38 -.-> n50 n38 -.-> n65 n38 -.-> n63 n38 -.-> n68 n39 -.-> n49 n39 -.-> n69 n40 -.-> n68 n44 --> n52 n44 --> n53 n51 -.-> n53 n48 -.-> n49 n48 -.-> n50 n42 --> n44 n42 --> n51 n42 --> n48 n42 --> n49 n42 --> n52 n49 --> n50 n50 -.-> n51 n52 -.-> n53 n45 -.-> n47 n45 -.-> n67 n46 -.-> n47 n46 -.-> n67 n37 --> n38 n37 -.-> n39 n37 -.-> n51 n37 --> n49 n37 -.-> n65 n64 -.-> n69 n47 -.-> n48 n47 -.-> n64 n63 -.-> n64 n62 -.-> n63 n57 -.-> n64 n57 --> n63 n57 --> n62 n43 -.-> n44 n43 -.-> n48 n43 -.-> n52 n43 -.-> n47 n43 -.-> n67 n58 -.-> n59 n55 --> n64 n55 --> n58 n55 --> n56 n55 --> n69 n59 -.-> n62 n59 -.-> n60 n59 -.-> n61 n60 -.-> n62 n60 -.-> n68 n61 -.-> n62 n61 -.-> n68 n56 --> n57 n56 --> n59 n56 --> n60 n56 --> n61 n56 --> n68 n102 -.-> n134 n106 --> n136 n106 --> n124 n106 --> n122 n92 -.-> n102 n92 --> n106 n100 -.-> n101 n100 -.-> n105 n88 -.-> n102 n88 --> n106 n88 --> n92 n76 --> n88 n76 --> n104 n76 --> n89 n76 -.-> n112 n78 -.-> n88 n81 -.-> n88 n81 --> n84 n81 -.-> n112 n79 -.-> n88 n79 --> n81 n79 --> n84 n79 --> n85 n79 --> n83 n77 --> n88 n77 --> n78 n77 --> n79 n84 -.-> n102 n84 --> n106 n84 -.-> n88 n84 --> n104 n104 --> n106 n85 -.-> n88 n85 --> n87 n87 -.-> n88 n87 --> n104 n83 -.-> n88 n101 -.-> n102 n105 --> n106 n109 --> n136 n110 --> n121 n74 --> n75 n74 --> n115 n74 --> n127 n111 --> n136 n103 --> n106 n103 --> n104 n103 --> n136 n103 --> n117 n89 -.-> n102 n89 --> n106 n89 -.-> n112 n112 -.-> n113 n112 -.-> n134 n75 --> n76 n75 --> n136 n75 --> n125 n75 --> n122 n75 --> n128 n72 --> n77 n72 --> n89 n72 -.-> n112 n72 --> n73 n72 --> n136 n73 --> n75 n113 -.-> n134 n80 -.-> n81 n80 -.-> n280 n86 -.-> n87 n86 -.-> n280 n71 --> n74 n71 --> n72 n71 --> n80 n71 --> n86 n71 --> n114 n71 --> n82 n71 --> n127 n71 --> n279 n114 --> n115 n114 -.-> n279 n82 -.-> n83 n82 -.-> n281 n94 --> n95 n94 --> n97 n90 --> n94 n90 --> n93 n90 --> n95 n90 --> n97 n90 --> n98 n90 --> n91 n93 -.-> n98 n93 --> n99 n116 -.-> n133 n95 -.-> n97 n134 -.-> n137 n97 -.-> n98 n96 -.-> n97 n118 --> n123 n118 --> n126 n118 --> n128 n118 --> n120 n118 --> n119 n118 --> n282 n127 --> n128 n117 --> n122 n129 --> n131 n130 --> n131 n125 --> n131 n123 --> n124 n126 --> n128 n126 -.-> n282 n131 -.-> n132 n124 -.-> n132 n132 -.-> n133 n122 --> n131 n122 --> n124 n128 --> n131 n98 -.-> n99 n99 -.-> n100 n99 -.-> n120 n91 -.-> n92 n91 -.-> n99 n121 --> n124 n121 --> n122 n120 --> n121 n119 --> n120 n119 -.-> n284 n119 --> n256 n215 -.-> n216 n215 -.-> n223 n213 -.-> n215 n213 -.-> n214 n213 -.-> n216 n213 --> n217 n213 -.-> n223 n213 --> n250 n214 -.-> n215 n207 --> n210 n216 -.-> n218 n211 --> n212 n211 --> n227 n224 -.-> n225 n220 -.-> n221 n220 --> n227 n217 --> n218 n210 --> n215 n210 --> n214 n210 --> n218 n212 --> n213 n212 --> n214 n212 --> n216 n212 --> n221 n212 --> n243 n223 -.-> n225 n222 --> n225 n222 --> n224 n222 --> n223 n235 --> n240 n236 --> n237 n237 --> n240 n248 --> n249 n239 --> n240 n239 --> n243 n241 --> n242 n244 --> n249 n240 --> n248 n240 --> n241 n242 --> n244 n243 --> n249 n243 --> n244 n238 --> n239 n238 --> n245 n246 --> n247 n247 --> n248 n247 --> n250 n245 --> n246 n231 --> n233 n233 --> n241 n229 --> n237 n229 --> n231 n227 --> n244 n227 --> n243 n227 --> n245 n252 -.-> n268 n234 --> n235 n234 --> n237 n234 --> n238 n234 -.-> n269 n234 --> n268 n268 -.-> n269 n259 --> n260 n253 --> n259 n253 --> n254 n254 -.-> n259 n254 --> n255 n255 --> n256 n260 --> n261 n258 --> n259 n258 -.-> n260 n205 --> n227 n205 -.-> n206 n205 --> n281 n273 --> n274 n275 --> n276 n274 --> n275 n274 --> n276 n272 --> n274 n272 --> n276 n276 -.-> n277 n206 --> n207 n206 --> n209 n151 --> n207 n151 --> n206 n151 --> n201 n151 --> n209 n201 -.-> n206 n209 --> n211 n209 --> n210 n280 --> n281 n279 --> n280 n279 --> n281 n282 --> n284 n232 --> n233 n232 --> n284 n200 -.-> n206 n283 --> n284 n228 --> n229 n228 --> n282 n228 --> n283 n228 --> n230 n230 -.-> n231 n230 --> n232 n155 -.-> n201 n155 -.-> n194 n148 --> n151 n148 --> n200 n148 --> n155 n148 --> n208 n148 --> n157 n148 --> n194 n148 --> n153 n208 --> n209 n157 -.-> n201 n157 -.-> n194 n194 -.-> n201 n194 -.-> n200 n153 -.-> n200 n197 -.-> n200 n262 -.-> n263 n204 -.-> n221 n204 -.-> n252 n204 -.-> n205 n204 -.-> n284 n204 -.-> n286 n204 -.-> n264 n286 -.-> n288 n287 -.-> n288 n203 -.-> n268 n203 -.-> n204 n203 -.-> n261 n256 --> n262 n256 --> n257 n256 --> n261 n256 --> n263 n257 -.-> n268 n257 -.-> n263 n202 -.-> n203 n261 -.-> n264 n263 -.-> n264 n219 -.-> n220 n219 --> n263 n219 -.-> n264 n267 -.-> n268 n267 -.-> n286 n264 -.-> n267 n266 -.-> n267 n265 -.-> n266 n170 -.-> n202 n170 -.-> n199 n170 -.-> n183 n170 -.-> n172 n142 --> n170 n142 -.-> n173 n142 --> n158 n142 --> n143 n142 --> n172 n173 -.-> n277 n173 -.-> n280 n173 -.-> n256 n173 -.-> n174 n173 -.-> n187 n165 -.-> n200 n165 -.-> n166 n149 --> n259 n149 --> n258 n149 -.-> n191 n149 --> n150 n154 --> n283 n154 --> n155 n154 --> n168 n154 --> n174 n154 --> n189 n154 --> n193 n185 -.-> n189 n185 --> n188 n168 --> n185 n168 --> n186 n168 --> n187 n174 --> n185 n174 -.-> n189 n293 --> n294 n189 -.-> n201 n189 -.-> n194 n189 --> n193 n193 -.-> n201 n193 -.-> n194 n193 -.-> n284 n193 --> n293 n193 -.-> n294 n156 --> n282 n156 --> n157 n156 --> n189 n156 --> n193 n156 --> n167 n186 -.-> n187 n188 -.-> n189 n187 -.-> n189 n167 --> n185 n167 --> n168 n192 --> n205 n192 -.-> n206 n192 -.-> n284 n192 -.-> n294 n192 --> n193 n169 -.-> n277 n169 -.-> n280 n169 -.-> n174 n169 -.-> n187 n152 --> n275 n152 --> n283 n152 --> n153 n152 --> n256 n152 --> n154 n159 -.-> n169 n159 --> n190 n159 --> n162 n190 -.-> n191 n166 --> n228 n166 --> n284 n166 -.-> n204 n166 --> n189 n166 --> n192 n161 -.-> n266 n161 --> n162 n162 --> n252 n162 -.-> n205 n162 --> n293 n162 -.-> n166 n162 --> n191 n191 -.-> n294 n191 -.-> n192 n160 --> n211 n160 -.-> n266 n160 --> n162 n150 --> n260 n150 --> n205 n150 --> n151 n150 --> n281 n150 --> n204 n150 --> n203 n150 --> n202 n150 --> n267 n150 --> n264 n150 --> n266 n150 --> n166 n150 --> n161 n150 --> n160 n199 -.-> n200 n198 -.-> n199 n147 --> n235 n147 --> n231 n147 --> n234 n147 --> n205 n147 --> n277 n147 --> n280 n147 --> n281 n147 --> n230 n147 --> n148 n147 --> n169 n147 --> n159 n147 --> n190 n147 --> n166 n147 --> n199 n147 --> n198 n147 --> n182 n147 --> n183 n147 --> n184 n147 --> n195 n158 -.-> n255 n158 -.-> n260 n158 -.-> n159 n158 -.-> n190 n158 -.-> n191 n158 -.-> n196 n158 -.-> n296 n143 -.-> n159 n143 --> n144 n143 --> n181 n143 -.-> n195 n144 --> n147 n175 --> n176 n175 --> n178 n175 --> n177 n176 -.-> n177 n178 -.-> n179 n182 --> n255 n182 --> n279 n182 --> n183 n183 -.-> n235 n183 -.-> n277 n183 -.-> n281 n183 -.-> n194 n183 -.-> n184 n184 -.-> n234 n184 --> n185 n184 -.-> n188 n179 --> n253 n179 --> n180 n181 -.-> n182 n177 --> n179 n177 -.-> n180 n180 -.-> n255 n180 --> n258 n180 -.-> n182 n141 --> n148 n141 --> n195 n195 --> n197 n195 --> n196 n196 -.-> n200 n196 -.-> n197 n196 --> n296 n145 --> n253 n145 --> n149 n145 --> n177 n145 --> n146 n145 --> n172 n145 --> n171 n146 --> n173 n146 --> n165 n146 --> n159 n146 --> n160 n146 --> n147 n146 --> n164 n146 --> n163 n172 -.-> n173 n171 -.-> n202 n171 -.-> n198 n171 -.-> n172 n164 -.-> n266 n164 -.-> n165 n163 -.-> n266 n163 -.-> n165 click n0 "../roadmap/appendix/index.html" "Appendix — 1 item · 1 ready to state" click n1 "../roadmap/appendix/classical-cw-bridge/index.html" "Classical CW bridge support — 1 item · 1 ready to state" click n2 "../roadmap/appendix/classical-cw-bridge/index.html#classical-cell-arrow-iso" "Classical and standard cells have isomorphic attaching arrows — 1 item · 1 fully proved" click n3 "../roadmap/appendix/index.html#compact-subspace-finite-subcomplex" "Compact subsets lie in finite subcomplexes — 1 item · 1 fully proved" click n4 "../roadmap/appendix/classical-cw-bridge/index.html#compact-subset-bounded-skeleton" "Compact subsets lie in a bounded skeleton — 1 item · 1 fully proved" click n5 "../roadmap/appendix/classical-cw-bridge/index.html#successor-skeleton-quotient" "A successor classical skeleton has the cell-attachment quotient topology — 1 item · 1 fully proved" click n6 "../roadmap/appendix/index.html#classical-skeleton-cell-attachment" "Classical skeleton inclusions are abstract cell attachments — 1 item · 1 fully proved" click n7 "../roadmap/cohomology/index.html" "Cohomology — 1 item · 1 ready to state" click n8 "../roadmap/cohomology/cohomology-groups/index.html" "Cohomology groups — 1 item · 1 not ready" click n9 "../roadmap/cohomology/cup-product/index.html" "Cup product — 1 item · 1 not ready" click n10 "../roadmap/cohomology/poincare-duality/index.html" "Poincaré duality — 1 item · 1 not ready" click n11 "../roadmap/fundamental-group/index.html" "The fundamental group — 1 item · 1 ready to state" click n12 "../roadmap/fundamental-group/basic-constructions/index.html" "Basic constructions — 1 item · 1 ready to state" click n13 "../roadmap/fundamental-group/basic-constructions/index.html#affine-path-homotopy" "Straight-line homotopy between paths — 1 item · 1 fully proved" click n14 "../roadmap/fundamental-group/basic-constructions/index.html#circle-covering" "The real line covers the circle — 1 item · 1 fully proved" click n15 "../roadmap/fundamental-group/basic-constructions/index.html#winding-number" "Winding number of a loop in the circle — 1 item · 1 fully proved" click n16 "../roadmap/fundamental-group/basic-constructions/index.html#fundamental-group-circle" "The fundamental group of the circle — 1 item · 1 fully proved" click n17 "../roadmap/fundamental-group/basic-constructions/index.html#loop-in-open-cover" "A loop splits across an open cover — 1 item · 1 fully proved" click n18 "../roadmap/fundamental-group/basic-constructions/index.html#sphere-simply-connected" "Higher spheres are simply connected — 1 item · 1 fully proved" click n19 "../roadmap/fundamental-group/basic-constructions/index.html#borsuk-ulam-sphere" "Borsuk–Ulam for the two-sphere — 1 item · 1 fully proved" click n20 "../roadmap/fundamental-group/basic-constructions/index.html#no-retraction-disc" "The circle is not a retract of the disc — 1 item · 1 fully proved" click n21 "../roadmap/fundamental-group/basic-constructions/index.html#brouwer-disc" "Brouwer's fixed point theorem for the disc — 1 item · 1 fully proved" click n22 "../roadmap/fundamental-group/basic-constructions/index.html#path-homotopy-equivalence" "Path homotopy is an equivalence relation — 1 item · 1 in mathlib" click n23 "../roadmap/fundamental-group/basic-constructions/index.html#fundamental-group-law" "Path concatenation gives the fundamental-group law — 1 item · 1 fully proved" click n24 "../roadmap/fundamental-group/basic-constructions/index.html#change-of-basepoint" "A path induces change of basepoint — 1 item · 1 in mathlib" click n25 "../roadmap/fundamental-group/basic-constructions/index.html#simply-connected-unique-path-classes" "Simply connected spaces have unique path-homotopy classes — 1 item · 1 in mathlib" click n26 "../roadmap/fundamental-group/basic-constructions/index.html#convex-trivial-fundamental-group" "Convex sets have trivial fundamental group — 1 item · 1 in mathlib" click n27 "../roadmap/fundamental-group/basic-constructions/index.html#euclidean-two-not-homeomorphic" "Euclidean two-space is distinguished by dimension — 1 item · 1 fully proved" click n28 "../roadmap/fundamental-group/basic-constructions/index.html#fundamental-theorem-algebra" "The fundamental theorem of algebra — 1 item · 1 fully proved" click n29 "../roadmap/fundamental-group/basic-constructions/index.html#homotopic-maps-fundamental-group" "Homotopic maps differ by basepoint change — 1 item · 1 fully proved" click n30 "../roadmap/fundamental-group/basic-constructions/index.html#homotopy-equivalence-fundamental-group" "A homotopy equivalence induces a fundamental-group isomorphism — 1 item · 1 fully proved" click n31 "../roadmap/fundamental-group/basic-constructions/index.html#product-fundamental-group" "The fundamental group of a product — 1 item · 1 fully proved" click n32 "../roadmap/fundamental-group/basic-constructions/index.html#retractions-fundamental-group" "Retractions and deformation retracts on the fundamental group — 1 item · 1 fully proved" click n33 "../roadmap/fundamental-group/basic-constructions/index.html#three-closed-sets-antipodal" "Three closed sets covering the sphere contain an antipodal pair — 1 item · 1 fully proved" click n34 "../roadmap/fundamental-group/basic-constructions/index.html#torus-fundamental-group" "The fundamental group of the torus — 1 item · 1 fully proved" click n35 "../roadmap/fundamental-group/covering-spaces/index.html" "Covering spaces — 1 item · 1 ready to state" click n36 "../roadmap/fundamental-group/covering-spaces/index.html#based-connected-cover" "Pointed connected covering spaces — 1 item · 1 fully proved" click n37 "../roadmap/fundamental-group/covering-spaces/index.html#monodromy-action" "The fundamental group acts on a covering fiber — 1 item · 1 in mathlib" click n38 "../roadmap/fundamental-group/covering-spaces/index.html#closed-lift-image" "The induced subgroup consists of loops with closed lifts — 1 item · 1 fully proved" click n39 "../roadmap/fundamental-group/covering-spaces/index.html#cover-basepoint-conjugacy" "Changing the lifted basepoint conjugates the image subgroup — 1 item · 1 fully proved" click n40 "../roadmap/fundamental-group/covering-spaces/index.html#covering-injective-path-classes" "Covering maps inject path-homotopy classes — 1 item · 1 in mathlib" click n41 "../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html" "Deck transformations and quotient actions — 1 item · 1 ready to state" click n42 "../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#deck-transformation-group" "Deck transformations and normal covers — 1 item · 1 in mathlib" click n43 "../roadmap/fundamental-group/covering-spaces/index.html#unique-lifting" "A lift is determined by one point — 1 item · 1 in mathlib" click n44 "../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#covering-space-action" "Covering-space actions give quotient coverings — 1 item · 1 fully proved" click n45 "../roadmap/fundamental-group/covering-spaces/index.html#lifting-criterion" "A map lifts exactly when its fundamental group lands in the covering subgroup — 1 item · 1 fully proved" click n46 "../roadmap/fundamental-group/covering-spaces/index.html#locally-path-connected-total-space" "Local path-connectedness ascends along a covering — 1 item · 1 fully proved" click n47 "../roadmap/fundamental-group/covering-spaces/index.html#pointed-cover-rigidity" "Equal image subgroups characterize pointed cover isomorphism — 1 item · 1 fully proved" click n48 "../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#deck-realization" "A deck transformation is determined by one lifted point — 1 item · 1 fully proved" click n49 "../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#normalizer-to-deck" "The normalizer acts by deck transformations — 1 item · 1 fully proved" click n50 "../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#normalizer-to-deck-exactness" "The normalizer map is surjective with kernel the covering subgroup — 1 item · 1 fully proved" click n51 "../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#deck-group-calculation" "The deck group is the normalizer quotient — 1 item · 1 fully proved" click n52 "../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#orbit-quotient-deck-group" "Orbit quotients are normal and have the expected deck group — 1 item · 1 fully proved" click n53 "../roadmap/fundamental-group/covering-spaces/deck-transformations/index.html#orbit-quotient-fundamental-group" "The orbit-quotient fundamental group recovers the acting group — 1 item · 1 fully proved" click n54 "../roadmap/fundamental-group/covering-spaces/index.html#homotopy-lifting" "Homotopies lift uniquely through a covering map — 1 item · 1 fully proved" click n55 "../roadmap/fundamental-group/covering-spaces/universal-cover/index.html#semilocally-simply-connected" "Semilocally simply-connected spaces — 1 item · 1 fully proved" click n56 "../roadmap/fundamental-group/covering-spaces/universal-cover/index.html#universal-cover-path-space" "The path-class universal-cover space — 1 item · 1 fully proved" click n57 "../roadmap/fundamental-group/covering-spaces/index.html#subgroup-cover-space" "The covering space associated to a subgroup — 1 item · 1 fully proved" click n58 "../roadmap/fundamental-group/covering-spaces/universal-cover/index.html#nullhomotopic-open-basis" "Small nullhomotopy neighborhoods form a basis — 1 item · 1 fully proved" click n59 "../roadmap/fundamental-group/covering-spaces/universal-cover/index.html#universal-cover-basis" "The sets U[γ] form the universal-cover basis — 1 item · 1 fully proved" click n60 "../roadmap/fundamental-group/covering-spaces/universal-cover/index.html#universal-cover-is-covering" "The endpoint map is a covering — 1 item · 1 fully proved" click n61 "../roadmap/fundamental-group/covering-spaces/universal-cover/index.html#universal-cover-path-connected" "The path-class cover is path-connected — 1 item · 1 fully proved" click n62 "../roadmap/fundamental-group/covering-spaces/index.html#subgroup-cover-is-covering" "The subgroup projection is a path-connected covering — 1 item · 1 fully proved" click n63 "../roadmap/fundamental-group/covering-spaces/index.html#subgroup-cover-image" "The subgroup cover realizes the chosen subgroup — 1 item · 1 fully proved" click n64 "../roadmap/fundamental-group/covering-spaces/index.html#pointed-cover-classification" "Pointed connected covers are classified by subgroups — 1 item · 1 fully proved" click n65 "../roadmap/fundamental-group/covering-spaces/index.html#sheet-index" "Sheets are cosets of the induced subgroup — 1 item · 1 fully proved" click n66 "../roadmap/fundamental-group/covering-spaces/universal-cover/index.html" "The path-class universal cover — 1 item · 1 ready to state" click n67 "../roadmap/fundamental-group/covering-spaces/index.html#universal-cover-initial" "A simply-connected cover maps uniquely to every pointed connected cover — 1 item · 1 fully proved" click n68 "../roadmap/fundamental-group/covering-spaces/universal-cover/index.html#universal-cover-simply-connected" "The path-class cover is simply-connected — 1 item · 1 fully proved" click n69 "../roadmap/fundamental-group/covering-spaces/index.html#unpointed-cover-classification" "Connected covers are classified by conjugacy classes — 1 item · 1 fully proved" click n70 "../roadmap/fundamental-group/van-kampen/index.html" "Van Kampen's theorem — 1 item · 1 ready to state" click n71 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#single-cone-open-cover" "A single cone attachment has a two-set open cover — 1 item · 1 fully proved" click n72 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#indexed-cone-open-cover" "An indexed family of cones has a two-set open cover — 1 item · 1 fully proved" click n73 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#indexed-cone-pushout" "An indexed family of cone attachments is a topological pushout — 1 item · 1 fully proved" click n74 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#cone-disk-homeomorphism" "The cone on a disk boundary is the disk — 1 item · 1 fully proved" click n75 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#indexed-basic-cell-attachment" "An indexed cone attachment is a standard cell attachment — 1 item · 1 fully proved" click n76 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#abstract-cell-attachment-indexed-model" "Every abstract cell attachment has an indexed cone model — 1 item · 1 fully proved" click n77 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/auxiliary/index.html#auxiliary-cell-attachment-space" "The strip-enlarged cell-attachment space — 1 item · 1 fully proved" click n78 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/auxiliary/index.html#auxiliary-attachment-retract" "The strip enlargement retracts onto the attached space — 1 item · 1 fully proved" click n79 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/auxiliary/index.html#auxiliary-cell-attachment-open-cover" "Hatcher's binary cover of the strip enlargement — 1 item · 1 fully proved" click n80 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#single-cone-base-retract" "The base-side cone cover retracts onto the original space — 1 item · 1 fully proved" click n81 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/auxiliary/index.html#auxiliary-base-cover-retract" "The base-side auxiliary cover retracts onto the original space — 1 item · 1 fully proved" click n82 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#single-cone-upper-contractible" "The cone-side cover member is contractible — 1 item · 1 fully proved" click n83 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/auxiliary/index.html#auxiliary-upper-cover-contractible" "The strip-connected upper cover is contractible — 1 item · 1 fully proved" click n84 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/auxiliary/index.html#auxiliary-cover-basepoint-transport" "The auxiliary cover basepoint transports to the original basepoint — 1 item · 1 fully proved" click n85 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/auxiliary/index.html#auxiliary-overlap-open-cover" "The auxiliary overlap has an indexed open cover — 1 item · 1 fully proved" click n86 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#single-cone-intersection" "The single-cone cover intersection has the homotopy type of its boundary — 1 item · 1 fully proved" click n87 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/auxiliary/index.html#auxiliary-overlap-piece-sphere" "Each overlap piece has the homotopy type of its attaching sphere — 1 item · 1 fully proved" click n88 "../roadmap/fundamental-group/van-kampen/index.html#cell-attachment-cover-model" "An open-cover model for attached cells — 1 item · 1 fully proved" click n89 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#empty-cell-attachment-iso" "An attachment with no cells is an isomorphism — 1 item · 1 fully proved" click n90 "../roadmap/fundamental-group/van-kampen/index.html#cover-group-presentation" "The group presentation associated to an open cover — 1 item · 1 fully proved" click n91 "../roadmap/fundamental-group/van-kampen/index.html#van-kampen-surjective" "The van Kampen cover map is surjective — 1 item · 1 fully proved" click n92 "../roadmap/fundamental-group/van-kampen/index.html#attaching-spheres-generate-intersection" "The attaching-sphere pieces generate the intersection group — 1 item · 1 fully proved" click n93 "../roadmap/fundamental-group/van-kampen/index.html#cover-map-relations" "Overlap relations vanish under the cover map — 1 item · 1 fully proved" click n94 "../roadmap/fundamental-group/van-kampen/index.html#cover-factorization" "Cover factorizations of a loop — 1 item · 1 fully proved" click n95 "../roadmap/fundamental-group/van-kampen/index.html#factorization-moves" "Elementary factorization moves preserve the quotient class — 1 item · 1 fully proved" click n96 "../roadmap/fundamental-group/van-kampen/index.html#homotopy-cover-decomposition" "A homotopy admits a threefold-incidence cover decomposition — 1 item · 1 fully proved" click n97 "../roadmap/fundamental-group/van-kampen/index.html#homotopic-factorizations" "Homotopic factorizations have the same quotient class — 1 item · 1 fully proved" click n98 "../roadmap/fundamental-group/van-kampen/index.html#van-kampen-kernel" "The kernel is generated by overlap relations — 1 item · 1 fully proved" click n99 "../roadmap/fundamental-group/van-kampen/index.html#van-kampen-quotient" "Van Kampen's quotient isomorphism — 1 item · 1 fully proved" click n100 "../roadmap/fundamental-group/van-kampen/index.html#binary-van-kampen-pushout" "Binary van Kampen is a group pushout — 1 item · 1 fully proved" click n101 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#binary-cover-contractible-piece" "A binary cover with a contractible second piece — 1 item · 1 fully proved" click n102 "../roadmap/fundamental-group/van-kampen/index.html#attach-higher-cells-fundamental-group" "Attaching higher cells preserves the fundamental group — 1 item · 1 fully proved" click n103 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#disk-boundary-two-circle" "The boundary of the two-disk is the circle — 1 item · 1 fully proved" click n104 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/auxiliary/index.html#auxiliary-overlap-attaching-map" "Overlap meridians recover the attaching loops — 1 item · 1 fully proved" click n105 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#binary-cover-trivial-piece-quotient" "A binary cover with a trivial second fundamental group — 1 item · 1 fully proved" click n106 "../roadmap/fundamental-group/van-kampen/index.html#attach-two-cells-fundamental-group" "Attaching 2-cells adds the attaching relations — 1 item · 1 fully proved" click n107 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html" "Cell-attachment support — 1 item · 1 ready to state" click n108 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/auxiliary/index.html" "Hatcher's auxiliary cell-attachment cover — 1 item · 1 ready to state" click n109 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#circle-degree-map" "The degree-n circle map sends the generator to the degree-n loop — 1 item · 1 fully proved" click n110 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#circle-well-pointed" "The circle is well-pointed at one — 1 item · 1 fully proved" click n111 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#cyclic-relation-quotient" "The degree-n circle relation gives the cyclic group — 1 item · 1 fully proved" click n112 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#higher-cell-attachment-path-components" "Higher-cell attachments preserve path components — 1 item · 1 fully proved" click n113 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#path-connected-two-skeleton" "The 2-skeleton of a path-connected CW complex is path-connected — 1 item · 1 fully proved" click n114 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#single-cone-pushout" "A single cone attachment is a topological pushout — 1 item · 1 fully proved" click n115 "../roadmap/fundamental-group/van-kampen/cell-attachment-support/index.html#single-basic-cell-attachment" "A single cone attachment is a standard cell attachment — 1 item · 1 fully proved" click n116 "../roadmap/fundamental-group/van-kampen/index.html#every-group-presentation" "Every group admits a generators-and-relations presentation — 1 item · 1 fully proved" click n117 "../roadmap/fundamental-group/van-kampen/presentation-complex/index.html#disk-boundary-fundamental-group-representative" "Every fundamental-group element has a based disk-boundary representative — 1 item · 1 fully proved" click n118 "../roadmap/fundamental-group/van-kampen/index.html#pointed-wedge" "The pointed wedge of a family of spaces — 1 item · 1 fully proved" click n119 "../roadmap/fundamental-group/van-kampen/index.html#well-pointed-wedge-cover" "The standard cover of a well-pointed wedge — 1 item · 1 fully proved" click n120 "../roadmap/fundamental-group/van-kampen/index.html#wedge-fundamental-group" "The fundamental group of a wedge — 1 item · 1 fully proved" click n121 "../roadmap/fundamental-group/van-kampen/index.html#wedge-circles-free-group" "The fundamental group of a wedge of circles — 1 item · 1 fully proved" click n122 "../roadmap/fundamental-group/van-kampen/presentation-complex/index.html#relator-cell-attachment" "Free-group relators form a standard two-cell attachment — 1 item · 1 fully proved" click n123 "../roadmap/fundamental-group/van-kampen/presentation-complex/index.html#pointed-wedge-path-connected" "Pointed wedges of path-connected spaces are path-connected — 1 item · 1 fully proved" click n124 "../roadmap/fundamental-group/van-kampen/presentation-complex/index.html#presentation-complex-fundamental-group" "The presentation complex has the presented fundamental group — 1 item · 1 fully proved" click n125 "../roadmap/fundamental-group/van-kampen/presentation-complex/index.html#point-zero-cell-attachment" "A point is one standard zero-cell — 1 item · 1 fully proved" click n126 "../roadmap/fundamental-group/van-kampen/presentation-complex/index.html#pointed-wedge-universal-property" "Continuous maps out of a pointed wedge — 1 item · 1 fully proved" click n127 "../roadmap/fundamental-group/van-kampen/presentation-complex/index.html#circle-one-cell-quotient" "Collapsing the boundary of a one-disk gives the circle — 1 item · 1 fully proved" click n128 "../roadmap/fundamental-group/van-kampen/presentation-complex/index.html#wedge-circles-one-skeleton" "A wedge of circles is an indexed one-cell attachment — 1 item · 1 fully proved" click n129 "../roadmap/fundamental-group/van-kampen/presentation-complex/index.html#empty-cell-attachment-constructor" "The identity attaches an empty family of cells — 1 item · 1 fully proved" click n130 "../roadmap/fundamental-group/van-kampen/presentation-complex/index.html#eventually-constant-cell-sequence" "Eventually constant cell sequences form abstract CW complexes — 1 item · 1 fully proved" click n131 "../roadmap/fundamental-group/van-kampen/presentation-complex/index.html#presentation-complex-cw-structure" "The presentation complex is an abstract two-dimensional CW complex — 1 item · 1 fully proved" click n132 "../roadmap/fundamental-group/van-kampen/presentation-complex/index.html#presentation-complex-realization" "Presented groups have two-dimensional presentation complexes — 1 item · 1 fully proved" click n133 "../roadmap/fundamental-group/van-kampen/index.html#every-group-fundamental-group" "Every group is a fundamental group — 1 item · 1 fully proved" click n134 "../roadmap/fundamental-group/van-kampen/index.html#finite-skeleton-fundamental-group" "Finite skeleta above dimension two have the same fundamental group — 1 item · 1 fully proved" click n135 "../roadmap/fundamental-group/van-kampen/presentation-complex/index.html" "Presentation-complex support — 1 item · 1 ready to state" click n136 "../roadmap/fundamental-group/van-kampen/presentation-complex/index.html#cyclic-presentation-complex" "The cyclic presentation complex — 1 item · 1 fully proved" click n137 "../roadmap/fundamental-group/van-kampen/index.html#two-skeleton-fundamental-group" "The 2-skeleton determines the fundamental group — 1 item · 1 fully proved" click n138 "../roadmap/homology/index.html" "Homology — 1 item · 1 ready to state" click n139 "../roadmap/homology/computations-and-applications/index.html" "Computations and applications — 1 item · 1 ready to state" click n140 "../roadmap/homology/computations-and-applications/degree/index.html" "Degree foundations and applications — 1 item · 1 ready to state" click n141 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#topological-triple" "Topological triples and their maps — 1 item · 1 fully proved" click n142 "../roadmap/homology/simplicial-and-singular/index.html#chain-map-homology" "A chain map induces a map on homology — 1 item · 1 in mathlib" click n143 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#simplicial-pair-relative-homology" "Relative homology of a simplicial-set pair — 1 item · 1 in mathlib" click n144 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#singular-pair-functor" "The singular set of a topological pair — 1 item · 1 fully proved" click n145 "../roadmap/homology/simplicial-and-singular/index.html#singular-chain-complex" "The singular chain complex — 1 item · 1 in mathlib" click n146 "../roadmap/homology/simplicial-and-singular/index.html#singular-homology" "Singular homology — 1 item · 1 in mathlib" click n147 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#relative-singular-homology" "Relative singular chains and homology — 1 item · 1 fully proved" click n148 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#standard-simplex-boundary-horn" "The boundary and zero horn of a standard topological simplex — 1 item · 1 fully proved" click n149 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#augmented-singular-chain-complex" "The augmented singular chain complex — 1 item · 1 fully proved" click n150 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#reduced-singular-homology" "Reduced singular homology — 1 item · 1 fully proved" click n151 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#double-simplex-fundamental-cycle" "The ordered difference of the two simplices is a cycle — 1 item · 1 fully proved" click n152 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#strong-deformation-retract" "Strong deformation retracts — 1 item · 1 fully proved" click n153 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#standard-simplex-zero-horn-retraction" "A standard simplex strongly deformation retracts onto its zero horn — 1 item · 1 fully proved" click n154 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#good-pair-data" "Good pairs and neighborhood deformation retracts — 1 item · 1 fully proved" click n155 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#standard-simplex-boundary-good-pairs" "Standard-simplex boundary and horn pairs are good — 1 item · 1 fully proved" click n156 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#point-quotient-functor" "Functorial point quotients of topological pairs — 1 item · 1 fully proved" click n157 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#standard-simplex-zero-face-point-quotient" "The zero face identifies the two simplex point quotients — 1 item · 1 fully proved" click n158 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#short-exact-homology-sequence" "A short exact sequence gives an exact homology sequence — 1 item · 1 in mathlib" click n159 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#pair-long-exact-sequence" "The long exact sequence of a pair — 1 item · 1 fully proved" click n160 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#reduced-positive-degree-comparison" "Reduced and ordinary homology agree in positive degrees — 1 item · 1 fully proved" click n161 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#pointed-zeroth-homology-splitting" "Zeroth homology splits into reduced homology and the coefficient object — 1 item · 1 fully proved" click n162 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#reduced-pair-long-exact-sequence" "The reduced long exact sequence of a nonempty pair — 1 item · 1 fully proved" click n163 "../roadmap/homology/simplicial-and-singular/index.html#zeroth-homology-components" "Zeroth homology is free on path components — 1 item · 1 in mathlib" click n164 "../roadmap/homology/simplicial-and-singular/index.html#totally-disconnected-higher-homology" "Higher homology vanishes for totally disconnected spaces — 1 item · 1 in mathlib" click n165 "../roadmap/homology/simplicial-and-singular/index.html#point-homology" "Homology of a point — 1 item · 1 fully proved" click n166 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#pointed-relative-reduced-homology" "Relative homology at a basepoint is reduced homology — 1 item · 1 fully proved" click n167 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#point-quotient-projection-topology" "Topology of the point-quotient projection — 1 item · 1 fully proved" click n168 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#good-pair-neighborhood-quotient" "Restricting the quotient to a good-pair neighborhood — 1 item · 1 fully proved" click n169 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#relative-homology-map-isomorphism-criterion" "Componentwise isomorphisms imply a relative isomorphism — 1 item · 1 fully proved" click n170 "../roadmap/homology/simplicial-and-singular/index.html#chain-homotopy-invariance" "Chain-homotopic maps induce the same homology map — 1 item · 1 in mathlib" click n171 "../roadmap/homology/simplicial-and-singular/index.html#topological-homotopy-chain-homotopy" "A topological homotopy gives a singular-chain homotopy — 1 item · 1 in mathlib" click n172 "../roadmap/homology/simplicial-and-singular/index.html#singular-homology-homotopy-invariance" "Homotopic maps induce the same singular-homology map — 1 item · 1 in mathlib" click n173 "../roadmap/homology/simplicial-and-singular/index.html#homotopy-equivalence-homology-iso" "A homotopy equivalence induces homology isomorphisms — 1 item · 1 fully proved" click n174 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#good-pair-neighborhood-relative-homology" "Enlarging to the chosen neighborhood preserves relative homology — 1 item · 1 fully proved" click n175 "../roadmap/homology/simplicial-and-singular/relative-homology/small-chains-and-excision/index.html#affine-barycentric-subdivision" "Affine barycentric subdivision is compatible with faces — 1 item · 1 fully proved" click n176 "../roadmap/homology/simplicial-and-singular/relative-homology/small-chains-and-excision/index.html#affine-chain-subdivision-homotopy" "Affine-chain subdivision is homotopic to the identity — 1 item · 1 fully proved" click n177 "../roadmap/homology/simplicial-and-singular/relative-homology/small-chains-and-excision/index.html#singular-chain-subdivision-homotopy" "Singular-chain subdivision is naturally homotopic to the identity — 1 item · 1 fully proved" click n178 "../roadmap/homology/simplicial-and-singular/relative-homology/small-chains-and-excision/index.html#barycentric-subdivision-diameter" "Barycentric subdivision contracts simplex diameter — 1 item · 1 fully proved" click n179 "../roadmap/homology/simplicial-and-singular/relative-homology/small-chains-and-excision/index.html#eventually-small-singular-simplices" "Iterated subdivision eventually makes every singular simplex small — 1 item · 1 fully proved" click n180 "../roadmap/homology/simplicial-and-singular/relative-homology/small-chains-and-excision/index.html#small-chain-inclusion-homotopy-equivalence" "Small singular chains include by a chain-homotopy equivalence — 1 item · 1 fully proved" click n181 "../roadmap/homology/simplicial-and-singular/relative-homology/small-chains-and-excision/index.html#relative-chain-union-devissage" "Relative excision reduces to the union subcomplex — 1 item · 1 fully proved" click n182 "../roadmap/homology/simplicial-and-singular/relative-homology/small-chains-and-excision/index.html#binary-cover-excision-chain-equivalence" "The binary-cover excision chain map is a homotopy equivalence — 1 item · 1 fully proved" click n183 "../roadmap/homology/simplicial-and-singular/relative-homology/small-chains-and-excision/index.html#binary-cover-excision-homology-isomorphism" "Binary-cover excision induces homology isomorphisms — 1 item · 1 fully proved" click n184 "../roadmap/homology/simplicial-and-singular/relative-homology/small-chains-and-excision/index.html#deleted-subset-excision-homology-isomorphism" "Deleted-subset excision induces homology isomorphisms — 1 item · 1 fully proved" click n185 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#good-pair-excision-diagram" "The complementary excision diagram — 1 item · 1 fully proved" click n186 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#point-quotient-neighborhood-contraction" "The quotient neighborhood contracts to its point — 1 item · 1 fully proved" click n187 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#point-quotient-neighborhood-relative-homology" "Enlarging the quotient point preserves relative homology — 1 item · 1 fully proved" click n188 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#point-quotient-neighborhood-excision" "The neighborhood quotient map preserves relative homology — 1 item · 1 fully proved" click n189 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#good-pair-point-quotient-relative-homology" "Good-pair relative homology is reduced quotient homology — 1 item · 1 fully proved" click n190 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#pair-long-exact-sequence-naturality" "The pair long exact sequence is natural — 1 item · 1 fully proved" click n191 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#reduced-pair-long-exact-sequence-naturality" "The reduced pair long exact sequence is natural — 1 item · 1 fully proved" click n192 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#pointed-relative-reduced-homology-naturality" "The pointed relative-to-reduced comparison is natural — 1 item · 1 fully proved" click n193 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#good-pair-quotient-comparison-naturality" "The good-pair quotient comparison is natural — 1 item · 1 fully proved" click n194 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#standard-simplex-zero-face-relative-homology" "The zero face induces an isomorphism in relative homology — 1 item · 1 fully proved" click n195 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#triple-chain-short-exact-sequence" "Relative chains of a triple form a short exact sequence — 1 item · 1 fully proved" click n196 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#triple-long-exact-sequence" "The long exact sequence of a triple — 1 item · 1 fully proved" click n197 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#triple-connecting-cycle-formula" "The triple connecting map sends a relative cycle to its boundary — 1 item · 1 fully proved" click n198 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#relative-singular-chain-homotopy" "A homotopy of pairs gives a relative chain homotopy — 1 item · 1 fully proved" click n199 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#relative-homology-homotopy-invariance" "Homotopic maps of pairs induce the same relative-homology map — 1 item · 1 fully proved" click n200 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#relative-simplex-fundamental-class" "The identity simplex generates relative simplex homology — 1 item · 1 fully proved" click n201 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#double-simplex-relative-comparison" "The first simplex computes homology relative to the second — 1 item · 1 fully proved" click n202 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#reduced-homology-homotopy-invariance" "Homotopic maps induce the same reduced-homology map — 1 item · 1 fully proved" click n203 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#homotopy-equivalence-reduced-homology-iso" "A homotopy equivalence induces reduced-homology isomorphisms — 1 item · 1 fully proved" click n204 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#contractible-space-reduced-homology" "Reduced homology of a contractible space vanishes — 1 item · 1 fully proved" click n205 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#contractible-subspace-relative-reduced-homology" "A contractible subspace identifies reduced and relative homology — 1 item · 1 fully proved" click n206 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#double-simplex-fundamental-class" "The double-simplex difference generates reduced homology — 1 item · 1 fully proved" click n207 "../roadmap/homology/computations-and-applications/degree/index.html#double-simplex-swap-class" "Swapping the double simplex negates its fundamental class — 1 item · 1 fully proved" click n208 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#standard-simplex-disk-pair-homeomorphism" "The standard simplex pair is homeomorphic to the disk pair — 1 item · 1 fully proved" click n209 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#double-simplex-sphere-homeomorphism" "The double simplex is a sphere — 1 item · 1 fully proved" click n210 "../roadmap/homology/computations-and-applications/degree/index.html#sphere-coordinate-sign-changes" "Coordinate sign changes on the sphere — 1 item · 1 fully proved" click n211 "../roadmap/homology/computations-and-applications/degree/index.html#integral-sphere-orientation" "The ordered class orients ordinary sphere homology — 1 item · 1 fully proved" click n212 "../roadmap/homology/computations-and-applications/degree/index.html#sphere-degree-definition" "Degree is the multiplier of the ordered sphere class — 1 item · 1 fully proved" click n213 "../roadmap/homology/computations-and-applications/degree/index.html#basic-degree-properties" "The formal properties of degree — 1 item · 1 fully proved" click n214 "../roadmap/homology/computations-and-applications/degree/index.html#coordinate-reflection-degree" "A sphere reflection has degree minus one — 1 item · 1 fully proved" click n215 "../roadmap/homology/computations-and-applications/degree/index.html#antipodal-degree" "The antipodal map has degree determined by dimension — 1 item · 1 fully proved" click n216 "../roadmap/homology/computations-and-applications/degree/index.html#fixed-point-free-degree" "A fixed-point-free sphere map has antipodal degree — 1 item · 1 fully proved" click n217 "../roadmap/homology/computations-and-applications/degree/index.html#sphere-action-degree-character" "Degree gives a character of a sphere action — 1 item · 1 fully proved" click n218 "../roadmap/homology/computations-and-applications/degree/index.html#free-even-sphere-action" "Only the antipodal group acts freely on an even sphere — 1 item · 1 fully proved" click n219 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#sphere-hemisphere-stereographic-models" "Stereographic models for hemispheres and the equator — 1 item · 1 fully proved" click n220 "../roadmap/homology/computations-and-applications/degree/index.html#punctured-sphere-stereographic" "A punctured sphere is Euclidean space — 1 item · 1 fully proved" click n221 "../roadmap/homology/computations-and-applications/degree/index.html#nonsurjective-degree-zero" "A nonsurjective sphere map has degree zero — 1 item · 1 fully proved" click n222 "../roadmap/homology/computations-and-applications/degree/index.html#tangent-vector-field-data" "Tangent vector fields and normalization — 1 item · 1 fully proved" click n223 "../roadmap/homology/computations-and-applications/degree/index.html#tangent-field-parity-obstruction" "A nonvanishing tangent field forces odd dimension — 1 item · 1 fully proved" click n224 "../roadmap/homology/computations-and-applications/degree/index.html#odd-sphere-tangent-field" "Odd spheres have a nonvanishing tangent field — 1 item · 1 fully proved" click n225 "../roadmap/homology/computations-and-applications/degree/index.html#nonzero-tangent-field-iff-odd" "A sphere has a nonvanishing tangent field exactly in odd dimension — 1 item · 1 fully proved" click n226 "../roadmap/homology/computations-and-applications/local-degree/index.html" "Local degree and the sum over a finite fiber — 1 item · 1 ready to state" click n227 "../roadmap/homology/computations-and-applications/local-degree/index.html#sphere-local-orientation" "The ordered sphere class orients local homology — 1 item · 1 fully proved" click n228 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#sigma-pointed-pair" "The coproduct pair of a family of pointed spaces — 1 item · 1 fully proved" click n229 "../roadmap/homology/computations-and-applications/local-degree/index.html#sigma-topological-pair" "The coproduct of a family of topological pairs — 1 item · 1 fully proved" click n230 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#singular-relative-chains-coproduct" "Relative singular chains commute with topological coproducts — 1 item · 1 fully proved" click n231 "../roadmap/homology/computations-and-applications/local-degree/index.html#relative-chains-sigma-pair" "Relative chains commute with coproducts of arbitrary pairs — 1 item · 1 ready to state" click n232 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#relative-homology-coproduct" "Relative homology commutes with exact coproducts — 1 item · 1 fully proved" click n233 "../roadmap/homology/computations-and-applications/local-degree/index.html#relative-homology-sigma-pair" "Relative homology commutes with coproducts of arbitrary pairs — 1 item · 1 planned" click n234 "../roadmap/homology/computations-and-applications/local-homology-and-dimension/index.html#local-homology-open-neighborhood" "Local homology is unchanged on an open neighborhood — 1 item · 1 fully proved" click n235 "../roadmap/homology/computations-and-applications/local-degree/index.html#deleted-pair-open-neighborhood" "Deleted-pair homology is local on an open neighborhood — 1 item · 1 fully proved" click n236 "../roadmap/homology/computations-and-applications/local-degree/index.html#disjoint-open-union-homeomorphism" "A disjoint open family is homeomorphic to its sigma type — 1 item · 1 fully proved" click n237 "../roadmap/homology/computations-and-applications/local-degree/index.html#disjoint-punctured-pair-iso" "Disjoint punctured neighborhoods form the deleted union pair — 1 item · 1 fully proved" click n238 "../roadmap/homology/computations-and-applications/local-degree/index.html#isolated-preimage-neighborhood" "An isolated preimage gives a map of punctured pairs — 1 item · 1 fully proved" click n239 "../roadmap/homology/computations-and-applications/local-degree/index.html#finite-fiber-neighborhoods" "A finite sphere-map fiber has disjoint isolated neighborhoods — 1 item · 1 fully proved" click n240 "../roadmap/homology/computations-and-applications/local-degree/index.html#finite-puncture-pair-excision" "The disjoint local pairs excise to the finite-puncture pair — 1 item · 1 fully proved" click n241 "../roadmap/homology/computations-and-applications/local-degree/index.html#finite-puncture-homology-coproduct" "Finite-puncture homology is the coproduct of the local groups — 1 item · 1 planned" click n242 "../roadmap/homology/computations-and-applications/local-degree/index.html#finite-puncture-projection-matrix" "Finite-puncture projections have the diagonal matrix — 1 item · 1 planned" click n243 "../roadmap/homology/computations-and-applications/local-degree/index.html#global-degree-fiber-square" "The finite-fiber pair map carries the global degree — 1 item · 1 fully proved" click n244 "../roadmap/homology/computations-and-applications/local-degree/index.html#finite-puncture-orientation-sum" "The finite-puncture class is the sum of the local classes — 1 item · 1 planned" click n245 "../roadmap/homology/computations-and-applications/local-degree/index.html#neighborhood-local-degree" "Local degree on a chosen isolated neighborhood — 1 item · 1 fully proved" click n246 "../roadmap/homology/computations-and-applications/local-degree/index.html#local-degree-shrinking" "Local degree is unchanged when the neighborhood shrinks — 1 item · 1 fully proved" click n247 "../roadmap/homology/computations-and-applications/local-degree/index.html#local-degree-well-defined" "Local degree is independent of its neighborhood — 1 item · 1 fully proved" click n248 "../roadmap/homology/computations-and-applications/local-degree/index.html#finite-fiber-local-map" "The finite-fiber pair map acts by the local degrees — 1 item · 1 fully proved" click n249 "../roadmap/homology/computations-and-applications/local-degree/index.html#degree-local-sum-formula" "Degree is the sum of the local degrees — 1 item · 1 planned" click n250 "../roadmap/homology/computations-and-applications/local-degree/index.html#homeomorphism-local-degree" "A local homeomorphism has local degree plus or minus one — 1 item · 1 ready to state" click n251 "../roadmap/homology/computations-and-applications/local-homology-and-dimension/index.html" "Local homology and invariance of dimension — 1 item · 1 ready to state" click n252 "../roadmap/homology/computations-and-applications/local-homology-and-dimension/index.html#contractible-ambient-relative-homology" "Relative homology in a contractible ambient space — 1 item · 1 fully proved" click n253 "../roadmap/homology/computations-and-applications/mayer-vietoris/index.html#binary-cover-chain-complex" "The binary-cover Mayer–Vietoris chain complex — 1 item · 1 fully proved" click n254 "../roadmap/homology/computations-and-applications/mayer-vietoris/index.html#binary-cover-chain-short-exact-sequence" "Binary-cover chains form a short exact sequence — 1 item · 1 fully proved" click n255 "../roadmap/homology/computations-and-applications/mayer-vietoris/index.html#binary-cover-mayer-vietoris-sequence" "The binary-cover Mayer–Vietoris sequence — 1 item · 1 fully proved" click n256 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#ordinary-neighborhood-mayer-vietoris" "The ordinary neighborhood-retract Mayer–Vietoris sequence — 1 item · 1 fully proved" click n257 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#punctured-space-radial-deformation-retract" "A sphere strongly deformation retracts from punctured Euclidean space — 1 item · 1 fully proved" click n258 "../roadmap/homology/computations-and-applications/mayer-vietoris/index.html#small-augmented-chain-inclusion-homotopy-equivalence" "Small augmented chains include by a chain-homotopy equivalence — 1 item · 1 fully proved" click n259 "../roadmap/homology/computations-and-applications/mayer-vietoris/index.html#augmented-binary-cover-chain-short-exact-sequence" "Augmented binary-cover chains form a short exact sequence — 1 item · 1 fully proved" click n260 "../roadmap/homology/computations-and-applications/mayer-vietoris/index.html#reduced-binary-cover-mayer-vietoris-sequence" "The reduced binary-cover Mayer–Vietoris sequence — 1 item · 1 fully proved" click n261 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#reduced-neighborhood-mayer-vietoris" "The reduced neighborhood-retract Mayer–Vietoris sequence — 1 item · 1 fully proved" click n262 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#closed-ball-radial-deformation-retract" "A closed ball strongly deformation retracts from Euclidean space — 1 item · 1 fully proved" click n263 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#sphere-hemisphere-neighborhood-cover" "The hemispheres have compatible neighborhood deformation retractions — 1 item · 1 fully proved" click n264 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#sphere-reduced-homology-recurrence" "The reduced homology of spheres satisfies the suspension recurrence — 1 item · 1 fully proved" click n265 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#zero-sphere-two-point-homeomorphism" "The zero-sphere is a two-point space — 1 item · 1 fully proved" click n266 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#zero-sphere-reduced-homology" "Reduced homology of the zero-sphere — 1 item · 1 fully proved" click n267 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#sphere-reduced-homology" "Reduced homology of spheres — 1 item · 1 fully proved" click n268 "../roadmap/homology/computations-and-applications/local-homology-and-dimension/index.html#punctured-euclidean-local-homology" "Local homology of positive-dimensional Euclidean space — 1 item · 1 fully proved" click n269 "../roadmap/homology/computations-and-applications/local-homology-and-dimension/index.html#invariance-of-dimension-open-sets" "Homeomorphic nonempty Euclidean open sets have equal dimension — 1 item · 1 fully proved" click n270 "../roadmap/homology/computations-and-applications/mayer-vietoris/index.html" "Mayer–Vietoris sequences — 1 item · 1 ready to state" click n271 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html" "Post-excision applications — 1 item · 1 ready to state" click n272 "../roadmap/homology/computations-and-applications/post-excision-applications/cw-subcomplex-neighborhood/index.html#subcomplex-intersection" "Intersections of CW subcomplexes — 1 item · 1 fully proved" click n273 "../roadmap/homology/computations-and-applications/post-excision-applications/cw-subcomplex-neighborhood/index.html#cell-boundary-collar" "The radial collar of a cell boundary — 1 item · 1 fully proved" click n274 "../roadmap/homology/computations-and-applications/post-excision-applications/cw-subcomplex-neighborhood/index.html#regular-neighborhood-system" "A common regular-neighborhood system for subcomplexes — 1 item · 1 fully proved" click n275 "../roadmap/homology/computations-and-applications/post-excision-applications/cw-subcomplex-neighborhood/index.html#regular-neighborhood-strong-deformation-retract" "A regular neighborhood strongly deformation retracts onto its subcomplex — 1 item · 1 fully proved" click n276 "../roadmap/homology/computations-and-applications/post-excision-applications/cw-subcomplex-neighborhood/index.html#subcomplex-neighborhood-cover" "Subcomplex decompositions admit compatible neighborhoods — 1 item · 1 fully proved" click n277 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#cw-subcomplex-excision" "Excision holds for a union of CW subcomplexes — 1 item · 1 fully proved" click n278 "../roadmap/homology/computations-and-applications/post-excision-applications/cw-subcomplex-neighborhood/index.html" "CW-subcomplex regular neighborhoods — 1 item · 1 ready to state" click n279 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#mapping-cone-model" "The mapping cone of a topological pair — 1 item · 1 fully proved" click n280 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#mapping-cone-cover-relative-homology" "The mapping-cone cover has the relative homology of the original pair — 1 item · 1 fully proved" click n281 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#mapping-cone-relative-reduced-homology" "Relative homology is reduced homology of the mapping cone — 1 item · 1 fully proved" click n282 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#pointed-wedge-point-quotient" "The pointed wedge is the point quotient of the sigma pair — 1 item · 1 fully proved" click n283 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#sigma-good-pair" "A nonempty coproduct of pointed good pairs is good — 1 item · 1 fully proved" click n284 "../roadmap/homology/computations-and-applications/post-excision-applications/index.html#wedge-reduced-homology" "Reduced homology of a wedge is the direct sum of the summands — 1 item · 1 fully proved" click n285 "../roadmap/homology/computations-and-applications/sphere-homology/index.html" "Mayer–Vietoris transport, sphere homology, and Brouwer — 1 item · 1 ready to state" click n286 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#disk-boundary-no-retraction" "The boundary sphere is not a retract of the disk — 1 item · 1 fully proved" click n287 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#fixed-point-free-disk-map-retraction" "A fixed-point-free disk map produces a boundary retraction — 1 item · 1 fully proved" click n288 "../roadmap/homology/computations-and-applications/sphere-homology/index.html#brouwer-fixed-point-disk" "Brouwer's fixed-point theorem for disks — 1 item · 1 fully proved" click n289 "../roadmap/homology/formal-viewpoint/index.html" "The formal viewpoint — 1 item · 1 not ready" click n290 "../roadmap/homology/simplicial-and-singular/index.html" "Simplicial and singular homology — 1 item · 1 ready to state" click n291 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html" "Relative homology and exact sequences — 1 item · 1 ready to state" click n292 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html" "Good pairs and quotient exact sequences — 1 item · 1 ready to state" click n293 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#good-pair-point-quotient-exact-sequence" "The good-pair quotient exact sequence — 1 item · 1 fully proved" click n294 "../roadmap/homology/simplicial-and-singular/relative-homology/good-pair-quotient/index.html#good-pair-point-quotient-sequence-naturality" "Naturality of the good-pair quotient sequence — 1 item · 1 fully proved" click n295 "../roadmap/homology/simplicial-and-singular/relative-homology/small-chains-and-excision/index.html" "Small chains and excision — 1 item · 1 ready to state" click n296 "../roadmap/homology/simplicial-and-singular/relative-homology/index.html#triple-long-exact-sequence-naturality" "The triple long exact sequence is natural — 1 item · 1 fully proved" click n297 "../roadmap/homotopy-theory/index.html" "Homotopy theory — 1 item · 1 ready to state" click n298 "../roadmap/homotopy-theory/connections-with-cohomology/index.html" "Connections with cohomology — 1 item · 1 not ready" click n299 "../roadmap/homotopy-theory/elementary-methods/index.html" "Elementary methods of calculation — 1 item · 1 not ready" click n300 "../roadmap/homotopy-theory/homotopy-groups/index.html" "Homotopy groups — 1 item · 1 not ready" click n301 "../roadmap/index.html" "Algebraic Topology (Hatcher) roadmap — 1 item · 1 ready to state" click n302 "../roadmap/underlying-geometric-notions/index.html" "Some underlying geometric notions — 1 item · 1 not ready"