Alphabeta MathHow 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.
Inverse image presheaf and inverse image sheaf
Definition
Let be a continuous map, and let be a presheaf on . The inverse-image presheaf
on is defined by
where runs over the open neighbourhoods of in , ordered by reverse inclusion. If , then every neighbourhood of is a neighbourhood of , so there is a natural restriction map .
The inverse image sheaf of a sheaf on is the sheafification of this presheaf:
When is open in and is an open set of with , there is a canonical map
into the colimit class represented by .
Depends on
Used by
- c-soft sheaves Definition
- Derived operations on analytic field sheaves Definition
- Pullback of a module along a morphism of ringed spaces Definition
- Restriction of a sheaf to an open subspace Definition
- Sheaf of relative Kähler differentials Definition
- Dualizing and support shifts on the complex line Example
- Actual analytic constructible sheaves admit coherent six operations Lemma
- Acyclic product fibers stabilize bounded constructible pullback Hom Lemma
- Bounded fibrewise-soft resolutions from a uniform all-sheaf dimension bound Lemma
- Cartesian simplicial sheaves model actual equivariant derived Hom Lemma
- Compact-support calculus along open and closed embeddings Lemma
- Complex algebraic constructible complexes have finite conical cochain models Lemma
- Derived tensor–Hom and inverse/direct image for field sheaves Lemma
- Finite simplicial constructible sheaves have an actual derived incidence model Lemma
- General linear Stiefel approximations stabilize bounded constructible Hom Lemma
- General linear Stiefel perverse normalization is exact and conservative Lemma
- Locally split Cech nerves give actual derived Cartesian sheaf descent Lemma
- Sections on a compact set extend to a neighbourhood Lemma
- Shifted smooth complex pullback is exact for the middle perverse t structure Lemma
- Support localization, base change, projection and trace calculus Lemma
- The stalk of an inverse image sheaf is the stalk over the image point Lemma
- Vanishing compactly supported first cohomology on opens characterises c-softness Lemma
- Inverse image of sheaves and pullback of modules are not the same construction Remark
- Coherent six operations on analytic constructible field sheaves Theorem
- Conormal sequence for a closed immersion Theorem
- Constructible six functors, proper base change and normalized equivariant duality Theorem
- Constructible Verdier duality and complex orientation Theorem
- Equivariant constructible Ext is degreewise finite and compatible with characteristic zero scalars Theorem
- Exceptional inverse image as the adjoint of derived proper-support image Theorem
- Inverse image is left adjoint to direct image on sheaves Theorem
- Middle perverse t structure glues and has simple intersection complexes Theorem
- Ordinary middle perverse t structure, recollement and intersection complexes Theorem
Dependency tree · two levels
7 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
- The Stacks Project, Lemma 6.21.3 and the definition after it (standard reference, not scraped)
- Ravi Vakil, The Rising Sea, Section 2.7.2 (standard reference, not scraped)