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

9 results · all verified · 7 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Presheaves Sheaves Stalks and Sheafification - Examples

1 · Prerequisites

2 · Summary

These examples keep the page grounded in the first concrete phenomena that make sheaf theory necessary. Continuous and locally constant functions show gluing working as intended, while bounded functions, constant presheaves, and objectwise images show exactly where presheaf data can fail to glue globally.

The remaining examples make the local picture visible: skyscraper sheaves and empty-outside extensions isolate support conditions, and the germ examples show why one stalk need not determine a section in general while all stalks together often do.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Continuous real-valued functions form a sheaf

Example

For each open set UX, let C0(U,R):={f:UR continuous}. With the usual restriction of functions, this is a sheaf of sets on X.

Facts & Assumptions

Given: An open cover U=iIUi of an open set U.

[L1]

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

Verification

technique · direct
1.1

Restriction of a continuous function is continuous, so UC0(U,R) is a presheaf. If two continuous functions on U agree on every Ui, then they agree pointwise on all of U because the Ui cover U.

given
2.1

Let fiC0(Ui,R) be compatible on overlaps. Define f:UR by f(x)=fi(x) for any i with xUi. Compatibility makes this well defined, and continuity is local on the open cover because fUi=fi is continuous for each i. Thus [L1] holds.

L1givenconstruct
ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
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.

Locally constant functions form a sheaf and have constant stalks

Example

Fix a set A. For each open set UX, let Aloc(U):={f:UA locally constant}. With the usual restriction maps, this is a sheaf of sets on X. For every xX, evaluation at x induces a canonical bijection Aloc,xA.

Facts & Assumptions

Given: A set A, an open set UX, and a point xX.

[L1]

The sheaf condition is locality and unique gluing on open covers (A sheaf on a topological space).

[F1]

The stalk at x is the colimit of sections on neighbourhoods of x (The stalk of a presheaf at a point).

[F2]

The germ of a section is its class in that stalk (Germs of sections).

Verification

technique · direct
1.1

Restriction preserves local constancy. If two locally constant functions on U agree on an open cover, then they agree pointwise on U. If locally constant functions fi:UiA are compatible on an open cover of U, the pointwise glued function f is well defined and locally constant because near any point it agrees with one of the local functions fi. Hence [L1] holds and Aloc is a sheaf.

L1givenconstruct
2.1

Define ϵx:Aloc,xA by ϵx([U,f])=f(x). This is well defined because equal germs agree on some neighbourhood of x, hence have the same value at x. Every aA is the value at x of the constant function a on any neighbourhood of x, so ϵx is surjective. If ϵx([U,f])=ϵx([V,g]), then f(x)=g(x). Since both functions are locally constant, there is a neighbourhood W of x on which f and g are both constantly this common value, so [U,f]=[V,g]. Therefore ϵx is bijective.

F1F2given
CounterexampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Bounded continuous functions need not form a sheaf

Statement refuted

The assignment UCb0(U,R):={f:UR continuous and bounded} with the usual restriction maps is a sheaf on R.

Facts & Assumptions

Given: The presheaf Cb0(,R) on R.

[F1]

Restriction of a bounded continuous function is again bounded and continuous, so this is a presheaf (A presheaf on a topological space).

[L1]

A sheaf must glue every compatible local family to a global section (A sheaf on a topological space).

Counterexample

technique · direct
1.1

For each integer n1, let Un:=(n,n) and let sn:UnR be the identity function sn(x)=x. Each sn lies in Cb0(Un,R) because Un is bounded.

F1givenconstruct
2.1

If mn, then snUm=sm, so the family (sn) is compatible on the open cover R=n1Un.

step 1.1given
3.1

Any glued section on R would have to equal the identity function xx, because it agrees with each sn on Un. But xx is not bounded on R, so it does not lie in Cb0(R,R). This violates the gluing requirement in [L1]. Therefore the stated presheaf is not a sheaf.

