Character classes and the contradiction 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 proved2Proved, and every prerequisite is fully proved too.ready to state3Nothing it needs is blocked, so the statement can be written in Lean.planned18Described in the blueprint only.
graph LR
n0["Character classes"]:::planned
n1("Character coproducts"):::planned
n2("Covariance of character classes"):::planned
n3("Homotopy of character classes"):::planned
n4("Contradiction on the invariant chart"):::planned
n5("Equal parts"):::planned
n6("Real orthogonality"):::planned
n7("Sum of the character classes"):::planned
n8["External chapter: Background prerequisites<br/><small>2 items · 2 ready to state</small>"]:::boundary
n9["External chapter: Preparing local tests<br/><small>5 items · 2 fully proved · 1 ready to state · 2 planned</small>"]:::boundary
n10["External chapter: Localization, germs, and dense subcategories<br/><small>2 items · 2 planned</small>"]:::boundary
n11["External chapter: Main theorems<br/><small>1 item · 1 planned</small>"]:::boundary
n12["External chapter: Sheaf categories and homotopy invariance<br/><small>2 items · 2 planned</small>"]:::boundary
n13["External chapter: A bounded lattice on the test sphere<br/><small>3 items · 3 planned</small>"]:::boundary
n8 -. 2 .-> n1
n9 -.-> n1
n9 -. 4 .-> n4
n9 -.-> n5
n10 --> n0
n10 -. 2 .-> n2
n10 -.-> n5
n12 -.-> n2
n12 -.-> n3
n12 -.-> n6
n13 --> n0
n13 -. 2 .-> n4
n13 -.-> n5
n0 --> n2
n0 --> n3
n0 --> n5
n0 --> n7
n1 -.-> n0
n1 -.-> n2
n1 --> n6
n2 -.-> n3
n2 -.-> n4
n3 -.-> n4
n4 -.-> n11
n5 -.-> n4
n6 -.-> n0
n7 -.-> n4
click n0 "../../roadmap/character-classes/index.html#character-classes" "Character classes — 1 item · 1 planned"
click n1 "../../roadmap/character-classes/index.html#character-coproduct" "Character coproducts — 1 item · 1 planned"
click n2 "../../roadmap/character-classes/index.html#class-covariance" "Covariance of character classes — 1 item · 1 planned"
click n3 "../../roadmap/character-classes/index.html#class-homotopy" "Homotopy of character classes — 1 item · 1 planned"
click n4 "../../roadmap/character-classes/index.html#contradiction" "Contradiction on the invariant chart — 1 item · 1 planned"
click n5 "../../roadmap/character-classes/index.html#equal-parts" "Equal parts — 1 item · 1 planned"
click n6 "../../roadmap/character-classes/index.html#orthogonality" "Real orthogonality — 1 item · 1 planned"
click n7 "../../roadmap/character-classes/index.html#sum-classes" "Sum of the character classes — 1 item · 1 planned"
click n8 "background.html" "Background prerequisites — 2 items · 2 ready to state"
click n9 "local-tests.html" "Preparing local tests — 5 items · 2 fully proved · 1 ready to state · 2 planned"
click n10 "localization.html" "Localization, germs, and dense subcategories — 2 items · 2 planned"
click n11 "main-theorem.html" "Main theorems — 1 item · 1 planned"
click n12 "sheaf-categories.html" "Sheaf categories and homotopy invariance — 2 items · 2 planned"
click n13 "sphere-lattice.html" "A bounded lattice on the test sphere — 3 items · 3 planned"