Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04
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 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),exp⁡U(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.1givenchooseconstruct

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

2.1step 1.1given

On the overlap U1∩U2, both local sections are equal to the same target section id⁡S1∣U1∩U2, so they are compatible.

3.1step 2.1given

Suppose id⁡S1 lay in the global objectwise image. Then there would be a continuous f:S1→R with e2πif(z)=z for every z∈S1. 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 1∈S1, namely n and n+1, a contradiction. Thus id⁡S1 is not in the global objectwise image.

4.1F1L1step 3.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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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