Alphabeta Math
LemmaStatement: 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.

The first plus construction is separated and preserves stalks

Statement

Let F be a presheaf on a topological space X, and let η:FF+ be the canonical map of The plus construction for a presheaf. Then:

  1. F+ is a separated presheaf.
  2. For every xX, the induced map on stalks ηx:Fx(F+)x is a bijection.

Facts & Assumptions

Given: A presheaf F on X and its plus construction η:FF+.

[F1]

A section of F+(U) is an equivalence class of germ-compatible local presentations over U, and ηU(s) is represented by the single-chart presentation (U,s) (The plus construction for a presheaf).

[F2]

A separated presheaf is one in which equality of sections can be checked on an open cover (Separated presheaves).

[L1]

Equality in a filtered colimit of sets is eventual at some smaller common stage (Two representatives in a filtered colimit of sets are equal exactly when they become equal at one common later stage).

Proof

technique · direct
1.1

Let σ,τF+(U) and suppose there is an open cover U=αAWα such that σWα=τWα for every α. Fix xU, and choose α with xWα. Equality on Wα means that the two restricted presentations determine the same germ at x, so σ and τ have the same germ at x. Since this holds for every xU, the two global presentations are equivalent by [F1]. Therefore σ=τ, and F+ is separated by [F2].

F1F2
1.2

To prove surjectivity of ηx, let ξ(F+)x. Choose an open neighbourhood U of x and a section σF+(U) representing ξ. Pick a local presentation (Ui,si) of σ with xUi for some index i. Then on the neighbourhood Ui the section σ equals ηUi(si) by [F1], so the germ ξ is the image of the germ of si at x. Hence ηx is surjective.

F1givenchoose
1.3

Now suppose ηx(a)=ηx(b) in (F+)x, where aFx and bFx. Represent a and b by sections sF(U) and tF(V) on neighbourhoods of x. By [L1], equality of their images in the stalk of F+ means that there exists an open neighbourhood WUV of x such that ηW(sW)=ηW(tW) in F+(W). By [F1], equality of these two single-chart classes says exactly that sW and tW have the same germ at every point of W, in particular at x. Thus a=b in Fx, so ηx is injective.

F1L1given
2.1

Steps 1.2 and 1.3 prove that every ηx is bijective, and step 1.1 proves that F+ is separated.

step 1.1step 1.2step 1.3

Depends on

Used by

Dependency tree · two levels

9 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