Direct images and open extension: 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.planned11Described in the blueprint only.
graph LR
n0("Sheaf pushforward toolkit"):::can_state
n1("Verdier duality formalism"):::can_state
n2["Test categories"]:::planned
n3("Verdier duality on test categories"):::planned
n4("Direct images and open extension"):::planned
n5("Homotopy invariance"):::planned
n6("Cutoff"):::planned
n7("Objects supported in an open set"):::planned
n8("Contractible quotient"):::planned
n9("Real orthogonality"):::planned
n10("Covariance of character classes"):::planned
n11("Open cover dense inclusion"):::planned
n12("Action of degree"):::planned
n0 -.-> n3
n0 -.-> n4
n1 -.-> n3
n1 -.-> n4
n7 --> n11
n6 -.-> n7
n6 -.-> n11
n5 -.-> n8
n5 -.-> n12
n2 --> n7
n2 --> n6
n2 --> n11
n2 --> n5
n2 --> n3
n2 --> n4
n2 --> n8
n2 --> n12
n3 -.-> n7
n3 -.-> n4
n4 -.-> n10
n4 -.-> n9
n4 -.-> n7
n4 -.-> n6
n4 -.-> n11
n4 --> n5
n4 -.-> n8
n4 -.-> n12
click n0 "../../../roadmap/background/index.html#sheaf-pushforward" "Sheaf pushforward toolkit — 1 item · 1 ready to state"
click n1 "../../../roadmap/background/index.html#verdier-duality" "Verdier duality formalism — 1 item · 1 ready to state"
click n2 "../../../roadmap/sheaf-categories/index.html#test-categories" "Test categories — 1 item · 1 planned"
click n3 "../../../roadmap/sheaf-categories/index.html#test-duality" "Verdier duality on test categories — 1 item · 1 planned"
class n4 focus
click n4 "../../../roadmap/sheaf-categories/index.html#test-pushforward" "Direct images and open extension — 1 item · 1 planned"
click n5 "../../../roadmap/sheaf-categories/index.html#homotopy-invariance" "Homotopy invariance — 1 item · 1 planned"
click n6 "../../../roadmap/localization/index.html#cutoff" "Cutoff — 1 item · 1 planned"
click n7 "../../../roadmap/localization/index.html#compact-support" "Objects supported in an open set — 1 item · 1 planned"
click n8 "../../../roadmap/sphere-lattice/index.html#contractible-quotient" "Contractible quotient — 1 item · 1 planned"
click n9 "../../../roadmap/character-classes/index.html#orthogonality" "Real orthogonality — 1 item · 1 planned"
click n10 "../../../roadmap/character-classes/index.html#class-covariance" "Covariance of character classes — 1 item · 1 planned"
click n11 "../../../roadmap/localization/index.html#open-cover" "Open cover dense inclusion — 1 item · 1 planned"
click n12 "../../../roadmap/sphere-lattice/index.html#degree-action" "Action of degree — 1 item · 1 planned"