Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07
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.

The sheaf condition can be checked on a basis with basis-refinable intersections

Statement

Assume the Axiom of Choice. Let X be a topological space and let B be a basis for its topology such that whenever B,B′∈B and x∈B∩B′, there exists C∈B with x∈C⊆B∩B′. Let F be a presheaf on X. Then F is a sheaf if and only if the following condition holds:

for every open set U⊆X, every cover U=⋃i∈IBi by basis elements Bi∈B, and every family si∈F(Bi) such that si∣C=sj∣C for every basis element C∈B with C⊆Bi∩Bj, there exists a unique section s∈F(U) with s∣Bi=si for all i.

Facts & Assumptions

Given: The Axiom of Choice, a basis B as in the statement, and a presheaf F on X.

[L1]

A basis means that every open set and every point of it admit a containing basis element inside that open set (Basis and subbasis for a topology, and the topology generated by a family of sets).

[L2]

A sheaf is a presheaf with locality and unique gluing on every open cover (A sheaf on a topological space).

Proof

technique · direct
1.1L1L2

Assume F is a sheaf. Let U=⋃iBi be a basis cover and let (si) satisfy the basis-overlap hypothesis. Fix i,j. The sets C∈B with C⊆Bi∩Bj cover Bi∩Bj by [L1] and the intersection hypothesis on B. On each such C the restrictions of si and sj agree, so locality from [L2] gives si∣Bi∩Bj=sj∣Bi∩Bj. Gluing in [L2] then produces a unique s∈F(U) with s∣Bi=si.

1.2L1givenchoose

Assume the displayed basis condition. Let U=⋃α∈AUα be an arbitrary open cover and let tα∈F(Uα) be compatible on overlaps. For each x∈U, choose α(x) with x∈Uα(x), and then choose Bx∈B with x∈Bx⊆Uα(x) by [L1]. Put rx:=tα(x)∣Bx.

2.1step 1.2given

Let C∈B satisfy C⊆Bx∩By. Then C⊆Uα(x)∩Uα(y), so compatibility of the original family gives rx∣C=tα(x)∣C=tα(y)∣C=ry∣C. Therefore the family (rx)x∈U satisfies the displayed basis condition for the basis cover U=⋃x∈UBx.

3.1step 2.1given

By the assumed basis condition applied to the compatible family from step 2.1, there is a unique s∈F(U) with s∣Bx=rx for every x∈U.

4.1L1L2step 2.1step 3.1givenchoose∎

Fix α∈A. For each y∈Uα, choose Cy∈B with y∈Cy⊆By∩Uα by [L1] and the basis-refinement hypothesis. Then the Cy form a basis cover of Uα. Since Cy⊆Uα(y)∩Uα, step 2.1 gives ry∣Cy=tα(y)∣Cy=tα∣Cy. Because s∣Cy=ry∣Cy by step 3.1, the two sections s∣Uα and tα restrict to the same family on the basis cover {Cy}y∈Uα. By the uniqueness part of the assumed basis condition, s∣Uα=tα. Since this holds for every α, the arbitrary compatible family glues uniquely, so [L2] implies that F is a sheaf.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 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