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 · 9 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; all 9 also cleared it.

Sheaf Operations Exactness Ringed Spaces and Module Pullback - Examples

1 · Prerequisites

2 · Summary

These examples isolate the first places where the new operations genuinely matter. Open immersions separate j! from j, skyscraper sheaves make stalkwise exactness visible, and the circle quotient example shows why sheafified cokernels are necessary.

The later examples keep the ringed-space block concrete. Continuous functions provide a locally ringed model, pullback is checked on free modules, and transition functions glue the basic line-bundle prototype.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Direct image along an open immersion is restriction-compatible intersection

Example

Let j:UX be an open immersion, and let F be a sheaf on U. Then for every open set VX one has

(jF)(V)=F(VU).

Facts & Assumptions

Given: An open inclusion j:UX, a sheaf F on U, and an open set VX.

[F1]

Direct image is computed by preimage opens: (jF)(V)=F(j1(V)) (Direct image of a sheaf along a continuous map).

[F2]

Restriction to an open subspace is inverse image along the inclusion (Restriction of a sheaf to an open subspace).

Verification

technique · direct
1.1

Because j is the inclusion of U into X, one has j1(V)=VU.

given
2.1

Substituting step 1.1 into [F1] gives (jF)(V)=F(VU). This is exactly the announced formula, and it is compatible with the restriction interpretation in [F2].

F1F2step 1.1
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Extension by zero can be strictly smaller than direct image on a punctured interval

Statement refuted

For every open immersion j:UX and every sheaf of abelian groups F on U, one has j!F=jF.

Facts & Assumptions

Given: The open immersion j:U=(1,0)(0,1)X=(1,1) and the constant sheaf Z on U.

[F1]

For an open immersion, direct image is computed by intersection: (jZ)(V)=Z(VU) (Direct image along an open immersion is restriction-compatible intersection).

[F2]

Extension by zero consists of sections whose support is closed in the test open (Extension by zero for abelian sheaves on an open subspace).

Counterexample

technique · direct
1.1

By [F1], the global section set of jZ is (jZ)(X)=Z(U)Z×Z, because U has two connected components. Let s be the section that is 1 on both components.

F1givenchoose
2.1

The germ of s is nonzero at every point of U, so its support is all of U. But U=(1,0)(0,1) is not closed in X=(1,1), since its closure contains 0. Therefore [F2] shows that s(j!Z)(X).

F2step 1.1
3.1

Thus s lies in jZ but not in j!Z, so the two sheaves are not equal. This refutes the statement.

step 1.1step 2.1
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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 short exact sequence of abelian groups gives a short exact sequence of skyscraper sheaves

Example

Let

0AAA0

be a short exact sequence of abelian groups, and let xX. Then applying the skyscraper construction at x gives a short exact sequence of sheaves

0ix,Aix,Aix,A0.

Facts & Assumptions

Given: A short exact sequence of abelian groups 0AAA0 and a point xX.

[F1]

A stalk is the colimit of sections over neighbourhoods of the point, and for the skyscraper sheaf those section groups are A on neighbourhoods containing x and 0 on neighbourhoods omitting x (The stalk of a presheaf at a point, A skyscraper sheaf of abelian groups at a point).

[L1]

Exactness of a sequence of abelian sheaves is equivalent to exactness on every stalk (A sequence of abelian sheaves is exact exactly when it is exact on every stalk).

[L2]

Short exactness of the displayed sheaf sequence is exactness in the sense of sheaves (Exact sequences of sheaves).

Verification

technique · direct
1.1

Fix a point yX. If every neighbourhood of y contains x, then [F1] shows that each stalk in the displayed skyscraper sequence is the original group at y, so the stalk sequence is exactly 0AAA0. If some neighbourhood of y omits x, then every smaller neighbourhood also omits x, so [F1] makes all three stalks equal to 0 and the stalk sequence is 0000. In either case the stalk sequence is exact.

F1given
2.1

The stalk sequence is therefore exact at every point, so [L1] implies that the skyscraper sequence is exact as a sequence of sheaves. By [L2], this is exactly the claimed short exact sequence of skyscraper sheaves.

