Small chains and excision dependency map
This map shows the container's direct articles. Nested containers are collapsed and clickable; dependency edges are rolled up from their leaves. in mathlib3Upstreamed into Mathlib.fully proved22Proved, and every prerequisite is fully proved too.
graph LR
n0("Affine barycentric subdivision is compatible with faces"):::fully_proved
n1["Affine-chain subdivision is homotopic to the identity"]:::fully_proved
n2("Barycentric subdivision contracts simplex diameter"):::fully_proved
n3("The binary-cover excision chain map is a homotopy equivalence"):::fully_proved
n4["Binary-cover excision induces homology isomorphisms"]:::fully_proved
n5["Deleted-subset excision induces homology isomorphisms"]:::fully_proved
n6("Iterated subdivision eventually makes every singular simplex small"):::fully_proved
n7("Relative excision reduces to the union subcomplex"):::fully_proved
n8["Singular-chain subdivision is naturally homotopic to the identity"]:::fully_proved
n9["Small singular chains include by a chain-homotopy equivalence"]:::fully_proved
n10["External chapter: Homology<br/><small>15 items · 3 in mathlib · 12 fully proved</small>"]:::boundary
n10 --> n3
n10 --> n4
n10 -.-> n4
n10 --> n5
n10 --> n7
n10 --> n8
n0 --> n1
n0 --> n2
n0 --> n8
n1 -.-> n8
n2 -.-> n6
n3 -->|2| n10
n3 --> n4
n4 -. 4 .-> n10
n4 -.-> n5
n5 --> n10
n5 -. 2 .-> n10
n6 --> n10
n6 --> n9
n7 -.-> n3
n8 --> n6
n8 -.-> n9
n9 --> n10
n9 -.-> n10
n9 -.-> n3
click n0 "../../../../../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 n1 "../../../../../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 n2 "../../../../../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 n3 "../../../../../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 n4 "../../../../../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 n5 "../../../../../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 n6 "../../../../../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 n7 "../../../../../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 n8 "../../../../../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 n9 "../../../../../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 n10 "../../../../chapters/homology.html" "Homology — 15 items · 3 in mathlib · 12 fully proved"