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.
Sheaves of sets are equivalent to local homeomorphisms over the base space
Statement
Let be a topological space. A continuous map is called a local homeomorphism if every point has an open neighbourhood such that is open in and is a homeomorphism.
- For every sheaf of sets on , the projection of The etale space of a sheaf of sets is a local homeomorphism.
- For every local homeomorphism , the assignment is a sheaf of sets on .
- These two constructions are inverse up to natural isomorphism, so they give an equivalence between sheaves of sets on and spaces over whose structure map is a local homeomorphism.
Facts & Assumptions
Given: A sheaf on , or a local homeomorphism .
The etale space is the disjoint union of the stalks with basic open sets , and is a bijection (The etale space of a sheaf of sets).
A sheaf is glued uniquely from compatible local sections on any open cover (A sheaf on a topological space).
Morphisms of presheaves are given by restriction-compatible component maps (Morphisms of presheaves).
Proof
For a sheaf , let be as in [F1]. If , then for some section . By construction is bijective. Its inverse is continuous because for any smaller basic open , the preimage is the open set , which is open by the sheaf locality encoded in [L1]. Hence is a homeomorphism onto the open set . Since every point of lies in some , is a local homeomorphism.
Let be a local homeomorphism, and let denote its continuous sections over an open set . Restriction of a section is again a section, so is a presheaf. If two sections of agree on an open cover, they are equal pointwise, so locality holds. If are compatible on an open cover , define for . Compatibility makes this well defined, and continuity is local on the cover because each is continuous. Thus [L1] holds, so is a sheaf.
A sheaf morphism induces a map over This is well defined by restriction compatibility. It is continuous: if lies in a basic open , equality of the two germs lets us shrink to an open on which ; then is a neighbourhood of mapped into . Identities and compositions are preserved. Conversely, a map over between local homeomorphisms sends a section to , naturally in the open set, and hence induces a sheaf morphism .
For a sheaf and an open set , send to the section By step 1.1 this is continuous. If , then for all , so [L1] gives . Conversely, let be a continuous section. For each , choose a basic open containing . Continuity makes an open neighbourhood of . Since is injective on and , the restriction equals . These local sections agree on overlaps because they induce the same map . By [L1], they glue to a unique with . Thus is a bijection, natural in .
For a local homeomorphism , define by sending to the germ at of any local section through . Such a local section exists because is a local homeomorphism, and two choices have the same germ because on a smaller common chart they are both the inverse of . On a chart , the map is a homeomorphism from onto the basic open defined by the inverse section. Hence is an isomorphism over . The formula makes the bijections of step 2.1 natural in , while the formula makes natural in . Thus the two functors constructed in steps 1.2 and 1.3 are quasi-inverse equivalences.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
8 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, Sheaves on Spaces, Sections 17 and 21 (standard reference, not scraped)
- Ravi Vakil, Foundations of Algebraic Geometry, Class 3 (standard reference, not scraped)