L1step 2.1
CounterexampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-04 rests on unproved material (inherited)Open item page →
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 constant presheaf need not be a sheaf on a disconnected open set

Statement refuted

Fix a set A with distinct elements ab. The constant presheaf Apre on a space X, defined by Apre(U)=A for every open set U and identity restriction maps, is always a sheaf.

Facts & Assumptions

Given: A space X containing a disconnected open set U=U1U2 with U1,U2, and a set A with ab.

[F1]

Identity restriction maps define a presheaf on X (A presheaf on a topological space).

[F2]

The sheafification aF of a presheaf is defined by the double plus construction (Sheafification of a presheaf).

[L1]

Locally constant A-valued functions form a sheaf (Locally constant functions form a sheaf and have constant stalks).

Counterexample

technique · direct
1.1

By [F1], Apre is a presheaf. On the disjoint cover U=U1U2, choose the local sections s1:=aApre(U1) and s2:=bApre(U2). Because U1U2=, there is no overlap condition to check, so the pair is compatible.

F1givenconstruct
2.1

A glued section over U would have to be an element sA whose restriction to U1 is a and to U2 is b. But every restriction map is the identity, so this would force s=a=b, contradicting the choice ab. Therefore Apre is not a sheaf.

step 1.1given
3.1

The sheafification of Apre records exactly the data obtained by gluing constant local sections on an open cover, which is the same as an A-valued locally constant function. By [L1], that sheaf is Aloc, so [F2] identifies the locally constant sheaf as the sheafification of the constant presheaf.

F2L1step 2.1
ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
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.

A set-valued skyscraper sheaf and its stalks

Example