L1L2step 1.1
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Global sections need not preserve surjections

Statement refuted

If φ:FG is an epimorphism of sheaves of abelian groups on a space X, then the induced map on global sections

Γ(X,F)Γ(X,G)

is always surjective.

Facts & Assumptions

Given: The circle X=S1.

[F1]

Global sections need not preserve epimorphisms in general (Global sections are left exact but need not preserve epimorphisms).

Counterexample

technique · direct
1.1

Let C be the sheaf of continuous real-valued functions on S1, and let Z be the subsheaf of locally constant integer-valued functions. Let Q be the sheafification of the presheaf quotient VC(V)/Z(V). Every germ of Q is represented locally by a continuous function, so the canonical map CQ is locally surjective and hence an epimorphism of sheaves.

construct
1.2

Cover the circle by the two arcs U0=S1{(1,0)} and U1=S1{(1,0)}. Choose continuous angle functions θ0:U0(1/2,1/2) and θ1:U1(0,1) with e2πiθi(z)=z. Their quotient classes agree on U0U1, because the difference θ1θ0 is locally constant integer-valued there. Thus they glue to a section qΓ(S1,Q). If q came from a global continuous real function g, then gθi would be an integer-valued continuous function on the connected set Ui, hence constant. On the two connected components of U0U1 this would force the same constant difference to be both 0 and 1, which is impossible. So Γ(S1,C)Γ(S1,Q) is not surjective.

constructcontradiction
2.1

Therefore an epimorphism of sheaves can fail to become surjective on global sections. This is exactly the phenomenon asserted in [F1], so the statement is refuted.

F1step 1.1step 1.2
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Continuous real-valued functions make a space into a locally ringed space

Example

For every topological space X, the sheaf CX0 of continuous real-valued functions makes (X,CX0) into a locally ringed space.

Facts & Assumptions

Given: A topological space X.

[F1]

A ringed space is a space equipped with a sheaf of rings (A ringed space).

[F2]

Stalks are germs of neighbourhood sections (The stalk of a presheaf at a point).

[L1]

A locally ringed space is a ringed space whose stalks are local rings (A locally ringed space, A local ring is a nonzero commutative ring with a unique maximal ideal).

Verification

technique · direct
1.1

The usual restriction of continuous functions makes UCX0(U) a sheaf of commutative rings on X, so [F1] gives a ringed space (X,CX0).

F1given
2.1

Fix xX. By [F2], the stalk CX,x0 consists of germs of continuous real-valued functions near x. The germs vanishing at x form an ideal mx. If a germ is not in mx, it has a representative g with g(x)0, so continuity makes g nonzero on a smaller neighbourhood of x; hence 1/g is continuous there and defines an inverse germ. Therefore the nonunits are exactly the germs in mx, so mx is the unique maximal ideal. Thus CX,x0 is a local ring, and [L1] shows that (X,CX0) is locally ringed.

F2L1given
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

A morphism of ringed spaces need not be a morphism of locally ringed spaces

Statement refuted

Every morphism of ringed spaces between locally ringed spaces is automatically a morphism of locally ringed spaces.

Facts & Assumptions

Given: A field k, the local ring A=k[y](y), and the field K=k(x).

[F1]

A morphism of ringed spaces between one-point spaces is exactly a ring map between their stalk rings (Morphisms of ringed spaces).

[F2]

A morphism of locally ringed spaces must induce local maps on stalks (Morphisms of locally ringed spaces).

[L1]

Counterexample

technique · direct
1.1

Regard ({},A) and ({},K) as one-point ringed spaces. The assignment yx defines a ring homomorphism AK, so by [F1] it defines a morphism of ringed spaces ({},K)({},A).

F1givenconstruct
2.1

The unique maximal ideal of A is (y) by [L1], while the unique maximal ideal of the field K is 0. Under the stalk map AK, the element y goes to the nonzero element x, hence to a unit of K. Therefore the image of (y) is not contained in 0, so the stalk map is not local. By [F2], the morphism is not a morphism of locally ringed spaces.

F2L1step 1.1
3.1

