How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Dualizing and support shifts on the complex line
Example
With the conventions of Constructible Verdier duality and complex orientation and coefficient field : on the complex line (an oriented smooth complex 1-fold) the dualizing object is . For the closed inclusion one has and . The example consumes the AC-assumed Verdier supplier; the displayed computation itself is choice-free.
Facts & Assumptions
Given: The complex line with its analytic topology, the closed inclusion , a coefficient field , and the conventions of Constructible Verdier duality and complex orientation and Derived operations on analytic field sheaves; AC is consumed through the Verdier supplier.
The Verdier supplier: and ; on a smooth complex -fold the complex orientation gives ; ; and dualizing transitivity holds (Constructible Verdier duality and complex orientation).
Closed-support localization and the exceptional adjoint: for a closed inclusion the object is the derived functor of , both localization triangles hold and (Support localization, base change, projection and trace calculus, Exceptional inverse image as the adjoint of derived proper-support image).
Compactly supported global sections and their derived functors are defined for locally compact Hausdorff spaces (Compactly supported global sections and their right derived functors).
Conventions: shifts satisfy and the cochain cone and derived-Hom conventions are those of Derived category of an abelian category and Derived hom in the bounded setting (Derived operations on analytic field sheaves, Inverse image presheaf and inverse image sheaf, Direct image of a sheaf along a continuous map, Extension by zero for abelian sheaves on an open subspace, A sheaf on a topological space).
Verification
A positively complex-oriented open disk , with closed-disk compactification , has compact-support cochain complex with a single cohomology generator in degree over : the closed disk with its boundary is the finite relative cellular model whose quotient is generated by the oriented -cell, which computes compact supports on by extension by zero to . Hence the dual local model has concentrated in degree , and the orientation normalization of [F1] at gives . This uses the same positive complex orientation generator as the diagonal Thom calculations.
Closed-support cohomology at the origin. By [F2] the object is , the derived functor of , and the localization triangle of [F2] computes it as the relative cohomology of the pair for a small open disk around the origin; radial retraction of the punctured disk to the circle gives the relative cellular model with a single generator in degree , so . Applying the shift of [F4] gives , consistently with dualizing transitivity of [F1]. The duality route produces the same answer: , and , with the same positive orientation generator used in both computations. The displayed computation involves only the finite relative cellular model of a disk and is choice-free; AC is present only because the consumed Verdier supplier assumes it.
Depends on
- The Axiom of Choice
- Compactly supported global sections and their right derived functors
- Derived category of an abelian category
- Derived hom in the bounded setting
- Derived operations on analytic field sheaves
- Direct image of a sheaf along a continuous map
- Extension by zero for abelian sheaves on an open subspace
- Inverse image presheaf and inverse image sheaf
- A sheaf on a topological space
- Support localization, base change, projection and trace calculus
- Exceptional inverse image as the adjoint of derived proper-support image
- Constructible Verdier duality and complex orientation
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
74 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Jean-Louis Verdier, Dualité dans la cohomologie des espaces localement compacts, Séminaire N. Bourbaki 1964–1966, exposé 300, pp. 337–349 (Novembre 1965) (standard reference, not scraped)
- The Stacks Project, Cohomology of Sheaves (chapter 20): §21 cohomology with support in a closed subset, §16 cohomology on Hausdorff quasi-compact spaces (standard reference, not scraped)