Character coproducts: local context
Project map · Chapter map · Full theorem DAG · Open textbook statement
This local map shows one dependency hop in either direction. The highlighted item is the current focus. ready to state2Nothing it needs is blocked, so the statement can be written in Lean.planned5Described in the blueprint only.
graph LR
n0("Sheaf cohomology bounds"):::can_state
n1("Stacks derived facts"):::can_state
n2("Rational orbit pullback"):::planned
n3("Character coproducts"):::planned
n4("Real orthogonality"):::planned
n5["Character classes"]:::planned
n6("Covariance of character classes"):::planned
n0 -.-> n3
n1 -.-> n3
n1 -.-> n2
n5 --> n6
n3 -.-> n5
n3 -.-> n6
n3 --> n4
n4 -.-> n5
n2 -.-> n3
click n0 "../../../roadmap/background/index.html#sheaf-cohomology-bounds" "Sheaf cohomology bounds — 1 item · 1 ready to state"
click n1 "../../../roadmap/background/index.html#stacks-derived" "Stacks derived facts — 1 item · 1 ready to state"
click n2 "../../../roadmap/local-tests/index.html#orbit-injectivity" "Rational orbit pullback — 1 item · 1 planned"
class n3 focus
click n3 "../../../roadmap/character-classes/index.html#character-coproduct" "Character coproducts — 1 item · 1 planned"
click n4 "../../../roadmap/character-classes/index.html#orthogonality" "Real orthogonality — 1 item · 1 planned"
click n5 "../../../roadmap/character-classes/index.html#character-classes" "Character classes — 1 item · 1 planned"
click n6 "../../../roadmap/character-classes/index.html#class-covariance" "Covariance of character classes — 1 item · 1 planned"