This gives a morphism of ringed spaces between locally ringed spaces that is not locally ringed. The statement is false.

step 1.1step 2.1
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Pullback carries a free module to the corresponding free module

Example

Let

(f,f):(X,OX)(Y,OY)

be a morphism of ringed spaces. For every integer n0, one has a canonical isomorphism

f(OYn)OXn.

Facts & Assumptions

Given: A morphism of ringed spaces (f,f):(X,OX)(Y,OY) and an integer n0.

[F1]

Pullback is defined by fG=OXf1OYf1G (Pullback of a module along a morphism of ringed spaces).

[L1]

Pullback is a left adjoint and therefore preserves finite coproducts (Pullback of modules is left adjoint to pushforward).

Verification

technique · direct
1.1

The sheaf OYn is the finite direct sum of n copies of OY, with the case n=0 giving the zero sheaf. Since [L1] makes f a left adjoint, it preserves these finite direct sums. Thus f(OYn)(fOY)n.

L1given
2.1

Applying [F1] to G=OY gives fOY=OXf1OYf1OYOX, because tensoring a module over a ring with the ring itself leaves the module unchanged. Substituting this into step 1.1 yields f(OYn)OXn.

F1step 1.1
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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.

Units satisfying the cocycle law glue local rank-one free modules into a line bundle

Example

Let (X,OX) be a ringed space with an open cover X=iUi. Suppose that for each pair (i,j) there is a unit

gijOX(UiUj)×

satisfying gii=1,gij=gji1,gjkgij=gik on triple overlaps. Then the free rank-one modules OXUi glue to a line bundle on X.

Facts & Assumptions

Given: A ringed space (X,OX), an open cover X=iUi, and units gij satisfying the displayed cocycle rules.

[F1]

An OX-module is a sheaf with compatible module structures on every open set (Modules on a ringed space).

[F2]

A gluing datum is given by overlap isomorphisms satisfying identity and cocycle conditions (A gluing datum for sheaves on an open cover).

[L1]

Compatible local sheaves glue uniquely up to unique isomorphism (Compatible local sheaves glue uniquely up to unique isomorphism).

Verification

technique · direct
1.1

On UiUj, define φij:OXUiUjOXUiUj,sgijs. Because gij is a unit, φij is an isomorphism of OX-modules, and the rules for the gij are exactly the identity and cocycle conditions of [F2].

F1F2given
2.1

By [L1], the local free rank-one modules OXUi glue to an OX-module L on X with LUiOXUi for every i. Therefore L is locally free of rank one, i.e. a line bundle.

L1step 1.1
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05 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 cokernel presheaf can fail to be a sheaf

Statement refuted

For a morphism of sheaves of abelian groups, the objectwise cokernel presheaf is automatically a sheaf.

Facts & Assumptions

Given: The circle X=S1, the sheaf C of continuous real-valued functions, and the subsheaf Z of locally constant integer-valued functions.

[F1]

Cokernel sheaves are obtained by sheafifying the objectwise cokernel presheaf (Kernel sheaves are objectwise, while cokernels and images are sheafified).

Counterexample

technique · direct
1.1

Let P be the presheaf cokernel of the inclusion ZC, so P(V)=C(V)/Z(V) for each open VS1. Cover S1 by the arcs U0=S1{(1,0)} and U1=S1{(1,0)}, and choose continuous angle functions θ0:U0(1/2,1/2) and θ1:U1(0,1) with e2πiθi(z)=z. On U0U1, the difference θ1θ0 is locally constant integer-valued, so the classes [θ0]P(U0) and [θ1]P(U1) agree on the overlap.

givenconstruct
2.1

If these local classes came from a global class [g]P(S1), then on each arc Ui the difference gθi would be integer-valued and continuous, hence constant because Ui is connected. On the two connected components of U0U1, this would force the same constant difference to be both 0 and 1, which is impossible. Therefore the compatible local classes of step 1.1 do not glue in the presheaf P.

step 1.1contradiction
3.1

So the objectwise cokernel presheaf is not a sheaf. By [F1], this is exactly why one sheafifies it to obtain the true cokernel sheaf. The statement is false.

F1step 2.1

Sources