Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)
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.

Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

Sheaves of sets are equivalent to local homeomorphisms over the base space

Statement

Let X be a topological space. A continuous map q:EX is called a local homeomorphism if every point eE has an open neighbourhood W such that q(W) is open in X and qW:Wq(W) is a homeomorphism.

  1. For every sheaf of sets F on X, the projection p:E(F)X of The etale space of a sheaf of sets is a local homeomorphism.
  2. For every local homeomorphism q:EX, the assignment U{σ:UE continuous:qσ=idU} is a sheaf of sets on X.
  3. These two constructions are inverse up to natural isomorphism, so they give an equivalence between sheaves of sets on X and spaces over X whose structure map is a local homeomorphism.

Facts & Assumptions

Given: A sheaf F on X, or a local homeomorphism q:EX.

[F1]

The etale space E(F) is the disjoint union of the stalks with basic open sets [s,U], and p:[s,U]U is a bijection (The etale space of a sheaf of sets).

[L1]

A sheaf is glued uniquely from compatible local sections on any open cover (A sheaf on a topological space).

[F2]

Morphisms of presheaves are given by restriction-compatible component maps (Morphisms of presheaves).

Proof

technique · direct
1.1

For a sheaf F, let p:E(F)X be as in [F1]. If ξ=sxE(F), then ξ[s,U] for some section sF(U). By construction p:[s,U]U is bijective. Its inverse xsx is continuous because for any smaller basic open [t,V][s,U], the preimage is the open set {xUV:sx=tx}, which is open by the sheaf locality encoded in [L1]. Hence p[s,U] is a homeomorphism onto the open set U. Since every point of E(F) lies in some [s,U], p is a local homeomorphism.

F1L1
1.2

Let q:EX be a local homeomorphism, and let Secq(U) denote its continuous sections over an open set U. Restriction of a section is again a section, so Secq is a presheaf. If two sections of Secq(U) agree on an open cover, they are equal pointwise, so locality holds. If σiSecq(Ui) are compatible on an open cover U=iUi, define σ(x)=σi(x) for xUi. Compatibility makes this well defined, and continuity is local on the cover because each σi is continuous. Thus [L1] holds, so Secq is a sheaf.

L1given
1.3

A sheaf morphism φ:FG induces a map over X E(φ):E(F)E(G),sx(φU(s))x. This is well defined by restriction compatibility. It is continuous: if E(φ)(sx) lies in a basic open [t,V], equality of the two germs lets us shrink to an open WUV on which φU(s)W=tW; then [sW,W] is a neighbourhood of sx mapped into [t,V]. Identities and compositions are preserved. Conversely, a map f:EE over X between local homeomorphisms sends a section σ to fσ, naturally in the open set, and hence induces a sheaf morphism Sec(f).

F1F2given
2.1

For a sheaf F and an open set U, send sF(U) to the section θU(s):UE(F),θU(s)(x)=sx. By step 1.1 this is continuous. If θU(s)=θU(t), then sx=tx for all xU, so [L1] gives s=t. Conversely, let σ:UE(F) be a continuous section. For each xU, choose a basic open [sx,Vx] containing σ(x). Continuity makes Wx:=UVxσ1([sx,Vx]) an open neighbourhood of x. Since p is injective on [sx,Vx] and pσ=idU, the restriction σWx equals y(sx)y. These local sections agree on overlaps because they induce the same map σ. By [L1], they glue to a unique sF(U) with θU(s)=σ. Thus θU is a bijection, natural in U.

F1L1step 1.1
3.1

For a local homeomorphism q:EX, define η:EE(Secq) by sending eE to the germ at x=q(e) of any local section through e. Such a local section exists because q is a local homeomorphism, and two choices have the same germ because on a smaller common chart they are both the inverse of q. On a chart Wq(W), the map η is a homeomorphism from W onto the basic open defined by the inverse section. Hence η is an isomorphism over X. The formula E(φ)(sx)=(φU(s))x makes the bijections θ of step 2.1 natural in F, while the formula η(f(e))=(fσ)x makes η natural in E. Thus the two functors constructed in steps 1.2 and 1.3 are quasi-inverse equivalences.

step 1.1step 1.2step 2.1step 1.3

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