A bounded lattice on the test sphere dependency map
Project map · Full theorem DAG · Open textbook chapter
This map contains the 8 decomposed items in this chapter. Dashed chapter boxes stand for external prerequisites or dependents. fully proved1Proved, and every prerequisite is fully proved too.ready to state3Nothing it needs is blocked, so the statement can be written in Lean.planned16Described in the blueprint only.
graph LR
n0("Bounded comparison"):::planned
n1("Contractible quotient"):::planned
n2("Action of degree"):::planned
n3("Finite diagram chases"):::fully_proved
n4("Signature on a finite relation"):::planned
n5("Point groups"):::planned
n6("Fixed sphere lattice"):::planned
n7("Rational sphere calculation"):::planned
n8["External chapter: Background prerequisites<br/><small>2 items · 2 ready to state</small>"]:::boundary
n9["External chapter: Character classes and the contradiction<br/><small>3 items · 3 planned</small>"]:::boundary
n10["External chapter: Localization, germs, and dense subcategories<br/><small>3 items · 1 ready to state · 2 planned</small>"]:::boundary
n11["External chapter: Sheaf categories and homotopy invariance<br/><small>4 items · 4 planned</small>"]:::boundary
n8 -.-> n2
n8 -.-> n4
n10 -. 3 .-> n0
n10 -.-> n1
n10 -. 3 .-> n7
n11 --> n0
n11 -.-> n0
n11 --> n1
n11 -. 2 .-> n1
n11 --> n2
n11 -. 2 .-> n2
n11 --> n4
n11 --> n5
n11 -.-> n5
n11 --> n6
n11 --> n7
n11 -.-> n7
n0 -.-> n6
n1 --> n9
n1 -.-> n9
n2 -.-> n9
n3 -.-> n0
n4 -.-> n6
n5 -.-> n0
n5 -.-> n1
n5 -.-> n7
n6 -.-> n9
n6 --> n2
n7 -.-> n4
n7 -.-> n6
click n0 "../../roadmap/sphere-lattice/index.html#bounded-comparison" "Bounded comparison — 1 item · 1 planned"
click n1 "../../roadmap/sphere-lattice/index.html#contractible-quotient" "Contractible quotient — 1 item · 1 planned"
click n2 "../../roadmap/sphere-lattice/index.html#degree-action" "Action of degree — 1 item · 1 planned"
click n3 "../../roadmap/sphere-lattice/index.html#finite-chases" "Finite diagram chases — 1 item · 1 fully proved"
click n4 "../../roadmap/sphere-lattice/index.html#generic-signature" "Signature on a finite relation — 1 item · 1 planned"
click n5 "../../roadmap/sphere-lattice/index.html#point-groups" "Point groups — 1 item · 1 planned"
click n6 "../../roadmap/sphere-lattice/index.html#sphere-lattice" "Fixed sphere lattice — 1 item · 1 planned"
click n7 "../../roadmap/sphere-lattice/index.html#sphere-rank" "Rational sphere calculation — 1 item · 1 planned"
click n8 "background.html" "Background prerequisites — 2 items · 2 ready to state"
click n9 "character-classes.html" "Character classes and the contradiction — 3 items · 3 planned"
click n10 "localization.html" "Localization, germs, and dense subcategories — 3 items · 1 ready to state · 2 planned"
click n11 "sheaf-categories.html" "Sheaf categories and homotopy invariance — 4 items · 4 planned"