Fix a point x0X and a set A. Define a presheaf Sx0,A by Sx0,A(U)={A,x0U,{},x0U, with identity restrictions between opens containing x0 and the unique map to {} when the target does not contain x0. Then Sx0,A is a sheaf. Its stalk at x0 is canonically A, and its stalk at any yX with an open neighbourhood V satisfying x0V is the singleton {}. In particular, this holds for every yx0 in a T1 space.

Facts & Assumptions

Given: A point x0X, a set A, and a point yX. For the second stalk computation, also assume y has an open neighbourhood V with x0V.

[L1]

The sheaf condition is locality and unique gluing on open covers (A sheaf on a topological space).

[F1]

Stalks are colimits over neighbourhoods, and germs are represented by local sections (The stalk of a presheaf at a point, Germs of sections).

Verification

technique · direct
1.1

If an open set U does not contain x0, then every section of Sx0,A(U) is the unique element , so locality and gluing are trivial. If x0U and U=iUi, then at least one Ui contains x0. Compatibility forces all sections on such Ui to be the same element of A, and every Uj not containing x0 contributes only the unique section . Thus there is a unique glued section on U. Therefore [L1] holds and Sx0,A is a sheaf.

L1given
1.2

For the stalk at x0, every neighbourhood of x0 has section set A and every transition map is the identity on A. Hence the colimit in [F1] is canonically A.

F1given
2.1

If y has an open neighbourhood V with x0V, then every smaller neighbourhood of y inside V also has section set {}. Hence the stalk diagram is eventually constant at {}, so [F1] gives (Sx0,A)y{}.

F1given
ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Sections on an open subset extended by the empty set outside it

Example

Fix an open subset WX. Define a presheaf EW on X by EW(V)={{},VW,,V⊈W. Then EW is a sheaf of sets on X. It is the simplest example of data carried on an open subset and extended by no sections outside that subset.

Facts & Assumptions

Given: An open subset WX and an open cover V=iIVi.

[L1]

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

Verification

technique · direct
1.1

If VW, then every ViW has the unique section , and the only possible glued section on V is again . If V⊈W, choose xVW. Some cover member Vi contains x, so Vi⊈W and EW(Vi)=. Hence there is no compatible family of local sections on this cover. In either case the gluing and uniqueness clauses in [L1] are satisfied.

L1given
2.1

Restriction maps are forced: from {} to {} they are the identity, and into there is only the empty function from . Thus EW is a presheaf, and step 1.1 shows it is a sheaf.

step 1.1construct
CounterexampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
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 objectwise image of a sheaf morphism need not be a sheaf

Statement refuted

For every morphism of sheaves of sets, the objectwise image presheaf is already a subsheaf of the target.

Facts & Assumptions

Given: The sheaf morphism exp:C0(,R)C0(,S1),expU(f)(z)=e2πif(z), on the circle X=S1.

[F1]

A subsheaf must in particular be a sheaf (Subsheaves).

[L1]

The image sheaf is obtained by sheafifying the objectwise image presheaf (The image sheaf is the sheafification of the presheaf image).

Counterexample

technique · direct
1.1

Let U1=S1{(1,0)} and U2=S1{(1,0)}. These open arcs cover S1. On each Ui choose a continuous argument θi:UiR with e2πiθi(z)=z. Therefore the identity map idS1 restricts to sections in the objectwise image presheaf on both U1 and U2.

givenchooseconstruct
2.1

On the overlap U1U2, both local sections are equal to the same target section idS1U1U2, so they are compatible.

step 1.1given
3.1

Suppose idS1 lay in the global objectwise image. Then there would be a continuous f:S1R with e2πif(z)=z for every zS1. Writing z=e2πit with t[0,1], the function g(t):=f(e2πit)t is continuous and integer valued, hence constant. So f(e2πit)=t+n for some fixed integer n. Evaluating at t=0 and t=1 gives two values of f at the same point 1S1, namely n and n+1, a contradiction. Thus idS1 is not in the global objectwise image.

step 2.1given
4.1

Steps 1.1 to 3.1 give compatible local sections in the image presheaf that do not glue globally, so the objectwise image is not a sheaf and hence not a subsheaf by [F1]. By [L1], its sheafification is the correct image sheaf.

F1L1step 3.1
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-04 rests on unproved material (inherited)Open item page →
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.

Distinct continuous functions can share one germ, but equal germs everywhere force equality

Example

On the sheaf of continuous real-valued functions on R, the zero function and the function g(x)=max(1x2,0) have the same germ at 0 but are not equal globally. On the other hand, if two continuous functions on an open set U have the same germ at every point of U, then they are equal.

Facts & Assumptions

Given: Continuous functions f,g:UR on an open set U.

[F1]

The germ of a section records equality on some neighbourhood of the point (Germs of sections).

[L1]

Sheaf morphisms are determined by stalk maps (Morphisms of sheaves are determined by their maps on stalks).

Verification

technique · direct
1.1

The function g vanishes on the neighbourhood (1,1) of 0, so its germ at 0 equals the germ of the zero function by [F1]. But g(2)=1, so the two functions are not equal globally.

F1given
1.2

If fx=gx for every xU, then [F1] gives for each x an open neighbourhood VxU on which fVx=gVx. The sets Vx cover U, so f and g agree at every point of U and hence are equal.

F1given
2.1

This pointwise-germ criterion is the section-level instance behind [L1]: one stalk does not determine a section, but all stalks together do.

L1step 1.1step 1.2
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

The empty space has a unique sheaf section over the empty open set

Example

Let X=. Then the only open set is , and every sheaf F on X has exactly one section over that open set.

Facts & Assumptions

Given: A sheaf F on the empty space.

[F1]

A topology on the underlying set has only one open subset, namely (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

[L1]

A sheaf has a unique section over the empty open set (A set-valued sheaf has a unique section over the empty open set).

Verification

technique · direct
1.1

By [F1], there is no open set to consider except , so the whole presheaf data of F is just the set F() together with its identity restriction map.

F1given
2.1

By [L1], this set F() is a singleton. Therefore every sheaf on the empty space has exactly one section over its only open set.

L1step 1.1

Sources